Does a Turing machine exist with output 1 if an unprovable statement is true and 0 otherwise?

Question

Suppose there is some statement $X$ that is unprovable in some system, e.g. ZFC. Let $L = \{x : x \in \Sigma^* \land X \text{ is true}\}$. Is there a Turing machine that decides $L$? I have had an argument about this where I have argued that $L$ is decidable as $X$ is either true or false, and in each case there is a deciding Turing machine. However they argued that if this were true, we could construct a proof of existence of a (dis)proof of $X$ as such:

Let $M$ be the Turing machine that decides $L$. If $M$ accepts $\varepsilon$, the proof is that $M$ accepts $\varepsilon$. If not, the proof is that $M$ does not accept $\varepsilon$.

I was of the opinion that this proof is not valid, since the proof needs to be convincing outside the context of the proof of existence of the proof, and in this case the proof depends on the output of $M$, which is not available in the proof (we don’t know what $M$ is), and the outcome of the decision in the proof of existence is not carried over to the proof. However I realize you might make the argument that if a supposed proof/disproof exists by this method, it might actually be a proof since the output of $M$ is inferrable from which proof exists.

Does such a Turing machine exist and do these arguments hold water?

Answer 1

If there existed such a machine, and it were known to be correct, then a transcript of its computation on an input proposition $P$ would constitute a proof of $P$. So it’s not the fact of the acceptance that would be the proof, but rather the sequence of its steps.

Answer 2

Your definition of $L$ is a bit confusing to me, because it's unclear whether your $x$ and $X$ are a typo, and are actually supposed to be the same. So, I'm assuming it isn't a typo, meaning that $L$ is the empty language if $X$ is false, and the language of all strings if $X$ is true.

In that case, then classical computability says that this language is decidable, and you can prove this within ZFC, regardless of what $X$ is. The proof goes like so:

• By excluded middle, $X ∨ ¬X$ so consider both possibilities
  1. If $X$, then the machine that accepts all strings decides $L$
  2. If $¬X$, then the machine that rejects all strings decides $L$

You can actually move the use of excluded middle around somewhat. For instance, put it in the transition function of the machine, so that it looks like you are only defining a single machine that decides the problem.

---

Now, the subtlety is, when $X$ is independent of ZFC, there is no ZFC proof of which machine in the above argument is the correct one to do the deciding.¹ By picking either $X$ or $¬X$ to add to your axioms, you can choose which becomes the correct one. And generally it is nonsensical to suggest that there is a 'right' answer of which one to pick in situations like this.

This is why the argument you mention doesn't go through. There is a ZFC proof of "either $M$ accepts $ε$ or it doesn't," but not which of those cases holds (because in general, either case can hold depending on an arbitrary choice of models). Classical decidability doesn't lead to a proof of $X$ or a proof of $¬X$, it leads to a proof of $X ∨ ¬X$, which is always classically true.

So, personally, I view this as a fundamental flaw in classical computability—it is tainted by its use of classical logic. It cannot avoid classifying these (admittedly rather trivial) problems as "decidable" without actually having a good reason to do so. I.E. there isn't a systematic procedure we could use to actually 'figure out' the answer (even in an idealized sense, where time and space resources are unlimited). The very idea that such a thing could exist is nonsense, because there is no single correct answer based on the axioms in play.

[1] To spell this out a bit more, there are ZFC proofs of things like $ε \in L ⇒ X$ and $\mathsf{Accepts}(M,ε) ⇒ X$. So, if there were a ZFC proof that the described machine accepts $ε$, then it would yield a proof of $X$. Similarly, if there were a ZFC proof that $ε$ were rejected, it would yield a proof of $¬X$. So, if $X$ is independent, so must be the proposition stating that the machine accepts $ε$. There can be no ZFC proof of exactly how the machine acts.

Answer 3

$\def\ed{\stackrel{\text{def}}{=}}$ By "system" I'll presume you mean some theory of first order logic—that is, a consistent set of sentences of a first-order logic which constitute the non-logical axioms of the system. This will include such systems as Peano arithmetic, ZFC. etc. If so, then there's a fundamental problem with your definition of $\ L\ ,$ in that that the truth or falsity of a sentence $\ X\ $ is only defined absolutely if either $\ X\ $ or $\ \neg X\ $ is a theorem. If neither is a theorem, then the truth or falsity of $\ X\ $ is only defined relative to a model, and there will always exist such models in which $\ X\ $ is true and others in which it is false. This follows from one of the fundamental theorems of model theory—namely that a set of sentences has a model if and only if it is consistent.

