• I
• olgerm
In summary, the conversation discusses the most well-known proof of the undecidability of the halting problem, which involves a hypothetical function H1 that can determine whether a program halts on a given input. It is shown that such a function cannot exist, as it leads to a contradiction in both cases when applied to a function D that is defined based on its input. The conversation also considers the existence of a modified function F3, but it is proven that this function is also non-computable. This further reinforces the understanding that there is a widespread misunderstanding about the halting problem.
SSequence said:
What would be correct to say would be that H1 are F3 are not computable functions.
Again, this depends on what mathematical domain you are working in. In the domain assumed in the OP to this thread, H1 and F3 do not exist. Since they do not exist, it is meaningless to even ask whether they are functions. Similar remarks apply to "computable".

If you expand your domain to include, for example, "oracles", as in your previous posts, then H1 and F3 can exist in that expanded domain and you can ask questions like whether they are computable or non-computable. But you have to be working in a domain where they exist to begin with to even pose those questions.

PeterDonis said:
Again, this depends on what mathematical domain you are working in. In the domain assumed in the OP to this thread, H1 and F3 do not exist. Since they do not exist, it is meaningless to even ask whether they are functions. Similar remarks apply to "computable".

If you expand your domain to include, for example, "oracles", as in your previous posts, then H1 and F3 can exist in that expanded domain and you can ask questions like whether they are computable or non-computable. But you have to be working in a domain where they exist to begin with to even pose those questions.

OK I will put it this way. In ZFC [and indeed many much much weaker theories that can talk about functions] H1 and F3 are functions. However, they are not computable functions in any of those theories.

It might be possible that there are some strict theories (that are based on constructivism) that can talk about functions but still H1 and F3 are indeed not functions [further, the basic idea of halting problem can still be carried out]. But someone well-versed in this would be more qualified to comment.

Last edited:
SSequence said:
In ZFC [and indeed many much much weaker theories that can talk about functions] H1 and F3 are functions.
Doesn't the proof referred to in the OP, that H1 does not exist (and similarly for F3 based on follow-up posts), contradict this claim?

PeterDonis said:
Doesn't the proof referred to in the OP, that H1 does not exist (and similarly for F3 based on follow-up posts), contradict this claim?
The proof in the OP shows that:
"There is no computer program computing a (total) function ##f:\mathbb{N}^2 \rightarrow \{0,1\}## such that:
(a) If the program with index ##a## halts on input ##b## then ##f(a,b)=1##.
(b) If the program with index ##a## loops forever on input ##b## then ##f(a,b)=0##."

Now if we think [for example, based on concerns raised by constructivism] that all the (total) functions ##f:\mathbb{N}^2 \rightarrow \{0,1\}## must necessarily be those that are computed by some computer program then what you wrote would indeed be correct and H1 would not exist.

============================

Note that when we say that much of mainstream mathematics is formalized by ZFC , then this also includes results like incompleteness theorems, halting problem etc. That is, they are theorems of ZFC. Of course this debate can go philosophical on "what comes first or not" [and honestly, I am not qualified to comment on this]. Nevertheless, there would be a (finite) proof of these results in ZFC.

For example, we will have an actual predicate ##P(x,y)## in language of set theory such that:
##P(x,y)=Halt(x,y)## for all ##x,y \in \omega##

Similarly:
"##Halt:\mathbb{N}^2 \rightarrow \{0,1\}## is not a computable function."
would be a theorem of ZFC and many weaker theories.

