Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise?

[Anarcocap-socdem]

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.

[vvs]

This is analogous to "sorry" in Lean.

"The sorry identifier magically produces a proof of anything, or provides an object of any data type at all. Of course, it is unsound as a proof method – for example, you can use it to prove false – and Lean produces severe warnings when files use or import theorems which depend on it. But it is very useful for building long proofs incrementally. Start writing the proof from the top down, using sorry to fill in subproofs. Make sure Lean accepts the term with all the sorry’s; if not, there are errors that you need to correct. Then go back and replace each sorry with an actual proof, until no more remain."

https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#propositions-as-types

[David A. Wheeler]

> 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