Lecture #10 —Continued (Oct. 9)
0.0.1 Metatheorem. (Hypothesis splitting/merging)
For any wff A,B,C and hypotheses Γ, we have Γ ∪ {A,B} ⊢ C iff
Γ ∪ {A ∧ B} ⊢ C.
Proof. ( Hilbert-style)
(I)ASSUMEΓ∪{A,B}⊢C andPROVEΓ∪{A∧B}⊢C.
So, armed with Γ and A ∧ B as hypotheses I have to prove C. (1) A ∧ B ⟨hyp⟩
(2) A
(3) B
(4) C
⟨(1) + A ∧ B ⊢ A rule ⟩
⟨(1) + A ∧ B ⊢ B rule ⟩ ⟨using HYP Γ + (2) and (3) ⟩
(II)ASSUMEΓ∪{A∧B}⊢C andPROVEΓ∪{A,B}⊢C. Exercise, or see Text.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
1
0.0.2 Theorem. (Modus Ponens) A, A → B ⊢ B Proof.
A→B
⇔ ⟨¬∨-theorem⟩
¬A∨B
⇔ ⟨(Leib) + hyp A + Red-⊤-META; “Denom:” ¬p ∨ B⟩
¬⊤∨B
⇔ ⟨(Leib) + theorem from class; “Denom:” p ∨ B⟩
⊥∨B
⇔ ⟨thm from class⟩
B
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
2
0.0.3 Theorem. (Cut Rule) A∨B,¬A∨C ⊢B∨C
Proof. We start with an AUXILIARY theorem —a Lemma— which makes the most complex hypothesis ¬A ∨ C usable (an EQUIVA- LENCE).
¬A∨C
⇔ ⟨how to lose a NOT⟩
A∨C≡C
Since ¬A ∨ C is a HYP hence also a THEOREM, the same is true for A ∨ C ≡ C from the Equational proof above.
B∨C
⇔ ⟨(Leib) + Lemma; “Denom:” B ∨ p⟩
B ∨ (A ∨ C)
⇔ ⟨shifting brackets to our advantage AND swapping wff⟩
(A∨B)∨C
⇔ ⟨(Leib) + HYP A ∨ B + Red-⊤-Meta; “Denom:” p ∨ C⟩
⊤∨C Bingo!
3
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
B.
0.0.5 Corollary. A ∨ B, ¬A ⊢ B Proof. Apply the rule ¬A ⊢ ¬A ∨ B.
We now can use the above Corollary!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
4
SPECIAL CASES of CUT:
0.0.4 Corollary. A ∨ B, ¬A ∨ B ⊢ B
Proof. From0.0.3wegetA∨B,¬A∨B⊢B∨B.
We have also learnt the rule B ∨ B ⊢ B.
Apply this rule to the proof above that ends with “B ∨ B” to get
(1) A
(2) ¬A
(3) A∨⊥ (4) ¬A∨⊥ (5) ⊥
⟨hyp⟩
⟨hyp⟩ ⟨1+ruleX⊢X∨Y⟩ ⟨2+ruleX⊢X∨Y⟩ ⟨3+4+rule0.0.4⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
5
0.0.6 Corollary. A, ¬A ⊢ ⊥ Proof. Hilbert-style.
(5) ¬A ∨ B
(6) ¬B ∨ C
(7) ¬A∨C
⟨(1, 3) + (Eqn)⟩
⟨(2, 4) + (Eqn)⟩ ⟨(5,6)+CUT⟩
The last line is provably equivalent to A → C by the ¬∨ theorem.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
6
0.0.7 Corollary. (Transitivity of →) A → B, B → C ⊢ A → C Proof. (Hilbert style)
(1) A→B ⟨hyp⟩
(2) B→C ⟨hyp⟩
(3) A→B≡¬A∨B ⟨¬∨thm⟩
(4) B→C≡¬B∨C⟨¬∨thm⟩
and
Thus,
A∨C≡C (1) B∨D≡D (2)
A∨B→C∨D ⇔ ⟨axiom⟩
A∨C∨B∨D≡C∨D ⇔⟨(Leib)+(1);“Denom:” p∨B∨D≡C∨D⟩
C∨B∨D≡C∨D ⇔⟨(Leib)+(2);“Denom:” C∨p≡C∨D⟩
C∨D≡C∨D Bingo!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
7
0.0.8 Theorem. A → C, B → D ⊢ A ∨ B → C ∨ D
Proof. As in the proof of 0.0.3, the analysis of the two HYPs gives as
the two theorems from our “Γ”:
0.0.9 Corollary. (The RULE of Proof By Cases)
A → C, B → C ⊢ A ∨ B → C Proof.
By 0.0.8, we get
A → C, B → C ⊢ A ∨ B → C ∨ C
But then
A∨B→C∨C
⇔ ⟨idemp. axiom + Leib; “Denom”: A ∨ B → p⟩
A∨B→C
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
8