[prop →^{pyk} “prop”] Forsoeg paa implikation: [x ⇒ y →^{val} y : If(∗, y, T)] [x ⇒ y →^{pyk} “∗ imply ∗”] Her er vores teori: [PropositionalCalculus →^{tex} “Propositional Calculus”] [PropositionalCalculus →^{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}] [PropositionalCalculus →^{pyk} “prop theory”] Vi forsoeger at definere axiom 1:

[A1 →^{tex} “A1”]

[A1 →^{stmt} PropositionalCalculus ⊢ ∀\underline{b}: ∀\underline{c}: \underline{b} ⇒ \underline{c} ⇒ \underline{b}][A1 →^{proof} Rule tactic] [A1 →^{pyk} “axiom one”] Saa er turen kommet til axiom 2:

[A2 →^{tex} “A2”]

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

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

[A3 →^{tex} “A3”]

[A3 →^{stmt} PropositionalCalculus ⊢ ∀\underline{b}: ∀\underline{c}: ¬\underline{c} ⇒ ¬\underline{b} ⇒ ¬\underline{c} ⇒ \underline{b} ⇒ \underline{c}][A3 →^{proof} Rule tactic]

[A3 →^{pyk} “axiom three”] Saa definerer vi modus ponens...

[MP →^{tex} “MP”]

[MP →^{stmt} PropositionalCalculus ⊢ ∀\underline{b}: ∀\underline{c}: \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{c}][MP →^{proof} Rule tactic]

[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”] [AutoImply →^{stmt} PropositionalCalculus ⊢ ∀\underline{b}: \underline{b} ⇒ \underline{b}] Saa langt saa godt... [AutoImply →^{proof} λc.λx.P(⌈PropositionalCalculus ⊢ ∀\underline{b}: A1 ≫ \underline{b} ⇒ \underline{b} ⇒

\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}; MP ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⊳ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{b} ≫ \underline{b} ⇒ \underline{b}⌉, p_{0}, c)]

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