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

[Theory propcalc] 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”]

[propcalc rule A1: ∀A: ∀B: A ⇒ B ⇒ A] [propcalc rule A2: ∀A: ∀B: ∀C: (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C] [propcalc rule A3: ∀A: ∀B: (¬B ⇒ ¬A) ⇒ (¬B ⇒ A) ⇒ B] [propcalc rule MP: ∀A: ∀B: A ⊢ A ⇒ B ⊢ B] [propcalc lemma mendelson lemma one eight: ∀A: A ⇒ A] ^{1} propcalc proof of mendelson lemma one eight:

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

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