| |
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.
|