Lecture # 21, Nov. 27, 2020
We saw in the lecture NOTES at link http://www.cs.yorku.ca/~gt/papers/ lec15.pdf page 1, our first utilisation of Axioms 5 and 6 towards proving the ∀- version of the “one point rule”.
Here are some more uses of these axioms. 0.0.1 Example. We prove that
⊢x=y→y=z→x=z (1) The above is the transitivity of Equality since (by tautological implication back and
forth) says the same thing as
⊢x=y∧y=z→x=z We prove (1): In the application of Ax6
t = s → (A[w := t] ≡ A[w := s]) in the proof below we took
• ttobex
• stobey
• Atobew=z
1) x=y→(x=z≡y=z) ⟨Ax6⟩
2) x=y→(y=z→x=z) ⟨1+Post⟩
I did
Line 2 above is (1), as we see if we omit redundant brackets.
Basic Logic© by George Tourlakis
p→(q≡r)|=taut p→(r→q)
1
2
0.0.2 Example. (“Replacing Equals by Equals”) Here we prove ⊢ x = y → f(x) = f(y), for any unary function symbols f
which, awkwardly,* is captured by the quoted phrase above. Here we use Ax6
in
1)
2) 3) 4)
t = s → (A[w := t] ≡ A[w := s])] the special form below:
• ttobex
• stobey
• Atobef(w)=f(y)
x=y→f(x)=f(y)≡f(y)=f(y) ⟨Ax6⟩
(∀x)x = x
f(y) = f(y) x=y→f(x)=f(y)
⟨Partial gen. of Ax5⟩ ⟨2 + spec⟩ ⟨(1,3)+Post⟩
I used the general version of spec in step 3 above with “f(y)” in place of the term “t” and “x = x” as “B”:
(∀x)B ⊢ B[x := t]
0.0.3 Exercise. Imitate the above proofs to prove commutativity of “=”. ⊢x=y→y=x
*Nothing is “Equal” in the absence of other things. Basic Logic© by George Tourlakis
0.1. Miscellaneous 3 0.1. Miscellaneous
Lecture # 22, Dec. 2, 2020
0.1.1 Example. Monotonicity of ∃, nickname ∃-MON or E-MON.
If Γ ⊢ A → B and there is no free x in any wff of Γ then we have also
Here is a Hilbert proof.
1) A → B
2) ¬B→¬A
3) (∀x)¬B → (∀x)¬A
4) ¬(∀x)¬A → ¬(∀x)¬B
⟨Γ-thm⟩
⟨1+Post⟩
⟨2 + A-MON; conditions on Γ good!⟩ ⟨3 + Post⟩
The last line can be abbreviated as (1)
Γ ⊢ (∃x)A → (∃x)B (1)
0.1.2 Corollary. If ⊢ A → B, then we have also
⊢ (∃x)A → (∃x)B (2)
Basic Logic© by George Tourlakis
4
0.1.3 Example. We have seen via a countermodel in class/Text/NOTES that we CANNOT prove from the axioms
A → (∀x)A
if A contains free occurrences of x. How about
A[x := c] → (∀x)A (2) where c is an unspecified (abstract) constant? Can I prove it from the axioms?
NO, here is a countermodel for the wff in (2), where I took A to be the atomic x = y (not bold; actual variables).
So (2) becomes —after the simplification of A— c = y → (∀x)x = y
TakeD=N,yD =42,cD =42. (2)translatesas
cD =yD →(∀x∈N)x=yD
or more explicitly
f
42 = 42 → (∀x ∈ N)x = 42
t
f
Basic Logic© by George Tourlakis