Axiomatic system.
Below is Lukasiewicz L3 Axiomatic System:
(A1) ⊢ A→(B→A)
(A2) ⊢ (A→(B→C))→((A→B)→(A→C))
(A3) ⊢ ((¬A→¬B))→(B→A)
(MP) A, A→B ⊢ B
You may set : (type - for ¬ and type = for →)
A:
B:
C:
and write axiom , , or .
Or apply to pr. and pr. .
Thm. ⊢ p→p
Proof.