@xamidi/luk-pmproofs (repository)

Variant of metamath/mmsolitaire/pmproofs of the Metamath Solitaire project which uses alternative axioms

	Infix notation	Polish notation
L1	(ψ→φ)→((φ→χ)→(ψ→χ))	CCpqCCqrCpr
L2	(¬ψ→ψ)→ψ	CCNppp
L3	ψ→(¬ψ→φ)	CpCNpq

from “Łukasiewicz (L₁)-system”.

Contributions

Please create an issue or a pull request in case you find a shorter proof.

Direct Links

• L-pmproofs.txt
• L-pmproofs-nowrap.txt
• L-pm.txt
• L-pm-compact.txt