Trying to understand 2p2e4

[Anarcocap-socdem]

Hello, I am trying to understand 2p2e4, as an excuse to understand metamath better.

I have a few questions:

1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated that "A longest path back to an axiom from 2 + 2 = 4 is 184 layers deep". However, if I run show trace_back 2p2e4 /count_steps, it is stated that "The maximum path length is 84". Is there a typo somewhere? (84 != 184).

2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a total of 619 different subtheorems are used.  The statement and subtheorems have a total of 12178 actual steps (...) The proof would have 5887862241803 =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess that 12178 steps refers to the case in which we take the axioms of the complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms of the complex numbers, starting from ZFC. But I am not 100% sure, and I would like to have confirmation of that.

3. Is there some way to print/export to file the 12178 steps, and even the 5.9 x 10^12 steps, all at once? I ask this since running  show trace_back 2p2e4 /tree gives me a tree, but with only the name of the subtheorems, not the steps themselves. And I have been unable to find a command that gives the full number of steps, all at the same time.

Thank you for your work on this great project.

[Mario Carneiro]

> 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated that "A longest path back to an axiom from 2 + 2 = 4 is 184 layers deep". However, if I run show trace_back 2p2e4 /count_steps, it is stated that "The maximum path length is 84". Is there a typo somewhere? (84 != 184).

Note that that statistic is one of those that will go out of date quickly due to changes in the library structure. So you should not expect it to be exact, unless we have an automated mechanism for keeping it up to date, and we don't currently. However, there is one major change between when that text was written and now which significantly decreased most of the numbers quoted, which is the isolation of the real numbers from their construction. 2+2 = 4 is a theorem very close to the axioms of real numbers, so it was reduced from something depending on the entire stack of set theory and the construction, down to just a few direct axiom applications (plus still a bunch of set theory because of the use of df-ov "operation value" for expressing the + function, defined in the set theory section).

In order to get something closer to the "true" original numbers, you should replace "ax-mulcom $a ... $." with ax-mulcom $p ... $= <apply axmulcom> $. and similarly for all the other axioms in the same section. This will allow metamath-exe to see that uses of these axioms actually depend on a big stack of other lemmas when calculating statistics like max depth and full-expansion theorem counts.

> 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a total of 619 different subtheorems are used.  The statement and subtheorems have a total of 12178 actual steps (...) The proof would have 5887862241803 =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess that 12178 steps refers to the case in which we take the axioms of the complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms of the complex numbers, starting from ZFC. But I am not 100% sure, and I would like to have confirmation of that.

No, this is not about that. Metamath theorems are able to refer to previous theorems multiple times, in multiple concrete instantiations. That is, a theorem is really a "theorem schema" over the assignments to the wff and class variables. If you wanted to perform the same proof in pure first order logic, you would have to redo the proof for every choice of those wff variables. So the statistic here (also calculated by metamath-exe) is working out an approximation to the (exponential) speedup this accomplishes, by seeing how many steps would have been taken if you had to replay each use of each theorem. Effectively, you can think of this as treating every metamath theorem as a macro which expands to a proof containing more macro references, and if we macro-expand everything all that remains are direct references to the axioms. It's easy to get exponential growth in this process, since theorem 2 can use theorem 1 twice, theorem 3 uses theorem 2 twice and so on. Of course the metamath library is not quite so pathological as that, but the nature of the process is still exponential, where the base is related to the density of converging paths in the DAG of theorem references.

> 3. Is there some way to print/export to file the 12178 steps, and even the 5.9 x 10^12 steps, all at once? I ask this since running  show trace_back 2p2e4 /tree gives me a tree, but with only the name of the subtheorems, not the steps themselves. And I have been unable to find a command that gives the full number of steps, all at the same time.

As far as I know, no. Both of these numbers are calculated by the metamath-exe tool, using the command "SHOW TRACE_BACK 2p2e4 /COUNT_STEPS". Internally, it only creates and manipulates the numbers, it doesn't actually perform the expansion (which would take exponentially long just to output). For the former number (12178 steps), an approximation to this is to just "show proof *" which will print all proofs, or look at the entire metamath web site on disk, which contains every step of every theorem. The 12178 steps are a subset of those, and you can get metamath-exe to print out all of the relevant theorems using "show trace_back 2p2e4" alone.

That said, it is certainly possible to calculate the actual 5.9 x 10^12 steps if you are interested in such a programming project. But be aware that the steps can also get pretty large in the process (I think also exponential in general). Although I'm sure your terabyte drive has better things to do...

Mario Carneiro

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com.

[Gino Giotto]

> 3. Is there some way to print/export to file the 12178 steps, and even the 5.9 x 10^12 steps, all at once? I ask this since running  show trace_back 2p2e4 /tree gives me a tree, but with only the name of the subtheorems, not the steps themselves. And I have been unable to find a command that gives the full number of steps, all at the same time.

Technically, there is a way to get the whole proof all the way back to axioms and definitions, but it only works for early theorems and ideally when dummy variables aren't involved.

