> On Thursday, August 20, 2020 at 2:00:49 PM UTC+3 Anarcocap-socdem wrote: > > Let us imagine I want to solve a problem (probably the argument would be > > the same to proof a theorem, but I "see" this argument better applied to > > problems and exercises than to theorems). ... > > However, it could be that these theorems are not proved in metamath ...
> > One possibility is to abandon the project to provide the solution of the > > problem with metamath. But another possibility would be to try and > > "convert" the three theorems into some kind of definitions or axioms. Then, > > these three theorems would be true by definition, and one would only need > > to apply the axioms of predicate calculus to really solve the problem. > > > > Does this approach make any sense? That absolutely makes sense! Adding definitions (in the set.mm) is no big deal. You can also just make the claim a hypothesis ($e), and again it's no big deal. Adding axioms *is* a big deal, but it's still quite doable. IIRC, early versions of set.mm were developed this way; there were some axioms about numbers that were eventually proved. However, there's a risk in this approach: your axioms might not be true. A lot of mathematical texts aren't rigorous and omit special cases and preconditions. If you axiomatize them, & later find your axioms are not true, it may be a lot of work to fix things. If you add axioms, put them in your mathbox and say " (New usage is discouraged.)". You should also probably note that this is a temporary structure & that you intend to eventually prove it. > > (this > > is another question: how reasonable it is that metamath eventually covers > > an undergraduate degree material? Will the modularity, i.e. using > > metamath-proven theorems, eventually explode up the amounts of content in > > metamath? Or will proofs become more and more complex, even within an > > undergraduate level, without the possibility to apply modularity to them?). I personally think it's completely reasonable, though others may disagree. The primary trick is to have reasonably-clear definitions. Set.mm has some small discouragement of new definitions; there's work to do for each one, expanding defintions takes steps, and definitions need extra review to make sure that "what was defined was what was meant". That said, new definitions are added all the time & they're vital for creating understandable abstractions. The proofs should *not* become more & more complex. Instead, wisely adding definitions should make later proofs be no more complex in principle, they're just working on higher-level abstractions. --- David A. Wheeler -- 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 on the web visit https://groups.google.com/d/msgid/metamath/E1k8o0H-0001EZ-5i%40rmmprod06.runbox.
