
Bulletin 3: Some sketches of solutions
(Three of you got inperson 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 wellknown 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.
