[1-basis C] [2-basis C-O] Question about the ideal minimization process #13
Replies: 3 comments 2 replies
-
This is false. Quoting from pmGenerator's readme:
However, as also noted in the readme, standard notation is mostly irrelevant for our syntactic approach. More precisely, the meaning of symbols that are not used in any inference rules is defined solely by axioms, thus only arity matters for them. For example, one could very well swap This entails that many non-standard systems can be defined in pmGenerator, even those which include weird stuff like custom modal operators. Proof systems are supported as long as there are available symbols of corresponding arity for its operators, and as long as no additional rules of inference are required. One can also introduce additional symbols using more axioms — the kind of axioms that are called definitions in Metamath. [example]
I don't think that fewer ingredients necessarily make something “more natural”, or similar. I consider C-N calculus more pure than C-O calculus since negations are straightforward and natural (we say “not” very often), whereas defining
It provides structure based on which modus ponens with substitution can do most of the job, at least.
I suppose you consider the 21-symbol C-N single axioms “overkill” since there are only 16 symbols in I agree that this 2-basis is neat and special in its own way. However, to minimize components, we can use D calculus or X calculus (NAND or NOR), each of which comes with a weird rule of inference and abominations as formulas. To minimize proof steps in general, we can use large sets of axioms, despite knowing very little as to how. But we don't even know what to use in order to minimize proof steps for 1-bases (or 2-bases, 3-bases, etc.). We need much more research to answer this, and it will also shed light on the previously mentioned “how”. Questions regarding complexity can only be answered when the systems in question are sufficiently explored, which is no easy task. In regard to complexity, all 1-bases are overkill, and certainly more so than some 2-bases, which are certainly more overkill than some 3-bases, and so on. Good points could also be made that all Hilbert systems are overkill in many ways. But they can still allow us to explore fundamental syntactic relationships. By the way, I chose minimal C-N bases to demonstrate pmGenerator's capabilities because comparing them with each other highlights how vastly intricate Hilbert systems are and how differently they behave, even when they appear similar at first glance.
Hilbert systems tend to emerge syntactically in ways that are far from trivial. So I doubt there is a general procedure to find near-minimal D-proofs that doesn't require lots of computing resources. Core features of pmGenerator are precisely to find non-trivial shortcuts using extensive computations. When looking for small proofs, I wouldn't bother to import and compress long proofs like those found in Metamath's .mm databases. Unless I really struggle to prove a theorem at all, in which case the imported proof should still be compressed based on data generated by pmGenerator! In summary, one should not expect great results by merely using proof compression on low-quality data.
For example, your proof of L1: I played with impsingle on my (slow and old) laptop last year for a few days. According to my notes, I used ./pmGenerator -c -n -s CCCpqrCCrpCsp -g -1to exhaustively generate up to ./pmGenerator -c -n -s CCCpqrCCrpCsp --extract -l 50 -dwhich extracted 205386 proofs of theorems with up to 50 symbols (out of 685742 proofs). ./pmGenerator -c -n -s CCCpqrCCrpCsp -e 1 -g 77 -l 50assuming that the previous extraction was stored in subfolder
Finally, I used (I didn't mean to reproduce this, so I may have missed some details of my approach.) The example is very sensitive on data: It requires theorems of certain lengths with certain proof lengths to not be filtered out. In contrast, proof compression depends highly on which theorems are included. Those which are merely included because they are useful in theory (which is what Metamath's databases mainly consist of) are unlikely very useful when it comes to short syntactic derivations. In my experience, (partial) exhaustive search is pretty effective to find good candidates to build upon. Back then, I did not find a short proof of A2: However, since you asked, I now started computing jobs to explore both Please tell me if you run into further troubles. |
Beta Was this translation helpful? Give feedback.
-
My bad! I should have spent more time reading the documentation. The fact that pmGenerator already supports constant symbols is very convenient and it solves my feature request. The support for a family binary operators is also a nice feature that I might use later on. Here is the MM1 proof of (a more general version of) ax-3 after a bit of compression with % ax_imp CCCpqrCCrpCsp = 1 % ax_fal COp = 2 % ax-3 [0] CCCpqCrOCrp = DDDDDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDDD1D1D1DDD1D1111111DDDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDD1DDDD1D1D1D1DDDD1D1D1DDD1D1111111111D1DDD1D1DDD1D1111111DDDD1D1D1DDD1D111111111DDD1DDDD1D1D1D1DDDD1D1D1DDD1D1111111111D1DDDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDDD1D1D1DDD1D1111111112 The proof is 319 steps long and it uses
In the last few days I attempted to use your method to find a further compression of ax-3, but I wasn't successfull. However I found other results within this system. The first is a shorter proof of [0] Cpp = DDDD1D11D1112 The proof has 13 steps instead of the 21 I showed before. If I understand correctly, the The second result is a statistical one. With the command DD1DDDD1DDD1DDD1D1D1DDDD1D1D1111111DDD1D111111122: C0CCCO1O2 Corresponding to the statement: |- ( p -> ( ( ( F. -> q ) -> F. ) -> r ) ) A feature of this system is the possibility of making predictions. In this example, since I know that the minimal proof of
Ok, so the method is system-dependent, which makes sense. I agree that generating lemmas with pmGenerator would yield higher quality data in general, so that's probably the strategy I should follow. Taking proofs from Metamath was more out of lazyness to get a quick starting point. Perhaps I will figure out some specialized methods like the ones seen on the challenges.
This is useful. I have a mediocre home computer and I haven’t investigated this system properly yet. University resources are very welcome.
This is indeed a lot better than what I did and could have done with my setup :)
I can confirm that I observed a similar growth factor myself.
How does it compare to Walsh and Meredith?
The thing that made me interested is that, while technically 2-base, this system has some properties that makes it resemble a 1-base one (but with a shorter axiom). Apart from the ones I mentioned, there is also the impossibility of min $e |- F. maj $e |- ( F. -> ps ) ax-mp $p |- ps In any proof of this 2-base system, |
Beta Was this translation helpful? Give feedback.
-
|
I emphasized in the readme that
and I am using this topic as an opportunity to demonstrate how this can be done, and to name just a few benefits. The process of providing initial proof data does not require much human effort — in fact, writing this comment took most of it in this case — but it tends to require a lot of computing time and patience. One can adjust the duration depending on how deep one chooses to prepare the data. Others can then dig deeper while not having to repeat computations. 1. GroundworkIn this case, I chose to exhaustively collect filtered proofs of up to 83 steps (based on close to 2× exponential growth and the fact that both filterings of The aforementioned procedures took six computing jobs for each system:
Note that the (low-memory) nodes with Intel Xeon Platinum 8468 CPUs turned out wasteful on computing time. So, since task 2 for A pitfall to avoid when starting with 2. TakeoffThe 119-step proof of L1: 119-step proof of L1:
|
| Identifier(s) | C-O | C-N | Typical Axiom in Fragment(s) |
|---|---|---|---|
A1, P₁:1, L₃:1 |
CpCqp |
⇠ | C, C-N, C-O |
A2, P₁:2, L₃:2 |
CCpCqrCCpqCpr |
⇠ | C, C-N, C-O |
P₁:3 |
CCCpOOp |
CNNpp |
C-N, C-O |
L1, L₁:1 |
CCpqCCqrCpr |
⇠ | C, C-N, C-O |
L2, L₁:2 |
CCCpOpp |
CCNppp |
C-N |
L3, L₁:3 |
CpCCpOq |
CpCNpq |
C-N |
A3, L₃:3 |
CCCpOCqOCqp |
CCNpNqCqp |
C-N |
(Reminder: If you prefer to read infix notation, you can use my converter.)
Note that L2C-O is proven without COp as its proper schema CCCpqpp (Peirce's law), which is often used in axiomatizations of the classical C fragment, i.e. implicational logic. It is addressed within I₁: CpCqp,CCpqCCqrCpr,CCCpqpp = (A1, L1, Peirce's law) and I₅:CCpqCCqrCpr,CCCpqpp,CpCCpqq = (A1, Peirce's law, CpCCpqq) in parts 14 and 25 of the previously mentioned paper series.
Initial Results
I will update the pmData repository in case of improvements, not this comment.
CCCpqrCCrpCsp
The shortest single axiom for classical implicational logic.
- Hash:
97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146[i.e. SHA512/224("CCC0.1.2CC2.0C3.0")] - System:
CCCpqrCCrpCsp[i.e.1:((p→q)→r)→((r→p)→(s→p))]
Data 
| Files up to.. | Size of Files [B] |
+Costs [≈core‑h] |
Recent Growth |
|---|---|---|---|
| dProofs81.txt | 2 449 297 774 | 15529.60 | 1.4706… |
| dProofs83.txt | 3 597 241 733 | 31224.00 | 1.4670… |
| dProofs85‑unfiltered85+.txt | 19 626 102 482 | 69.15 | 13.9631… |
| dProofs87‑unfiltered85+.txt | 60 909 402 788 | 130.28 | 2.5755… |
| dProofs89‑unfiltered85+.txt | 153 150 493 111 | 271.16 | 2.2343… |
| dProofs91‑unfiltered85+.txt | 320 324 295 368 | 518.62 | 1.8123… |
| dProofs93‑unfiltered85+.txt | 649 288 832 712 | 1039.80 | 1.9677… |
- Smallest 10k theorems (with minimal proofs): top10000SmallestConclusions_1to93Steps.txt (1.640806 MB)
- Includes all up-to-19-symbol theorems that can be generated in up to 93 steps.
Cardinalities 
1 dProofs3.txt
1 dProofs5.txt
3 dProofs7.txt
8 dProofs9.txt
14 dProofs11.txt
21 dProofs13.txt
31 dProofs15.txt
42 dProofs17.txt
65 dProofs19.txt
98 dProofs21.txt
135 dProofs23.txt
197 dProofs25.txt
270 dProofs27.txt
388 dProofs29.txt
551 dProofs31.txt
783 dProofs33.txt
1106 dProofs35.txt
1563 dProofs37.txt
2211 dProofs39.txt
3116 dProofs41.txt
4400 dProofs43.txt
6223 dProofs45.txt
8774 dProofs47.txt
12413 dProofs49.txt
17529 dProofs51.txt
24829 dProofs53.txt
35088 dProofs55.txt
49805 dProofs57.txt
70539 dProofs59.txt
100323 dProofs61.txt
142420 dProofs63.txt
202794 dProofs65.txt
288534 dProofs67.txt
411654 dProofs69.txt
586547 dProofs71.txt
837981 dProofs73.txt
1196203 dProofs75.txt
1710627 dProofs77.txt
2444582 dProofs79.txt
3499861 dProofs81.txt
5006994 dProofs83.txt
68838412 dProofs85-unfiltered85+.txt
170845717 dProofs87-unfiltered85+.txt
335691857 dProofs89-unfiltered85+.txt
584703462 dProofs91-unfiltered85+.txt
1060815488 dProofs93-unfiltered85+.txt
Extracted & Partially Generated
- (
--extract -l 50)-dProofs1-93-unfiltered91+ (Folder:extraction-l50)- Up to
dProofs89.txtwere created via-mfrom-l 50-extractions of exhaustive files, thus are complete w.r.t.-l 50entries. - The remaining unfiltered files (
dProofs{91,93}-unfiltered85+.txt) must be renamed to be loaded by pmGenerator.
- Up to
- (
--extract -l 40)-dProofs1-93-(-g -l 40)-111-(-g -l 30)-153 (Folder:extraction-l40l30)- Up to
dProofs93.txtwere created via-mfrom-l 40-extractions of exhaustive files, thus are complete w.r.t.-l 40entries. - Smallest 24820 theorems (with proofs): l40l30-top24820SmallestConclusions_1to153Steps.txt (4.661867 MB)
- Includes all generated up-to-19-symbol theorems. All proofs with up to 95 steps are minimal.
- Smallest 76307 theorems (with proofs): l40l30-top76307SmallestConclusions_1to153Steps.txt (15.172891 MB)
- Includes all generated up-to-21-symbol theorems. All proofs with up to 95 steps are minimal.
- Up to
- (
--extract -l 40)-dProofs1-41-(-e l40l30 --extract -l 21)-153-(-g -l 21)-239 (Folder:extraction-l21)- Exemplary search:
pmGenerator -c -n -s CCCpqrCCrpCsp -e l21 --search Cpp,CpCqp,CCpCqrCCpqCpr,CCpqCCqrCpr,CCCpOpp,CCCpqpp -n -s
- Exemplary search:
Exemplary Proofs
Concrete D-proofs / “Proof List”
% Identity principle (Cpp), i.e. 0→0 ; 21 steps
DDDDD1D1111DDD1D11111,
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 15 steps
DDD11DDD1D11111,
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 239 steps
DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D11111111111DDD1DDDDDD1D1D1D1DDDD1D1D1111111111D1DDDDDD1D1D1D1DDDD1D1D111111111DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D1111111111111,
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 101 steps
DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D111111111111,
% Axiom 2 by Łukasiewicz (CCCpOpp [C-N: CCNppp]), i.e. ((0→⊥)→0)→0 [C-N: (¬0→0)→0], instance of:
% Peirce's law (CCCpqpp), i.e. ((p→q)→p)→p ; 31 steps
DDD1DDD1D1DDD1D111111DDD1D11111
- Exemplary parse:
pmGenerator -c -n -s CCCpqrCCrpCsp --parse proofList.txt -f -u -j 1 pmGenerator -c -n -s CCCpqrCCrpCsp --parse DDDDD1D1111DDD1D11111,DDD11DDD1D11111,DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D11111111111DDD1DDDDDD1D1D1D1DDDD1D1D1111111111D1DDDDDD1D1D1D1DDDD1D1D111111111DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D1111111111111,DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D111111111111,DDD1DDD1D1DDD1D111111DDD1D11111 -u -j 1
Abstract Representation / “Proof Summary”
CCCpqrCCrpCsp = 1
[0] CCCpqpCrp = DDD1D1111
[1] CpCqp = DDD11[0]1
[2] Cpp = DD[0][0]1
[3] CCpCqrCCCpsrCqr = DDDDD1D1D1D1DDDD1D1D111111111
[4] CCCpqpp = DDD1DDD1D1[0]11[0]1
[5] CCpqCCqrCpr = DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1[0]11111111
[6] CCpCqrCCpqCpr = DDDD1D1D1D[3][3]11DDD1D[3]1D1D[3][5]1
- Exemplary transform:
pmGenerator --transform proofSummary.txt -f -n -t Cpp,CpCqp,CCpCqrCCpqCpr,CCpqCCqrCpr,CCCpqpp -p -2 -d pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDD1D1111,[1]=DDD11[0]1,[2]=DD[0][0]1,[3]=DDDDD1D1D1D1DDDD1D1D111111111,[4]=DDD1DDD1D1[0]11[0]1,[5]=DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1[0]11111111,[6]=DDDD1D1D1D[3][3]11DDD1D[3]1D1D[3][5]1" -n -w -t Cpp,CpCqp,CCpCqrCCpqCpr,CCpqCCqrCpr,CCCpqpp -p -2 -d
CCCpqrCCrpCsp,COp
The shortest single axiom for classical implicational logic, together with the principle of explosion. They axiomatizatize classical propositional logic in terms of {→,⊥}.
- Hash:
d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9[i.e. SHA512/224("CCC0.1.2CC2.0C3.0CO0")] - System:
CCCpqrCCrpCsp,COp[i.e.1:((p→q)→r)→((r→p)→(s→p)),2:⊥→p]
Data 
| Files up to.. | Size of Files [B] |
+Costs [≈core‑h] |
Recent Growth |
|---|---|---|---|
| dProofs81.txt | 2 531 886 162 | 17310.40 | 1.4742… |
| dProofs83.txt | 3 719 804 925 | 35792.00 | 1.4655… |
| dProofs85‑unfiltered85+.txt | 20 719 453 444 | 112.69 | 14.3104… |
| dProofs87‑unfiltered85+.txt | 64 772 912 668 | 213.68 | 2.5914… |
| dProofs89‑unfiltered85+.txt | 163 246 801 423 | 434.06 | 2.2353… |
| dProofs91‑unfiltered85+.txt | 341 553 471 625 | 881.99 | 1.8106… |
| dProofs93‑unfiltered85+.txt | 691 422 259 426 | 1815.61 | 1.9621… |
- Smallest 10k theorems (with minimal proofs): top10000SmallestConclusions_1to93Steps.txt (1.622864 MB)
- Includes all up-to-17-symbol theorems that can be generated in up to 93 steps.
Cardinalities 
2 dProofs1.txt
1 dProofs3.txt
1 dProofs5.txt
3 dProofs7.txt
8 dProofs9.txt
15 dProofs11.txt
22 dProofs13.txt
33 dProofs15.txt
45 dProofs17.txt
69 dProofs19.txt
101 dProofs21.txt
140 dProofs23.txt
205 dProofs25.txt
280 dProofs27.txt
404 dProofs29.txt
568 dProofs31.txt
809 dProofs33.txt
1140 dProofs35.txt
1614 dProofs37.txt
2278 dProofs39.txt
3217 dProofs41.txt
4529 dProofs43.txt
6426 dProofs45.txt
9042 dProofs47.txt
12829 dProofs49.txt
18076 dProofs51.txt
25667 dProofs53.txt
36224 dProofs55.txt
51530 dProofs57.txt
72889 dProofs59.txt
103901 dProofs61.txt
147416 dProofs63.txt
210360 dProofs65.txt
299183 dProofs67.txt
427694 dProofs69.txt
609264 dProofs71.txt
872065 dProofs73.txt
1244628 dProofs75.txt
1782980 dProofs77.txt
2547752 dProofs79.txt
3653261 dProofs81.txt
5226411 dProofs83.txt
74024284 dProofs85-unfiltered85+.txt
185049299 dProofs87-unfiltered85+.txt
364350012 dProofs89-unfiltered85+.txt
633578953 dProofs91-unfiltered85+.txt
1146953429 dProofs93-unfiltered85+.txt
Extracted & Partially Generated
- (
--extract -l 50)-dProofs1-93-unfiltered85+ (Folder:extraction-l50) - (
--extract -l 40)-dProofs1-93-(-g -l 40)-111-(-g -l 30)-141 (Folder:extraction-l40l30)- Up to
dProofs93.txtwere created via-mfrom-l 40-extractions of exhaustive files, thus are complete w.r.t.-l 40entries. - Smallest 42679 theorems (with proofs): l40l30-top42679SmallestConclusions_1to141Steps.txt (7.851301 MB)
- Includes all generated up-to-19-symbol theorems. All proofs with up to 95 steps are minimal.
- Smallest 124246 theorems (with proofs): l40l30-top124246SmallestConclusions_1to141Steps.txt (24.082907 MB)
- Includes all generated up-to-21-symbol theorems. All proofs with up to 95 steps are minimal.
- Up to
- (
--extract -l 40)-dProofs1-41-(-e l40l30 --extract -l 21)-141-(-g -l 21)-159 (Folder:extraction-l21)- Exemplary search:
pmGenerator -c -n -s CCCpqrCCrpCsp,COp -e l21 --search Cpp,CpCqp,CCpCqrCCpqCpr,CCCpOOp,CCCpqOp,CCpqCCqrCpr,CCCpOpp,CCCpqpp,CpCCpOq,CCCpOCqOCqp,CCCpqCrOCrp -n -s
- Exemplary search:
Exemplary Proofs
Concrete D-proofs / “Proof List”
% Identity principle (Cpp), i.e. 0→0 ; 13 steps
DDDD1D11D1112,
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 15 steps
DDD11DDD1D11111,
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 239 steps
DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D11111111111DDD1DDDDDD1D1D1D1DDDD1D1D1111111111D1DDDDDD1D1D1D1DDDD1D1D111111111DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D1111111111111,
% Double negation elimination (CCCpOOp [C-N: CNNpp]), i.e. ((0→⊥)→⊥)→0 [C-N: ¬¬0→0], instance of:
% CCCpqOp, i.e. ((0→1)→⊥)→0 ; 31 steps
DDDD1DDD1D1DDDD1D1D11111D111112,
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 101 steps
DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D111111111111,
% Axiom 2 by Łukasiewicz (CCCpOpp [C-N: CCNppp]), i.e. ((0→⊥)→0)→0 [C-N: (¬0→0)→0], instance of:
% Peirce's law (CCCpqpp), i.e. ((p→q)→p)→p ; 31 steps
DDD1DDD1D1DDD1D111111DDD1D11111,
% Axiom 3 by Łukasiewicz (CpCCpOq [C-N: CpCNpq]), i.e. 0→((0→⊥)→1) [C-N: 0→(¬0→1)] ; 111 steps
DDDD1DDD1D1DDDD1D1D11111DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111111D1DDDDDD1DDD1D1D1D1D1DDDD1D1D1111111111121112,
% Axiom 3 for Frege by Łukasiewicz (CCCpOCqOCqp [C-N: CCNpNqCqp]), i.e. ((0→⊥)→(1→⊥))→(1→0) [C-N: (¬0→¬1)→(1→0)], instance of:
% CCCpqCrOCrp, i.e. ((0→1)→(2→⊥))→(2→0) ; 155 steps
DDD1DDDDDD1D1D1D1DDDD1D1D1111111111DDDDDD1D1D1D1DDDD1D1D111111111DDDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D11111111121
- Exemplary parse:
pmGenerator -c -n -s CCCpqrCCrpCsp,COp --parse proofList.txt -f -u -j 1 pmGenerator -c -n -s CCCpqrCCrpCsp,COp --parse DDDD1D11D1112,DDD11DDD1D11111,DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D11111111111DDD1DDDDDD1D1D1D1DDDD1D1D1111111111D1DDDDDD1D1D1D1DDDD1D1D111111111DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D1111111111111,DDDD1DDD1D1DDDD1D1D11111D111112,DDDD1D1D1D1DDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D111111111111,DDD1DDD1D1DDD1D111111DDD1D11111,DDDD1DDD1D1DDDD1D1D11111DDDD1D1D1DDDDDD1D1D1D1DDDD1D1D111111111111D1DDDDDD1DDD1D1D1D1D1DDDD1D1D1111111111121112,DDD1DDDDDD1D1D1D1DDDD1D1D1111111111DDDDDD1D1D1D1DDDD1D1D111111111DDDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D11111111121 -u -j 1
Abstract Representation / “Proof Summary”
CCCpqrCCrpCsp = 1
COp = 2
[0] Cpp = DDDD1D11D1112
[1] CpCqp = DDD11DDD1D11111
[2] CCCpqCCCrCqstCutCvCCCrCqstCut = D1D1DDDD1D1D11111
[3] CCpCqrCCCpsrCqr = DDDDD1D1[2]1111
[4] CCCpqpp = DDD1DDD1D1DDD1D111111DDD1D11111
[5] CCCpqOp = DDDD1DD[2]D111112
[6] CCpCqCrsCCrpCqCrs = DDD1DDDD1DDD1D1D1[2]1111DDD1DDD1DDD1[2]11D1D1DDD1D111111111
[7] CCpqCCqrCpr = DDDD1D1D1D1[6]111
[8] CpCCpOq = DDDD1DD[2]DDDD1D1D1D[3]111D1DDDDDD1DDD1D1D1[2]11111121112
[9] CCCpqCrOCrp = DDD1D[3]1D[3]D[6]21
[10] CCpCqrCCpqCpr = DDDD1D1D1D[3][3]11DDD1D[3]1D1D[3][7]1
- Exemplary transform:
pmGenerator --transform proofSummary.txt -f -n -t Cpp,CpCqp,CCCpqpp,CCCpqOp,CCpqCCqrCpr,CpCCpOq,CCCpqCrOCrp,CCpCqrCCpqCpr -p -2 -d pmGenerator --transform "CCCpqrCCrpCsp=1,COp=2,[0]=DDDD1D11D1112,[1]=DDD11DDD1D11111,[2]=D1D1DDDD1D1D11111,[3]=DDDDD1D1[2]1111,[4]=DDD1DDD1D1DDD1D111111DDD1D11111,[5]=DDDD1DD[2]D111112,[6]=DDD1DDDD1DDD1D1D1[2]1111DDD1DDD1DDD1[2]11D1D1DDD1D111111111,[7]=DDDD1D1D1D1[6]111,[8]=DDDD1DD[2]DDDD1D1D1D[3]111D1DDDDDD1DDD1D1D1[2]11111121112,[9]=DDD1D[3]1D[3]D[6]21,[10]=DDDD1D1D1D[3][3]11DDD1D[3]1D1D[3][7]1" -n -w -t Cpp,CpCqp,CCCpqpp,CCCpqOp,CCpqCCqrCpr,CpCCpOq,CCCpqCrOCrp,CCpCqrCCpqCpr -p -2 -d
Comparison: CCCpqrCCrpCsp vs. CCCpqrCCrpCsp,COp
This section is part of pmData/CCCpqrCCrpCsp,COp.
#₁⬚ means number of ⬚ w.r.t. CCCpqrCCrpCsp; #₂⬚ means number of ⬚ w.r.t. CCCpqrCCrpCsp,COp. F stands for derived formulas.
Full table: Σfiltered 
| #₁F | #₂F | ΔF | #₁C |
#₂C |
#₁1 |
#₂1 |
#₂2 |
#₂O |
|
|---|---|---|---|---|---|---|---|---|---|
| dProofs1.txt | 1 | 2 | +1 | 6 | 7 | 1 | 1 | 1 | 1 |
| dProofs3.txt | 1 | 1 | 0 | 8 | 8 | 2 | 2 | 0 | 0 |
| dProofs5.txt | 1 | 1 | 0 | 11 | 11 | 3 | 3 | 0 | 0 |
| dProofs7.txt | 3 | 3 | 0 | 21 | 21 | 12 | 12 | 0 | 0 |
| dProofs9.txt | 8 | 8 | 0 | 53 | 53 | 40 | 40 | 0 | 0 |
| dProofs11.txt | 14 | 15 | +1 | 113 | 115 | 84 | 89 | 1 | 1 |
| dProofs13.txt | 21 | 22 | +1 | 181 | 180 | 147 | 152 | 2 | 1 |
| dProofs15.txt | 31 | 33 | +2 | 312 | 325 | 248 | 261 | 3 | 6 |
| dProofs17.txt | 42 | 45 | +3 | 477 | 496 | 378 | 401 | 4 | 7 |
| dProofs19.txt | 65 | 69 | +4 | 779 | 801 | 650 | 686 | 4 | 4 |
| dProofs21.txt | 98 | 101 | +3 | 1238 | 1273 | 1078 | 1107 | 4 | 7 |
| dProofs23.txt | 135 | 140 | +5 | 1955 | 1997 | 1620 | 1675 | 5 | 6 |
| dProofs25.txt | 197 | 205 | +8 | 3093 | 3182 | 2561 | 2657 | 8 | 15 |
| dProofs27.txt | 270 | 280 | +10 | 4603 | 4700 | 3780 | 3910 | 10 | 12 |
| dProofs29.txt | 388 | 404 | +16 | 7017 | 7231 | 5820 | 6044 | 16 | 30 |
| dProofs31.txt | 551 | 568 | +17 | 10583 | 10774 | 8816 | 9071 | 17 | 21 |
| dProofs33.txt | 783 | 809 | +26 | 15887 | 16287 | 13311 | 13727 | 26 | 47 |
| dProofs35.txt | 1106 | 1140 | +34 | 23769 | 24224 | 19908 | 20486 | 34 | 44 |
| dProofs37.txt | 1563 | 1614 | +51 | 35434 | 36347 | 29697 | 30615 | 51 | 96 |
| dProofs39.txt | 2211 | 2278 | +67 | 52527 | 53534 | 44220 | 45493 | 67 | 91 |
| dProofs41.txt | 3116 | 3217 | +101 | 77476 | 79459 | 65436 | 67456 | 101 | 182 |
| dProofs43.txt | 4400 | 4529 | +129 | 114271 | 116514 | 96800 | 99509 | 129 | 182 |
| dProofs45.txt | 6223 | 6426 | +203 | 168650 | 173034 | 143129 | 147595 | 203 | 373 |
| dProofs47.txt | 8774 | 9042 | +268 | 247206 | 252211 | 210576 | 216740 | 268 | 395 |
| dProofs49.txt | 12413 | 12829 | +416 | 363522 | 373063 | 310325 | 320307 | 418 | 755 |
| dProofs51.txt | 17529 | 18076 | +547 | 531630 | 542814 | 455754 | 469425 | 551 | 832 |
| dProofs53.txt | 24829 | 25667 | +838 | 780867 | 801565 | 670383 | 692168 | 841 | 1541 |
| dProofs55.txt | 35088 | 36224 | +1136 | 1140459 | 1165544 | 982464 | 1013125 | 1147 | 1799 |
| dProofs57.txt | 49805 | 51530 | +1725 | 1675162 | 1720351 | 1444345 | 1492620 | 1750 | 3170 |
| dProofs59.txt | 70539 | 72889 | +2350 | 2446527 | 2502666 | 2116170 | 2184280 | 2390 | 3875 |
| dProofs61.txt | 100323 | 103901 | +3578 | 3591891 | 3691405 | 3110013 | 3217291 | 3640 | 6745 |
| dProofs63.txt | 142420 | 147416 | +4996 | 5248186 | 5375375 | 4557440 | 4712210 | 5102 | 8451 |
| dProofs65.txt | 202794 | 210360 | +7566 | 7702008 | 7922611 | 6692202 | 6934161 | 7719 | 14296 |
| dProofs67.txt | 288534 | 299183 | +10649 | 11261412 | 11550346 | 9810156 | 10161303 | 10919 | 18539 |
| dProofs69.txt | 411654 | 427694 | +16040 | 16532019 | 17022511 | 14407890 | 14952832 | 16458 | 30653 |
| dProofs71.txt | 586547 | 609264 | +22717 | 24176669 | 24831016 | 21115692 | 21910141 | 23363 | 40414 |
| dProofs73.txt | 837981 | 872065 | +34084 | 35489102 | 36581821 | 31005297 | 32231334 | 35071 | 65634 |
| dProofs75.txt | 1196203 | 1244628 | +48425 | 51931319 | 53412391 | 45455714 | 47245936 | 49928 | 87827 |
| dProofs77.txt | 1710627 | 1782980 | +72353 | 76223828 | 78657948 | 66714453 | 69461548 | 74672 | 140625 |
| dProofs79.txt | 2444582 | 2547752 | +103170 | 111570583 | 114916243 | 97783280 | 101803368 | 106712 | 190526 |
| dProofs81.txt | 3499861 | 3653261 | +153400 | 163784713 | 169205301 | 143494301 | 149624880 | 158821 | 301027 |
| dProofs83.txt | 5006994 | 5226411 | +219417 | 239795256 | 247330300 | 210293748 | 219281640 | 227622 | 412019 |
| Σfiltered | 16668725 | 17373082 | +704357 | 755010823 | 778386055 | 661067944 | 688376301 | 728078 | 1330249 |
| #₁F | #₂F | ΔF | #₁C |
#₂C |
#₁1 |
#₂1 |
#₂2 |
#₂O |
|
|---|---|---|---|---|---|---|---|---|---|
| Σfiltered | 16668725 | 17373082 | +704357 | 755010823 | 778386055 | 661067944 | 688376301 | 728078 | 1330249 |
| dProofs85-unfiltered85+.txt | 68838412 | 74024284 | +5185872 | 3447875490 | 3633993208 | 2960051716 | 3177386277 | 5657935 | 9847396 |
| dProofs87-unfiltered85+.txt | 170845717 | 185049299 | +14203582 | 8984407350 | 9522321881 | 7517211548 | 8127221988 | 14947168 | 26349695 |
| dProofs89-unfiltered85+.txt | 335691857 | 364350012 | +28658155 | 21100407016 | 22388393933 | 15106133565 | 16366042880 | 29707660 | 61263473 |
| dProofs91-unfiltered85+.txt | 584703462 | 633578953 | +48875491 | 38592404748 | 40930919963 | 26896359252 | 29093971016 | 50660822 | 109999861 |
| dProofs93-unfiltered85+.txt | 1060815488 | 1146953429 | +86137941 | 77867616745 | 82380233788 | 49858327936 | 53817494470 | 89316693 | 216232606 |
| Σall | 2237563661 | 2421329059 | +183765398 | 150747722172 | 159634248828 | 102999151961 | 111270492932 | 191018356 | 425023280 |
The tables above demonstrate effects of adding COp (the principle of explosion) to CCCpqrCCrpCsp.
For example, by Σfiltered(ΔF) ∕ Σfiltered(#₁F) ≈ 4.23% and Σall(ΔF) ∕ Σall(#₁F) ≈ 8.21%, there are approximately 4.23% more theorems provable in up to 83 steps, but when accounting also for unfiltered files since dProofs85-unfiltered85+.txt, we already have 8.21% more theorems in up to 93 steps.
| Calculation | Observation |
|---|---|
0.11% ≈ Σfiltered(#₂2) ∕ (Σfiltered(#₂1)+Σfiltered(#₂2))0.17% ≈ Σfiltered(#₂ O) ∕ (Σfiltered(#₂C)+Σfiltered(#₂O))0.17% ≈ Σall(#₂ 2) ∕ (Σall(#₂1)+Σall(#₂2))0.27% ≈ Σall(#₂ O) ∕ (Σall(#₂C)+Σall(#₂O)) |
In minimal proofs of up to 83 steps, only around 0.11% of used axioms are instances of COp, while around 0.17% of the operators of their theorems are ⊥. The proportions go up to 0.17% and 0.27%, respectively, when also including proofs from unfiltered files of up to 93 steps. |
45.295 ≈ Σfiltered(#₁C) ∕ Σfiltered(#₁F)44.804 ≈ Σfiltered(#₂ C) ∕ Σfiltered(#₂F)0.0766 ≈ Σfiltered(#₂ O) ∕ Σfiltered(#₂F) |
Without COp, a theorem minimally proven by up to 83 steps has roughly 45.295 → operators on average. With COp, such a theorem has roughly 44.804 → and 0.0766 ⊥ operators (together ≈44.881) on average. |
39.659 ≈ Σfiltered(#₁1) ∕ Σfiltered(#₁F)39.623 ≈ Σfiltered(#₂ 1) ∕ Σfiltered(#₂F)0.0419 ≈ Σfiltered(#₂ 2) ∕ Σfiltered(#₂F) |
On average, there are ≈39.659 axiom references per collected minimal 1-basis proof of up to 83 steps, and ≈39.665 axiom references (≈39.623×1 and ≈0.0419×2) per collected 2-basis proof of up to 83 steps.[Note: Each pure D-proof of length 2k+1 has k+1 axiom references.] |
| 134.24 ≈ Σall(#₁F) ∕ Σfiltered(#₁F) 199.66 ≈ Σall(#₁ C) ∕ Σfiltered(#₁C)155.81 ≈ Σall(#₁ 1) ∕ Σfiltered(#₁1) |
For CCCpqrCCrpCsp, the five files dProofs{85,…,93}-unfiltered85+.txt multiply the total number of theorems, → operators, and axiom references by approximate factors of 134.24, 199.66, and 155.81, respectively. |
| 139.37 ≈ Σall(#₂F) ∕ Σfiltered(#₂F) 205.08 ≈ Σall(#₂ C) ∕ Σfiltered(#₂C)161.64 ≈ Σall(#₂ 1) ∕ Σfiltered(#₂1)319.51 ≈ Σall(#₂ O) ∕ Σfiltered(#₂O)262.36 ≈ Σall(#₂ 2) ∕ Σfiltered(#₂2) |
In contrast to the observation above, with COp as a second axiom, these files multiply the total number of theorems, → operators, and CCCpqrCCrpCsp-references by approximately 139.37, 205.08, and 161.64, respectively. The approximate factors for the total number of ⊥ operators and COp-references are 319.51 and 262.36, respectively. |
5.95 ≈ Σfiltered(#₂F) ∕ ΣdProofs{1,…,73}.txt(#₂F)6.78 ≈ Σfiltered(#₂ C) ∕ ΣdProofs{1,…,73}.txt(#₂C)6.82 ≈ Σfiltered(#₂ 1) ∕ ΣdProofs{1,…,73}.txt(#₂1)6.71 ≈ Σfiltered(#₂ O) ∕ ΣdProofs{1,…,73}.txt(#₂O)6.60 ≈ Σfiltered(#₂ 2) ∕ ΣdProofs{1,…,73}.txt(#₂2) |
To elaborate on the above, the five files dProofs{75,…,83}.txt multiply the total number of theorems, → operators, CCCpqrCCrpCsp-references, ⊥ operators, and COp-references only by approximate factors of 5.95, 6.78, 6.82, 6.71, and 6.60, respectively. That the last two are not increased compared to the two before them shows that ⊥ operators and COp-references are merely drastically increased in the prior case due to not being filtered out. However, since they are much rarer in total amounts (see first entry), these numbers still show their increasing proportions. |
I invite you to draw further interesting connections! Please turn it into a comment or submit a pull request.
The data listed above is insufficient to combine multiple properties of a single entry, e.g. to determine usage distributions of primitives per proof or theorem. The following table shows how many proofs have one or multiple 2-references, and how many 2-referencing proofs derive O-free theorems. These numbers appear alongside #₂F and #₂2 — the numbers of formulas and 2-references (already listed above) — for easier comparison.
Full table: Σfiltered 
| #₂F | #₂2 |
#₂F[#2≥1] |
#₂F[#2≥2] |
#₂F[#2≥3] |
#₂F[#2≥1,#O=0] |
|
|---|---|---|---|---|---|---|
| dProofs1.txt | 2 | 1 | 1 | 0 | 0 | 0 |
| dProofs3.txt | 1 | 0 | 0 | 0 | 0 | 0 |
| dProofs5.txt | 1 | 0 | 0 | 0 | 0 | 0 |
| dProofs7.txt | 3 | 0 | 0 | 0 | 0 | 0 |
| dProofs9.txt | 8 | 0 | 0 | 0 | 0 | 0 |
| dProofs11.txt | 15 | 1 | 1 | 0 | 0 | 0 |
| dProofs13.txt | 22 | 2 | 2 | 0 | 0 | 1 |
| dProofs15.txt | 33 | 3 | 3 | 0 | 0 | 0 |
| dProofs17.txt | 45 | 4 | 4 | 0 | 0 | 0 |
| dProofs19.txt | 69 | 4 | 4 | 0 | 0 | 0 |
| dProofs21.txt | 101 | 4 | 4 | 0 | 0 | 0 |
| dProofs23.txt | 140 | 5 | 5 | 0 | 0 | 0 |
| dProofs25.txt | 205 | 8 | 8 | 0 | 0 | 0 |
| dProofs27.txt | 280 | 10 | 10 | 0 | 0 | 0 |
| dProofs29.txt | 404 | 16 | 16 | 0 | 0 | 0 |
| dProofs31.txt | 568 | 17 | 17 | 0 | 0 | 0 |
| dProofs33.txt | 809 | 26 | 26 | 0 | 0 | 0 |
| dProofs35.txt | 1140 | 34 | 34 | 0 | 0 | 0 |
| dProofs37.txt | 1614 | 51 | 51 | 0 | 0 | 0 |
| dProofs39.txt | 2278 | 67 | 67 | 0 | 0 | 0 |
| dProofs41.txt | 3217 | 101 | 101 | 0 | 0 | 0 |
| dProofs43.txt | 4529 | 129 | 129 | 0 | 0 | 0 |
| dProofs45.txt | 6426 | 203 | 203 | 0 | 0 | 0 |
| dProofs47.txt | 9042 | 268 | 268 | 0 | 0 | 0 |
| dProofs49.txt | 12829 | 418 | 416 | 2 | 0 | 0 |
| dProofs51.txt | 18076 | 551 | 548 | 3 | 0 | 1 |
| dProofs53.txt | 25667 | 841 | 839 | 2 | 0 | 1 |
| dProofs55.txt | 36224 | 1147 | 1141 | 6 | 0 | 7 |
| dProofs57.txt | 51530 | 1750 | 1739 | 11 | 0 | 14 |
| dProofs59.txt | 72889 | 2390 | 2371 | 19 | 0 | 20 |
| dProofs61.txt | 103901 | 3640 | 3610 | 30 | 0 | 38 |
| dProofs63.txt | 147416 | 5102 | 5051 | 50 | 1 | 54 |
| dProofs65.txt | 210360 | 7719 | 7644 | 74 | 1 | 83 |
| dProofs67.txt | 299183 | 10919 | 10777 | 140 | 2 | 136 |
| dProofs69.txt | 427694 | 16458 | 16242 | 214 | 2 | 215 |
| dProofs71.txt | 609264 | 23363 | 23023 | 336 | 4 | 314 |
| dProofs73.txt | 872065 | 35071 | 34539 | 526 | 6 | 482 |
| dProofs75.txt | 1244628 | 49928 | 49129 | 788 | 11 | 736 |
| dProofs77.txt | 1782980 | 74672 | 73416 | 1238 | 18 | 1130 |
| dProofs79.txt | 2547752 | 106712 | 104808 | 1867 | 37 | 1725 |
| dProofs81.txt | 3653261 | 158821 | 155869 | 2899 | 53 | 2632 |
| dProofs83.txt | 5226411 | 227622 | 223183 | 4337 | 101 | 4023 |
| Σfiltered | 17373082 | 728078 | 715299 | 12542 | 236 | 11612 |
| #₂F | #₂2 |
#₂F[#2≥1] |
#₂F[#2≥2] |
#₂F[#2≥3] |
#₂F[#2≥1,#O=0] |
|
|---|---|---|---|---|---|---|
| Σfiltered | 17373082 | 728078 | 715299 | 12542 | 236 | 11612 |
| dProofs85-unfiltered85+.txt | 74024284 | 5657935 | 5528486 | 128054 | 1381 | 30545 |
| dProofs87-unfiltered85+.txt | 185049299 | 14947168 | 14589508 | 353747 | 3877 | 76422 |
| dProofs89-unfiltered85+.txt | 364350012 | 29707660 | 28980041 | 719214 | 8309 | 375085 |
| dProofs91-unfiltered85+.txt | 633578953 | 50660822 | 49380674 | 1263772 | 16193 | 774720 |
| dProofs93-unfiltered85+.txt | 1146953429 | 89316693 | 87112821 | 2176502 | 27028 | 1338214 |
| Σall | 2421329059 | 191018356 | 186306829 | 4653831 | 57024 | 2606598 |
I collected the entries that count towards Σfiltered(#₂F[#2≥2]), Σall(#₂F[#2≥3]), and Σfiltered(#₂F[#2≥1,#O=0]). The corresponding files are linked in their respective cells. They should provide numerous use cases of the principle of explosion and thus contribute to a better understanding. Additional excerpts from extraction-l40l30 have been uploaded to the same location but are also included in the archive of the full extraction.
| Calculation | Observation |
|---|---|
1.62% ≈ Σfiltered(#₂F[#2≥1,#O=0]) ∕ Σfiltered(#₂F[#2≥1])1.40% ≈ Σall(#₂F[# 2≥1,#O=0]) ∕ Σall(#₂F[#2≥1]) |
Only around 1.62% of the minimal COp-referencing proofs of up to 83 steps derive a ⊥-free theorem. The proportion grows even lower when including longer unfiltered proofs. |
4.12% ≈ Σfiltered(#₂F[#2≥1]) ∕ Σfiltered(#₂F)0.072% ≈ Σfiltered(#₂F[# 2≥2]) ∕ Σfiltered(#₂F)0.0014% ≈ Σfiltered(#₂F[# 2≥3]) ∕ Σfiltered(#₂F)7.69% ≈ Σall(#₂F[# 2≥1]) ∕ Σall(#₂F)0.192% ≈ Σall(#₂F[# 2≥2]) ∕ Σall(#₂F)0.0024% ≈ Σall(#₂F[# 2≥3]) ∕ Σall(#₂F) |
Approximate proportions of minimal proofs of up to 83 steps that reference the principle of explosion at least once, twice, and thrice are 4.12%, 0.072%, and 0.0014% (less than 1 in 73614), respectively. The proportions grow to 7.69%, 0.192%, and 0.0024% (less than 1 in 42461) when also including dProofs{85,…,93}-unfiltered85+.txt . |
Remarks
About the CCCpqrCCrpCsp,COp-proofs of A3C-O:CCCpOCqOCqp
Just like your 319-step proof, my 155-step proof also derives CCCpqCrOCrp [i.e. merco1lem3:((p→q)→(r→⊥))→(r→p)], which is a schema of A3C-O:((p→⊥)→(q→⊥))→(q→p). But your final step is
CCCpqCrOCrp = D<CCpCqrCCCrsCqpCqr>2 = D<(p→(q→r))→(((r→s)→(q→p))→(q→r))><⊥→p>
i.e.
$ pmGenerator -c -n -s CCCpqrCCrpCsp,COp --parse DDDDDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDDD1D1D1DDD1D1111111DDDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDD1DDDD1D1D1D1DDDD1D1D1DDD1D1111111111D1DDD1D1DDD1D1111111DDDD1D1D1DDD1D111111111DDD1DDDD1D1D1D1DDDD1D1D1DDD1D1111111111D1DDDDDD1D1D1D1DDDD1D1D1DDD1D1111111111DDDD1D1D1DDD1D1111111112 -u -j 1
[…]
1. ⊥→(2→0) (2)
2. (⊥→(2→0))→(((0→1)→(2→⊥))→(2→0)) (R):49
3. ((0→1)→(2→⊥))→(2→0) (D):1,2
while mine is
CCCpqCrOCrp = D<CpCCCqrCsOCsq>1 = D<p→(((q→r)→(s→⊥))→(s→q))><((p→q)→r)→((r→p)→(s→p))>
i.e.
$ pmGenerator -c -n -s CCCpqrCCrpCsp,COp --parse DDD1DDDDDD1D1D1D1DDDD1D1D1111111111DDDDDD1D1D1D1DDDD1D1D111111111DDDD1DDDD1DDD1D1D1D1D1DDDD1D1D111111111DDD1DDD1DDD1D1D1DDDD1D1D1111111D1D1DDD1D11111111121 -u -j 1
[…]
1. ((3→4)→5)→((5→3)→(6→3)) (1)
2. (((3→4)→5)→((5→3)→(6→3)))→(((0→1)→(2→⊥))→(2→0)) (R):40
3. ((0→1)→(2→⊥))→(2→0) (D):1,2
Graph Images
I generated scatter plots with the RapidTables tool — press "Zoom In" nine times to match dimensions of my existing behavioral graphs. The tool processed data like 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 5 […], generated by --plot -s -x <n>. I additionally used SVG compression tools (1. Compress-Or-Die, 2. Vecta) to beautify the output, then replaced all >< by >\n< (where \n is the newline character). In order to not deal with layouts again, I then copied the grid and <circle […]/> entries over their counterparts in copies of already finished vector graphics.
Vertical lines (illustrating averages and medians) were adjusted by modifying the relevant x-coordinates in their <path […]/> entries after obtaining target values from drawing single-dot entries (e.g. 77 0 for median 77) with the RapidTables tool.
Collecting Data for Comparison
I obtained data for the first two tables via shell scripts like
for i in {1..83..2}; do
tr -cd 'C' < dProofs${i}.txt | wc -m
done
for i in {85..93..2}; do
tr -cd 'C' < dProofs${i}-unfiltered85+.txt | wc -m
donewhich I used in dProofs-withConclusions (for 'C' and 'O') and dProofs-withoutConclusions (for '1' and '2').
I first had to use ./pmGenerator -c -n -s CCCpqrCCrpCsp --variate 0 and ./pmGenerator -c -n -s CCCpqrCCrpCsp,COp --variate 0 to create the proof files with removed conclusions.
To obtain the more intricate numbers of #₂F[#2≥1], #₂F[#2≥2], #₂F[#2≥3], and #₂F[#2≥1,#O=0], I used regular expressions ^[^:]*2[^:]*:.*$, ^[^:]*2[^:]*2[^:]*:.*$, ^[^:]*2[^:]*2[^:]*2[^:]*:.*$, and ^[^:]*2[^:]*:[^O]*$, respectively, in shell code like
count=0
while IFS= read -r line || [ -n "$line" ]; do
if [[ "$line" =~ ^[^:]*2[^:]*:[^O]*$ ]]; then
((count++))
# In case of collecting entries
echo "$line" >> "$LOG_FILE"
fi
done < "$file"
echo "$(basename "$file"): $count"
total_sum=$((total_sum + count))but it turned out very slow. An optimized compiled language can probably do these things tens if not hundreds of times faster.
Thanks to Notepad++'s excellent editing capabilities (e.g. Alt + Left Mouse drag or Ctrl + Left Mouse click to edit or copy many places at once) and some online tools (Quick Sum Calculator, Equation Solver, and Merge lists), I could quickly assemble the massive Markdown tables from raw data. To remove columns at the front or back, I used regex replacements with expressions like (?<=\n)\|([^\|]+\|){2} and \n\|([^\|]+\|){2}\K[^\n]+(?=\n).
Time Calculations
Each log file has a manually added header where I noted wall-clock time in hours and computing costs in core-hours. I copy timestamps from the log files and paste them like May 20 04:37:24 2026 - May 26 09:21:33 2026 to Wolfram|Alpha in order to produce the number of seconds as an output, e.g. 535449 seconds. The documented numbers are based on this number, e.g. 535449 ∕ 3600 = 148.7358333… h wall-clock time, which makes 148.7358333… * 96 = 14278.64 core-h in case 96 total cores were used. Sometimes Slurm reports durations in D⁺‑H⁺:M⁺:S⁺ format (e.g. in email notifications), which I quickly convert to hours with my custom duration converter.
Large & Additional Files
I did not recompress and upload the exhaustively generated unfiltered85+ files since they are of little use on machines with more regular consumer-sized RAM, whereas on machines with 2 TiB of RAM they can quickly be regenerated from …,dProofs83.txt. Much of their value was also extracted into the partial generations. I may still upload them (or larger extractions thereof) upon request.
7-Zip & Memory Issues
I usually repack files on Windows in order to make use of the better compression options of the 7-Zip GUI application for Windows. When I repacked CCCpqrCCrpCsp,COp's exhaustively generated dProofs83.txt (1 187 918 763 bytes) for the first time on a local machine using 7-Zip, it resulted in an archive with a single . character replaced by a /. I suppose it was due to malfunctioning non-ECC RAM (this particular PC met the blue screen of death several times recently), which shouldn't happen on the cluster machines due to ECC.
Details 
- Original file, line 4500578
DD1DDD1D1DDD1D111111D1D1DDDDD1D1D11111D1D1DD1D1D1D1DDDDD1D1D11111D1D1DD1DD11D1D1111:C0CCC1C2CCC3.4CCC5C6CCC7.8CCCC9.10C10.10.10C11.10C12CCCC9.10C10.10.10C11.10.13C14.13C15CCC5C6CCC7.8CCCC9.10C10.10.10C11.10C12CCCC9.10C10.10.10C11.10.13C14.13C16.17C16.17 - Corrupted file, same line
DD1DDD1D1DDD1D111111D1D1DDDDD1D1D11111D1D1DD1D1D1D1DDDDD1D1D11111D1D1DD1DD11D1D1111:C0CCC1C2CCC3.4CCC5C6CCC7.8CCCC9.10C10.10.10C11.10C12CCCC9.10C10.10.10C11.10.13C14.13C15CCC5C6CCC7.8CCCC9.10C10.10/10C11.10C12CCCC9.10C10.10.10C11.10.13C14.13C16.17C16.17 - Query to quickly✻ print this entry:
pmGenerator -c -n -s CCCpqrCCrpCsp,COp --search DD1DDD1D1DDD1D111111D1D1DDDDD1D1D11111D1D1DD1D1D1D1DDDDD1D1D11111D1D1DD1DD11D1D1111 -p
✻Assuming the hard disk is fast; e.g., it takes close to 2 seconds on my SSD (Samsung 870 EVO).
This is the first time I noticed that such an error occurred when I compressed a file, but I find it worth mentioning that it can happen. So it is important to verify in the end that the compressed files match the originals. In this case, comparing the CRC hash values within 7-Zip on Windows would have revealed the error, since they changed from EA336972 (result from server) to 3D44B005.
But I was a little hasty and only realized that something was wrong when pmGenerator -c -n -s CCCpqrCCrpCsp,COp --plot -s -x 400 (the command to collect data for the behavioral graph) counted a theorem of even symbolic length (which C-O formulas cannot form).
I double-checked all the other recompressed files afterwards.
Making sure two archives (with many files) are equal
"D:/Program Files/7-Zip/7z" l -slt <archive1>.7z > slt1.txt"D:/Program Files/7-Zip/7z" l -slt <archive2>.7z > slt2.txtdiff slt1.txt slt2.txt | grep CRC- Should have empty output.
- Two equal CRCs listed? Sometimes the files listed in
slt1.txtandslt2.txtmust be rearranged to the same order via editing.
- Two equal CRCs listed? Sometimes the files listed in
- Should have empty output.
diff slt1.txt slt2.txt | grep Path- Should only print paths of the two compared
.7zarchives.
- Should only print paths of the two compared
Beta Was this translation helpful? Give feedback.

Uh oh!
There was an error while loading. Please reload this page.
-
I chose the "General" category because I figured that this post contains a bit more than just a question: it contains some thoughts, results and a feature suggestion as well.
I've recently been exploring in the proof system derived from impsingle, which is a single axiom for implicational calculus. It has as many symbols as ax-2, but with the strength of { ax-1, ax-2, peirce }, therefore it can derive every tautology that contains the implication symbol only. A peculiarity of impsingle is that it is apparently not only the shortest axiom for implicational calculus, but it is also supposed to be the unique shortest axiom, so it captured my attention.
So far, I've derived a few theorems:
I started with a proof of ax-2 with roughly 40.000 steps and managed to compressed it to 573 with fairly little effort. The question is what would be the ideal procedure to compress it further. So far I’ve just been lazily using
--transform [-z] [-x <limit>]with few minutes of computing time and it was good enough, but I’m sure there are more systematic methods for this kind of exploration.To make the system complete for classical propositional calculus, it is sufficient to add the principle of explosion falim
|- ( F. -> ph ), which is also the unique shortest possible second axiom we could add. So overall, this pair of axioms form an elegant axiomatization of classical propositional calculus.Unfortunately pmGenerator does not support the falsum constant, so I'm not sure how to show the derivation of ax-3 using the D-notation. However, I proved ax-3 in this MM1 database. I named impsingle
ax_imp, since effectively, it describes implication. The mm0-rs LSP server shows no errors on VS Code so the proofs should be correct (I also verified it with mm0-c paired with the corresponding MM0 file). Lately, I’ve found that MM1 is more convenient to use than MM, because it can handle these "long and ugly" proofs without a perceptible slowdown. The proofs are also more easily readable than MM and they can be converted into condensed detachment with a simple script.It would be nice if pmGenerator supported the falsum constant, even Meredith's single axiom becomes shorter if we use C-O calculus:
This version has 19 symbols instead of the 21 of the traditional Meredith's axiom, so maybe the set of connectives
{ -> , ⊥ }is more natural than the set{ -> , ¬ }for propositional logic. I wonder if this choice of terms would allow a slight speed-up in computation or parsing.Soapbox thoughts
It is known that Meredith's axiom and Walsh's six axioms are the shortest possible single axioms for classical propositional calculus. However, I would argue that the shorter ax_imp already does most of the job on its own, despite containing only the implication connective.
Here is the reason I think so, starting with an example:
Let's take a tautology that has the negation connective, say ax-3:
We can write it in terms of
F.and->like so:How do we prove it using ax_imp and ax_fal? Well, there is a trick, we can replace all occurrences of
F.with a new variable, sayr, and add an antecedent that says that such new vairiablerimplies the conclusion (in this casep). Such procedure generates the expression:This new statement has two properties: it is still a tautology and it is expressed exclusively using the implication connective, therefore it is provable using only ax_imp (see the MM1 file for the proof).
To derive ax-3, it's sufficient to discharge the newly added antecedent with
ax_mpandax_fal, that's it. This shows that the computational heavy lifting is effectively performed byax_imp. The principle of explosionax_falis such a vestigial axiom that can be used just once at the end of the proof. My conjecture is that the same method can be applied to every theorem that needsax_fal, that is, for every theorem that requires the principle of explosion, it exists a proof that usesax_faljust once at the end of the proof, like in the example of ax-3 (although this method probably doesn't provide the minimal proof).Another example with a longer formula:
Expressed in the
{ -> , ⊥ }basis, it becomes:Now we apply the method. We replace the constant
F.with a new variablesand we add an antecedent that says that such new variablesimplies the conclusionr:Once more, we obtained a tautology of implicational calculus, therefore provable with
ax_imp. To derive the original, it suffices to writeD[0]2as D-proof, whereDis modus ponens,[0]is the above lemma and2isax_fal.But there is more. The axiom ax_imp is more powerful that intuition might suggest. Consider this tautology:
It is a conjunction of notnotr and ax-3, and it has the negation symbol, therefore its proof should require both ax_imp and ax_fal, right? No,
ax_impsuffices to prove it.We first unwrap the defined symbols
/\and~, which can be done natively in MM1 (I'm actually not sure if this works in MM):We observe that the generated statement is an instance of a theorem of implicational calculus. Therefore we can simply choose a generalization by replacing
F.with a new variable (we don't need to add an antecedent here):Since the last statement is provable using
ax_imponly, the original conjunction is provable from it as well, without the need of usingax_fal.I think this system is quite neat, and it may suggest that Meredith’s axiom and Walsh’s axioms are a bit "overkill". At the end of the day, impsingle suffices to derive the structural complexity of propositional logic, and it looks even more special if we consider that it is apparently unique in its minimal length.
Beta Was this translation helpful? Give feedback.
All reactions