I have constructed a function of seemingly contradictory nature.

Let $f$ be a function which, given an input $n\in \mathbb{N}$, lexicographically searches through all strings and finds the $n$th pair $\langle T, P\rangle$ where $T$ is a valid Turing machine encoding, and $P$ is a valid formal proof (in Peano Arithmetic, for example) that $T$ halts with output in $\{0,1\}$ for any input in $\mathbb{N}$. Then, $f$ returns $1-T(n)$ (where $T(n)$ is the output of the Turing machine $T$ encodes when given input $n$).

First of all, $f$ appears to be a computable function, as to the best of my knowledge each of its subprocesses (lexicographically searching through strings, checking if a string is a syntactically correct TM-encoding, checking whether a given formal proof actually proves a given result) are themselves computable.

I also have a 'proof' that $f$ returns $0,1$ given every natural number input $n$. There are infinitely many of these pairs $\langle T, P\rangle$: for example, let $T$ be the $1$-state Turing machine which immediately halts with output $0$ no matter the input, and let $P_i$ be the (trivial) formal proof that $T$ has this behavior where $i$ unnecessary variables are introduced at the beginning of the proof. Since there are infinitely many such pairs, when lexicographically searching through the set of strings $f$ will find an $n$th such pair. Since there exist halting programs which can verify if a string represents a valid TM-encoding or whether a given formal proof proves if a given TM has the desired behavior, the function will duly return $1-T(n)$, which must be in $\{0,1\}$ as $T(n)$ must be in $\{0,1\}$ by the proof $P$.

Here is where I reach a contradiction. If my description of $f$ is precise enough it can be formally translated into a Turing machine encoding $T'$ which performs the behavior claimed. And if my proof is indeed correct, it should be translateable into a formal proof $P'$ that $T'$ halts with output in $\{0,1\}$ for every input in $\mathbb{N}$.

But then the pair $\langle T', P'\rangle$ is the $n$th pair satisfying our conditions for some $n$. And here we reach two distinct contradictions

  1. $f$ will end up outputting $1-T(n)$ given input $n$, contradicting the claim that $T$ matches $f$'s claimed behavior
  2. When running $T$ on input $n$, eventually $T(n)$ will be called (in order to return $1-T(n)$), leading to an infinite loop, and contradicting the fact that the verified proof $P$ asserted this loop would not happen.

So there is a clear contradiction here. Obviously my 'proof' is missing many technical details, thus here are all the places where I think it could go wrong:

  1. It could be impossible to computationally determine if a string $T$ is a valid Turing Machine encoding.
  2. It could be impossible to computationally determine if a string $P$ represents a valid formal proof (in a chosen language).
  3. Given a Turing machine encoding $T$ and a formal proof $P$, it is impossible to computationally determine whether $P$ is a correct proof that $T$ halts with output in $\{0,1\}$ for any input in $\mathbb{N}$.
  4. It is not possible to translate my description of $f$ into a Turing Machine for some other reason
  5. $f$ is a computable functions with the properties I claim, yet my proof is not translatable into the same formal system used to judge the proofs in the pairs $\langle T,P\rangle$, and a more expressive or stronger system is needed
  6. f doesn't even halt for all $n$. I think this would necessitate the existence of a pair $\langle T, P\rangle$ such that $P$ proves that $T$ halts with output in $\{0,1\}$, yet for the input $n$ $T$ actually doesn't halt (thus the chosen formal system would be unsound).

Of these, I feel as though $5$ is the most likely to be the issue. Although, looking back at my proof, while I admit there are numerous missing technical details, none of the steps stand out to me as as all that likely to implicitly go beyond any chosen formal system.

So where is the issue in my reasoning?

  • 3
    $\begingroup$ In short, you are saying, the set of Turing machines that provably halt with all inputs and only return $0$ or $1$ for each input is recursively enumerable. Past my bedtime, so I'll have to think further tomorrow. $\endgroup$ Commented May 7 at 2:51

