2
$\begingroup$

Is there a set $B$ about which it provably cannot be decided whether it is computable in $\mathsf{ZFC}$?

$\endgroup$
6
  • 6
    $\begingroup$ Let $B=\emptyset$ if $\mathrm{Con}(\mathsf{ZFC})$ and $B=0'$ otherwise. $\endgroup$ Commented Nov 29, 2018 at 19:13
  • $\begingroup$ @AndrésECalcedo : I' m probably missing something, but why is it provably undecidable whether your set $B$ is computable? If we enumerate all valid deductions in ZFC, we can decide for each such deduction whether its result is say 0=1. If such contradiction occurs, then $B$ is computable... By saying it is provably undecidable, you in fact assert Con(ZFC),... but then $B$ is also computable. Or in case you're correct, what am I missing? $\endgroup$ Commented Nov 29, 2018 at 19:57
  • 4
    $\begingroup$ @Frank The question cannot be whether there is (provably) a decision algorithm for the question "Is $B$ computable?", since that is trivial (yes, there is such a decision algorithm for any $B$). Instead, the question is (should be?) whether we can define a set $B$ (in a way that $\mathsf{ZFC}$ proves uniquely specifies a set of numbers) and such that it is independent of $\mathsf{ZFC}$ whether $B$ is computable. $\endgroup$ Commented Nov 29, 2018 at 20:02
  • $\begingroup$ @AndrésECalcedo thanks for clarifying, I might perhaps or should have figured that out myself... but it's late and I'm lazy... $\endgroup$ Commented Nov 29, 2018 at 20:11
  • 3
    $\begingroup$ So let $S_0$ be a set that is provably not computable, $S_1$ a set that is computable, $Q$ a statement that is independent of ZFC, and take $$ B = \cases{S_0 & if $Q$ is true \cr S_1 & otherwise}$$ $\endgroup$ Commented Nov 29, 2018 at 20:14

2 Answers 2

5
$\begingroup$

An explicit example: $B=$ the set of all theorems of ZFC.

$\endgroup$
3
  • $\begingroup$ Wait, that B is uncomputable due to Gödel's incompleteness theorem, which is provable in ZFC. So don't we have ZFC proves "B is not computable"? $\endgroup$
    – none
    Commented Nov 30, 2018 at 11:40
  • 3
    $\begingroup$ @none ZFC cannot prove that ZFC is consistent. If ZFC is inconsistent, then $B$ consists of all sentences in the language of set theory, which makes it computable. $\endgroup$ Commented Nov 30, 2018 at 12:10
  • $\begingroup$ As Andreas Blass commented above, "X is undecidable in ZFC" implies ZFC is consistent. So when someone says "prove that X is undecidable in ZFC", I interpret this as meaning "prove that Con(ZFC) implies that X is independent of ZFC". In this case, Con(ZFC) implies that $B$ is not computable, so Con(ZFC) presumably does not imply the that statement "$B$ is computable" is independent of ZFC. I apologize if I am confused here. $\endgroup$ Commented Nov 30, 2018 at 14:34
4
$\begingroup$

It's worth noting that the answer above is answering the following question: is there a formula $\phi(x)$ in the language of ZFC such that ZFC can't prove either $\lbrace x \in \omega \mid \phi(x) \rbrace$ is computable nor that it's not computable. One might worry the answer above is 'cheating' in a certain sense by picking a formula $\phi$ which behaves very differently depending on whether or not CON(ZFC) is true.

If we wanted to think about sets a bit more extensionally we could insist that our formula not change it's mind about what actual integers are in $B$ depending on the model. In other words we could interpret the question as asking if there is some definition of a set $B$ whose standard part is the same in all models of $ZFC$ but some models extend to be computable while others extend it to be uncomputable.

The answer here is yes as well. Let $B$ be the set of $n$ such that $n \in 0'$ (or any other provably uncomputable set) and $n$ greater than the first proof of contradiction from the ZFC axioms. The standard part of $B$ is clearly empty in every model of ZFC and $B$ clearly computable in any model of $ZFC+CON(ZFC)$ and not in any model of $ZFC+\lnot CON(ZFC)$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .