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:

Excerpt from Turing's "On Computable Numbers with an Application to the Entscheidungsproblem" where he defines a formula U that defines the sequence alpha generated by the function G(x), where x is a non-negative integer

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:

Excerpt from Turing's "On Computable Numbers with an Application to the Entscheidungsproblem" where he explained what he means by the formula U defining the sequence alpha

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?

Another, possibly incorrect, formulation of the above implications

Sorry if I am overlooking something here.

Edit 1:

Here are the footnotes:

The footnotes refereed to in the excerpts attached above

  • $\begingroup$ Regarding notation, we can use MathJax on this site. I've submitted an edit that makes use of it. $\endgroup$ Jun 22, 2020 at 15:22
  • $\begingroup$ @user34258 Perfect! Thank you for that $\endgroup$
    – Wololo
    Jun 22, 2020 at 15:24

1 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$

  • $\begingroup$ Thank you for your detailed answer, and the examples. By "extend[ing] the language of first-order Peano arithmetic with a unary predicate $G$" do you mean we add $G$ as the 10th axiom to it? Also, I cannot quite understand the definition of $\alpha$. It is 1 "if Peano axioms prove $\mathfrak{U}(\overline{n}) \Rightarrow G(\overline{n})$", but since $\mathfrak{U}$ is already constructed from (the extended) Peano axioms, shouldn't it always be provable using the Peano axioms. Sorry I only have a very basic & informal introduction to Logic (and that from Charles Petzold's The Annotated Turing) $\endgroup$
    – Wololo
    Jun 22, 2020 at 20:53
  • $\begingroup$ A formal system has some symbols and relations. Peano arithmetic has symbols $0$, $S$, $+$ and $\times$. We add to it another symbol $G$. So this is not about axioms, but about what symbols we may use. $\endgroup$ Jun 22, 2020 at 22:24
  • $\begingroup$ $\mathfrak{U}$ is not "constructed from Peano axioms". It is constructed using the symbols of the language ($0$, $S$, $+$, $\times$=, $G$, $=$ and all of first-order logic). The Peano axioms may be used to prove or disprove $\mathfrak{U}$. $\endgroup$ Jun 22, 2020 at 22:26
  • $\begingroup$ For instance, $\mathfrak{U}$ could be the formula $S(S(x)) + S(0) = x + x \Rightarrow G(x + S(0))$. It is constructed from the symbols of Peano arithmetic, $G$ and logical operators. Simply constructing or "writing down" a formula has nothing to do with axioms. The axioms become important when we try to prove or disprove the formula. $\endgroup$ Jun 22, 2020 at 22:28
  • $\begingroup$ Ah, I see! Perfectly makes sense now. Thank you very much! $\endgroup$
    – Wololo
    Jun 23, 2020 at 19:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.