Of course actually formalizing this requires much more understanding and attention to quite a bit of details (and tbh I don't know the details well at all ..... only the basic idea).

Last edited:
SSequence said:
Now if we someone thinks [for example, based on concerns raised by constructivism] that all the (total) functions ##f:\mathbb{N}^2 \rightarrow \{0,1\}## must necessarily be those that are computed by some computer program then what you wrote would indeed be correct.
Hm, ok, if we leave aside the proof in the OP for a moment, how do we know that such a total function does exist in ZFC?

Here is one way to think about it. The real numbers are not countable in ZFC. But every real number can be thought of as being associated with a unqiue function from ##\mathbb{N}## to ##\{0,1,2,3,4,5,6,7,8,9\}##. And hence also to a function from ##\mathbb{N}## to ##\mathbb{N}##.Regarding your specific question in previous post, I will try to do so later (but I don't know the details too well). Nevertheless, I will try to describe based on how much I know (even if its limited).

SSequence said:
Why do you think that the number of (total) function from ##\mathbb{N}## to ##\mathbb{N}## will be countable in ZFC?
It might not be. But that's really a separate question from the one we're discussing. We are discussing one particular (claimed) total function (or two of them, but we can focus on just H1), which has certain known properties. That set of known properties pins things down to a smaller set of functions than the set of all possible total functions from ##\mathbb{N}^2## to ##(0, 1)##. That smaller set might be countable even if the larger one is not.

SSequence said:
Regarding your specific question in previous post, I will try to do so later (but I don't know the details too well). Nevertheless, I will try to describe based on how much I know (even if its limited).
Ok.

Regarding the first quote, fair point. The questions may not be the same.

PeterDonis said:
Ok.
If we are thinking about it from a basic perspective then, as I described in previous post, we can write a predicate ##P(x,y)## [in language of set theory ...... useful link: https://mathweb.ucsd.edu/~sbuss/CourseWeb/Math260_2012F2013W/AxiomList.pdf] with two open variables ##x,y## such that:
##P(x,y)=Halt(x,y)## for all ##x,y \in \omega##
It seems to me that firstly we will need to have a convention to encode functions as relations though.

=======================

If we think from a more indirect perspective (and not the details), then for every model of ZFC the reals numbers ##\mathbb{R}## will necessarily contain all the arithmetic sets [link: https://en.wikipedia.org/wiki/Arithmetical_set]. Note that we are thinking about real numbers as subsets of ##\omega## here. And the arithmetic sets also contain the halting set [and essentially also the halting function using a suitable computable bijection from ##\mathbb{N}^2## to ##\mathbb{N}##].Edit: I modified my previous reply, because I felt that it was a bit of over-kill approach (and maybe would distract from main discussion).

Last edited:
SSequence said:
we can write a predicate ##P(x,y)## [in language of set theory ...... useful link: https://mathweb.ucsd.edu/~sbuss/CourseWeb/Math260_2012F2013W/AxiomList.pdf] with two open variables ##x,y## such that:
##P(x,y)=Halt(x,y)## for all ##x,y \in \omega##
It seems to me that firstly we will need to have a convention to encode functions as relations though.
Functions are easy, they are just sets of ordered pairs, where for each pair the first element is from the domain, and the second element is from the range.

The key part is encoding what Halt actually means in a formula of set theory; that is required in order to express the predicate you describe. You can't just wave your hands and assume that can be done; you have to prove it.

Note that your reference is to first-order set theory, but we can't really express what we need to express in first-order set theory. The kind of formula we are after is something like this:

$$\exists P \forall x \forall y [ x \in \mathbb{N}, y \in \mathbb{N}: P(x, y) = Halt(x, y)]$$

To make this a fully well-formed formula we would then have to unpack ##Halt(x, y)## appropriately.

But since this quantifies over a predicate, it is a second-order formula, not a first-order formula. So we can't prove it using just first-order set theory.

PeterDonis said:
$$\exists P \forall x \forall y [ x \in \mathbb{N}, y \in \mathbb{N}: P(x, y) = Halt(x, y)]$$

To make this a fully well-formed formula we would then have to unpack ##Halt(x, y)## appropriately.
I am afraid you are incorrect here. The names we assign to predicates are just short-hands for a logical formula. They are not part of the "actual" set theory language. If you look at the link I posted in previous post, several short-hands are already described there. There are no base symbols there except ##\in##.

##Halt## can absolutely be unpacked. However, I don't know the way it is done unfortunately. So I don't think I can help in the detail of that at all. Couple of things that I can say I have written below. Sorry they are definitely imprecise and roughly written, so I am not confident about the precision of what I have written (even if that is how the basic idea goes like).==================From the first line of link in my previous post:
"In mathematical logic, an arithmetical set (or arithmetic set) is a set of natural numbers that can be defined by a formula of first-order Peano arithmetic. The arithmetical sets are classified by the arithmetical hierarchy."

And the arithmetical hierarchy contains the halting set etc. Very roughly, Peano arithmetic quantifies over ##\omega## or ##\mathbb{N}##. In ZFC once we have the finite ordinals and ##\omega##, we can quantify over it [well sort of ..... formally the quantification is always on universe of sets ..... but we can simulate a quantification over ##\omega##].

Last edited:
SSequence said:
The names we assign to predicates are just short-hands for a logical formula.
Doesn't matter. I'm not saying you can't have predicates in first-order logic. I'm saying you can't quantify over predicates in first-order logic. That's what second-order logic is for.

SSequence said:
##Halt## can absolutely be unpacked.
I'm not saying it can't. I'm just saying that once it's unpacked, we have to actually look to see if the formula can be proved. We can't just assume it.

I will try to describe very roughly little bit I know. To determine halt first we form a predicate ##P(a,b,t)## that describes the state of a program with index ##a## (with input ##b##) at a finite time ##t##. These variables ##a##,##b##,##t## quantify over natural numbers.

So ##P(a,b,t)## is true iff the program with index ##a## and input ##b## halted at some time ##\leq t##. Now we define ##Halt(a,b)## as [note that ##a## and ##b## are open variables in the formula below]:
##\exists i \in \mathbb{N} [P(a,b,i)=1]##.

=====================

It seems that this is called kleene's T predicate. However, the full details of how it fits into the complete picture (of only using logic) I don't know very well:
https://en.wikipedia.org/wiki/Kleene's_T_predicate

I don’t know if this helps, but here’s how I think about it. The crux of non-computability (and its baby brother undecidability) comes from the encoding of the computational model. Everything falls out of Cantor’s theorem ultimately.

A program/algorithm/computational model is encoded as a finite string, or equivalently, as a natural number. So to use the most famous example, a Turing machine is encoded as an n-tuple (finite n) that is equivalent to a member of the set ##\mathbb{N}^n##. Importantly, this encoding is a bijection (an encoder is pretty useless without a decoder). So we have a bijective encoding function from the set of all Turing machines to the set of all n-tuples over the natural numbers:
$$E:{}TM\to\mathbb{N}^n$$
The Turing machine takes a set of tape marks as an input and returns a set of tape marks as output, each of which can be represented as members of ##\mathbb{N}##. So the Turing machine is essentially a function on the natural numbers: $$TM:\mathbb{N}\to\mathbb{N}$$
(A decision problem is just an algorithm returning a yes/no response ##D:\mathbb{N}\to\{0,1\}##)
However, from Cantor’s theorem, we have that the cardinality of all functions from ##\mathbb{N}## to ##\{0,1\}## is ##|2^{\mathbb{N}}|=|\mathbb{R}|##, which is strictly larger than the cardinality of ##\mathbb{N}## (and of course the same result holds for the set of all functions from ##\mathbb{N}## to ##\mathbb{N}##). But the cardinality of the set of all Turing machines is ##|\mathbb{N}^n|=|\mathbb{N}|##, since the encoding function is a bijection. This means that the set of all functions from ##\mathbb{N}## to ##\mathbb{N}## is strictly larger than the set of all Turing machines. So there must exist functions from ##\mathbb{N}## to ##\mathbb{N}## that are not Turing-computable.

So the halting function clearly exists (as a function from ##\mathbb{N}^2## to ##\{0,1\}##, it takes as input an encoded Turing machine and its input), but it is not a member of the pre-image of the encoding function, which means it can’t take itself as an input.

olgerm
Quick correction: I don’t think the encoding function has to be bijective. It definitely must be injective (every Turing machine has a unique encoding to the natural numbers), but I don’t know if it has to be onto. Regardless, this just means that the set of all Turing machines still has cardinality at most ##|\mathbb{N}|##, so the argument still goes through: the halting function cannot be represented as a Turing-equivalent machine and therefore can’t take “itself” as an input (since it cannot be encoded into the natural numbers).

TeethWhitener said:
I don’t know if this helps, but here’s how I think about it. The crux of non-computability (and its baby brother undecidability) comes from the encoding of the computational model. Everything falls out of Cantor’s theorem ultimately.
I didn't read the whole post yet. However, I suppose there are few ways diagonalization can be thought of in this context.

For example, think of all total computable functions placed [possibly with repetition] in rows just like in cantor's theorem. So, for example ##F_x(y)## is the output of the ##x##-th function in the list when given the input ##y##. Then the following function ##g:\mathbb{N} \rightarrow \mathbb{N}## is both total (by definition) and non-computable (due to diagonalization):
##g(x)=F_x(x)+1##But indeed if we are thinking about it from computational perspective, the problem of determining that whether a function computed by a given program is total or is not decidable [in fact, not even ##0'##-computable ..... it is ##0''##-computable].

=======================

If we try a similar thing for index of all programs of course it won't (and shouldn't) work. For example, let ##\phi_x(y)## be the output of the program with index ##x## when given the input ##y##. Note that output can possibly be undefined.

Now we define a function [that may or may not be defined on some inputs] ##h: \mathbb{N} \rightarrow \mathbb{N}## as:
##h(x)=\phi_x(x)+1##
What this is supposed to mean is that:
(a) We return ##h(x)=\phi_x(x)+1## if ##\phi_x(x)## is well-defined (returns a value).
(b) We return ##h(x)## as undefined if ##\phi_x(x)## is undefined.The resulting function ##h## will have following properties:
(1) It will be undefined on some inputs. That is, it will not be total.
(2) The resulting function will be a "partial computable function".Here one thing to is that the set ##\{Halt(x,x)| x \in \mathbb{N}\}## is not a computable set. Since the set is c.e. (computably enumerable) but not computable, it can be shown without much difficulty that it can't be a co-c.e. set [because a set which is c.e. and co-c.e. at the same time must be computable]. So we can't (computationally) hope to "identify" those points where the function ##h## is undefined [in hope of diagonalizing them].

Last edited:
There is something that came to my mind (and I have noticed it for first time). Perhaps someone else may also find it interesting. It can be thought of as a comment to first paragraph from post#48.

I noticed that we can use the function ##h:\mathbb{N} \rightarrow \mathbb{N}## in last post [defined as ##h(x)=\phi_x(x)+1##] can be used with one basic modification to show the following (essentially via diagonalization and simulating other programs):
(a) The function from ##\mathbb{N}## to ##\mathbb{N}## that maps ##x## to ##Halt(x,x)## can't be a total computable function.
(b) From (a) we can easily infer that the function ##Halt:\mathbb{N}^2 \rightarrow \{0,1\}## can't be a total computable function.This method via diagonalization (very similar to cantor's theorem) is almost certainly very well-known (but I haven't read it before or seen it mentioned).

Last edited:
PeterDonis said:
It's not just that you could; it's that any implementation of F3 must be logically equivalent to the one using H1 that I wrote. And that means that if H1 does not exist, F3 cannot exist either.
Since this is a correct implementation of F3, all other correct implementations of F3 must be logically equivalent to this one.

All correct implementations of F3 must be also logically equivalent to implementations of F3 that use functions that can be "simplified out" from there.
All correct implementations of F3 must be also logically equivalent to this implementation:
Python:
def F3(x1, x2):
if 2+2==3:
return unneeded_function(0)
if x1 == x2:
return False
else:
return H1(x1, x2)
but unneeded_function can be simplified out from this definition.

But how does this prove that an implementation of F3 that does not use H1 can not exist? How does this prove that if H1 does not exist, F3 cannot exist either?

Last edited:
olgerm said:
But how does this prove that an implementation of F3 that does not use H1 can not exist?

We already have a proof that F3 cannot exist that is independent of its implementation:

pbuk said:
Consider the following subprogram:

pseudocode:
def A(x):
if F3(A, x):
while True:
pass
return x

If F3(A, 1) returns True then it has determined that A(1) halts, however if F3(A, 1) is True then A(1) enters an infinite loop, a contradiction.

On the other hand if F3(A, 1) returns False then it has determined that A(1) does not halt, however if F3(A, 1) is False then A(1) halts returning 1, a contradiction.

olgerm
One of the direct reasons why ##F_3:\mathbb{N}^2 \rightarrow \{0,1\}## is not computable is because we have:
##Halt \leq_T F_3##
Here ##\leq_T## is the notion of "turing reducibility". This is what is shown in post#8.

What the above inequality (and post#8) implies, in more direct wording, is that ##F_3:\mathbb{N}^2 \rightarrow \{0,1\}## can't be computable. Let's suppose ##F_3## was computable. Then, by definition, it means that we have a program to compute ##F_3##. And it can be shown (as in post#8) that if we had a program to compute ##F_3## then we would also have a program to compute ##Halt:\mathbb{N}^2 \rightarrow \{0,1\}##. That would imply that ##Halt## is computable, which we already know to be false. Hence our original assumption of ##F_3## being computable must be incorrect.
Edit:
I removed my comment about the idea in previous post being accurate [as an argument that shows ##F_3## is not computable]. Not because I think it is inaccurate (my guess is that it is quite likely to be accurate). But rather because, after some more thought, there are certain aspects that seem somewhat more subtle to me (and I can't fully justify using my personal knowledge, understanding etc.).

However, it seems to me that such concerns might be addressed by recursion theorem [though this is still a guess....]. However, my understanding of that theorem is quite weak. Or maybe I am missing out on something simpler. I don't know for sure yet.

In the case that such concerns can be addressed [and my feeling is that they can .... but I am having some difficulty doing it based on my current understanding/knowledge], then my comments in post#23 would probably apply.

Last edited:
Perhaps I should mention that a similar method to one in post#51 [that can be used to show that ##x \mapsto Halt(x,x)## is non-computable] can also be used to show that ##F_3:\mathbb{N}^2 \rightarrow \{0,1\}## is not computable. I will describe a brief sketch.

We write ##\phi_x(y)## to describe the output of the program of index ##x## when given the input ##y##. If the program doesn't halt on given input then ##\phi_x(y)## is undefined. Now we construct a function ##f(x):\mathbb{N}^2 \rightarrow \{0,1\}## as follows:
If ##x=0## then we set ##f(x)=0##. If ##x \geq 1## then we define:
##f(x)=\phi_{pre(x)}(x)+1## --- if ##F_3(pre(x),x)=1##
##f(x)=0## --- if ##F_3(pre(x),x)=0##
Above ##pre(x)## is subtraction by ##1## function for natural numbers (returning ##0## on input ##0##).

Note that the function ##f## is total (same with ##F_3##). Now if ##F_3## was computable then it would mean that there exists a program to compute it. However, if that was the case then there would also be a program to compute the above function ##f##. That would mean that ##f## is a total computable function. However, by its construction, the function ##f## is different from every (total) computable function. Therefore we conclude that our assumption of ##F_3## being computable was wrong.

==========================

Edit:

The above might be a bit difficult to follow if one hasn't seen the sketch for showing that the function, say ##K:\mathbb{N} \rightarrow \{0,1\}##, defined as ##x \mapsto Halt(x,x)## is non-computable using the same method as above.

In that case, we construct the function ##f:\mathbb{N} \rightarrow \{0,1\}## [used for showing that ##K:\mathbb{N} \rightarrow \{0,1\}## is not computable] as follows:
##f(x)=\phi_x(x)+1## --- if ##K(x)=1##
##f(x)=0## --- if ##K(x)=0##
Note that the specific value of ##f## that we have set as ##0## in second line of definition isn't particularly important. We could have set the value to ##1##, ##100##, ##20## etc. and it would make no difference.

Now we can use the similar reasoning as above (in the last paragraph of first half of the post) to conclude that ##K:\mathbb{N} \rightarrow \{0,1\}## isn't computable.

Last edited:

• Set Theory, Logic, Probability, Statistics
Replies
16
Views
2K
• Set Theory, Logic, Probability, Statistics
Replies
15
Views
4K
• Computing and Technology
Replies
9
Views
2K
• Set Theory, Logic, Probability, Statistics
Replies
16
Views
2K
• Engineering and Comp Sci Homework Help
Replies
6
Views
2K
• Set Theory, Logic, Probability, Statistics
Replies
3
Views
796
• Programming and Computer Science
Replies
26
Views
2K
• Programming and Computer Science
Replies
1
Views
1K
• Set Theory, Logic, Probability, Statistics
Replies
6
Views
2K
• Differential Geometry
Replies
9
Views
582