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

[Bryan Ford]

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  
thereby``quantifying 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