@xamidi/pmData

A curated list of proof systems based on detachment (so-called Hilbert systems), with analyses, proof data, and logs.

Exhaustive and refined proof collections were generated and can be processed with pmGenerator. Large, highly compressed proof files are hosted on cloud servers. They are made available via download links. Smaller files are hosted here or on the pmGenerator page for demonstration purposes.

Sharing data in this manner enables researchers to build upon past work rather than constantly reinventing the wheel.

Classical Implicational Logic

System	Fragment	Number of Symbols	Axioms
Łukasiewicz's implicational axiom	C	13 (minimal 1‑basis)	((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ))

Classical Logic

System	Fragment	Number of Symbols	Axioms
Łukasiewicz's implicational axiom with the principle of explosion	C-O	13+3 = 16 (minimal 2‑basis)	((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ)) ⊥→ψ
Meredith's axiom	C-N	21 (minimal 1‑basis)	((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ))
Walsh's 1st axiom	C-N	21 (minimal 1‑basis)	(ψ→((¬ψ→φ)→χ))→(ξ→((¬τ→(χ→τ))→(ψ→τ)))
Walsh's 2nd axiom	C-N	21 (minimal 1‑basis)	ψ→((φ→(ψ→χ))→((¬χ→((¬ξ→τ)→φ))→(ξ→χ)))
Walsh's 3rd axiom	C-N	21 (minimal 1‑basis)	ψ→((¬φ→((¬χ→ξ)→(ψ→τ)))→((τ→φ)→(χ→φ)))
Walsh's 4th axiom	C-N	21 (minimal 1‑basis)	ψ→((¬φ→((¬χ→ξ)→(τ→φ)))→((χ→τ)→(χ→φ)))
Walsh's 5th axiom	C-N	21 (minimal 1‑basis)	(ψ→φ)→(((χ→(ξ→τ))→(φ→(¬ξ→¬ψ)))→(ψ→ξ))
Walsh's 6th axiom	C-N	21 (minimal 1‑basis)	((ψ→φ)→(((¬χ→¬ξ)→χ)→τ))→((τ→ψ)→(ξ→ψ))
Łukasiewicz (L₁)-system (no data apart from luk‑pmproofs)	C-N	11+6+6 = 23 (smallest known 3‑basis)	(ψ→φ)→((φ→χ)→(ψ→χ)) (¬ψ→ψ)→ψ ψ→(¬ψ→φ)
Łukasiewicz (L₃)-system	C-N	5+13+9 = 27	ψ→(φ→ψ) (ψ→(φ→χ))→((ψ→φ)→(ψ→χ)) (¬ψ→¬φ)→(φ→ψ)

Classical Modal Logic

System	Fragment	Number of Symbols	Axioms
S5 (extension of Łukasiewicz (L₃)‑system)	C-N-L	5+13+9+4+10+10 = 51	ψ→(φ→ψ) (ψ→(φ→χ))→((ψ→φ)→(ψ→χ)) (¬ψ→¬φ)→(φ→ψ) □ψ→ψ □(ψ→φ)→(□ψ→□φ) ¬□¬ψ→□¬□¬ψ  [alias ◇ψ→□◇ψ]