Logiweb codex of propositional calculus

Up Help

propositional calculus, T_{PC}, A1, A2, A3, MP, LEMMA1.8, ∗ ⇒ ∗,

propositional calculus

[propositional calculus →^{pyk} “propositional calculus”]

T_{PC}

[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} →^{tex} “T {PC}”] [T_{PC} →^{pyk} “propositional theory”]

A1

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

[A1 →^{tex} “A1”]

[A1 →^{pyk} “axiom one”]

A2

[A2 →^{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 →^{tex} “A2”]

[A2 →^{pyk} “axiom two”]

A3

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

[A3 →^{tex} “A3”]

[A3 →^{pyk} “axiom three”]

MP

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

[MP →^{tex} “MP”]

[MP →^{pyk} “mp”]

LEMMA1.8

[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)] [LEMMA1.8 →^{stmt} T_{PC} ⊢ ∀\underline{b}: [ \underline{b} ⇒ \underline{b} ] ] [LEMMA1.8 →^{tex} “LEMMA 1.8”] [LEMMA1.8 →^{pyk} “mendelson lemma one eight”]

∗ ⇒ ∗

[x ⇒ y →^{val} [ ¬x ] ∨ y]

[x ⇒ y →^{tex} “#1.

\Rightarrow #2.”] [x ⇒ y →^{pyk} “∗ imply ∗”]

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-06-06.UTC:10:04:56.802958 = MJD-53527.TAI:10:05:28.802958 = LGT-4624769128802958e-6