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
- $f$ will end up outputting $1-T(n)$ given input $n$, contradicting the claim that $T$ matches $f$'s claimed behavior
- 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:
- It could be impossible to computationally determine if a string $T$ is a valid Turing Machine encoding.
- It could be impossible to computationally determine if a string $P$ represents a valid formal proof (in a chosen language).
- 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}$.
- It is not possible to translate my description of $f$ into a Turing Machine for some other reason
- $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
- 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?
Best Answer
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.