Propositional Calculus Axioms

Lukasiewicz's Axioms

Law of affirmation of the consequent
Lk1: P ⇒ ( Q ⇒ P )

Law of self-distributivity of implication

Lk2: [P ⇒ ( Q ⇒ R )] ⇒ [( P ⇒ Q ) ⇒ ( P ⇒ R )]

Converse law of contraposition

Lk3: ( ¬ Q ⇒ ¬ P ) ⇒ ( P ⇒ Q )

Lukasiewicz's Alternative Axioms
Lka1: (A ⇒ B) ⇒ [(B ⇒ C) ⇒ (A ⇒ C)]
Lka2: (¬P ⇒ P) ⇒ P
Lka3: P ⇒ (¬P ⇒ Q)

Meredith's Axiom

M1: ({[(P ⇒ Q) ⇒ (¬L ⇒ ¬M)] ⇒ L} ⇒ N) ⇒ [(N ⇒ P) ⇒ (M ⇒ P)]

Tarski's Axioms

T1: P ⇒ (Q ⇒ P)
T2: [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)
T3: (P ⇒ Q) ⇒ [(Q ⇒ R) ⇒ (P ⇒ R)]
T4: (P ⇔ Q) ⇒ (P ⇒ Q)
T5: (P ⇔ Q) ⇒ (Q ⇒ P)
T6: (P ⇒ Q) ⇒ [(Q ⇒ P) ⇒(P ⇔ Q)]
T7: (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)

P. T. Johnstone's Axioms

J1: P ⇒ [Q ⇒ P]
J2: {P ⇒ [Q ⇒ R]} ⇒ {[P ⇒ Q] ⇒ [P ⇒ R]}
J3: {¬[¬P] } ⇒ P