0.1. First-order Proofs and Theorems 1
Lecture # 15, Nov. 6
0.1. First-order Proofs and Theorems
A Hilbert-style proof from Γ (Γ-proof) is exactly as defined in the case of Boolean Logic. Namely:
It is a finite sequence of wff
A1,A2,A3,…,Ai,…,An
such that each Ai is ONE of
1. Axiom from Λ1 OR a member of Γ
OR
2. IsobtainedbyMPfromX→Y andXthatappeartotheLEFTofAi (Ai is
the same string as Y then.)
However, here “wff” is 1st-order, and Λ1 is a DIFFERENT set of axioms than the old Λ. Moreover we have ONLY one rule up in front.
As in Boolean definitions, a 1st-order theorem from Γ (Γ-theorem) is a formula that occurs in a 1st-order Γ-proof.
As before we write “Γ ⊢ A” to say “A is a Γ-theorem” and write “⊢ A” to say
“A is an absolute theorem”.
Basic Logic© by George Tourlakis
2
Hilbert proofs in 1st-order logic are written vertically as well, with line numbers and annotation.
The metatheorems about proofs and theorems
• proof tail removal,
• proof concatenation,
• awffisaΓ-theoremiffitoccursattheendofaproof • hypothesis strengthening,
• hypothesis splitting,
• usability of derived rules,
• usability of previously proved theorems
hold with the same metaproofs as in the Boolean case.
Basic Logic© by George Tourlakis
0.1. First-order Proofs and Theorems 3 We trivially have Post’s Theorem (the weak form that we proved for Boolean
logic).
0.1.1 Theorem. (Weak Post’s Theorem for 1st-order logic)
If A1,…,An |=taut B then A1,…,An ⊢ B Proof. Exactly the same as in Boolean logic.
Thus we may use
A1,…,An ⊢B
as a DERIVED rule in any 1st-order proof, if we know that
A1,…,An |=taut B .
Basic Logic© by George Tourlakis
4
0.2. Deduction Theorem
This Metatheorem of First-Order Logic says:
0.2.1 Metatheorem. If Γ,A ⊢ B, then also Γ ⊢ A → B Proof. Induction on the proof length L we used for Γ, A ⊢ B:
1. L = 1 (Basis). There is only one formula in the proof: The proof must be B
Only two subcases apply:
• B∈Γ. ThenΓ⊢B. ButB|=taut A→B,thusby0.1.1alsoB⊢A→B. So
B, A → B isaΓ-prooftoo. Thatis,Γ⊢A→B.
• B IS A. So, A → B is a tautology hence axiom hence Γ ⊢ A → B. • B ∈ Λ1. Then Γ ⊢ B. Conclude as above.
2. Assume (I.H.) the claim for all proofs of lengths L ≤ n. 3. I.S.: The proof has length L = n + 1:
n+1
…,B IfB∈Γ∪Λ1 thenwearedonebytheargumentin1.
Assume instead that it is the result of MP on formulas to the left of B: n+1
By the I.H. we have
Basic Logic© by George Tourlakis
…,X,…,X → B,…,B
≤n
n
Γ⊢A→X (∗)
0.2. Deduction Theorem 5 and
Γ⊢A→(X →B) (∗∗) The following Hilbert proof concludes the case and the entire proof:
1) A→X ⟨thmby(∗)⟩
2) A→(X→B) ⟨thmby(∗∗)⟩
3) A → B ⟨1 + 2 + taut. implication⟩
The last line proves the metatheorem.
Comment. In line 3 above, seeing that
A→X, A→(X→B)|=taut A→B
is trivially verifiable, we used the “RULE”
A → X, A → (X → B) ⊢ A → B
that we obtain from the above via 0.1.1.
The annotation said “1 + 2 + taut. implica- tion”.
It could also have said instead “1 + 2 + Post”.
Basic Logic© by George Tourlakis
6
0.3. Generalisation and “weak” Leibniz Rule We learn here HOW exactly to handle the quantifier ∀.
0.3.1. Adding and Removing “(∀x)”
0.3.1 Metatheorem. (Weak Generalisation) Suppose that for any wff X in Γ
X has no free occurrences of x.
Then if we have Γ⊢A, we will also have Γ⊢(∀x)A.
Proof. Induction on the length L of the Γ-proof used for A.
1. L = 1 (Basis). There is only one formula in the proof: The proof must be
A
Only two subcases apply:
• A∈Γ. ThenAhasnofreex. But⊢A→(∀x)Abyaxiom3. Thus,we have a Hilbert proof (written horizontally for speed),
Γ−proved axiom MP on the previous two
A , A → (∀x)A, (∀x)A
• A ∈ Λ1. Then then so is (∀x)A ∈ Λ1 by partial generalisation.
Hence Γ ⊢ (∀x)A once more. (WHY?)
AHA! So that’s what “partial generalisation” does for
us!
Basic Logic© by George Tourlakis
0.3. Generalisation and “weak” Leibniz Rule 7 2. Assume (I.H.) the claim for all proofs of lengths L ≤ n.
3. I.S.: The proof has length L = n + 1: n+1
…,A IfA∈Γ∪Λ1 thenwearedonebytheargumentin1.
Assume instead that A is the result of MP on formulas to the left of it: n+1
…,X,…,X → A,…,A
≤n
n
By the I.H. we have
and
The following Hilbert proof concludes the case and the entire proof:
1) (∀x)X
2) (∀x)(X → A)
3) (∀x)(X → A) → (∀x)X → (∀x)A
5) (∀x)X → (∀x)A
6) (∀x)A
The last line proves the metatheorem.
⟨thm by (∗)⟩ ⟨thm by (∗∗)⟩ ⟨axiom 4⟩
⟨2 + 3 + MP⟩ ⟨1 + 5 + MP⟩
Basic Logic© by George Tourlakis
Γ ⊢ (∀x)X (∗) Γ ⊢ (∀x)(X → A) (∗∗)
8
0.3.2 Corollary. If ⊢ A, then ⊢ (∀x)A.
Proof. The condition that no X in Γ has free x is met: Vacuously. Γ is empty!
0.3.3 Remark.
1. So, the Metatheorem says that if A is a Γ-theorem then so is (∀x)A as long as
the restriction of 0.3.1 is met.
But then, since I can invoke THEOREMS (not only axioms and hypotheses) in a proof, I can insert (∀x)A anywhere AFTER A in any Γ-proof of A where Γ obeys the restriction.
2. Why “weak”? Because I need to know how the A was obtained before I may use(∀x)A.
Basic Logic© by George Tourlakis
0.3. Generalisation and “weak” Leibniz Rule 9 0.3.4 Metatheorem. (Specialisation Rule) (∀x)A ⊢ A[x := t]
Goes without saying that IF the expression A[x := t] is undefined, then we have nothing to prove.
Proof.
(1) (∀x)A
(2) (∀x)A → A[x := t] (3) A[x:=t]
⟨hyp⟩
⟨axiom 2⟩ ⟨1+2+MP⟩
0.3.5 Corollary. (∀x)A ⊢ A
Proof. This is the special case where t is x.
Basic Logic© by George Tourlakis
10
Really Important! The metatheorems 0.3.5 and 0.3.1 (or 0.3.2) —which we nick- name “spec” and “gen” respectively— are tools that make our life easy in Hilbert proofs where handling of ∀ is taking place.
0.3.5 with no restrictions allows us to REMOVE a leading “(∀x)”.
Doing so we might uncover Boolean glue and thus benefit from applications of
“Post” (0.1.1).
If we need to re-INSERT (∀x) before the end of proof, we employ 0.3.1 to do so. This is a good recipe for success in 1st-order proofs!
Basic Logic© by George Tourlakis
0.3. Generalisation and “weak” Leibniz Rule 11 0.3.2. Examples
Ping-Pong proofs.
Hilbert proofs are not well-suited to handle equivalences.
However, trivially and —by 0.1.1—
A→B,B→A|=taut A≡B
A → B, B → A ⊢ A ≡ B (1)
Thus, to prove Γ ⊢ A ≡ B in Hilbert style it suffices —by (1)— to offer TWO Hilbert proofs:
Γ ⊢ A → B AND Γ ⊢ B → A
This back and forth motivates the nickname “ping-pong” for this proof technique.
Basic Logic© by George Tourlakis
12
0.3.6 Theorem. (Distributivity of ∀ over ∧) ⊢ (∀x)(A ∧ B) ≡ (∀x)A ∧ (∀x)B Proof. By Ping-Pong argument.
We will show TWO things:
1. ⊢(∀x)(A∧B)→(∀x)A∧(∀x)B
and
2. ⊢ (∀x)A ∧ (∀x)B → (∀x)(A ∧ B)
(→) (“1.” above)
By DThm, it suffices to prove (∀x)(A ∧ B) ⊢ (∀x)A ∧ (∀x)B.
(1) (∀x)(A ∧ B)
(2) A∧B
(3) A
(4) B
(5) (∀x)A
(6) (∀x)B
(7) (∀x)A ∧ (∀x)B
⟨hyp⟩
⟨1 + spec (0.3.5)⟩
⟨2 + Post⟩
⟨2 + Post⟩
⟨3 + gen; OK: hyp contains no free x⟩ ⟨4 + gen; OK: hyp contains no free x⟩ ⟨(5,6) + Post⟩
NOTE. We ABSOLUTELY MUST acknowledge for each application of “gen” that the restriction is met.
Basic Logic© by George Tourlakis
0.3. Generalisation and “weak” Leibniz Rule 13
Lecture #16, Nov. 11
(←) (“2.” above)
By DThm, it suffices to prove (∀x)A ∧ (∀x)B ⊢ (∀x)(A ∧ B).
(1) (∀x)A ∧ (∀x)B
(2) (∀x)A
(3) (∀x)B
(4) A
(5) B
(6) A∧B
(7) (∀x)(A ∧ B)
⟨hyp⟩
⟨1 + Post⟩
⟨1 + Post⟩
⟨2 + spec⟩
⟨3 + spec⟩
⟨(4,5) + Post⟩
⟨6 + gen; OK: hyp has no free x⟩
Easy and Natural! Right?
Basic Logic© by George Tourlakis
14
0.3.7 Theorem. ⊢ (∀x)(∀y)A ≡ (∀y)(∀x)A Proof. By Ping-Pong. ⊢ (∀x)(∀y)A→←(∀y)(∀x)A.
(→) direction.
By DThm it suffices to prove (∀x)(∀y)A ⊢ (∀y)(∀x)A
(1) (∀x)(∀y)A
(2) (∀y)A
(3) A
(4) (∀x)A
⟨hyp⟩
⟨1 + spec⟩
⟨2 + spec⟩
⟨3 + gen; OK hyp has no free x⟩ ⟨4 + gen; OK hyp has no free y⟩
(5) (∀y)(∀x)A
Exercise! Justify that you can write the above proof backwards!
(←)
Basic Logic© by George Tourlakis
0.3. Generalisation and “weak” Leibniz Rule 15 0.3.8 Metatheorem. (Monotonicity of ∀) If Γ ⊢ A → B, then Γ ⊢ (∀x)A →
(∀x)B, as long as no wff in Γ has a free x. Proof.
(1) A → B
(2) (∀x)(A→B)
(3) (∀x)(A → B) → (∀x)A → (∀x)B (4) (∀x)A→(∀x)B
⟨invoking a Γ-thm⟩ ⟨1+gen;OKnofreexinΓ⟩ ⟨axiom 4⟩
⟨(2,3)+MP⟩
0.3.9 Corollary. If ⊢ A → B, then ⊢ (∀x)A → (∀x)B. Proof. Case of Γ = ∅. The restriction is vacuously satisfied.
Basic Logic© by George Tourlakis
16
0.3.10 Corollary. If Γ ⊢ A ≡ B, then also Γ ⊢ (∀x)A ≡ (∀x)B, as long as Γ does not contain wff with x free.
Proof.
(1) A≡B
(2) A→B
(3) B→A
(4) (∀x)A → (∀x)B
(5) (∀x)B → (∀x)A
(6) (∀x)A ≡ (∀x)B
⟨Γ-theorem⟩
⟨1 + Post⟩
⟨1 + Post⟩
⟨2 + ∀-mon (0.3.8)⟩
⟨3 + ∀-mon (0.3.8)⟩
⟨(4,5) + Post⟩
0.3.11 Corollary. If ⊢ A ≡ B, then also ⊢ (∀x)A ≡ (∀x)B. Proof. Take Γ = ∅.
Basic Logic© by George Tourlakis