3 Answers 3


Your claimed proof that $f$ always halts and returns $0$ or $1$ relies on the assumption that if there is a PA-proof that a Turing machine halts for all inputs, then it actually halts for all inputs. But PA itself cannot prove that claim, hence the proof that $f$ works as intended cannot be done inside PA.

  • 1
    $\begingroup$ If a proof of a statement exists, how could it be false? What am I missing here? $\endgroup$
    – user3490
    Commented May 7 at 12:52
  • 4
    $\begingroup$ @user3490 PA cannot prove its own consistency (ie if there is a PA-proof of something then that something holds). $\endgroup$
    – ronno
    Commented May 7 at 12:58
  • 1
    $\begingroup$ To be clear: And thus the turning machine $T_f$ has no $T_f, P$ pair, so isn't enumerated by $f$ in its set of turing machines it will run and emulate and return $1-T(n)$ on. What more this provides a Godel-like restriction on what kinds of proofs a consistent system can prove; the OP basically replicated a more complex "It can be proven that this proof does not exist" Godel-number trick. $\endgroup$
    – Yakk
    Commented May 7 at 16:04
  • $\begingroup$ @user3490 If PA is inconsistent, it has a proof of false. How can false be false? $\endgroup$
    – Trebor
    Commented May 7 at 18:28
  • 1
    $\begingroup$ @Yakk: While that is true, it should perhaps be mentioned that there is a more straightforward construction of Gödelian incompleteness based on Turing machines and the halting problem. You can just directly construct a TM that searches for a proof that corresponds to its input, and then such a TM would be a halting oracle, so some of the time the proof must not exist. $\endgroup$
    – Kevin
    Commented May 8 at 0:01

@arno's answer is great. But in case you are wondering what goes on practically.

In your Turing machine $T_f$ you have a proof checker. This proof checker encodes the system of proof - what arguments you consider valid - about the behavior of Turing Machines.

When trying to prove things about $T_f$, your system of proofs (encoded in the TM) has to understand proofs about itself (also encoded in the TM) - about its ability to prove provable things in this case. This - getting an axiom system to reason about itself - is the basic technique that Gödel used in his incompleteness theorem.

And Gödel's result was that no system is capable of doing that - sufficiently powerful systems are either incomplete, unable to prove (certain) statements about themselves, or inconsistent.

Whatever proof machinery you provide to $f$ cannot reason about itself effectively. You have shown that if it can prove it always halts, you get a contradiction: thus, you can prove that it cannot prove it always halts.

And any attempt to make $T_f$ smarter so that it knows it always halts leads to a contradiction, or the machine proving something about a different machine than itself.


Let me try a more straightforward answer : The set of pairs $\langle P,T\rangle$ is indeed recursively enumerable since valid proofs can be verified by a computer. Hence the Turing-machine $T_f$ must halt on all its inputs, because if $\langle T, P\rangle$ is the $n^\text{th}$ valid pair as recognized by $T_f$, this means that $P$ is a valid proof that $T$ terminates, so $T_f$ must terminate when it runs $T$. But I just used a meta-argument : if there is a proof, then it must be true. Because otherwise our logical system would be broken, and we all know it's not. Because it's consistent and sound.

However, as @Yakk points out, by Gödel's argument, the consistency of a logical system (which can formalize Peano's arithmetic) is not provable within this logical system. What is means is that all the previous point is not a valid logical proof in the point of view of the machine $T_f$, and there must not exist a valid proof $P$ for the termination of $T_f$.

  • $\begingroup$ @RedFive In what way does this not answer the question? I mean, in the last paragraph they literally explain why the OP's tempting argument does not work. $\endgroup$
    – Suzet
    Commented May 9 at 3:19
  • $\begingroup$ I'll read it again then. $\endgroup$
    – Red Five
    Commented May 9 at 3:30

You must log in to answer this question.

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