You already know that removing a leading ∀ “uncovers” (in general†) “Boolean structure” which is amenable to proofs “by Post”.
It would be a shame if we did not have techiques to remove a leading ∃.
We DO have such a technique! Read on.
0.0.1 Metatheorem. (Aux. Hypothesis Metatheorem)
Suppose that Γ ⊢ (∃x)A.
Moreover, suppose that we know that Γ,A[x := z] ⊢ B,
where z is fresh for ALL of Γ, (∃x)A, and B. Then we have Γ ⊢ B.
1
†Clearly, removing ∀ from (∀x)x = y uncovers x = y. But that has no Boolean structure —no glue. Hence I said “in general”.
Basic Logic© by George Tourlakis
2
In our annotation we call A[x := z] an “auxiliary hypothe- sis associated with (∃x)A”. z is called the auxiliary variable that we chose.
Essentially the fact that we proved (∃x)A allows us to adopt A[x := z] as a NEW AUXILIARY HYPOTHESIS to help in the proof of B.
How does it help? (1) I have a new hypothesis to work with; (2) A[x := z] has NO LEADING QUANTIFIER.
(2), in general, results in uncovering the Boolean structure of A[x := z] to enable proof by “Post”!
Halt-and-Take-Notice-Important! A[x := z] is an ADDED HYPOTHESIS!
It is NOT TRUE that either (∃x)A ⊢ A[x := z] or that Γ ⊢ A[x := z].
WE WILL PROVE LATER IN THE COURSE THAT SUCH A THING IS NOT TRUE!
Basic Logic© by George Tourlakis
Proof. of the Metatheorem.
By the DThm, the metatheorem assumption yields Γ ⊢ A[x := z] → B
Thus, ∃-Intro —Corollary 0.1.5 on p.7 of the lecture Notes http://www.cs.yorku.ca/~gt/papers/lec15.pdf we get
Γ ⊢ (∃z)A[x := z] → B (1) We now can prove Γ ⊢ B as follows:
3
1) (∃x)A
2) (∃z)A[x := z] → B
3) (∃z)A[x := z] ≡ (∃x)A
4) (∃x)A → B
5) B
⟨Γ − thm⟩
⟨Γ − thm; (1) above⟩
⟨Bound var. renaming since z fresh⟩ ⟨(2, 3) + Post⟩
⟨(1, 4) + MP⟩
Basic Logic© by George Tourlakis
4
The most frequent form encountered in using Metatheorem 0.0.1 is the following corollary.
0.0.2 Corollary. To prove (∃x)A ⊢ B IT SUFFICES to pick a z that is FRESH for (∃x)A and B and
PROVE INSTEAD (∃x)A, A[x := z] ⊢ B.
Proof. Take Γ = {(∃x)A} and invoke Metatheorem 0.0.1.
Basic Logic© by George Tourlakis
Some folks believe that the most important thing in logic is to know that the following is provable but the converse is not.
True, it is important.
But so are so many other things in logic, like Metatheorem 0.0.1, precisely and correctly formulated AND proved in our earlier pages.
0.0.3 Example. ⊢ (∃x)(∀y)A → (∀y)(∃x)A.
Let us share two proofs!
First Proof. By DThm it suffices to prove instead: (∃x)(∀y)A ⊢ (∀y)(∃x)A
5
(1) (∃x)(∀y)A
(2) (∀y)A[x := z]
(3) A[x := z]
(4) (∃x)A
(5) (∀y)(∃x)A
⟨hyp⟩
⟨aux. hyp for (1); z fresh⟩
⟨(2) + spec⟩
⟨(3) + Dual spec⟩
⟨(4) + gen; OK, all hyp lines, (1,2), have no free y⟩
We used the Corollary 0.0.2 of Metatheorem 0.0.1.
Basic Logic© by George Tourlakis
6
Second Proof. ⊢ A → (∃x)A (that is, the Dual of Ax2) we get ⊢ (∀y)A → (∀y)(∃x)A by ∀-mon.
Applying ∃-intro (Cor. 0.1.5 in the previous lecture Notes PDF, referred to also on p.3 of the present Notes) we get
⊢ (∃x)(∀y)A → (∀y)(∃x)A
Basic Logic© by George Tourlakis
0.0.4 Example. We prove (∃x)(A → B), (∀x)A ⊢ (∃x)B.
(1) (∃x)(A → B)
(2) (∀x)A
(3) A[x:=z]→B[x:=z]
(4) A[x := z]
(5) B[x := z]
(6) (∃x)B
⟨hyp⟩
⟨hyp⟩
aux. hyp for (1); z fresh ⟨(2) + spec⟩
⟨(3, 4) + MP⟩
⟨(5) + Dual spec⟩
7
Remark. The above proves the conclusion using 0.0.1 and Γ = {(∃x)(A → B), (∀x)A}. Of course, this Γ proves (∃x)(A →
B).
Basic Logic© by George Tourlakis
8
0.0.5 Example. We prove (∀x)(A → B), (∃x)A ⊢ (∃x)B.
(1) (∀x)(A → B)
(2) (∃x)A
(3) A[x := z]
(4) A[x:=z]→B[x:=z]
(5) B[x := z]
(6) (∃x)B
⟨hyp⟩
⟨hyp⟩
⟨aux. hyp for (2); z fresh⟩ ⟨(1)+spec⟩
⟨(3, 4) + MP⟩
⟨(5) + Dual spec⟩
Basic Logic© by George Tourlakis
0.0.6 Example. Here is a common mistake people make when arguing informally.
Let us prove the following informally. ⊢ (∃x)A ∧ (∃x)B → (∃x)(A ∧ B).
So let (∃x)A(x) and (∃x)B(x) be true.†
Thus, for some value c of x we have that A(c) and
B(c) are true.
But then so is A(c) ∧ B(c).
The latter implies the truth of (∃x)A(x) ∧ B(x). Nice, crisp and short.
And very, very wrong as we will see once we have 1st-order Soundness in hand. Namely, we will show in the near future that (∃x)A∧(∃x)B → (∃x)(A∧B) is NOT a theorem schema. It is NOT provable.
†The experienced mathematician considers self-evident and unworthy of mention at least two things:
(1) The deduction theorem, and
(2) The Split Hypothesis metatheorem.
Basic Logic© by George Tourlakis
9
10
What went wrong above?
We said
“Thus, for some value c of x we have that A(c) and B(c) are true”.
The blunder was to assume that THE SAME c verified BOTH A(x) and B(x).
Let us see that formalism protects even the inexperienced from such blunders.
Basic Logic© by George Tourlakis
Here are the first few steps of a(n attempted) FORMAL proof via the Deduction theorem:
(1) (∃x)A ∧ (∃x)B
(2) (∃x)A
(3) (∃x)B
(4) A[x := z]
(5) B[x := w]
⟨hyp⟩
⟨(1) + Post⟩
⟨(1) + Post⟩
⟨aux. hyp for (2); z fresh⟩ ⟨aux. hyp for (3); w fresh⟩
The requirement of freshness makes w DIFFERENT from z. These variables play the role of two distinct c and c′. Thus the proof cannot continued. Saved by freshness!
Basic Logic© by George Tourlakis
11
12
0.0.7 Example. The last Example in this section makes clear that the Russell Paradox was the result of applying bad Logic, not just bad Set Theory!
I will prove that for any binary predicate φ we have
⊢ ¬(∃y)(∀x)(φ(x, y) ≡ ¬φ(x, x)) (R)
By the Metatheorem “Proof by Contradiction” I can show (∃y)(∀x)(φ(x, y) ≡ ¬φ(x, x)) ⊢ ⊥
instead. Here it is
(1) (∃y)(∀x)(φ(x, y) ≡ ¬φ(x, x))
(2) (∀x)(φ(x, z) ≡ ¬φ(x, x))
(3) φ(z, z) ≡ ¬φ(z, z)
(4) ⊥
⟨hyp⟩
⟨aux. hyp for (1); z fresh⟩ ⟨(2) + spec⟩
⟨(3) + Post⟩
If we let the atomic formula φ(x, y) be Set Theory’s “x ∈ y” then (R) that we just proved (in fact for ANY binaru predicate φ not just ∈) morphs into
⊢ ¬(∃y)(∀x)(x ∈ y ≡ x ∈/ x) (R′)
Basic Logic© by George Tourlakis
In plain English (R′) says that there is NO set y that con- tains ALL x satisfying x ∈/ x.
This theorem was proved without using even a single axiom of set theory, indeed not even using “{. . .}-notation” for sets, or any other symbols from set theory.
After all we proved (R′) generally and abstractly in the form (R) and that expression and its proof has NO SYMBOLS from set theory!
In short, Russell’s Paradox can be expressed AND demonstrated in PURE LOGIC.
It is remarkable that Pure Logic can tell us that NOT ALL
COLLECTIONS are SETS, a fact that escaped Cantor.
13
Basic Logic© by George Tourlakis
14
Basic Logic© by George Tourlakis
Semantics of First-Order Languages —Simplified
Lecture #19 Nov. 20, 2020
0.1. Interpretations
An interpretation of a wff —and of THE ENTIRE language, that is, the set of ALL Terms and wff— is INHERITED from an interpretation of all symbols of the Alphabet.
This tool —the Interpretation— Translates each wff to some formula of a familiar branch of mathematics that we choose, and thus questions such as is the “translated formula true?” can in principle be dealt with (see 0.1.2 below for de- tails).
An interpretation is totally up to us, just as states were in Boolean logic.
The process is only slightly more complex. Basic Logic© by George Tourlakis
16
Here we need to interpret not only wff but also terms as well.
The latter requires that we choose a NONEMPTY set of objects to begin with. We call this set the Domain of our
Interpretation and generically call it “D” but in specific cases it could be D = N or D = R (the reals) or even something “small” like D = {0, 5}.
Basic Logic© by George Tourlakis
0.1. Interpretations 17 An Interpretation of a 1st-order language consists of a PAIR
of two things:
The aforementioned domain D and a translation mapping M —the latter translates the abstract symbols of the Alphabet of logic to concrete mathematical symbols.
This translation of the ALPHABET INDUCES a trans- lation for each term and wff of the language; thus of ALL THE LANGUAGE.
We write the interpretation “package” as D = (D,M) dis- playing the two ingredients D and M in round brackets.
The unusual calligraphy here is German capital letter callig- raphy that is usual in the literature to name an interpretation package. The letter for the name chosen is usually the same as that of the Domain.
Let me repeat that both D and M are our choice.
Basic Logic© by George Tourlakis
18
0.1.1 Definition. (Translating the Alphabet V1)
An Interpretation D = (D, M ) gives concrete counterparts
(translations) to ALL elements of the Alphabet as follows:
In the listed cases below we may use notation M(X) to indicate the concrete translation (mapping) of an abstract linguistic object X.
We also may use XD as an alternative notation for M(X). The literature favours XD and so will we.
(1) For each FREE variable (of a wff) x, xD —that is, the translation M (x)— is some chosen (BY US!) FIXED mem- ber of D.
BOUND variables are NOT translated! They stay AS
IS.
(2) For each Boolean variable p, pD is a member of {t, f}. (3)⊤D =tand⊥D =f.
This is just we did —via states— in the Boolean case. As was the case there, I will remind the reader once again that we choose the value pD anyway we please, but for ⊤ and ⊥ we follow the fixed (Boolean) rule.
Basic Logic© by George Tourlakis
0.1. Interpretations 19
(4) For any (object) constant of the alphabet, say, c, we choose
a FIXED cD, as we wish, in D.
(5) For every function symbol f of the alphabet, the trans- lation fD is a mathematical function of the metatheory (“real” or “concrete” MATH) of the same arity as f.
fD —which WE choose!— takes inputs from D and gives outputs in D.
(6) For every predicate φ of the alphabet OTHER THAN “=”, our CHOSEN translation φD is a mathematical RELATION of the metatheory with the same arity as φ. It takes its in- puts from D while its outputs are one or the other of the truth values t or f.
NOTE THAT ALL the Boolean glue as well as the equality symbol translate exactly as THEM- SELVES: “=” for “equals”, ∨ for “OR”, etc.
Finally, brackets translate as the SAME TYPE
of bracket (left or right).
Basic Logic© by George Tourlakis
20
We have all we need to translate wff, terms and thus the entire Language:
0.1.2 Definition. (The Translation of wff)
Consider a wff A in a† first-order language.
Suppose we have chosen an interpretation D = (D,M) of
the alphabet.
The interpretation or translation of A via D a mathematical (“concrete”) formula of the metatheory or a concrete object of the metatheory that we will denote by
AD
It is constructed as follows one symbol at a time, scanning
A from left to right until no symbol is left:
†A, not THE. For every choice of constant, predicate and function symbols we get a different alphabet, as we know, hence a different first-order language. Remember the examples of Set Theory vs. Peano Arithmetic!
Basic Logic© by George Tourlakis
0.1. Interpretations 21
(i) We replace every occurrence of ⊥, ⊤ in A by ⊥D, ⊤D —that is, by f,t— respectively.
(ii) We replace every occurrence of p in A by pD —this is an assigned by US TRUTH VALUE; we assigned it when we translated the alphabet.
(iii) We replace each FREE occurrence of an object variable x of A by the value xD from D that we assigned when we translated the alphabet.
(iv) We replace every occurrence of (∀x) in A by (∀x ∈ D), which means “for all values of x in D”.
(v) We emphasise again that Boolean connectives (glue) trans- late as themselves, and so do “=” and the brackets “(” and “)”.
Theory-specific symbols in A:
(vi) We replace every occurrence of a(n object) constant c in A by the specific fixed cD from D —which we chose when translating the alphabet.
(vii) We replace every occurrence of a function f in A by the specific fixed fD —which we chose when translating the alphabet.
Basic Logic© by George Tourlakis
22
(viii) We replace every occurrence of a predicate φ in A by the specific fixed φD —which we chose when translating the
alphabet.
0.1.3 Definition. (Partial Translation of a wff) Given a wff A in a first-order language and an interpretation D of the alphabet.
Sometimes we do NOT wish to translate a FREE variable x of A. Then the result of the translation that leaves x as is is denoted by ADx .
Similarly, if we choose NOT to translate ANY of x1,x2,…,xn,…
that (may) occur FREE in A, then we show the result of such “partial” translation as
ADx1,…,xn
Thus AD has no free variables, but ADx will have x free IF x actually DID occur free in A —the notation guarantees that if x so occurred, then we left it alone.
Basic Logic© by George Tourlakis
0.1. Interpretations 23 0.1.4 Remark. What is the use of the concept and notation
“ADx ”?
Well, note that when we translate (∀x)A FROM LEFT TO
RIGHT, we get “(∀x ∈ D)” followed by the translation of A.
However, ANY x that occur free IN A BELONG to (∀x) in the wff (∀x)A thus are NOT FREE in the latter and hence are NOT translated!
Therefore, “(∀x ∈ D)” concatenated with “ADx ” is what we
get: “(∀x ∈ D)ADx ”.
Basic Logic© by George Tourlakis
24
0.1.5 Example. Consider the AF φ(x, x), φ is a binary pred- icate.
Here are some possible interpretations:
(a)D=N,φD =<.
Here “<” is the “less than” relation on natural numbers.
So φ(x,x)D, which is the same as φD(xD,xD) —in fa- miliar notation is the formula over N:
xD < xD
More specifically, if we took xD = 42, then φ(x, x)D is
specifically “42 < 42”.
Incidentally, φ(x, x)D is false for ANY choice of xD.
We will write φ(x, x)D = f to denote the above sentence symbolically.
I would have preferred to write something like “V φ(x, x)D = t —“V ” for value— but it is so much easier to agree that
writing the above I mean the same thing! 🙂
Basic Logic© by George Tourlakis
0.1. Interpretations 25 For the sake of practice, here are two partial interpreta-
tions.
In the first we exempt the variables y, z. In the second we
exempt x:
D D D
(i) φ(x,x) isx