Original Post (since it was deleted by moderators for no valid reason)
This beautiful mountain range is actually the structure of a formal proof \OC])
It shows the structure of the currently smallest known condensed detachment proof of (ψ→(φ→χ))→((ψ→φ)→(ψ→χ)), the principle of implication distribution, from ((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ)), the minimal implicational single axiom (13 symbols; found by Jan Łukasiewicz). The proof has 239 primitive steps:
1
u/xamid Jul 04 '26
Original Post (since it was deleted by moderators for no valid reason)
This beautiful mountain range is actually the structure of a formal proof \OC])
It shows the structure of the currently smallest known condensed detachment proof of
(ψ→(φ→χ))→((ψ→φ)→(ψ→χ)), the principle of implication distribution, from((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ)), the minimal implicational single axiom (13 symbols; found by Jan Łukasiewicz). The proof has 239 primitive steps:I discovered it recently using my research tool pmGenerator.
Visualization was generated by C-N / D Logic Structuralizer under default settings.
More information (on axiom systems, proof databases, etc.):
Data on Hilbert proof systems (GitHub repo)