If $\ \mathscr{A}\ $ is the set of non-logical axioms of your system, and $\ X\ $ is not provable, then $\ \mathscr{A}\cup\{\neg X\}\ $ is a consistent set of sentences and therefore has a model, by the above-quoted theorem, and $\ X\ $ must be false in that model. On the other hand, if $\ \neg X\ $ is not provable, then $\ \mathscr{A}\cup\{X\}\ $ must have a model, by the same argument, and $\ X\ $ will be true in that model.

Thus, for your language $\ L\ $ to be well-defined you have to say what model or set of models of $\ \mathscr{A}\ $ it is that $\ X\ $ is supposed to be true in. There are three obvious ways you could modify your definition to do this:

• $L_1\ed\big\{x:\big(x\in E^*\big) \wedge \big (X\ \text{ is true in every model for }\ \mathscr{A}\big)\big\}\ ,$
• $L_2\ed\big\{x:\big(x\in E^*\big) \wedge \big (X\ \text{ is true in some model for }\ \mathscr{A}\big)\big\}\ ,$
• $L_3\ed\big\{x:\big(x\in E^*\big) \wedge \big (\mathscr{M}\ \text{ is a model for }\ \mathscr{A}\cup\{X\}\big)\big\}\ ,$

where $\ \mathscr{M}\ $ is some specific interpretation of your system that now becomes another parameter, along with $\ \mathscr{A}\ $ and $\ X\ $, in the specification of $\ L_3\ $. Assuming the set $\ E\ $ is finite and entirely unrelated to $\ X\ ,$$\ \mathscr{A}\ ,$ or $\ \mathscr{M}\ $, then your argument, applied to these languages, namely concluding that they're all decidable, is perfectly correct, for the same reason Dan Doel gives in his answer—namely $\ L_1=\emptyset\ $ and $\ L_1,L_2\ $ are either $\ \emptyset\ $ or $\ E^*\ $, all of which are trivially decidable.

The completeness theorem for first-order logic tells us that if $\ X\ $ is true in every model of $\ \mathscr{A}\ $, then $\ X\ $ is a theorem. But since you've specified that $\ X\ $ is not a theorem, it follows that $\ L_1=\emptyset\ $. Likewise, if $\ \neg X\ $ is a theorem, then $\ L_2=\emptyset\ $, and if $\ \neg X\ $ is not a theorem, then $\ L_2=E^*\ $. Your acquaintance would appear to be both conflating satisfiability (viz. truth in some model) for validity (viz. theoremhood, or truth in every model), and mistaking the parameter $\ X\ $ that appears in the definitions of the languages $\ L_i\ $ for inputs that must be given to the Turing machines for deciding them. It is true that when constructing a Turing machine for deciding any of these languages, you will have to incorporate appropriate knowledge about $\ X\ $ into its design, but this may be no more than knowing, for instance, that $\ \neg X\ $ is a not theorem, in which case you can simply design the Turing machine for $\ L_2\ $ to accept all words, without incorporating anything at all about a proof of $\ X\ $ into it (and, in fact, $\ X\ $ will not necessarily be provable in this case).

Your acquaintance is possibly confusing your $\ L\ $ with something like one of the following more interesting languages:

• $\mathscr{L}_1\ed\big\{X\,:\,X\ \text{ is true in every model for }\ \mathscr{A}\,\big\}\ ,$
• $\mathscr{L}_2\ed\big\{X\,:\,X\ \text{ is true in some model for }\ \mathscr{A}\,\big\}\ ,$
• $\ \mathscr{L}_3\ed\big\{(\mathscr{M},X)\,:\,\mathscr{M}\ \text{ is a model for }\ \mathscr{A}\cup\{X\}\,\big\}\ .$

As alluded to above, $\ \mathscr{L}_1\ $ is just the set of theorems of your theory. It's true that if there were a Turing machine for deciding $\ \mathscr{L}_1\ ,$ then its computation on any input $\ X\ $ would either provide a proof of $\ X\ $ or a proof that $\ X\ $ is not provable. Another fundamental theorem of first-order logic, however, tells us that $\ \mathscr{L}_1\ $ is recursively enumerable, but not recursive. That is, there is a surjective Turing computable function from the natural numbers onto $\ \mathscr{L}_1\ $, but no Turing machine for deciding $\ \mathscr{L}_1\ $. The languages $\ \mathscr{L}_2\ $ and $\ \mathscr{L}_3\ $ are not even recursively enumerable, let alone recursive. If there were a Turing machine to recursively enumerate either $\ \mathscr{L}_2\ $ or $\ \mathscr{L}_3\ $, it could be used to construct a Turing machine for deciding $\ \mathscr{L}_1\ ,$ which is known to be impossible.