[propositional calculus →^{pyk} “propositional calculus”] [T_{PC} →^{stmt} ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: \underline{b} ⇒ \underline{c} ⇒ \underline{d} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{b} ⇒ \underline{d} ⊕ ∀\underline{b}: ∀\underline{c}: \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{c} ⊕

∀\underline{b}: ∀\underline{c}: \underline{b} ⇒ \underline{c} ⇒ \underline{b} ⊕ ∀\underline{b}: ∀\underline{c}: ¬\underline{c} ⇒ ¬\underline{b} ⇒ ¬\underline{c} ⇒ \underline{b} ⇒ \underline{c}] [T_{PC} →^{pyk} “propositional theory”] [x ⇒ y →^{pyk} “∗ imply ∗”]

[x ⇒ y →^{val} ¬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”]

[A1 →^{stmt} T_{PC} ⊢ ∀\underline{b}: ∀\underline{c}: \underline{b} ⇒ \underline{c} ⇒ \underline{b}][A1 →^{proof} Rule tactic] [A2 →^{stmt} T_{PC} ⊢ ∀\underline{b}: ∀\underline{c}: ∀\underline{d}: \underline{b} ⇒ \underline{c} ⇒ \underline{d} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{b} ⇒ \underline{d}][A2 →^{proof}

Rule tactic] [A3 →^{stmt} T_{PC} ⊢ ∀\underline{b}: ∀\underline{c}: ¬\underline{c} ⇒ ¬\underline{b} ⇒ ¬\underline{c} ⇒ \underline{b} ⇒ \underline{c}][A3 →^{proof} Rule tactic] [MP →^{stmt} T_{PC} ⊢ ∀\underline{b}: ∀\underline{c}: \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{c}][MP →^{proof} Rule tactic] [LEMMA1.8 →^{pyk} “mendelson lemma one eight”] [LEMMA1.8 →^{stmt} T_{PC} ⊢ ∀\underline{b}: \underline{b} ⇒ \underline{b}] [LEMMA1.8 →^{proof} λc.λx.P(⌈T_{PC} ⊢ ∀\underline{b}: A2 ≫ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒

\underline{b} ⇒ \underline{b} ⇒ \underline{b}; A1 ≫ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ≫ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b}; A1 ≫ \underline{b} ⇒ \underline{b} ⇒ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ≫ \underline{b} ⇒ \underline{b}⌉, p_{0}, c)]

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”]