## Question arising from Voevodsky’s talk on inconsistency

This question arises from the talk by Voevodsky mentioned in this recent MO question. On one of his slides, Voevodsky says that

a general formula even with one free variable describes a subset of natural numbers for which one can prove, using an argument similar to the one which is used in Goedel's proof, that there is not a single number n which can be shown to belong to this subset or not to belong to it.

And in his spoken commentary he adds that there is a formula defining

I interpret this as the claim that there is an arithmetically definable set $S$ for which there is no theorem of Peano arithmetic of the form $n\in S$ or $n\not\in S$. Perhaps I am misinterpreting, but can anyone supply (informally) the definition of such a set?

-
Surely his last statement is making a slightly stronger claim: that also, for instance, you couldn't prove “$S$ and its complement are both infinite”? More precisely, that there is a formula $S(n)$ about which no non-trivial theorem is provable? Clearly you can always prove things like $\forall n.\ (S(n) \Leftrightarrow S(n))$, so I'd formalise the claim as something like: any theorem PA proves about $S$, it proves about any predicate. – Peter LeFanu Lumsdaine Oct 6 2010 at 1:59
@Peter: In that case this question is still open, because about $\Omega$ you can prove many nontrivial things, e.g. that it is ML-random. But is it possible to define "nontrivial"? – Bjørn Kjos-Hanssen Oct 6 2010 at 2:43
Couldn't you, by Goedel-style methods, cook up a sequence of statements $p_1,p_2,\ldots$ such that $p_n$ is undecidable even if for each $i<n$ we adjoin $p_i$ or $\neg p_i$ to ZFC? Then define $S$ to be the set of $n$ for which $p_n$ is true. Can't say much about that. – James Cranch Aug 28 2011 at 8:57
Where by ZFC I mean Peano arithmetic... – James Cranch Aug 28 2011 at 8:58

Let $S$ be a first order definable Martin-Löf random set such as Chaitin's $\Omega$. If Peano Arithmetic, or ZFC, or any other theory with a computable set of axioms, proves infinitely many facts of the form $n\in S$ or $n\not\in S$ then it follows that $S$ is not immune or not co-immune and hence not ML-random after all.

(The set of theorems of our theory of the form $n\in S$ (or $n\not\in S$) is computably enumerable and infinite, hence has an infinite computable subset. Being immune means having no infinite computable subset.)

So only finitely many such facts can be proved. Now using an effective bijection between $\mathbb N$ and $\mathbb N\times \mathbb N$, decompose $S$ into infinitely many "columns", $S=S_0\oplus S_1\oplus\cdots$. Then one of these columns has the required property.

The theory should be strong enough to deal effectively with breaking a definable set up into columns and associating values in a column with values in the original set, but this is certainly doable in PA or ZFC.

-
Thanks! This is the kind of thing I had in mind, but I couldn't get round the finitely many exceptions. – John Stillwell Oct 5 2010 at 22:56
Alternatively, look at a tail of $\Omega$, namely $\{n: n+k\in\Omega\}$ where $k$ is large enough to take you beyond the finitely many exceptions. – Bjørn Kjos-Hanssen Oct 5 2010 at 22:59

(n=n)&(con(ZF))

-
Well, yes, but this set has another definition (either the empty set or $\mathbb{N}$) for which all the membership statements are provable. – John Stillwell Oct 5 2010 at 23:06
Nice. Well, my more complicated set has the redeeming quality that no matter which first order definition of it you use, you can only prove finitely many facts of the form $n\in S$, $n\not\in S$. – Bjørn Kjos-Hanssen Oct 5 2010 at 23:11
I guess the conclusion here is that Voevodsky's claim should have been reformulated, replacing "nothing" by "only finitely much". – Bjørn Kjos-Hanssen Oct 5 2010 at 23:19
In terms of proof theory and definability, it's not the case that either $\phi$ nor $\mathbb{N}$ is another definition of this set — that's something that only holds in a specific model, and in that setting, every set has alternative definitions about which some membership statements are provable. So it's fair to say you can't prove any statements of the form $n \in S$ or $n \nin S$ for this set. But you still can prove something non-trivial about it: you can prove “either $\forall n. S(n)$, or $\forall n. \lnot S(n)$”; so surely it doesn’t fit Voevodsky’s claim? – Peter LeFanu Lumsdaine Oct 6 2010 at 2:05
@Peter: I'm sure Voevodsky had in mind something more like my answer than Rodrigo Freire's answer. But if we really want to talk about all the facts about $S$ being undecided then Rodrigo's answer is just as correct as mine (and simpler). Because for any finitely many $n_i$ one could make another definition of my column of $\Omega$ where the facts about whether $n_i\in$ that column are built into the definition. – Bjørn Kjos-Hanssen Oct 6 2010 at 2:31
show 1 more comment