# Nelson's program to show inconsistency of ZF

At the end of the paper Division by three by Peter G. Doyle and John H. Conway, the authors say:

Not that we believe there really are any such things as infinite sets, or that the Zermelo-Fraenkel axioms for set theory are necessarily even consistent. Indeed, we’re somewhat doubtful whether large natural numbers (like $80^{5000}$, or even $2^{200}$) exist in any very real sense, and we’re secretly hoping that Nelson will succeed in his program for proving that the usual axioms of arithmetic—and hence also of set theory—are inconsistent. (See Nelson [E. Nelson. Predicative Arithmetic. Princeton University Press, Princeton, 1986.].) All the more reason, then, for us to stick with methods which, because of their concrete, combinatorial nature, are likely to survive the possible collapse of set theory as we know it today.

Here are my questions:

What is the status of Nelson's program? Are there any obstruction to finding a relatively easy proof of the inconsistency of ZF? Is there anybody seriously working on this?

-
Note that on the first page footnotes, Doyle says about Conway  But he has never approved of this exposition, which he regards as full of `fluff.' –  Will Jagy Aug 25 '10 at 21:50
A central obstruction to finding an "easy" proof of the syntactic inconsistency of ZF is that nobody has managed to do it in 80+ years, and not for lack of trying. More recently, there was fear (or hope) that large cardinals might be useful for finding inconsistencies in ZF, but that idea hasn't panned out either. Arithmetic is even worse: there are multiple, unrelated consistency proofs for arithmetic, so it would be remarkable to find a syntactic inconsistency there. –  Carl Mummert Aug 25 '10 at 21:55
This is not a disagreement with what Carl Mummert says but it is worth remembering that when Zermelo first proposed his axioms for set theory, there was considerable scepticism that they really would avoid contradictions. People like Bertrand Russell, Philip Jourdain and Henri Poincaré criticised his axioms. Russell wrote that "I suspect that his axioms will not really avoid contradictions, i.e., I suspect new contradictions could be manufactured specially designed to be consistent with his axioms." [quoted on p. 91 of Ebbinghaus's biography of Zermelo tinyurl.com/2fskff7 ] –  Marko Amnell Aug 26 '10 at 7:50
Note that the question states that Nelson's program is about the consistency of arithmetic. So there is even more than 80 years of work that did not come up with inconsistencies. The Russell quote by Marko Amnell is interesting. If you change "contradictions" to "undecidable statements" you get a prediction of the incompleteness theorems. And I would guess that the incompleteness phenomenon is something that Russell wouldn't have thought of at that time. –  Stefan Geschke Aug 26 '10 at 10:41

Nelson claims to have succeeded just now.

http://www.math.princeton.edu/~nelson/papers/outline.pdf

I hope consensus about this forms soon, so I can know what to do with the rest of my life. If only I had been born a few years later, I wouldn't be put into the position of worrying that my chosen career path is doomed and I must go build houses or something.

-
Maybe I'm missing something but what do the above two links have to do with the topic? –  Sid Sep 27 '11 at 4:07
@Sid: I think Will is, in his idiosyncratic way (no offence meant) riffing on the last sentence of mbsq. –  Yemon Choi Sep 27 '11 at 4:59
Nelsons article links to a book he is currently writing on the topic: math.princeton.edu/~nelson/books/elem.pdf –  Michael Bächtold Sep 27 '11 at 11:29
It seems Nelson has withdrawn his claim. In any case I'd like to point out that the first section of chapter 1 of his (unfinished) book on the subject (math.princeton.edu/~nelson/books/elem.pdf, "Potential vs. actual infinity") still stands. I find it to be a great motivation for his search, regardless of the outcome. –  godelian Oct 1 '11 at 15:40
the claim was withdrawn: golem.ph.utexas.edu/category/2011/09/… –  Michael Bächtold Oct 1 '11 at 15:41

This is perhaps an obvious remark, but it may be helpful for those who haven't yet gotten used to the fact that one must think about consistency questions slightly differently from how we think of "ordinary" mathematical questions. Namely, let us ask what an "obstruction to finding an inconsistency in ZF" might look like? The obvious "obstruction" would be a proof that ZF is consistent. But we can't expect to find such a thing, by Goedel's 2nd incompleteness theorem. Therefore, we cannot hope to find a mathematical obstruction in the usual sense.

-
I do not think I properly understand this comment. By the 2nd IT you cannot expect to prove Con(ZFC), providing ZFC is consistent. But in case you do not believe in consistency of ZFC you are not forbidden (at least by 2nd IT) to hope to show that $ZFC\vdash Con(ZFC)$. (This is not that I do not believe in consistency of ZFC, I just do not understand the argument.) –  Mad Hatter Jan 25 '13 at 15:07
If you show that ZF⊢Con(ZF) then it immediately follows that ZF is inconsistent, by Goedel's 2nd. That is, far from finding an obstruction to finding an inconsistency in ZF, you've actually found the exact opposite, namely an inconsistency in ZF. Probably you're so used to thinking that a proof of something in ZF tells you that it's true that you are misled into thinking that showing that ZF⊢Con(ZF) would show that ZF really is consistent. But in fact ZF⊢Con(ZF) shows exactly the opposite, that ZF is really inconsistent. –  Timothy Chow Jan 25 '13 at 16:52
But this is exactly my point - if you want to prove inconsistency of some axiomatizable theory $T$ extending, say Peano Artihmetic, show $T\vdash Con(T)$ and apply Goedel's 2nd. And my point is that you cannot hope to prove such a thing ONLY IF you believe in consistency of $T$. Otherwise, why not to look for a proof of $Con(T)$ within $T$ itself to demonstrate $T$ is flawed. Actually, I do not believe that this would be the easiest way to prove $T$'s inconsistency, but at least a possible way. –  Mad Hatter Jan 26 '13 at 8:19
O.K., I think I see your confusion. When I said "a proof that ZF is consistent," I meant an ordinary mathematical proof, of the type you read in journals and find yourself persuaded by. I did not mean a formal proof of Con(ZF) from the axioms of ZF. As you say, the latter is something that a skeptic about ZF might hope to discover. But neither the skeptic nor the believer can hope to find a proof that ZF is consistent in the sense that I intended it. –  Timothy Chow Jan 27 '13 at 3:38
But you mean a proof like that by methods available in a theory not stronger that ZF(C)? –  Mad Hatter Jan 28 '13 at 7:24
show 1 more comment

I cannot judge how serious these are, I just put Nelson predicative arithmetic in Google and came up with lots of stuff: