Pyk-definitioner: [propcalc →^{pyk} “propcalc”] [x ⇒ y →^{pyk} “∗ implies ∗”] [A1 →^{pyk} “axiom one”] [A2 →^{pyk} “axiom two”] [A3 →^{pyk} “axiom three”] [MP →^{pyk} “rule mp”] [Mendelson1.8 →^{pyk} “lemma id”]

[propcalc →^{stmt} ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⊕ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}]

Tex-definitioner: [¬x →^{tex} “\neg #1.”] [x ⇒ y →^{tex} “#1. \Rightarrow{} #2.”] [A1 →^{tex} “A1”] [A2 →^{tex} “A2”] [A3 →^{tex} “A3”] [MP →^{tex} “MP”] [Mendelson1.8 →^{tex} “Mendelson 1.8”]

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

Rule tactic] [A3 →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}][A3 →^{proof} Rule tactic] [MP →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{a} ⇒ \underline{b} ⊢ \underline{b}][MP →^{proof} Rule tactic] [mendelson lemma one eight →^{stmt} propcalc ⊢ ∀\underline{a}: \underline{a} ⇒ \underline{a}] ^{1} [mendelson lemma one eight →^{proof} λc.λx.P(⌈propcalc ⊢ ∀\underline{a}: A2 ≫ \underline{a} ⇒ \underline{a} ⇒

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

1[mendelson lemma one eight →^{pyk} “mendelson lemma one eight”]