One common method of resolving this is to cash out “representable” numbers in terms of outputs of halting turing machines, so that paradoxes of Berry’s sort require solving the halting problem and are therefore not themselves representations.
Some Turing machines have been proven to not halt; some have not. There must exist at least one Turing machine which no Turing machine can ever prove does not halt. (It is trivial to prove that a Turing machine halts if it does)
Since there are a countably infinite number of Turing machines, there must be at most a countably infinite number of characteristics such that only every non-halting Turing machine has one or more of those characteristics. If we suppose that each of these characteristics can be checked by a single Turing machine that halts when it proves that the target does not halt, then we have a contradiction (since we can build a Turing metamachine oracle that diagonalizes a countably infinite number of machines each testing one property).
Therefore there exists some characteristic of a Turing machine which is sufficient for that machine to be non-halting, such that it cannot be proven that said characteristic is sufficient.
I wonder what a program that doesn’t halt but cannot be proven not to halt looks like? What does the output look like after 2BB(n) steps? It must have a HALT function somewhere accessible, or else it would be trivial to prove that it never halted, but likewise said function must never happen, which means that the condition must never happen; but the condition must be accessible, or it would be trivial to prove that it never halted...
I think the typical example is if you do a search for a proof of inconsistency in Peano arithmetic. You don’t expect to find any inconsistencies, but you can’t prove that you won’t.
One common method of resolving this is to cash out “representable” numbers in terms of outputs of halting turing machines, so that paradoxes of Berry’s sort require solving the halting problem and are therefore not themselves representations.
… Unless there exists something other than a Turing machine that can solve the halting problem.
Which of course leads us to things like “The set of Turing machines that do not halt and cannot be proven to not halt by any Turing machine”.
See the Church-Turing thesis for more on this topic.
I think I was on a slightly different topic:
Some Turing machines have been proven to not halt; some have not. There must exist at least one Turing machine which no Turing machine can ever prove does not halt. (It is trivial to prove that a Turing machine halts if it does)
Since there are a countably infinite number of Turing machines, there must be at most a countably infinite number of characteristics such that only every non-halting Turing machine has one or more of those characteristics. If we suppose that each of these characteristics can be checked by a single Turing machine that halts when it proves that the target does not halt, then we have a contradiction (since we can build a Turing metamachine oracle that diagonalizes a countably infinite number of machines each testing one property).
Therefore there exists some characteristic of a Turing machine which is sufficient for that machine to be non-halting, such that it cannot be proven that said characteristic is sufficient.
I wonder what a program that doesn’t halt but cannot be proven not to halt looks like? What does the output look like after 2BB(n) steps? It must have a HALT function somewhere accessible, or else it would be trivial to prove that it never halted, but likewise said function must never happen, which means that the condition must never happen; but the condition must be accessible, or it would be trivial to prove that it never halted...
I think the typical example is if you do a search for a proof of inconsistency in Peano arithmetic. You don’t expect to find any inconsistencies, but you can’t prove that you won’t.
More like trying to find the Godel statement of the universe; it provably exists, and provably cannot be positively identified.