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.)