If I correctly understand the issue here, seems like the request is to
carry the axiom tracking from the justification theorem to usages of the
definition.
It doesn't appear to affect what we can prove, but given that we do seem
to often care about axiom usage, it seems like a plausible thing to
want. (I'm not sure I have an opinion about *how* this tracking would
work, but I'm not sure we would have to change a lot of things to make
it possible).
On 7/13/25 06:34, Steven Nguyen wrote:
This would be a really good idea if there weren't historical reasons.
I think ideally this is how it would go:
1. the definition checker generates $k proofs for all relevant definitions
2. the axioms of the $k proofs are propagated forward to theorems
3. $j usage would also check for axioms that would be used in $k proofs
This would be more elegant and rigorous than hypotheses
On Sun, Jul 13, 2025 at 4:35 AM Gino Giotto
<[email protected]> wrote:
can you prove False with your method?
I think the answer is no, you cannot prove False from sound definitions. The
reason I think so is because definitions that follow the convention rules
always have a provable justification theorem inside the full axiomatic system
of set.mm. To prove false, you have to show that your definition has a
justification theorem that is stronger than what set.mm allows. This is the way
proofs of false have been produced historically so far, like I did in
https://github.com/metamath/set.mm/pull/4909. So, if you only care about set.mm
as a whole, then this is an axiom usage issue, but if you care about subsystems
of set.mm (or non-set.mm systems) then it becomes a bigger problem.
It would be nice if this could be resolved by leaving metamath standard as
is, and, for instance, improving the definition checker in mmj2 or
metamath-knife. Seems like adding the $k token would make all the verifiers we
wrote over the years obsolete.
Yeah , this is a problem. I guess the simplest solution is the first option
then, which is to add the justification theorems as definition hypotheses. It's
not super elegant, and in my eyes it fails the promise of absolute rigour of
the metamath book, but it should work in practice.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/1cabdb6f-4afe-49c9-bf17-b3eeeea40f7fn%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/3fc77edd-7766-4d07-a3ca-1b41c1035386%40panix.com.
