Lecture #7 (Sept. 30)
0.0.1 Corollary. If Γ⊢A and also Γ∪{A}⊢B, then Γ⊢B.
In words, the conclusion says that A drops out as a hypothesis and we
get Γ ⊢ B.
That is, a THEOREM A can be invoked just like an axiom in a
proof! Proof. We have two proofs:
and
When the second box is standalone, the justification for A is “hyp”. Now concatenate the two proofs above in the order
Now change all the justifications for that A in the right box from “hyp” to the same exact reason you gave to the A in box one.
Thus, the status of A as “hyp” is removed and B is proved from Γ
1
from Γ
…A
from Γ ∪ {A}
…A…B
from Γ
…A
from Γ ∪ {A}
…A…B
alone.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.2Corollary. IfΓ∪{A}⊢Band⊢A,thenΓ⊢B.
Proof. By hyp strengthening, I have Γ ⊢ A. Now apply the previous theorem.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
2
0.0.3Theorem. A≡B⊢B≡A Proof.
(1) A≡B ⟨hyp⟩
(2) (A≡B)≡(B≡A)⟨axiom⟩
(3) B≡A ⟨(1,2)+Eqn⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
3
Proof.
(1) ((A≡B)≡C)≡(A≡(B≡C))⟨axiom⟩
(2) (A≡(B≡C))≡((A≡B)≡C)⟨(1)+0.0.3⟩
0.0.5 Remark. Thus, in a chain of two “≡” we can shift brackets from left to right (axiom) but also right to left (above theorem).
So it does not matter how brackets are inserted in such chain.
An induction proof on chain length (see course URL) extends this remark to any chain of “≡”, of any length.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
4
0.0.4Theorem. ⊢(A≡(B≡C))≡((A≡B)≡C)
NOTE. This is the mirror image of Axiom (1).
(1)
(2)
(3)
(4) A ⟨(1, 3) + (Eqn)⟩
(1) ⊤≡⊥≡⊥⟨axiom⟩
(2) ⊥ ≡ ⊥ ⟨theorem⟩
(3) ⊤ ⟨(1, 2) + (Eqn)⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
5
0.0.6 Theorem. (The other (Eqn))
Proof.
Lecture #8 (Oct. 2)
0.0.7 Corollary. ⊢ ⊤ Proof.
B, A ≡ B ⊢ A
B ⟨hyp⟩ A≡B⟨hyp⟩ B≡A⟨(2)+0.0.3⟩
0.0.8Theorem. ⊢A≡A≡B≡B
(1) (A≡B≡B)≡A⟨axiom⟩
(2) A≡(A≡B≡B)⟨(1)+0.0.3⟩
0.0.9Corollary. ⊢⊥≡⊥≡B≡Band⊢A≡A≡⊥≡⊥
NOTE absence of brackets in theorem AND corollary!
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
6
0.0.10Corollary.(Redundant⊤) ⊢⊤≡A≡Aand⊢A≡A≡⊤.
Proof.
(1) ⊤≡⊥≡⊥ ⟨axiom⟩
(2) ⊥ ≡ ⊥ ≡ A ≡ A ⟨absolute theorem⟩
(3) ⊤ ≡ A ≡ A ⟨(Trans) + (1, 2)⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
7
0.0.11 Metatheorem. For any Γ and A, we have Γ⊢A iff Γ⊢A≡⊤.
Proof. Say Γ ⊢ A.
Thus
Γ .
(1) A ⟨Γ-theorem⟩
(2) A ≡ A ≡ ⊤⟨theorem⟩
(3) A ≡ ⊤ ⟨(1, 2) +Eqn⟩
The other direction is similar.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
8
EQUATIONAL PROOFS
Example from high school trigonometry.
Prove that 1 + (tan x)2 = (sec x)2 given the identities tanx= sinx
cos x
secx= 1 cos x
(sin x)2 + (cos x)2 = 1 (Pythagoras’ Theorem)
Equational proof with annotation
1+(tanx)2 = ⟨by (i)⟩
1+(sinx/cosx)2 = ⟨arithmetic⟩
(sin x)2 + (cos x)2 (cos x)2
= ⟨by (iii)⟩ 1
(cos x)2 = ⟨by (ii)⟩
(sec x)2
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
(i)
(ii)
(iii)
9
(E)
An equational proof looks like:
reason reason reason
A1 ≡ A2, A2 ≡ A3,…,An ≡ An+1 (1)
10
0.0.12 Metatheorem.
A1 ≡ A2,A2 ≡ A3,…,An−1 ≡ An,An ≡ An+1 ⊢ A1 ≡ An+1 (2) Proof. By repeated application of (derived) rule (Trans).
For example to show the “special case”
the proof is
(1) A≡B
(2) B≡C
(3) C≡D
(4) D≡E
(5) A≡C
(6) A≡D
(7) A≡E
A ≡ B, B ≡ C, C ≡ D, D ≡ E ⊢ A ≡ E (3)
⟨hyp⟩
⟨hyp⟩
⟨hyp⟩
⟨hyp⟩ ⟨1+2+Trans⟩ ⟨3+5+Trans⟩ ⟨4+6+Trans⟩
For the “general case (2)” do induction on n with Basis at n = 1
(see text; better still do it without looking!)
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.13 Corollary. In an Equational proof (from Γ) like the one in (1) of p.10 we have Γ ⊢ A1 ≡ An+1.
Proof. So we have n Γ-proofs, for i = 1,…,n,
Concatenate them all to get ONE Γ-proof … …
By the DERIVED RULE 0.0.12 the following is a Γ-proof of A1 ≡ An+1 … … A1 ≡An+1
0.0.14 Corollary. In an Equational proof (from Γ) like the one in (1) of p.10 we have Γ⊢A1 iff Γ⊢An+1.
Proof. From the above Corollary we have
Γ⊢A1 ≡An+1 (†)
Now split the “iff” in two directions:
• IF: So we have
This plus (†) plus Eqn yield Γ ⊢ A1.
• ONLY IF: So we have
This plus (†) plus Eqn yield Γ ⊢ An+1.
Γ ⊢ An+1
Γ ⊢ A1
…Ai ≡Ai+1
…Ai ≡Ai+1
…An ≡An+1
11
…A1 ≡A2
…A1 ≡A2
…Ai ≡Ai+1
Γ ⊢ A1 ≡ An+1. Telei’wnoume m’esw tou (Eqn). Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
…An ≡An+1
Equational Proof Layout
Successive equivalences like “Ai ≡ Ai+1 and Ai+1 ≡ Ai+2” we write vertically, without repeating the shared formula Ai+1.
WITH annotation in ⟨. . .⟩ brackets
A1
≡ ⟨annotation⟩
A2
≡ ⟨annotation⟩
. (ii) An−1
≡ ⟨annotation⟩ An
≡ ⟨annotation⟩ An+1
EXCEPT FOR ONE THING!
(ii) is just ONE FORMULA, namely A1 ≡A2 ≡…≡An ≡An+1
which is NOT the same as (1) of p.10.
For example, “⊤ ≡ ⊥ ≡ ⊥” is NOT the same as “⊤ ≡ ⊥
AND ⊥≡⊥”
The former (blue) is true but the latter (red) is false.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
12
What do we do?
We introduce a metasymbol for an equivalence that acts ONLY on two formulas!
Cannot be chained to form ONE formula.
The symbol is “⇔” and thus
“A ⇔ B ⇔ C” MEANS “A ⇔ B AND B ⇔ C”.
We say that “⇔” is CONJUNCTIONAL while “≡” is associative.
13
So the final layout is:
An+1
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
A1
⇔ ⟨annotation⟩
A2
⇔ ⟨annotation⟩
. (The Architecture of an Equational Proof)
An−1
⇔ ⟨annotation⟩
An
⇔ ⟨annotation⟩
Examples.
0.0.15 Theorem. ⊢¬(A≡B)≡¬A≡B
Proof. (Equational)
¬(A ≡ B) ⇔ ⟨axiom⟩
A≡B≡⊥
⇔⟨(Leib)+axiom: B≡⊥≡⊥≡B;Denom: A≡p;pfresh⟩
A≡⊥≡B
⇔⟨(Leib)+axiom: A≡⊥≡¬A;Denom: q≡B;qfresh⟩
¬A ≡ B
0.0.16 Corollary. ⊢ ¬(A ≡ B) ≡ A ≡ ¬B Proof. (Equational)
¬(A ≡ B) ⇔ ⟨axiom⟩
A≡B≡⊥
⇔⟨(Leib)+axiom: B≡⊥≡¬B;Denom: A≡p;pfresh⟩
A ≡ ¬B
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
14
Lecture #9, Oct. 7
0.0.17 Theorem. (Double Negation) ⊢ ¬¬A ≡ A Proof. (Equational)
¬¬A
⇔ ⟨axiom “¬X ≡ X ≡ ⊥”⟩
¬A ≡ ⊥
⇔⟨(Leib)+axiom: ¬A≡A≡⊥;Denom: p≡⊥⟩
A≡⊥≡⊥
⇔⟨(Leib)+axiom: ⊤≡⊥≡⊥;Denom: A≡q⟩
A≡⊤ ⇔ ⟨red. ⊤⟩
A
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
15