``` 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. Ping-pong. (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 2-line Hilbert proof.) // Now the second theorem is easily proven bullet-fashion: (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 4-6 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 2-place 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". ```