Lecture #9, Oct. 7 —Continued
0.0.1 Theorem. ⊢ ⊤ ≡ ¬⊥ Proof. (Equational)
⊤
⇔ ⟨axiom⟩
⊥≡⊥
⇔ ⟨axiom⟩
¬⊥
0.0.2 Theorem. ⊢ ⊥ ≡ ¬⊤ Proof. (Equational)
¬⊤
⇔ ⟨axiom⟩
⊤≡⊥
⇔ ⟨red. ⊤⟩
⊥
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
1
0.0.3 Theorem. ⊢ A ∨ ⊤ Proof.
A∨⊤
⇔ ⟨(Leib) + axiom: ⊤ ≡ ⊥ ≡ ⊥; “Denom:” A ∨ p; Mind the brackets!⟩
A∨(⊥ ≡ ⊥) ⇔ ⟨axiom⟩
A∨⊥≡A∨⊥ Bingo!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
2
Recall about ≡ that, by axiom (1) and a theorem we proved in class, if we read Axiom (1) right to left we get a theorem.
This meant that in a chain of TWO “≡” it does not matter how we inserted brackets, and thus can totally omit them.
Without proof we stated that in a chain of any number of ≡ we may omit brackets. See course URL
http://www.cs.yorku.ca/~gt/courses/MATH1090F20/1090.html
bullet three under “Misc Notes”.
The same holds for a chain of ∨ using the same kind of steps:
• Prove that ⊢ A ∨ (B ∨ C) ≡ (A ∨ B) ∨ C, that is, reading axiom (5) right to left is a theorem. Indeed here is a short Hilbert proof:
(1) (A∨B)∨C≡A∨(B∨C) ⟨axiom(5)⟩
(2) A∨(B∨C)≡(A∨B)∨C ⟨1+Rulecomm.⟩
Thus, in a chain of TWO “∨” it does not matter how we inserted brackets, and thus can totally omit them.
• The NOTE in the URL above generalises this to a chain of any number of “∨”.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
3
OK, so we do not need to show bracketing in a chain of ≡ or ∨. How about moving formulas around in such a chain? (Permuting
them).
It is OK! I prove this for ∨-chains. The proof is identical for ≡- chains.
EXERCISE!!
Start with this theorem:
⊢B∨C∨D≡D∨C∨B
Indeed here is a proof:
B∨C∨D ⇔ ⟨axiom (6)⟩
D∨B∨C (∗) ⇔ ⟨(Leib) + axiom (6). “Denom:” D ∨ p⟩
D∨C∨B
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
4
More generally we CAN DO an arbitrary swap (not only the END- FORMULAS), that is, we have the theorem
⊢A∨B∨C∨D∨E≡A∨D∨C∨B∨E
Follows by an application of the previous special case:
A∨B∨C∨D∨E
⇔ ⟨(Leib) + special case. “Denom:” A ∨ p ∨ E⟩
A∨D∨C∨B∨E
5
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.4 Theorem. ⊢A∨⊥≡A Proofs. (Equational)
This time we work with the entire formula, not just one of the sides of “≡”.
How do we know? We don’t. It is just practice.
A∨⊥≡A ⇔⟨(Leib)+axiomA≡A∨A;“Denom:” A∨⊥≡p⟩
A∨⊥≡A∨A ⇔ ⟨axiom ∨ over ≡⟩
A ∨ (⊥ ≡ A)
⇔⟨(Leib)+axiom: ⊥≡A≡¬A;“Denom:” A∨p⟩
A∨¬A Bingo!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
6
0.0.5 Theorem. ⊢ A → B ≡ ¬A ∨ B Proof.
A→B ⇔ ⟨axiom⟩
A∨B≡B HERE ⇔ ⟨(Leib) + 0.0.4; “Denom:” A ∨ B ≡ p⟩
A∨B≡⊥∨B ⇔ ⟨axiom⟩
(A ≡ ⊥)∨B
⇔ ⟨(Leib) + axiom; “Denom:” p ∨ B⟩
¬A∨B Comment on “same” p in above proof.
0.0.6 Corollary. ⊢ ¬A ∨ B ≡ A ∨ B ≡ B Proof. Start the above proof from “HERE”.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
7
0.0.7 Theorem. (de Morgan 1) ⊢ A ∧ B ≡ ¬(¬A ∨ ¬B)
Proof.
Long but obvious. Start with the most complex side!
¬(¬A ∨ ¬B)
⇔ ⟨axiom⟩
¬A ∨ ¬B ≡ ⊥
⇔ ⟨(Leib) + 0.0.6; “Denom:” p ≡ ⊥⟩
A ∨ ¬B ≡ ¬B ≡ ⊥
⇔ ⟨(Leib) + axiom; “Denom:” A ∨ ¬B ≡ p —order does not matter!⟩
A ∨ ¬B ≡ B
⇔ ⟨(Leib) + 0.0.6; “Denom:” p ≡ B⟩
A∨B≡A≡B
⇔ ⟨GR axiom —order does not matter⟩
A∧B
0.0.8 Corollary. (de Morgan 2) ⊢ A ∨ B ≡ ¬(¬A ∧ ¬B) Proof. See Text. Better still, EXERCISE!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
8
About “∧”
0.0.9 Theorem. ⊢A∧A≡A Proof.
A∧A≡A
⇔ ⟨axiom —order does not matter⟩
A∨A≡A Bingo!
0.0.10 Theorem. ⊢ A ∧ ⊤ ≡ A Proof.
A∧⊤≡A
⇔ ⟨GR axiom⟩
A∨⊤≡⊤
⇔ ⟨Red. ⊤⟩
A∨⊤ Bingo!
0.0.11 Theorem. ⊢ A ∧ ⊥ ≡ ⊥ Proof.
A∧⊥≡⊥ ⇔ ⟨GR axiom⟩
A∨⊥≡A Bingo! Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
9
0.0.12 Theorem.
(i) ⊢A∨B∧C ≡(A∨B)∧(A∨C) and
(ii) ⊢ A ∧ (B ∨ C) ≡ A ∧ B ∨ A ∧ C
The above are written in least parenthesised notation! Proof.
We just prove (i).
(A∨B)∧(A∨C) ⇔ ⟨GR⟩
A∨B∨A∨C≡A∨B≡A∨C ⇔⟨(Leib)+scramblean∨-chain;“Denom:” p≡A∨B≡A∨C⟩
A∨A∨B∨C≡A∨B≡A∨C ⇔⟨(Leib)+axiom;“Denom:” p∨B∨C≡A∨B≡A∨C⟩
A∨B∨C≡A∨B≡A∨C
HERE WE STOP, and try to reach this result from the other side: A ∨ B ∧ C.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
10
A∨B∧C
⇔ ⟨(Leib) + GR; “Denom:” A ∨ p; mind brackets!⟩
A ∨ (B ∨ C ≡ B ≡ C) ⇔ ⟨axiom⟩
A ∨ B ∨ C ≡ A ∨ (B ≡ C) ⇔⟨(Leib)+axiom;“Denom:” A∨B∨C≡p⟩
A∨B∨C≡A∨B≡A∨C
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
11
0.0.13 Corollary. ⊢ A ∨ B → C ≡ (A → C) ∧ (B → C) Proof.
A∨B→C
⇔ ⟨0.0.5⟩
¬(A∨B)∨C
⇔ ⟨(Leib) + 0.0.8; “Denom:” ¬p ∨ C⟩
¬¬(¬A∧¬B)∨C
⇔ ⟨(Leib) + double neg.; “Denom:” p ∨ C⟩
(¬A∧¬B)∨C
⇔ ⟨0.0.12⟩
(¬A ∨ C) ∧ (¬B ∨ C)
⇔ ⟨obvious (Leib), twice + 0.0.5⟩
(A → C) ∧ (B → C)
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
12
Lecture #10, Oct. 9
0.0.14 Corollary. ⊢A→B∧C ≡(A→B)∧(A→C) Proof.
A→B∧C ⇔ ⟨0.0.5⟩
¬A ∨ B ∧ C ⇔ ⟨0.0.12⟩
(¬A∨B)∧(¬A∨C)
⇔ ⟨obvious (Leib) twice + 0.0.5⟩
(A → B) ∧ (A → C)
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
13
Until now we only proved absolute theorems Equationally.
How about theorems with HYPOTHESES?
To do so we use the Redundant ⊤ METAtheorem: Γ ⊢ A iff Γ ⊢ A ≡ ⊤
The Technique is demonstrated via Examples!
0.0.15 Example. (1) A, B ⊢ A ∧ B (2) A ∨ A ⊢ A
(3) A ⊢ A ∨ B
(4) A ∧ B ⊢ A
For (1):
A∧B
⇔ ⟨(Leib) + hyp B + Red. ⊤ META; “Denom:” A ∧ p⟩
A∧⊤ ⇔ ⟨0.0.10⟩
A Bingo!
A,B⊢B. HenceA,B⊢B≡⊤
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
14
For (3):
A
⇔ ⟨axiom⟩ A∨A
A∨B
⇔ ⟨(Leib) + Hyp A + Red-⊤-META; “Denom:” p ∨ B⟩
⊤ ∨ B ⟨Bingo!⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
15
For (2):
(4) is a bit trickier:
A
⇔ ⟨0.0.10⟩ A∧⊤
⇔ ⟨(Leib) + Hyp A ∧ B + Red-⊤-META; “Denom:” A ∧ p⟩ A∧A∧B
⇔ ⟨(Leib) + 0.0.9; “Denom:” p ∧ B⟩
A∧B Bingo!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
16