``` Bulletin 3: Some sketches of solutions (Three of you got in-person explanations of the solution below from me on Monday or Tuesday; you can look quickly at what is below or not, as you like.) Problem 9 on Assignment 5: Look through the list of axioms and theorems, etc. for predicate logic (I don't anticipate any changes in this sheet, by the way; what you had at Test 2 is what you will have at the exam). Only TWO of them have anything to do with the symbol = in predicate logic. So you know you'll have to use one and maybe both of them to do problem 9. Actually I think one needs both of them. My suggestion is to use Ax 6 with a suitable wff A. The key to a proof is finding the right wff A. I suggest an atomic wff A (no boolean connectives, i.e., complexity 0), in fact, an equality. Note that if the wff given in problem 9 is a theorem, then by Spec spec the conditional in its body is also a theorem. And if that wff is a theorem then it can be proven from the empty set of assumptions, so that by 6.1.1 its universal qtfcn., the wff given in problem 9, is also a theorem. So it is enough to prove the conditional which is the body of the given wff. I suggest a pf. using the D.T. Then your Hilbert proof would begin (1) x = f(x) < ass > Take x as t and f(x) as s in Ax 6 now. The job now is to think of an appropriate wff A to use in our instance of Ax 6. Then after writing that instance in line (2), we have (3) A[w:= x] == A[w:= f(x)] < (1), (2), M.P. > Now the goal should be to choose A so that the left side of (3) is a well-known theorem and the right side is what we want -- the consequent of the conditional discussed in the paragraph above, f(x) = f(f(x)). If you want to think about this for a while, do so. I will suggest two different wffs A that work, about 60 lines down from the rest of this file. You can also just scroll there immediately to check that my A works. After finding such an A, mention that one side is a theorem -- write it in line (4), stating somehow that it is a theorem, in the annotation to that line, and either giving a reference for it (we proved this in class, or "something just like this" was on assignment 3 -- but in general beware of doing things like this on the exam -- sometimes I want you to prove again things we already proved...) or proving it in a separate Lemma outside the Hilbert proof. Then conclude by Equanimity that our desired consequent is also a theorem, in line (5) or so. Then cite D.T., then put the (forall x) on, using 6.1.1. Exercise 1 on p. 187: One way, which uses 6.5.6: Begin with two assumptions, in the usual way when one wants to prove a "repeated conditional" U --> (V --> W) by the D.T. Put U in line (1) and V in line (2). In line (3) eliminate the (forall x) in one of the assumptions by Spec spec. In line (4) you could write A, with a suitable annotation pointing to line (2), involving 6.5.6. Annotate as I did in class and as GT does in similar steps in proofs which use 6.5.6. And draw the right conclusion at the end of such a Hilb. pr., as GT does in similar pfs. in his book. (We did one in class, and I suggested several days ago reading two others in GT.) I leave the rest of what you must do in such a proof to you. Another way: Rewrite the consequent of the given conditional as what it really is without the \exists quantifiers (write out what the given consequent really abbreviates). GT must have had this proof in mind, given the Hint he gives at the end of exercise 1. Do a Lemma or so, proving that |-- U --> V == notV --> notU; you should know this as "contrapositive" from a course taken before 1090. A proof via 2.4.11 and 2.4.4 is very short and easy. That gives you a wff synt. equiv. to the (ex. x)A --> (ex. x)B we began with, which looks just like the right side of Ax 3, which is closely related to your assumption in line (1). Figure out the rest yourself. This way avoids 6.5.6. First way: Let A be (f(x) = f(z)). Let z be the variable substituted for, in Ax 6. With our t and s in the discussion above, we get as the consequent of Ax 6 in this case (f(x) = f(x)) == (f(x) = f(f(x))). :^D Note that if the atomic wff A above is thought of as a wall of a house with a window in it, into which can be put any term, just by substitution for z, then the left and right sides of the above biconditiional are that wall with the window filled with our terms t and s, respectively, from line (1) of our proof. We proved that |-- (term = same term) in class, or at least proved that |-- (g(y) = g(y)) or some such thing, and remarked that the same proof works for any term. So the left side of the biconditional :^D is a known theorem. Second way: Let A be (z = f(z)), again with z being the variable substituted for. Then A[z:=t] is (x = f(x)), the guy in line (1) of our Hilb. pf. And A[z:=s] is (f(x) = f(f(x))). :*D Again by M.P. we get the above biconditional from Ax 6 and line (1). This time the left side of our biconditional right side of Ax 6 is our assumption in line (1), so by equanimity we get our desired equation f(x) = f(f(x)) from the biconditional before :*D and line (1). I actually prefer this proof (this choice of A) to the first proof, since it does not require referring to something proven in class or on Test 2. It's kinda neat because the instance of Ax 6 turns out to be of the form U --> (U == V), so that assuming U gives V, by M.P. followed by Equanimity. This, by the way, is a fairly typical proof of a theorem involving equality. For others, peek at Chapter 7 in our text. ```