Principia Mathematica theorems derived from Łukasiewicz axioms
26 views
Skip to first unread message
samiro.d...@rwth-aachen.de
Nov 11, 2025, 1:34:32 PM (9 days ago) Nov 11
to Metamath
In case anyone cares, I created a variant of pmproofs.txt based on axioms CCpqCCqrCpr,CCNppp,CpCNpq, which are
luk-1 ((P -> Q) -> ((Q -> R) -> (P -> R)))
luk-2 ((~ P -> P) -> P)
luk-3 (P -> (~ P -> Q))
in Metamath.
I used the new '--rebase' feature of pmGenerator, and then proof compression.
The latter was mainly due to an attempt of finding a shorter proof of ax-2 (i.e. *2.77) than the current 91-step derivation. (So far, I didn't find one.)
Direct link: L-pmproofs.txt [repo]
The repo is open for contributions.
luk-1 ((P -> Q) -> ((Q -> R) -> (P -> R)))
luk-2 ((~ P -> P) -> P)
luk-3 (P -> (~ P -> Q))
in Metamath.
I used the new '--rebase' feature of pmGenerator, and then proof compression.
The latter was mainly due to an attempt of finding a shorter proof of ax-2 (i.e. *2.77) than the current 91-step derivation. (So far, I didn't find one.)
Direct link: L-pmproofs.txt [repo]
The repo is open for contributions.
Reply all
Reply to author
Forward
0 new messages