``` Bulletin 2: More on Section 6.5 If you are thinking about preparation for our exam, these bulletins are probably even better preparation than Assignment 5. I can see myself asking for proofs like 6.5.11 and 6.5.13 (see below, toward the end of this Bulletin). For ease of typing in HTML I will not make boldface symbols to represent arbitrary nonBoolean variables. It is understood that my "x" really means "bold x", i.e., any nonBoolean variable (e.g., u, v, w, x, y, z). We used "transitivity of arrow" in a proof recently. We indicated an easy proof of it using D.T. and M.P., but it is also 2.5.9 in the text, and can be proven fairly easily by a bullet proof not using the powerful, relatively fancy D.T. I just mention this for no particular reason here. I think actually the following form of Metathm. 6.5.4 makes more sense to me and is more easily remembered, given the general principles of proof we have spent time on in Predicate Logic, than the version in the text. Again, I mention this and state the version I like, and prove it, for no particular reason. Moreover, its proof is cleaner and shorter. There is no need to mention Ax4 explicitly as in the Tourlakis proof of 6.5.4, and no need to mention either "tautological implication" or "transitivity of arrow". More mainstream stuff provides the proof, namely, the powerful sledgehammers Spec spec, Weak Gen, M.P., and D.T. Here it is: Metatheorem 6.5.4: Let Gamma be a set of wffs, and A, B be wffs. Suppose that (i) x dnof in any wff of Gamma, and (ii) x dnof in A. Then: If Gamma U {A} |-- B, then Gamma U {A} |-- (forall x) B. Comments: The converse "if, then" ALWAYS holds. No dnof condition necessary. That's because, given any n-step proof of (forall x) B from Gamma and A, one just tacks on B in line n+1, with annotation "(n) and Spec spec". And the above, 6.5.4 itself, is easy, too: Suppose we have an n-step proof of B from Gamma and A. Then just write (forall x) B in line n+1, with annotation "(n) with Weak Gen 6.1.1, since x dnof in any wff in Gamma U {A}". One immediately gets the 6.5.4 in the text from this version of it, just by using D.T. and the converse of D.T. (which is really just the general M.P. inf. rule for Whamma theorems, where Whamma is an arbitrary set of wffs. No dnof condition is present in either D.T. or its converse, M.P. Again for no particular reason, but just as a short proof to look at, notice this easily proven statement: (exists x) A --> B |-- A --> B. (**) Proof: (1) (exists x) A --> B < ass. > (2) A < ass. > (3) (exists x) A < (2) and 6.5.3 > (4) B < (1), (3), M.P. > By D.T., (exists x) A --> B |-- A --> B. // Note that there is absolutely no dnof condition for this no-name metatheorem (**) above. x can occur freely in A or B or both or neither; we don't care. The Auxiliary Variable Metatheorem (6.5.6) -- Or: "How to remove an existential quantifier from a Γ-theorem correctly, to prove other Γ-theorems" Let Γ be a set of wffs, A and B be wffs, and x and z be object variables. Suppose that z does not occur at all in i) any wffs in Γ, and dno in ii) (exists x) A, and dno in iii) B. Suppose also that iv) Γ |-- (exists x) A and v) Γ U {A[x:=z]} |-- B. Then: Γ |-- B, as well. Let's prove the darned thing first, and then talk about it. :-) Tourlakis' proof is basically fine, but I don't know why he makes a big deal out of SL (we didn't even talk about SL, but it's "strong" Leibniz with our usual "substitute only if there is no capture", and it works not just for theorems but for Γ- theorems). BL (basically I mean just old-fashioned Leibniz, the one we have been using since the start of the course) works just as well; the applications of Leibniz in the proof of 6.5.6 do not involve substitutions inside any quantifications. And, of course, Ganong does not allow things like Tourlakis' "tautology" or "tautological implication" annotation. Pf: By v) above, and thinking of z as the variable mentioned in "our" 6.5.5, A[x:=z] as the wff "A" mentioned in "our" 6.5.5, and B as the B ditto, all the conditions of our 6.5.5 are satisfied, by i), iii) and v) above. So, by our 6.5.5, we have (*) Γ U {(exists z) A[x:=z]} |-- B. So: (1) Γ < assumptions > (2) (exists x) A < iv) above > (3) (exists z) A[x:=z] < Dummy Renaming (for existentials) to the rescue! And (2), of course. 6.4.5 applies because, by ii) above, z dno in A. Notice, by the way, that we have now used all five of i) - v) in the statement of 6.5.6! 6.4.5 says that the wff in line (2) is REALLY syntactically equivalent to the wff in line (3), hence certainly Γ-synt. equiv. to it, so this line is just Eqn for Γ-theorems. > (4) B < (*) above! > // Some discussion: Feel free to read through the 15 lines at the bottom of p. 161 if you want to. What it amounts to is this: The important case, and the case that comes up most in practice, is the case where the scope A in the existential (exists x) A actually does have free occurrences of x in it, and the "fresh" variable z is (therefore) NOT x ! The metatheorem tells us that if WE are careful to CHOOSE the variable z so that it is FRESH with respect to EVERYBODY (heh heh, so to speak). and we have (exists x) A available as a Gamma-theorem, AND we can prove B from Γ and A[x:=z], then we are in business: B is a Gamma-theorem. Tourlakis explains that the way a mathematician uses an existential assumption in a proof (semantically) is something like this: "There is SOME guy x, such that A holds for x. Let q be such a guy. (And here the mathematician is very careful to use a name "q" that has not been used ANYWHERE else in her entire proof. This is the "fresh z" in 6.5.6.) Keep q fixed. Then ... [And now comes logic, use of theorems, deducing results from earlier results, etc., involving this particular, fixed guy q.] ... Hence [finally], B." Then the mathematician claims that B follows logically from the assumptions (the wffs in Γ) that led to the first sentence in quotes above. The "q", as Tourlakis says, has vanished totally, and MUST vanish. It was a vehicle to make the proof go, and once it has served its purpose, the conclusion, the B, is not allowed to mention the "q". (That's the part about z not occurring in B.) Notice also the point that Tourlakis makes in the middle of p. 162 in his continuation of comments on 6.5.6: In v), in our statement of 6.5.6, we assumed that we are able to prove B from Γ together with A[x:=z]. Now, in the cases in practice, z WILL occur freely in A[x:=z]. So no "Weak Gen" step, tacking a "(forall z)" onto some wff already proven, is allowed in that proof we give of B. -- Semantically, the "q", or the "z", is particular, and fixed -- it does not change, and there may be only one such guy, such that A holds for him. So it is clearly idiotic to deduce that A (or indeed any statement) holds for ALL guys z, if the z "represented" potentially just ONE guy. End of discussion 6.5.7 and 6.5.8 are simpler, cleaner, special cases of 6.5.6: 6.5.7: Suppose that i) |-- (exists x) A, and ii) A[x:=z] |-- B, for some variable z fresh with respect to both B and (exists x) A. Then |-- B. Pf: This is just 6.5.6 with Γ being the empty set of wffs. // 6.5.8: Suppose that A and B are wffs, and z dno in B and dno in (exists x) A. Suppose also that {A[x:=z]} |-- B. Then: {(exists x) A} |-- B. Proof: This is 6.5.6 with Γ being {(exists x) A}, thanks to our 6.5.5. Take my word for it if you like. // Read thoroughly also Examples 6.5.11, 6.5.13. Except that where Tourlakis uses "tautological implication" to justify a step in a proof, I would require you to prove whatever little theorem in boolean logic is involved in that step, syntactically. Also Ganong does not allow this sloppy term "fresh". I actually require people to say that the variable under discussion dno in this wff and that wff (whichever ones one needs it not to occur in). These are CLASSIC sorts of theorems in predicate logic. (Note that any provability statement of the form P, Q |-- R , for instance, is "the same", in meaning, thanks to the Deduction Theorem and its converse, as the assertion that a certain conditional is a theorem -- such as |- P --> (Q --> R), or, by Shunting, |- (P /\ Q) --> R.) Examples similar to 6.5.12 or 6.5.13 are highly likely sorts of problems to appear on our final exam. They appear on final exams in this course every year, no matter who the instructor is. By the way, read also Tourlakis' very well-written Remark 6.5.14 to see how a mathematician would informally do example 6.5.13. Maybe also see Example 6.5.15 if you are interested in seeing how a careless person might "prove" (heh, heh) something that is certainly NOT a theorem. Some of the exercises at the end of Chapter 6 would be likely exam-type problems. Try (starting on p. 187): exercises 1 through 5, 11 through 13, 18, 19, 22. Exercise 13 especially, as I recall, provides a workout! Bulletin 3 may follow. ```