> 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.
