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/ ]