
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, doublespacing, stapling, etc.
Problem 4: Let φ be a 2ary (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 pingpong) 
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 Hilbertstyle 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.)
