
Bulletin 1
Last night I started to prove 6.5.10 as Tourlakis (GT, below) does
in his book and got stuck. I promised to get back to you folks
about this.
The reason I got stuck is that GT's proof is wrong.
I have pointed out flaws in his book in the past and all he does
is pretend not to understand what I am saying, so that he doesn't
have to admit that he made mistakes. I have literally many hundreds
of emails going back a dozen years, of this sort of nonsense. No
more.
So I won't tell him about this. But feel free yourselves to
tell him. You'll see what I mean.
Here is how to fix his proof:
I don't want to have to type bold face all the time in this clunky
text editor, so for bold x I will type x and for bold y, y. But
these are symbols meant to represent arbitrary object variables,
such as u,v,w,x,y,z, x , etc.
119
6.5.10 is the theorem (ex. x)(forall y) A > (forall y)(ex. x) A.
The case where GT's proof fails is the one where x and y are the
same object variable. It turns out that that is easily handled, and
it leads us to an important fact in predicate logic:
FACT $: If a wff B has no free occurrences of x in it, then
 (forall x) B == B. Also  (ex. x) B == B.
Proof: Suppose that x dnof in B.
First, a proof of the first theorem above. Pingpong.
(1) (forall x) B < hyp >
(2) B < (1), Spec spec >
So  (forall x) B > B, by the D.T.
(1) B < hyp >
(2) (forall x) B < B  B and x dnof in B,
so, by Gen (6.1.1), B 
(forall x) B. >
So  B > (forall x) B, by the D.T.
Or, even simpler,  B > (forall x) B, because this
is an instance of Ax 4. (So we don't even need the above
2line Hilbert proof.) //
Now the second theorem is easily proven bulletfashion:
(ex. x) B
is
¬(forall x) ¬B
<==> < first thm. in FACT $, since x dnof in ¬B >
¬¬B
<==> < 2.4.4 >
B. //
Now, 6.5.10 in the case where y is the same variable as x
becomes
(ex. x)(forall x) A > (forall x)(ex. x) A, which,
 
by two applications of FACT $ (because  and 
have no free occurrences of x in them), and two applications
of WL, is syntactically equivalent to
(**) (forall x) A > (ex. x) A. So it is enough to prove THIS.
(1) (forall x) A < ass >
(2) A < (1), Spec spec >
(3) (ex. x) A < (2), 6.5.3 >
So we are done, by the D.T. //
Note that (**) makes perfect semantic sense. If a statement is true
for all elements of some NONEMPTY set D, then it is certainly true
for at least one element of D.
By the way, I am not sure whether you are allowed just to QUOTE
FACT $ on the exam. Maybe if you want to use the fact in a proof
then you should just jot down a quick proof of it as I did above.
OK, now let's go back and prove the general case of 6.5.10, by
what I labelled Proof #1 last night, i.e., prove it by 6.5.6,
the "auxiliary hypothesis" metatheorem. Assume that x and y
are DIFFERENT object variables, now.
Let z be a variable which dno at all in the wff in line (1)
below, or in (forall y)(ex. x) A (that actually follows
automatically...). Note that in our case Γ is the set
consisting of just one wff  the wff in line (1) below. So
that wff is a Γaxiom, hence certainly a Γtheorem,
and it is an existential quantification. So we are in position
to use 6.5.6.
(1) (ex. x)(forall y) A < ass >
(2) ((forall y) A)[x := z] < aux. hypothesis associated
with (1). See the remarks
46 lines above. >
Now, the above substitution is defined, because z was pulled
"out of left field", so no capture is possible. And 4.1.28
tells us to push the substitution past the quantifier into
the body above, so that the wff in line (2) is actually
(forall y) A[x:=z].
(3) A[x:=z] < (2), Spec spec >
(4) (ex. x) A < (3) and 6.5.2, dual of Spec >
(5) (forall y)(ex. x) A < (4), 6.1.1  y dnof in
either of the assumptions in
lines (1), (2) >
So (1), (2)  (5), but, since all conditions of 6.5.6 are met,
we may conclude that also
(1)  (5), and we are done, by the D.T. //
6.5.10 makes good sense sementically, as should have been
pointed out in a decent 1190 or 1019 course. If there is
one guy "x" who "works" for all guys "y", then for each guy
"y" there is a guy "x" who works for him. The same guy "x"
works for everyone.
But the converse of 6.5.10 is false. The same guy need not
work for all guys "y"  maybe different guys "x" work for
different guys "y". Here's the simplest PROOF (using
Soundness of Predicate Logic) that the converse of 6.5.10 is
NOT a theorem:
Let $phi;(x,y) be a 2place predicate. Let the universe of
discourse D be {17, 19}. Interpret φ(x,y) as the statement
that x points to y in this directed graph:
{ (17, 19), (19, 17) }, i.e., the graph in which
17 points to 19 and 19 points to 17.
So for each guy in D, there is a guy in D who points to him.
So (forall y) (ex. x) φ(x,y) interprets as t ("true").
But (ex. x)(forall y) φ(x,y) interprets as f, since
it is not the case that there is a guy in D such that
he points to all guys in D.
So the converse of 6.5.10 interprets as f in this
interpretation, with A being φ(x,y). So by
Soundness it is not a theorem.
I will now go do something else. I will post more here later
today or later in the week. Watch for further "Bulletins".
