Logiweb codex of prop

Up Help

prop, ∗ ⇒ ∗, A1, A2, A3, MP, PropositionalCalculus, AutoImply,

prop

[prop →^{pyk} “prop”]

∗ ⇒ ∗

[x ⇒ y →^{val} y : If(∗, y, T)]

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

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

A1

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

[A1 →^{tex} “A1”]

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

A2

[A2 →^{proof} Rule tactic] [A2 →^{stmt} PropositionalCalculus ⊢ ∀\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} PropositionalCalculus ⊢ ∀\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} PropositionalCalculus ⊢ ∀\underline{b}: ∀\underline{c}: [ \underline{b} ⊢ [ [ \underline{b} ⇒ \underline{c} ] ⊢ \underline{c} ] ] ]

[MP →^{tex} “MP”]

[MP →^{pyk} “mp”]

PropositionalCalculus

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

[PropositionalCalculus →^{pyk} “prop theory”]

AutoImply

[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)]

[AutoImply →^{stmt} PropositionalCalculus ⊢ ∀\underline{b}: [ \underline{b} ⇒ \underline{b} ] ]

[AutoImply →^{tex} “AutoImply”] [AutoImply →^{pyk} “auto imply”]

The pyk compiler, version 0.grue.20050502+ by Klaus Grue GRD-2005-06-02.UTC:08:43:13.701947 = MJD-53523.TAI:08:43:45.701947 = LGT-4624418625701947e-6