``` Continuation of Assignment 5 (due at Ganong's office by midnight, 8 April 2013): Same rules as on all previous assignments -- underlining or circling of last names, double-spacing, stapling, etc. Problem 4: Let φ be a 2-ary (binary) predicate symbol. Note that (\forall u)(\forall v) φ(u,v) --> (\forall v) φ(v,v) is NOT an instance of Ax2 ( with "A" being, of course, (\forall v) φ(u,v) ), because substitution of v for u in "A" is undefined. Nevertheless, using only facts on the sheets which have been handed out in class either at Test 2 or before Test 2, and of course our usual metatheorems and derived inference rules and proof techniques, prove that the above wff is a theorem. (As usual, you may not use Completeness of either Boolean or Predicate Logic, in the proof of a theorem. One proof of the above that occurs to me uses Dummy Renaming at some point. It may be possible to do this problem without Dummy Renaming, too.) Problem 5: Let C and D be wffs, such that y does not occur freely in C. Using only facts covered in class before 2 April -- but see below, too!, prove that this wff is a theorem: (\forall y)(D --> C) == ( (\exists y)D --> C ). Give an "equational" proof (not Hilbert style, no ping-pong) -- basically, bullet (with level of detail for the steps as indicated in class before April 2). Problem 6: Fill in the missing bits in this framework for a start to a proof that |-- (u = v) --> (v = u). (Write this one out, completed; don't print out this thing.) Proof: (1) u = v < > (2) (u = v) --> ( (v = u) == (v = v) ) < much explanation > (3) v = u == v = v < > Now finish the Hilbert-style proof, with more lines, and ending with an English sentence. Once the proof is done, it is done, but just note that this wff had *better* be a theorem. If blup *is the same as* blap, it had better be the case that blap is the same as blup. Problem 7: Now prove that |-- ((u = v) /\ (v = w)) --> (u = w). Suggestion: Use 2.5.2 and the D.T. You may also use the result of Problem 3 if you think that helps. Problem 8: Let A, B be wffs, as usual. Give a bullet proof that if x dnof in A, then ((\forall x)B) --> A == (\exists x)(B --> A). If at any point in your proof you need a fact which we proved in class, you may give as a reason "fact proven in class". Problem 9: Prove that the following wff is a theorem: (\forall x)( (x = f(x)) --> (f(x) = f(f(x))) ). Here, of course, f is a function symbol. (It won't help you to prove this, to think of it semantically, but it says that if g is a function from a nonempty set D to D, then for any guy a in the set whose value under g is just a, it is also the case that g(g(a)) is just g(a). That's certainly true. This at least should remove any doubt you might have had as to whether this is a theorem.) ```