[prop =^{pyk} “prop”] Forsoeg paa implikation: [x ⇒ y ˙= y : (∗ ¨⇒ y)] [x ⇒ y =^{pyk} “∗ imply ∗”] Her er vores teori: [PropositionalCalculus =^{tex} “Propositional Calculus”] [Theory PropositionalCalculus] [PropositionalCalculus =^{pyk} “prop theory”] Vi forsoeger at definere axiom 1:

[A1 =^{tex} “A1”]

[PropositionalCalculus rule A1: ∀B: ∀C: B ⇒ C ⇒ B] [A1 =^{pyk} “axiom one”] Saa er turen kommet til axiom 2:

[A2 =^{tex} “A2”]

[PropositionalCalculus rule A2: ∀B: ∀C: ∀D: (B ⇒ C ⇒ D) ⇒ (B ⇒ C) ⇒ B ⇒ D]

[A2 =^{pyk} “axiom two”] Efter aksiom 2 kommer aksiom 3:

[A3 =^{tex} “A3”]

[PropositionalCalculus rule A3: ∀B: ∀C: (¬C ⇒ ¬B) ⇒ (¬C ⇒ B) ⇒ C] [A3 =^{pyk} “axiom three”] Saa definerer vi modus ponens...

[MP =^{tex} “MP”]

[PropositionalCalculus rule MP: ∀B: ∀C: B ⊢ B ⇒ C ⊢ C]

[MP =^{pyk} “mp”]

Vi kan nu formelt udtrykke den paastand, at ethvert udsagn implicerer sig selv: HVAD SKER DER HEEEEERR?????? [AutoImply =^{tex} “AutoImply”]

[AutoImply =^{pyk} “auto imply”] [PropositionalCalculus lemma AutoImply: ∀B: B ⇒ B] Saa langt saa godt... PropositionalCalculus proof of AutoImply:

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

Tests: [2 + 3 ≈ 7]^{−}