On the Foundation of Computer Science

On the Foundation of Computer Science

[Patrik Eklund]

Dear All,

For quite a while I've been puzzled by some Turing constructions, and I
don't know if I am puzzled rightfully so, and therefore I would
appreciate comments, so that, if I am indeed wrongfully so, I could
happily sit down corrected.

---

In his "Computability and ??-Definability", The Journal of Symbolic
Logic, Vol. 2, No. 4 (Dec., 1937), pp. 153-163,
https://www.jstor.org/stable/2268280?seq=1, Turing defines f using ??
(xi) on p. 161, and then says "it can easily be brought into ..."
involving

    ??y in ??y[i(x,y)=0]

My problem is understanding how Turing possibly uses a 'powertype' which
is, as far as I can see, not explicitly introduced in his machinery.

We clearly have

    e : nat -> nat

and

    i : nat x nat -> nat

as defined in footnote 8 on p. 161.

As far as I can see, ??y[i(x,y)=0], can be denoted as g(x) where

    g : nat -> nat

so

    g(_) = ??y[i(_,y)=0]

Whereas nat, as a type, is used within the system, the use of the
powertype Pnat is not similarly recognized. Indeed, the powertype
constructor P is not defined, and, as far as I can see, not even
considered to be defined.

Anyway, let me proceed by using that powertype, thereby, in this
posting, using the powertype constructor informally.

If

    h(x) = {y | i(x,y) = 0}

we have

    h : nat -> Pnat

Infimum, inf, of a set (of natural numbers) A, written inf A, means we
could write

    inf : Pnat -> nat

This would mean that

    g = inf o h

I'm not saying that Turing says he has

    ?? : Pnat -> nat

but ?? in his paper is used as kind of a "partial operator" from Pnat to
nat, whereas, in comparison, inf is a "total operator".

Turing's construction indeed does not explicitly recognize the use of
the powertype Pnat, and, in particular, does not explicitly recognize
that the informal symbol ?? is used like a "partial operator over a
non-recognized and undefined powertype".

---

My general question is:

    Is this a problem?

In Turing's paper it is taken to be OK to use g as an operator from nat
to nat, even if it is composed using bits and pieces that are "brought
in from the outside", like the powertype constructor P.

---

My confusion may indeed come from my desire to understand the underlying
signatures, to understand syntax before semantics. The natural number
signature is in there, with the constant operator 0 : -> nat, and the
successor S : nat -> nat. And indeed, additionally, Turing seems to use
the powertype Pnat, and operators working over this powertype, but my
primitive question is then:

    Where does P come from? Is there a signature where it resides?

---

My question relates perhaps also more generally to foundations.

Best,

Patrik


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]