Question arising from Voevodsky's talk on inconsistency - MathOverflow

Question arising from Voevodsky's talk on inconsistency

2010-10-05T22:43:53Z

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

a subset about which you can prove that it is impossible to say anything about this subset, whatsoever.

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?

Answer by Rodrigo Freire for Question arising from Voevodsky's talk on inconsistency

2010-10-05T22:50:20Z

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

Answer by Bjørn Kjos-Hanssen for Question arising from Voevodsky's talk on inconsistency

2010-10-05T22:51:36Z

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.