2
$\begingroup$

I'm trying to get my head around page 252 of Turing's "On Computable Numbers [...]", specifically near the end of the page where he talks about -U (logical negation of U, the German blackletter U).

The relevant context:

[...]

Now let α be a sequence, and let us denote by Gα(x) the proposition "The x-th figure of α is 1", so that —Gα(x) means "The x-th figure of α is 0".

Suppose further that we can find a set of properties which define the sequence α and which can be expressed in terms of Gα(x) and of the propositional functions N(x) meaning "x is a non-negative integer" and F(x,y) meaning "y = x + 1".

When we join all these formulae together conjunctively, we shall have a formula, U say, which defines α.

The terms of U must include the necessary parts of the Peano axioms, viz.,

(Eu)N(u)&(x)(N(x)->(ey)F(x,y))&(F(x,y) -> N(y)),

which we will abbreviate to P.

When we say "U defines α", we mean that —U is not a provable formula, and also that, for each n, one of the following formulae (An) or (Bn) is provable.

U & F(n) -> Gα(u(n)), (An),

U & F(n) -> —Gα(u(n)), (Bn),

where F(n) stands for F(u,u') & F(u',u'') & ... F(u(n-1),u(n)).

[...]

I understand (mostly) the motivation of this part of the paper, but I'm not grasping yet the reason for specifically stating "we mean that —U is not a provable formula".

My question --

When Turing mentions —U above, is he stating something we already know (or will know soon) about U, and if so, how? Or is he stating a requirement for which U's we'll be considering, and if so, why is this requirement important? I'm at little lost here; maybe I'm missing something simple.

(I'm currently reading Petzold's "The Annotated Turing". This is on page 226.)

2 Answers 2