Lecture #6 (Continued; Sept. 25)
0.0.1 Definition. (Axioms of Boolean Logic) In the following, (1)–(11), A, B, C name or
stand for arbitrary wff.
Properties of ≡
Associativity of ≡ ((A ≡ B) ≡ C) ≡ (A ≡ (B ≡ C)) (1) Symmetry (commutativity) of ≡ (A ≡ B) ≡ (B ≡ A) (2)
Properties of ⊥, ⊤
⊤ and ⊥ ⊤ ≡ ⊥ ≡ ⊥ (3) Properties of ¬
Introduction of ¬ ¬A ≡ A ≡ ⊥ (4) Properties of ∨
1
Associativity of ∨ Symmetry (commutativity) of ∨ Idempotency of ∨ Distributivity of ∨ over ≡ “Excluded Middle”
(A∨B)∨C≡A∨(B∨C) (5) A∨B≡B∨A (6) A∨A≡A (7) A∨(B≡C)≡A∨B≡A∨C (8) A∨¬A (9)
Properties of ∧
“Golden Rule” A ∧ B ≡ A ≡ B ≡ A ∨ B (10) Properties of →
Implication A→B≡A∨B≡B (11)
All of the above (1)–(11) except (3) are schemata for axioms. We call them Axiom Schemata, while (3) is an Axiom. Each axiom schema above defines infinitely many axioms that are its Instances.
So our axioms are (3) and all the instances of the Axiom Schemata (1), (2), (4)–(11).
We reserve the Greek letter Λ for the set of all Axioms of Boolean
Logic.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.2 Definition. (Theorem Constructions —or, simply said, “Proofs”) Let Γ be some set of wff.
A proof from Γ is any finite ordered sequence of formulas that satisfy the following two specifications:
At every step of the Construction (Proof) we may write
Proof 1. Any ONE formula from Λ or Γ.
Proof 2. Any wff A which is the result of an Application of the rule Leib or rule Eqn to wff(s) that appeared in THIS proof before A.
A proof from Γ is also called “Γ-proof”.
2
0.0.3 Remark. (1) So, a proof is a totally syntactic construct, totally devoid of semantic concepts.
(2) Γ is a convenient set of “additional hypotheses”.
Syntactically the elements of Γ “behave” like the Axioms from Λ but semantically
they are NOT the same:
While every member of Λ is a tautology by choice,
this need NOT be the case for the members of Γ.
(3) Since every proof (from some Γ) has finite length, only a finite part of Γ and Λ can
ever appear in some proof.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
3
0.0.4 Definition. (Theorems) Any wff A that appears in a Γ-proof is called a Γ-theorem. We also say, “A is a theorem from Γ”.
In symbols, the sentence “A is a Γ-theorem”, is denoted by “Γ ⊢ A”.
If Γ=∅ then we write ⊢A.
That is, Λ never appears to the left of the turnstile “⊢”.
We call an A such that ⊢ A an absolute or logical theorem.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
Lecture #7 (Sept. 30)
0.0.5 Remark. That A is a Γ-theorem is certified by a Γ-proof like this
B1,…,Bn,A,C1,…,Cm (1)
the sequence (1) obeying the specifications of 0.0.2.
Clearly, the sequence (2) below also satisfies the specifications, since each specification for a Bi
or A that utilises rules refers to formulas to the left only. Thus the sequence (2) is also a Γ-proof of A!
B1,…,Bn,A (2)
The bottom line of this story is expressed as either
1. If you are proving a theorem A, just stop as soon as you wrote it
down with justification in a proof!
OR
2. A Γ-theorem is a wff that appears at the end of some proof.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
4
and
results in a Γ-proof.
Indeed, checking
B1,B2,…,Br
A1,…,An,B1,B2,…,Br
from left to right we give EXACTLY the same reasons we gave for
writing the formulas down in each standalone proof.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
5
Concatenating two Γ-proofs A1,…,An
The reader did not miss to note the similarity between a theorem construction and a formula construction.
Let us develop an Inductive definition for the concept “theorem” just as we did before for the concept “wff”.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
6
So we learnt that a Γ-theorem, let’s call it A, satisfies
1. AismemberofΛorΓ
2. A appears in a Γ-proof as the result of an application of Eqn to wff to its left in the proof.
3. A appears in a Γ-proof as the result of an application of Leib to wff to its left in the proof.
Let us rephrase remembering that a Γ-theorem is a formula that ap- pears in a Γ-proof.
1. AismemberofΛorΓ
2. A is the result of an application of Eqn to two Γ-theorems. 3. A is the result of an application of Leib to one Γ-theorem.
7
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.6 Exercise. How do we do this?
By providing a Γ-proof where our target theorem appears, OR by using the Inductive Definition
of the previous page.
(1) {A} ⊢ A, for any wff A
(2) More generally, if A ∈ Σ, then Σ ⊢ A (3) ⊢ B, for all B ∈ Λ.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
8
9
0.0.7 Remark. (Hilbert-style Proofs)
A Γ-proof is also called a “Hilbert-style proof” —in honour of the great math-
ematician David Hilbert, who was the first big supporter of the idea to use logic as a TOOL in order to do mathematics.
We arrange Hilbert proofs vertically, one formula per line, numbered with its position number, adding “annotation ” to the right of the formula we just wrote, articulating briefly HOW exactly we followed the spec of Definition 0.0.2.
Practical Note. Forget numbering or annotation, or that each line contains ONE wff and as a result forget a decent grade! 🙂
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.8 Example. (Some very simple Hilbert Proofs)
(a) We verify that “A, A ≡ B ⊢ B” (goes without saying, for all wff A and B).
Well, just write a proof of B with “Γ” being {A, A ≡ B}.
BTW, we indicate a finite “Γ” like {A, A ≡ B} without the braces “{ }” when writing it to the left of “⊢”.
(1) A ⟨hypothesis⟩
(2) A ≡ B ⟨hypothesis⟩
(3) B ⟨(1) + (2) + (Eqn)⟩
Incidentally, members of Γ are annotated as “hypotheses” and going for- ward we just write “ hyp”.
Members of Λ we annotate as “Axioms”.
Since A and B are arbitrary undisclosed wff, the expression A, A ≡ B ⊢ B is a Theorem Schema (a theorem, no matter what formulas we plug into A and B).
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
10
(b) Next verify the Theorem Schema
A ≡ B ⊢ C[p := A] ≡ C[p := B] Here you go:
(1) A≡B ⟨hyp⟩
(2) C[p:=A]≡C[p:=B]⟨(1)+Leib⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
11
≡ —or simply “Trans”. How? We write a Hilbert proof! A ≡ B,B ≡ C ⊢ A ≡ C
(1) A≡B ⟨hyp⟩ (2) B≡C ⟨hyp⟩
(3) (A≡B)≡(A≡C)(2)+(Leib),Denom.“A≡p”wherepis“fresh” (4) A≡C ⟨(1)+(3)+(Eqn)⟩
(Trans)
Why must p be fresh?
Say A is p∧q. Then feeding B to p I get B∧q≡B
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
12
(c) Something more substantial. Our First Derived Rule!
We establish the following Theorem Schema that we will refer to as Transitivity of
13
(d) And a Tricky One! Verify that “A ≡ A” is an absolute theorem for all A. That is,
⊢A≡A No “HYP” in the proof below!!
(1) A∨A≡A⟨axiom⟩
(2) A≡A ⟨(1)+(Leib): A[p:=A∨A]≡A[p:=A]wherepis“fresh”⟩
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
0.0.9 Metatheorem. (Hypothesis Strengthening) If Γ ⊢ A and Γ ⊆ ∆, then also ∆ ⊢ A.
Proof. A Γ-proof for A is also a ∆-proof, since every time we say about a formula B
in the proof “legitimate since B ∈ Γ” we can say instead “legitimate since B ∈ ∆”.
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
14
Proof.
We have Γ-proofs
We also have a {B1, . . . , Bn}-proof
…,B1
…,B2
.
(1) (2)
(n)
(n+1)
Concatenate all proofs (1)–(n) (in any order) and to the right of the result glue the proof (n+1). We have the following proof:
, ,…, ,
↑
obtained earlier; see box i
Lecture Notes (outline) for MATH 1090 A (Fall 2020) © George Tourlakis, 2020.
15
0.0.10 Metatheorem. (Transitivity of ⊢) Assume Γ ⊢ B1, Γ ⊢ B2, . . . , Γ ⊢ Bn. Let also B1,…,Bn ⊢ A. Then we have Γ ⊢ A.
…,Bn
…,Bi,…,A
…,B1
…,B2
…,Bn
…,Bi,…,A