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).
I know how to solve the problem: the solution depends on say three well-known theorems, and just applying the axioms of predicate calculus in a reasonable way. The amount of steps is reasonably low. So, if these three theorems were proved in metamath, everything would be easy. However, it could be that these theorems are not proved in metamath (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?). 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? For proof of theorems, probably not, since there could eventually be a doubt whether a theorem had been really proved, or if it had been "proved" via "defining/axiomatizing" the hard parts of the proof. This would be unacceptable. But for problems/exercises, this should never(?) be a problem, I think. -- 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/5408abaf-648d-4f65-8a19-413ae4c60dbco%40googlegroups.com.
