Logiweb codex of propcalc

Up Help

¬∗, propcalc, A1, A2, A3, MP, mendelson lemma one eight, Mendelson1.8,

∗ ⇒ ∗,

¬∗

[¬x →^{tex} “\neg #1.”]

propcalc

[propcalc →^{stmt} [ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ⊢ [ [ \underline{a} ⇒ \underline{b} ] ⊢ \underline{b} ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ⇒ [ \underline{b} ⇒ \underline{c} ] ] ⇒ [ [ \underline{a} ⇒ \underline{b} ] ⇒ [ \underline{a} ⇒ \underline{c} ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ⇒ [ \underline{b} ⇒ \underline{a} ] ] ] ⊕ ∀\underline{a}: ∀\underline{b}: [ [ [ ¬\underline{b} ] ⇒ ¬\underline{a} ] ⇒ [ [ [ ¬\underline{b} ] ⇒ \underline{a} ] ⇒ \underline{b} ] ] ] ] ]

[propcalc →^{pyk} “propcalc”]

A1

[A1 →^{proof} Rule tactic]

[A1 →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ⇒ [ \underline{b} ⇒ \underline{a} ] ] ]

[A1 →^{tex} “A1”]

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

A2

[A2 →^{proof} Rule tactic]

[A2 →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ⇒ [ \underline{b} ⇒ \underline{c} ] ] ⇒ [ [ \underline{a} ⇒ \underline{b} ] ⇒ [ \underline{a} ⇒ \underline{c} ] ] ] ]

[A2 →^{tex} “A2”]

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

A3

[A3 →^{proof} Rule tactic]

[A3 →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: [ [ [ ¬\underline{b} ] ⇒ ¬\underline{a} ] ⇒ [ [ [ ¬\underline{b} ] ⇒ \underline{a} ] ⇒ \underline{b} ] ] ]

[A3 →^{tex} “A3”]

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

MP

[MP →^{proof} Rule tactic]

[MP →^{stmt} propcalc ⊢ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ⊢ [ [ \underline{a} ⇒ \underline{b} ] ⊢ \underline{b} ] ] ]

[MP →^{tex} “MP”]

[MP →^{pyk} “rule mp”]

mendelson lemma one eight

[mendelson lemma one eight →^{proof} λc.λx.P(⌈propcalc ⊢ ∀\underline{a}: [ [ A2 ≫ [ [ \underline{a} ⇒ [ [ \underline{a} ⇒ \underline{a} ] ⇒ \underline{a} ] ] ⇒ [ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ] ; [ [ A1 ≫ [ \underline{a} ⇒ [ [ \underline{a} ⇒ \underline{a} ] ⇒ \underline{a} ] ] ] ; [ [ [ [ MP ⊳ [ \underline{a} ⇒ [ [ \underline{a} ⇒ \underline{a} ] ⇒ \underline{a} ] ] ] ⊳ [ [ \underline{a} ⇒ [ [ \underline{a} ⇒ \underline{a} ] ⇒ \underline{a} ] ] ⇒ [ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ] ≫ [ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ; [ [ A1 ≫ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ; [ [ [ MP ⊳ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ⊳ [ [ \underline{a} ⇒ [ \underline{a} ⇒ \underline{a} ] ] ⇒ [ \underline{a} ⇒ \underline{a} ] ] ] ≫ [ \underline{a} ⇒ \underline{a} ] ] ] ] ] ] ⌉, p_{0}, c)]

[mendelson lemma one eight →^{stmt} propcalc ⊢ ∀\underline{a}: [ \underline{a} ⇒ \underline{a} ] ]

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

Mendelson1.8

[Mendelson1.8 →^{tex} “Mendelson 1.8”]

[Mendelson1.8 →^{pyk} “lemma id”]

∗ ⇒ ∗

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

\Rightarrow{} #2.”]

[x ⇒ y →^{pyk} “∗ implies ∗”]

The pyk compiler, version 0.grue.20050603 by Klaus Grue GRD-2005-06-16.UTC:21:00:55.684114 = MJD-53537.TAI:21:01:27.684114 = LGT-4625672487684114e-6