Propositional Calculus

Allan Hvam Petersen

GRD-2005-06-02.UTC:18:16:36.700631

[propositional calculus =^{pyk} “propositional calculus”] Define theory: [Theory T_{Prop}]^{1}

Implication

[x ⇒ y ˙= ¬x ∨ y] ^{2}

Axioms

[T_{Prop} rule A1: ∀A: ∀B: A ⇒ B ⇒ A] ^{3} [T_{Prop} rule A2: ∀A: ∀B: ∀C: (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C] ^{4} [T_{Prop} rule A3: ∀A: ∀B: (¬A ⇒ ¬B) ⇒ (¬A ⇒ B) ⇒ A] ^{5} [T_{Prop} rule A4: ∀A: ∀B: ∀C: C free for B in A ⊢⊢ ∀B: A ⇒ ⟨A |B:= C⟩] ^{6} [T_{Prop} rule A5: ∀A: ∀B: ∀C: ¬C free in A ⊢⊢ (∀C: A ⇒ B) ⇒ A ⇒ ∀C: B] ^{7} [T_{Prop} rule MP: ∀A: ∀B: A ⊢ A ⇒ B ⊢ B] ^{8} [T_{Prop} rule Gen: ∀A: ∀B: A ⊢ ∀B: A] ^{9}

Proof

[T_{Prop} lemma Mendelson 1.8: ∀A: A ⇒ A] ^{10} T_{Prop} proof of Mendelson 1.8:

L01: Arbitrary ≫  A  ;
L02: A2 ≫  {(A ⇒ (A ⇒ A) ⇒ A) ⇒ (A ⇒ \atop A ⇒ A) ⇒ A ⇒ A  ;}

1[T_{Prop} =^{pyk} “propositional theory”]

2[x ⇒ y =^{pyk} “∗ imply ∗”]

3[A1 =^{pyk} “axiom one”]

4[A2 =^{pyk} “axiom two”]

5[A3 =^{pyk} “axiom three”]

6[A4 =^{pyk} “axiom four”]

7[A5 =^{pyk} “axiom five”]

8[MP =^{pyk} “axiom mp”]

9[Gen =^{pyk} “axiom gen”]

10[Mendelson 1.8 =^{pyk} “mendelson lemma one eight”]

L03: A1 ≫  A ⇒ (A ⇒ A) ⇒ A  ;
L04: MP ⊳ L03 ⊳ L02 ≫  (A ⇒ A ⇒ A) ⇒ A ⇒ A  ;
L05: A1 ≫  A ⇒ A ⇒ A  ;
L06: MP ⊳ L05 ⊳ L04 ≫  A ⇒ A  □

Experimental

[T_{Prop} lemma Mendelson 1.10a: ∀E: ∀D: ∀F: D ⇒ E ⊢ E ⇒ F ⊢ D ⇒ F] ^{11} T_{Prop} proof of Mendelson 1.10a:

L01: Arbitrary ≫  E  ;
L02: Arbitrary ≫  D  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  D ⇒ E  ;
L05: Premise ≫  E ⇒ F  ;
L06: A2 ≫  {(D ⇒ E ⇒ F) ⇒ (D ⇒ E) ⇒ \atop D ⇒ F  ;}
L07: A1 ≫  (E ⇒ F) ⇒ D ⇒ (E ⇒ F)  ;
L08: MP ⊳ L05 ⊳ L07 ≫  D ⇒ (E ⇒ F)  ;
L09: MP ⊳ L08 ⊳ L06 ≫  (D ⇒ E) ⇒ D ⇒ F  ;
L10: MP ⊳ L04 ⊳ L09 ≫  D ⇒ F  □

[T_{Prop} lemma Mendelson 1.10b: ∀D: ∀E: ∀F: D ⇒ E ⇒ F ⊢ E ⊢ D ⇒ F] ^{12} T_{Prop} proof of Mendelson 1.10b:

L01: Arbitrary ≫  D  ;
L02: Arbitrary ≫  E  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  D ⇒ E ⇒ F  ;
L05: Premise ≫  E  ;
L06: A2 ≫  {(D ⇒ E ⇒ F) ⇒ (D ⇒ E) ⇒ \atop D ⇒ F  ;}
L07: A1 ≫  E ⇒ D ⇒ E  ;
L08: MP ⊳ L05 ⊳ L07 ≫  D ⇒ E  ;
L09: MP ⊳ L04 ⊳ L06 ≫  (D ⇒ E) ⇒ D ⇒ F  ;
L10: MP ⊳ L08 ⊳ L09 ≫  D ⇒ F  □

[T_{Prop} lemma Mendelson 1.11a: ∀G: ¬¬G ⇒ G] ^{13} T_{Prop} proof of Mendelson 1.11a:

L01: Arbitrary ≫  G  ;
L02: A3 ≫  {(¬G ⇒ ¬¬G) ⇒ (¬G ⇒ ¬G) ⇒ \atop G  ;}
L03: Mendelson 1.8 ≫  ¬G ⇒ ¬G  ;
L04: A1 ≫  ¬¬G ⇒ (¬G ⇒ ¬¬G)  ;
L05: Mendelson 1.10b⊳L02⊳L03 ≫ (¬G ⇒ ¬¬G) ⇒ G  ;

11[Mendelson 1.10a =^{pyk} “mendelson corollary one ten a”]

12[Mendelson 1.10b =^{pyk} “mendelson corollary one ten b”]

13[Mendelson 1.11a =^{pyk} “mendelson lemma one eleven a”]

L06: Mendelson 1.10a⊳L04⊳L05 ≫ ¬¬G ⇒ G  □

A TEX definitions

[T_{Prop} =^{tex} “

T {Prop}”]

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

\Rightarrow{}#2.”]

[A1 =^{tex} “A1”]

[A2 =^{tex} “A2”]

[A3 =^{tex} “A3”]

[A4 =^{tex} “A4”]

[A5 =^{tex} “A5”]

[MP =^{tex} “MP”]

[Gen =^{tex} “Gen”] [Mendelson 1.8 =^{tex} “Mendelson\ \textbf{1.8}”] [Mendelson 1.10a =^{tex} “Mendelson\ \textbf{1.10} a”] [Mendelson 1.10b =^{tex} “Mendelson\ \textbf{1.10} b”] [Mendelson 1.11a =^{tex} “Mendelson\ \textbf{1.11} a”]

B Test

[T ⇒ T]^{·} [T ⇒ F]^{−} [F ⇒ T]^{·} [F ⇒ F]^{·}

C Priority table

Priority table Preassociative [propositional calculus], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [array-plus(∗, ∗)], [array-remove(∗, ∗, ∗)], [arrayput(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)],

[S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)], [S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)],

[S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)], [S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [color(∗ : ∗)], [color^{∗}(∗ : ∗)], [vars(∗)], [vars^{∗}(∗)], [instantiate(∗ + ∗ : ∗)], [instantiate^{∗}(∗ + ∗ : ∗)], [unify(∗ : ∗ = ∗ : ∗ + ∗)], [unify^{∗}(∗ : ∗ = ∗ : ∗ + ∗)], [unify_{1}(∗ : ∗ = ∗ : ∗ + ∗)], [unify_{2}(∗ + ∗)], [unify_{3}(∗ = ∗ + ∗)], [check], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗)], [occur^{∗}(∗, ∗)], [circular(∗ = ∗, ∗)], [circular^{∗}(∗ = ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [T_{Prop}], [A1], [A2], [A3], [A4], [A5], [MP], [Gen], [Mendelson 1.8], [Mendelson 1.10a], [Mendelson 1.10b], [Mendelson 1.11a], [nani teta saka...:13]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}]; Preassociative [∗ · ∗], [∗ ·_{0} ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗]; Preassociative [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ¨⇒ ∗]; Postassociative [∗ : ∗], [∗!∗]; Postassociative [∗ ⇒ ∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; End table