[propositional calculus =^{pyk} “propositional calculus”] [Theory T_{PC}] [T_{PC} =^{pyk} “propositional theory”] [x ⇒ y =^{pyk} “∗ imply ∗”] [x ⇒ y ˙= ¬x ∨ y] [T ⇒ T]^{·} [T ⇒ F]^{−} [F ⇒ T]^{·} [F ⇒ F]^{·} [A1 =^{pyk} “axiom one”] [A2 =^{pyk} “axiom two”] [A3 =^{pyk} “axiom three”]

[MP =^{pyk} “mp”]

[T_{PC} rule A1: ∀B: ∀C: B ⇒ C ⇒ B] [T_{PC} rule A2: ∀B: ∀C: ∀D: (B ⇒ C ⇒ D) ⇒ (B ⇒ C) ⇒ B ⇒ D] [T_{PC} rule A3: ∀B: ∀C: (¬C ⇒ ¬B) ⇒ (¬C ⇒ B) ⇒ C] [T_{PC} rule MP: ∀B: ∀C: B ⊢ B ⇒ C ⊢ C] [LEMMA1.8 =^{pyk} “mendelson lemma one eight”] [T_{PC} lemma LEMMA1.8: ∀B: B ⇒ B] T_{PC} proof of LEMMA1.8:

L01: Arbitrary ≫  B  ;
L02: A2 ≫  {(B ⇒ (B ⇒ B) ⇒ B) ⇒ (B ⇒ \atop B ⇒ B) ⇒ B ⇒ B  ;}
L03: A1 ≫  B ⇒ (B ⇒ B) ⇒ B  ;
L04: MP ⊳ L03 ⊳ L02 ≫  (B ⇒ B ⇒ B) ⇒ B ⇒ B  ;
L05: A1 ≫  B ⇒ B ⇒ B  ;
L06: MP ⊳ L05 ⊳ L04 ≫  B ⇒ B  □

A TEX definitions

[T_{PC} =^{tex} “T {PC}”]

[x ⇒ y =^{tex} “#1.

\Rightarrow #2.”]

[A1 =^{tex} “A1”]

[A2 =^{tex} “A2”]

[A3 =^{tex} “A3”]

[MP =^{tex} “MP”]

[LEMMA1.8 =^{tex} “LEMMA 1.8”]