Confusion in Turings proof of the undecidability of the Entscheidungsproblem

Question

I was reading Turing's paper on computable numbers and the Entscheidungsproblem. There is this part of Section 9, Part II that I cannot quite seem to understand. He says:

It is pretty straight forward until the part where he introduces $\mathfrak{U}$. So $\mathfrak{U}$, he says, includes the Peano axioms; but what else does it include? I guess it includes the axioms for $G(x)$ as well, because only then would $\mathfrak{U}$ be able to "define" the sequence $\alpha$ that is being computed by $G(x)$. I am taking the word "define" here in its usual sense, but Turing explains what he means by "$\mathfrak{U}$ defining $\alpha$" as:

So for $\mathfrak{U}$ to define $\alpha$, $-\mathfrak{U}$ must not be provable? I am not sure why that is required? Because by restricting that $-\mathfrak{U}$ must not be provable we are saying that $\mathfrak{U}$ must not be refutable, which means that the sequence $\alpha$ cannot be all 0's (or so I think). But why would we want $\alpha$ to not be all 0's?

I am also confused about the two formulas ($A_n$ and $B_n$) he has written above. I am not sure why if has included the $F^{(n)}$ part. If $x$ satisfies the Peano axioms and the axioms of $G(x)$, then $U$ being a conjection of all these axioms is given to be TRUE, and if $x$ does not satisfy these axioms then $\mathfrak{U}$ is obviously FALSE. So, just based on $\mathfrak{U}$ we can tell whether $A_n$ is TRUE or $B_n$. So what is the point of $F^{(n)}$ here? I think the following set of implications say pretty much the same thing as what Turing has?

Sorry if I am overlooking something here.

Edit 1:

Here are the footnotes:

Answer 1

The transliteration of the passage into modern langauge would go as follows.

We extend the language of first-order Peano arithmetic with a unary predicate $G$ (and no axioms for $G$). For a number $n \in \mathbb{N}$, let $\overline{n}$ be the numeral $$\underbrace{S(S(\cdots S}_{n}(0)))$$ where $S$ is the successor symbol. For example, $\overline{3} = S(S(S(0))$.

Consider a formula $\mathfrak{U}(x)$ written in this language, whose only free variable is $x$ such that, for every $n \in \mathbb{N}$:

1. Peano axioms prove $\mathfrak{U}(\overline{n}) \Rightarrow G(\overline{n})$, or
2. Peano axioms prove $\mathfrak{U}(\overline{n}) \Rightarrow \lnot G(\overline{n})$.
3. Peano axioms do not prove $\lnot \mathfrak{U}(\overline{n})$.

Define $\alpha : \mathbb{N} \to \{0,1\}$ by $$\alpha(n) = \begin{cases} 1 & \text{if Peano axioms prove $\mathfrak{U}(\overline{n}) \Rightarrow G(\overline{n})$},\\ 0 & \text{if Peano axioms prove $\mathfrak{U}(\overline{n}) \Rightarrow \lnot G(\overline{n})$.} \end{cases} $$ We say that $\mathfrak{U}$ defines the sequence $\alpha$.

Intuitively, we think of $G(x)$ as stating "the $x$-th digit of $\alpha$ is $1$", and of $\lnot G(x)$ as stating "the $x$-th digits of $\alpha$ is $0$".

The first and second condition on $\mathfrak{U}$ ensure that $\mathfrak{U}$ always assigns $\alpha(n)$ the value $0$ or the value $1$.

The third condition ensures that $\mathfrak{U}$ never assigns both $0$ and $1$ to $\alpha(n)$ (because it follows from the first two conditions that $\lnot \mathfrak{U}(\overline{n})$ is equiprovable with $G(\overline{n}) \land \lnot G(\overline{n})$).

Example: The formula $G(x)$ defines the sequence $1, 1, 1, 1, 1, \ldots$.

Example: The formula $G(S(x))$ does not define a sequence because $G(S(0)))$ does not imply $G(0)$ and it does not imply $\lnot G(0)$. (Remember that $G$ is a primitive symbol and that we have no axioms about it.)

Example: The formula $G(0) \land \forall x \,.\, \lnot G(S(x))$ defines the sequence $1, 0, 0, 0, 0, \ldots$

Example: The formula $x \neq 0 \land \Rightarrow G(x)$ does not define the sequence because Peano axioms prove $\lnot (0 \neq 0 \land G(0)$, thus the third condition is violated. If we tried to use this formula to define a sequence, it would assign $0$ and $1$ to $\alpha(0)$ (and it would assign $1$ to all other terms of $\alpha$).

Example: The formula $G(0) \land \lnot G(S(0)) \land \forall x . G(S(S(x)))$ defines the sequence $1, 0, 1, 1, 1, 1, \ldots$

Example: The formula $$((\exists y . x = 2 \cdot y) \Rightarrow G(x)) \land ((\exists y . x = S(2 \cdot y)) \Rightarrow \lnot G(x)) $$ defines the sequence $0, 1, 0, 1, 0, 1, \ldots$