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/CAAfCLnjyghb3%2B9xZOb1tRY0cEevBPNCCWm8-iaTLPpnPu%3DuAKw%40mail.gmail.com.
