[PMC] 2-year anniversary | Deriving minimal single axioms from one another
samiro.d...@rwth-aachen.de
Dear Metamath community,
as part of celebrating the 2-year anniversary of the “Minimal 1-bases for C-N propositional calculus” proof minimization challenge (PMC), today I am opening another PMC: “Traversing minimal classical C-N single axioms”.
Both are inspired from Metamath's PMC “Shortest known proofs of the propositional calculus theorems from Principia Mathematica” (aka 'pmproofs.txt').
The challenge mentioned first is about finding smaller effective/constructive proofs (i.e. derivations within the actual Hilbert system) from minimal 1-bases (i.e. down to a minimal single axiom with the detachment rule) for classical propositional logic that demonstrate their completeness. This is done by deriving the axioms of two systems of Polish logician Jan Łukasiewicz [who used Polish notation (PN) to present formulas]:
(A1) ψ→(φ→ψ) [PN: CpCqp]
(A2) (ψ→(φ→χ))→((ψ→φ)→(ψ→χ)) [PN: CCpCqrCCpqCpr]
(A3) (¬ψ→¬φ)→(φ→ψ) [PN: CCNpNqCqp]
(L1) (ψ→φ)→((φ→χ)→(ψ→χ)) [PN: CCpqCCqrCpr]
(L2) (¬ψ→ψ)→ψ [PN: CCNppp]
(L3) ψ→(¬ψ→φ) [PN: CpCNpq]
I also included the smallest C-N tautology, (id) ψ→ψ [PN: Cpp], as a target theorem. Notably, (A1)–(A3) are also the propositional axioms of Metamath's “set.mm” database.
Thanks also to valuable contributions from the Metamath community,
specifically Gino Giotto and Steven Nguyen, we found the first
constructive completeness proof for one of the seven minimal single
axioms (w2: Walsh's 2nd axiom) on July 12, 2024.
This solved an open challenge problem that was established by Walsh and
Fitelson on June 26, 2021 — they had found constructive proofs for all
but this axiom, which proved quite difficult to handle due to the
generation of almost exclusively long formulas for very short proofs —
see also this list of 1000 shortest theorems for w2-proofs of up to 43 steps.
However, we have since found proofs from w2 that are much smaller than
their counterparts in other 1-bases, which makes sense since the
exhaustion barrier of w2 is the lowest of them all, i.e. the number of
theorems explodes the fastest for longer proofs.
In case you want to look at
- the status of the 1-basis completeness PMC: https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs
- the progression of the 1-basis completeness PMC: https://github.com/xamidi/pmGenerator/discussions/2#progress
In my opinion, we made amazing progress. Not only in the scope of the
challenge, since it also led to the discovery of very effective proof
compression algorithms and the aforementioned resolution of the open
challenge problem.
The new PMC is about deriving the minimal single axioms from one another in fewer amounts of steps than previously achieved. These proofs tend to be longer since larger theorems tend to have longer proofs. The shortest proofs I've found while preparing the new challenge mostly have step numbers in the 1000s rather than in the 10s and 100s, with not a single one known to be minimal (i.e. contained in an exhaustively generated set).
These preparations, consisting of extensive computations over a period of nine months, also led to further improvements to the preceding challenge — from 22561 down to 18547 proof steps in total — along with the birth of a new preoptimized challenge. ;-)
In contrast to 18547 total proof steps for 49 proofs (33 of which are not known to be minimial), the starting point for the new PMC is at 102278 total proof steps for 42 proofs.
In case you want to look at
- the status of the 1-basis traversal PMC: https://github.com/xamidi/pmGenerator/discussions/10#challenge-proofs
- the progression of the 1-basis traversal PMC: https://github.com/xamidi/pmGenerator/discussions/10#progress
I wish all participants the best of luck and lots of fun! Keep in mind, however, that these are some of the hardest challenges humanity has to offer, or as it was put regarding the mmsolitaire project by Dr. Norman D. Megill, founder of Metamath:
You can play around with it for curiosity or fun, or if you're serious it will be the hardest "game" in the world!
— Samiro Discher
PS: This shouldn't even have to be mentioned but these challenges, and by extension the entire pmGenerator
project, are no place for LLM-generated contents and contributions.
To be clear, I never used them for anything related except testing
whether they can get anything right and the clear answer is, no, they
fail miserably at pretty much everything related to formal condensed
detachment proofs, yet confidently claim the opposite and lie all the
time!
I don't even let LLMs assist me with coding because I think they're
terrible garbage producing compulsive liars and deceivers, and producing
bug-free high-quality code is much more important to me than getting
things done faster with less effort.
Nonetheless, I was already accused by some self-proclaimed "math nerd" on Reddit of producing AI slop after sharing my new introduction
(which took me several days to put together), where someone was
apparently not understanding what they were reading. I hope this is
clear enough to any reasonably educated person, and I am welcoming
feedback.
PPS: I documented all procedures of how I obtained the initial proofs for the new challenge with my pmGenerator tool within a file archive to reproduce these results. It is important to note that the used compression algorithms are inherently nondeterministic (due to parallelization), so using them from scratch might produce different results. But the vault files contain the exact findings and can be used to reconstruct the same proof collections. However, several of the procedures do not work with the (latest) 1.2.2 released binaries, but require more recent features. There will likely soon be the (sufficient) 1.2.3 release. This poses no issue if you build the executable from C++ on your own, which is required for non-Windows platforms regardless.