On Thursday, September 24, 2020 at 2:41:00 AM UTC-4 ArndtS... freenet.de
wrote:
> I'm neither a mathematician nor too familiar with Metamath (more of a
> crank really), but I'm wondering whether it is possible to build a program
> that automatically checks and financially rewards proofs of theorems not
> yet contained in the set.mm database, say the ones from the Metamath 100
> list. Seeing the OpenAI work made me interested in this again.
>
> The main problems I see are:
>
> 1. Definitions vs. axioms. The proof either (1.1) must not contain $a
> statements, to avoid directly or indirectly proving the end result with
> spurious assumptions, or (1.2) $a statements must somehow be restricted to
> those that only allow syntactic rewriting, without changing any semantics.
> I'm not sure if this is possible, or if this has been done before.
>
We need axioms before we can prove anything. There is no problem with a
proof containing references to axioms; indeed, in principle every theorem
referenced in a proof can have its proof expanded; recursively working
back, we will end up with a proof consists of nothing but references to
axioms and rules of inference (which is the strict definition of a formal
proof). An intermediate "theorem" referenced in a proof is essentially no
more than a way to avoid having to repeat its proof from axioms over and
over again.
(There is a metamath.exe tool that will do just this, but only for trivial
theorems in early prop calc since otherwise proofs explode and become too
large. E.g. "prove mpi" then "expand *" will result in a proof with
nothing but direct axiom references.)
The important thing is to know exactly what axioms we are ultimately basing
a proof on. Commands in metamath.exe such as "show trace_back" provide a
means for determining that. But it is a little more complicated.
Most of the the large number of $a statements in set.mm are definitions
(which are "syntactic rewriting" as you call it). Some of the other ones
are theorems restated as axioms for various purposes. And finally there
are the proper axioms themselves, which everything can ultimately be traced
back to.
What follows is from an email about this I wrote recently, which you might
find helpful:
We use $a statements for both axioms and definitions. From the point of
view of a proof verifier, all $a statements are treated identically. A
separate algorithm is used to check that definitions are sound (i.e.
eliminable and conservative). This is currently mainly done by an option
of the mmj2 program, using an algorithm written by Mario Carneiro.
We make an (artificial) distinction between axioms and definitions by
prefixing the label with "ax-" and "df-" respectively. Breaking it down
this way, the full set.mm database has 115 axioms and 1231 definitions.
In principle, everything can be derived from 13 axioms of first-order logic
("ax-1" through "ax-13") and 7 axioms of ZFC set theory (plus the
Tarski-Grothendieck axiom "ax-groth" if we need inaccessible cardinals for
category theory), which gives us 21 axioms total. FOL also has the 2
inference rules of modus ponens ("ax-mp") and generalization ("ax-gen"),
which will give us 23 total if we count them as axioms (which we do).
The main reason set.mm has more than 23 axioms is that sometimes we restate
theorems as axioms for various purposes. For example, the Axiom of
Separation is redundant in ZFC since it follows from the Axiom of
Replacement. However, Replacement ("ax-rep") is a strong axiom that some
people prefer to avoid when possible. So we prove a theorem called "axsep"
from Replacement, then restate that theorem as axiom "ax-sep". That makes
it easy to see whether a proof needs only Separation rather than the full
strength of Replacement (using, for example, the "This theorem was proved
from axioms" list on the web pages with proofs).
We also prove the complex number properties as theorems, then at the end of
their construction restate them as axioms, giving us a couple of dozen
additional axioms. One motivation for doing this is to obtain a
construction-independent starting point for complex numbers, so we could in
principle plug in an alternate construction. (An original motivation was
simply to make the "This theorem depends on definitions" list on the web
pages for complex number proofs much less cluttered. Having the complex
number construction restated as axioms makes that list more compact and
meaningful.)
Finally, set.mm has two major parts, one which we call the "main part of
set.mm" and the other which we call "mathboxes". The start of the mathbox
section is identified by a dummy placeholder theorem called "mathbox".
Mathboxes are essentially workspaces for individual users, with work under
development as well as experimental work. When we feel that a set of
theorems in a mathbox is stable and useful, we will often import it into
the main part of set.mm.
Some mathbox work also involves experiments with other axiom systems and
thus adds more "ax-*" $a's to the set.mm total, even though they will never
be imported in order to keep the main part of set.mm pure ZFC. However, it
artificially adds to the axiom count for set.mm as a whole. For this
reason, it will be easier to restrict our attention to the "main" part to
analyze the axioms used. In addition to mathboxes, the end of the main
part has a deprecated section at the end that will eventually become
deleted, and to make things easier I will exclude that section as well.
If we exclude deprecated material and mathboxes (i.e. everything in set.mm
after statement "df-rprm"), we end up with 55 axioms ("ax-*"), 751
definitions ("df-*"), and 24196 theorems ($p statements). Of these 55
axioms, 32 of them are theorems restated as axioms as described above,
leaving us with the 23 "proper" axioms that represent pure FOL+ZFC+ax-groth.
> 2. Since no new assumptions can be introduced, I'm not sure if all axioms
> contained in set.mm suffice to allow the formulation of all the remaining
> proofs in the MM100, or say, even cutting edge research. Is this known? Do
> current mathematical researchers know for certain that their assumptions
> are restricted to ZFC?
>
The 23 axioms of FOL + ZFC + ax-groth suffices for all mainstream
mathematics, including the MM100. (Certainly it is true, by demonstration,
for the 74 that we've proved.)
The only place additional axioms are sometimes introduced is in the study
of large cardinals <https://en.wikipedia.org/wiki/Large_cardinal> by set
theorists. In addition, there are axioms such as the Continuum Hypothesis
(or its negation) that are independent of ZFC. However, these can also be
stated as hypotheses rather than stand-alone axioms, e.g. "if the Continuum
Hypothesis is true, then (some consequence)," so that ZFC + ax-groth will
still suffice for filling in the details. An example in set.mm is "gchac".
>
> 3. Vast proof lengths, especially with proofs involving arithmetic. A
> while ago I graphed the full proof dependency graph of 2p2e4:
> https://twitter.com/dd4ta/status/1050433711416721408 and it was pretty
> big :) and created plots of the number of proof steps vs the number of
> theorems a proof depended on, see the readme here:
> https://github.com/void4/mmplot Could you estimate where "cutting edge"
> mathematical research would be? Millions of proof steps and tens of
> thousands of dependencies?
>
I have no idea of the size of something like Fermat's Last Theorem, if it
were proved in set.mm, other than to say it would be huge (gigabytes?).
But for the 74 MM100 theorems already proved, it isn't hard to find their
lengths with the tools you've already used like "show trace_back". There
is also a recently added option to "write source" called "/extract" which
will save exactly and only what's needed for a specific proof all the way
back to axioms. Some experiments were described in this post:
https://groups.google.com/g/metamath/c/E08icuHZ_4M/m/N3NkW2zWDAAJ
Norm
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/6c8b4066-24dd-4114-8690-6ea2feaa3e65n%40googlegroups.com.
