# [FOM] Re: your paper on partial models of ZF

Bryan Ford baford at mit.edu
Fri Apr 30 07:52:47 EDT 2004

Dear Prof. Holmes,

Thanks again for taking the time to look over the draft.  I've thought about
your argument, and I guess I don't quite follow you.  It seems that you're
use a model-theoretic argument to show that the portion of my argument in
Section 5.2 "cannot" be valid because if it were it would lead to a
(model-theoretic) contradiction - an argument I can entirely believe, but
given that my argument is leading to a contradiction anyway, that doesn't
seem to say much.  Model-theoretic arguments about ZF- assume from the start
that ZF- (or some stronger theory) is consistent; if ZF- were inconsistent,
then of course it would prove your model-theoretic argument that my direct
argument is unprovable in ZF-, _in addition to_ proving my direct argument
within ZF-.  But I admit that I'm not yet very well-versed in model theory
yet, so I may just be missing the point somehow.

At any rate, since your concern is about how the axiom scheme of separation is
handled, here is how I would fill out the argument on p.21 for that axiom
scheme.  (Note that in my development, technically I'm treating _all_ the
axioms as axiom schemes, not just the one - separation - that really has to
be treated as such.)

---

The separation scheme is	[[x \in {y in z | f}] <-> [[x in z] & f[x/y]]],
where x, y, and z are distinct variables, and x does not occur bound in f.
>From Theorems 5.4 and 5.5, the term {y in z|f} represents a set s in
environment E iff the term z represents s' in E---that is, if s' = E(z)---and
s is the set of all members x of s' such that f is true in the environment
E(y := x).

Note that the proposition f is true in the environment E(y := x)'', which I
use in the proof, is simply a _single formula_ of ZF-, with f, E, y, and x as
free variables. Thus, the proof is using _a single instance_ of the
Separation axiom scheme in our "meta-level" instance of ZF-,  for a single
particular ZF- formula, to form the set s.  In doing so, it is
therebyquantifying over'' and expressing the semantics of _all_ of the
infinite number of instances of the separation scheme in the object-level ZF-
theory all at once. This obviously should not be possible according to
model-theoretic arguments, but if ZF is inconsistent then it certainly might
well prove those model-theoretic arguments while also going right ahead and
proving the semantic correspondence of that infinite collection of
object-level Separation instances using only a finite number of such
instances in the (meta-level) proof.  At any rate, to continue the argument
in the obvious way...

Now the formula [x in {y in z|f}] is true in E iff E(x) is a member of the set
s above: that is, if E(x) is a member of E(z) and f is true in the
environment E(y := E(x)). The formula [x in z] is true iff E(x) is a member
of E(z), and because x does not occur bound in f, the formula f[x/y] is true
in E iff the formula f is true in E(y := E(x)). Thus, the axiom is
semantically true in E.

---

Can you point out exactly how this argument goes wrong, in direct terms -
i.e., "Y doesn't follow from X" - rather than as a model-theoretic argument
stating that such a thing "shouldn't" be provable?  When I was writing this
section in the draft, it seemed to me that if the proof got this far, we were
already deep in the waters of absurdity, which is why I thought any critical
errors were probably in the construction and didn't take the time to fill out
every tedious step of this last part of the argument.  But it interests me
greatly that you think the construction itself is more-or-less correct (or at
least plausible).  I'll definitely look into the prior work you mentioned.

BTW, Prof. Solovay of Berkeley has pointed out two errors in the construction
itself - one (in Theorem 4.12) fixable I think, though not in the way I
alluded to in my last message; the other (in Theorem 4.21) is not so
obviously fixable.  In Theorem 4.21 I mistakenly assume that R'_2 is a robust
interpretation when in fact we only know that it is correct.  This latter
problem might well be that "smoking gun" as he puts it (or one of them
anyway :)).  I have to look into it further - but for the moment, I'm
assuming that's probably the first point at which the argument falls apart.

At any rate, thanks again for spending the time to look at the paper!
Although as I mentioned before I hadn't intended for the draft to be seen
publicly yet, having it mentioned on the FOM list certainly turned out to be
by far the quickest way to get some solid, expert analysis and critique on
it. :)  I have plenty to chew on now.

Cheers,
Bryan