Below I show an example with a theorem called "mpgbi", which has a small enough "global proof" to make this possible:

READ set.mm

PROVE mpgbi

SET SCROLL CONTINUOUS

SET WIDTH 9999

EXPAND *

OPEN LOG proof.log

SHOW NEW_PROOF /LEMMON /RENUMBER

CLOSE LOG

The above command sequence will save the expanded proof in a log file, shown in all its glory. It's possible to observe that every step of that proof is an application of axioms and definitions only. If you attempt to do this for 2p2e4 then the command  EXPAND * may take days, weeks or months to complete the calculations. It's likely that metamath-exe will crash before finishing, and even if it finishes the final proof won't be technically "complete" because of dummy variables to be filled. So as a rule of thumb, only do this for theorems whose global proof is no bigger than a few thousands steps, and certainly don't do this for 2p2e4 (who has trillions of steps).

[Mario Carneiro]

On Tue, Apr 2, 2024 at 6:56 PM Anarcocap-socdem <jordi.moli...@gmail.com> wrote:

Thank you very much for the answer.

Let us see if I understand this:

Let us assume I take the 619 different subtheorems used in 2p2e4 (I get this number, 619, by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). These 619 subtheorems can be listed by doing show trace_back 2p2e4. The total number of steps of these 619 subtheorems is 12178 (again, this number is obtained by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS).

So, is it correct to say the following:

- I can create a new file, let us call it set_simplified.mm, which corresponds to taking set.mm, and only keeping the 619 subtheorems used in the proof of 2p2e4.

- I can run python3 mmverify.py set_simplified.mm --logfile set.log to check that the proof is correct. mmverify.py has about 690 lines.

So, with 12178 steps, plus 690 lines, I can get a full proof of 2p2e4. All these steps could be written in a pdf file (long, but not unreasonably long).

Is this correct? Or maybe the way I have defined set_simplified.mm is "too simplified"?

Yes, that is basically correct. Strictly speaking though it is "too simplified", because it doesn't account for statement types other than $p / $a :

* ${ , $}  - obviously we need these for grouping a statement with its hypotheses

* $e - (hypotheses) these are "attached" to each theorem and usually directly precede them, although sometimes they can be in the same scope as an earlier theorem and shared across multiple theorems

* $d - (disjoint variable conditions) these are also hypothesis-like in their scoping pattern and semantics

* $v, $f - (variable declarations) for set.mm these are basically global, but there is still a well defined notion of "use" of a variable: just look for its token in any of the 619 subtheorems. If you see it then it must be declared, otherwise it can be dropped.

* $c - (constant declarations) These are global, and have the same kind of "use" as variables: if you see it in the $p ... $= or $a ... $. text then it must be declared first.

For all these reasons, you probably want to use a "metamath aware" slicer for constructing these *_simplified.mm databases. But this is all very straightforward and will not add much on top of the 619 theorems you identified. None of these count as "steps" though toward the 12178 step count; these are for proof steps (I don't know whether syntax steps are included or omitted in the count), and the best you can say about its relation to the simplified.mm file is that every step requires at least one character so set_simplified.mm should be at least 12178 characters and probably more because of theorem statements, delimiters, formatting, and comments if you are keeping them.

In general, no this process will not produce long proofs. In fact it's about as short as we know how to make them, since this is taking full advantage of metamath's abstraction and reuse mechanisms, and the library itself is optimized for overall proof size. However you can find some inefficiencies in this process because set.mm is trying to prove more than just 2+2 = 4 so it will prove things in "unnecessary" generality that becomes pure overhead once you cut literally everything else out. So it's likely that after extracting such a database you can run minimizers over the code and get still more savings.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com.

[Gino Giotto]

> Now I want to create this set_simplified.mm file. Mario Carneiro suggests to use a ""metamath aware" slicer". Is there such a slicer already created? 

Yes, there is already such slicer, you do the following:

READ set.mm

WRITE SOURCE 2p2e4.mm /EXTRACT 2p2e4

This creates a working .mm file that contains only the 619 theorems needed for 2p2e4, the necessary axioms, and the other technical stuff (latex definitions, variables, constants ecc..).

Il Sab 6 Apr 2024, 00:56 Anarcocap-socdem <jordi.moli...@gmail.com> ha scritto:

Thank you for all the answers, they are quite informative.

Now I want to create this set_simplified.mm file. Mario Carneiro suggests to use a ""metamath aware" slicer". Is there such a slicer already created? I guess it is not as easy as just deleting, from set.mm, the subtheorems that are not needed for 2p2e4. I guess that quite a few other steps need to be taken in order to ensure the set_simplified.mm works properly.

Could somebody give me a hand on this project?

Thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6300ff6f-9d28-468a-9716-589787a2e2e4n%40googlegroups.com.

[Anarcocap-socdem]

Wow, thank you very much!

Just FYI, in the 20190602 version of the Metamath book, in the "write source" subsection (5.3.2) there is no option for /extract.