A really interesting post. All the intricacies of the above examples are way over my head, so sorry if this is a dumb question: can you prove False with your method? Or our definitions conventions guarantee that the extended axiom system is consistent, given that the original system was? If the latter is the case, does that mean that the flaw you found will mainly influence the work on trying to minimize axiom usage, especially predicate calculus axioms?
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. -- 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/763110cd-13ea-4566-8cb8-94fe56b43fdan%40googlegroups.com.
