Clarification on halting predicate computability

I am tackling the halting problem right now and its remarkable theorem. My book states $\text{HALT}(x,y)$ is true if $\psi^{(1)}_{\mathcal P}$ is defined and conversely $\text{HALT}(x,y)$ is false if $\psi^{(1)}_{\mathcal P}$ is undefined.

The purpose of the theorem, of course, is showing that $\text{HALT}(x,y)$ is a not computable predicate. I will report the extract of the proof given:

Suppose $\text{HALT}(x,y)$ were computable. Then we could construct the program $\mathcal P$:

$$[A]\;\;\;\;\;\text{IF HALT}(X,X)\text{ GOTO } A$$

It is quite clear that $\mathcal P$ has been constructed so that

\begin{equation}
\psi^{(1)}_{\mathcal P}=
\begin{cases}
\text{undefined} \;\;\; \text{if HALT}(x,x) \\
0 \;\;\;\;\;\;\;\;\;\;\;\;\;\;\text{if ~HALT}(x,x)
\end{cases}
\end{equation}

I don't understand how $\psi^{(1)}_{\mathcal P}$ is undefined if $\text{HALT}(x,x)$ is true, shouldn't $Y$ be equal to $0$ by default and moreover how could a non-terminating program be defined can have $0$ as output value. What am I missing here?

Edit: $\psi^{(1)}_{\mathcal P}(x)$ is the value of the output variable $Y$ at the terminal snapshot.

Let's walk through the proof given by [Davis94]. I am familiar with this text and have it in front of me. The HALT predicate is defined:

$$
HALT(x,y) \Longleftrightarrow \text{program number $y$ eventually halts on input $x$.}
$$

Given this defintion of HALT, don't worry about how such a program would be defined. It is not important. Just assume that HALT exists, that it works, and that this is what it does: It uses $y$ (a Gödel number -- see Section 8 of Ch. 3) which represents a particular program, and $x$, an input to that program, and tells us if that program halts when it is run with that input. It can do this for any program, with any input.

Now, let's define a new program called $P$:

$$
[A]~\text{IF}~HALT(X,X)~\text{GOTO A}
$$

Look at how we are using HALT here: we are asking "Does program X halt when given an input of X (itself)?" And if it does halt, we loop infinitely -- creating a program that does not terminate -- a program that does not halt. In other words:

$$
\psi_P^{(1)}(x) =
\begin{cases}
\text{undefined} & \text{if} & ~~~~HALT(x,x) \\
0 & \text{if} & \sim HALT(x,x)
\end{cases}
$$

Let's pause and answer your first question about $\psi_P^{(m)}$ being undefined: this is part of the definition given in Section 4 of Chapter 2: $\psi_P^{(m)}(r_1,...,r_m)$ is undefined if $P$ never terminates. And our program never terminates when $HALT(x,x)$ is true because we have written it that way, it loops infinitely. As to your second question about the default output of 0: this happens when the program $P$ does terminate.

Now let the Gödel number of our new program $P$ be $y_0$. This means that

$$
HALT(x,y_0) \Longleftrightarrow ~ \sim HALT(x,x).
$$

(we are taking the left side from the definition of HALT and the right side from our program $P$). Since this is true for any input $x$ we could also write:

$$
HALT(y_0,y_0) \Longleftrightarrow ~ \sim HALT(y_0,y_0),
$$

which is clearly a contradiction; HALT cannot exist.

StackExchange Computer Science Q#9040, answer score: 5