I have a question on Alan Turing's Dissertation Systems of Logic Based on Ordinals, a scanned copy you can find here, or rewritten in LaTeX here, and also a copy of the published version here (but in section 3 I found some errors not present in the original scan, so maybe the original one is preferable).
The unclear paragraph comes quite early at the end of section two. After the abstract, introducing the $\lambda$ calculus and what it means for a function to be "effective calculable" he writes:
Those computable functions which take only the values $0$ and $1$ are of particular importance, since they determine and are determined by computable properties, as may be seen by replacing "0" and "1" by "true" and "false". But, besides this type of property, we may have to consider a different type, which is, roughly speaking, less constructive than the computable properties, but more so than the general predicates of classical mathematics. Suppose that we have a computable function of the natural numbers taking natural numbers as values, then corresponding to this function there is the property of being a value of the function. Such a property we shall describe as "axiomatic"; the reason for using this term is that it is possible to define such a property by giving a set of axioms, the property to hold for a given argument if and only if it is possible to deduce that it holds from the axioms. Axiomatic properties may also be characterized in this way. A property $\psi$ of positive integers, such that $\psi(x)$ is true if and only if there is a positive integer $y$ such that $\psi(x,y)$ is true. Or again $\psi$ is axiomatic if and only if there is a W.F.F F such that $\psi(n)$ is true if and only if F(n) conv 2.
I do not understand what he wants to say here. My ideas are, that with computable functions he always means total computable functions (otherwise the term property would not make much sense, and how I interpret the statemets). So, a property $\psi(x)$ is axiomatic if there exists some total computable function $f : \mathbb N \to \mathbb N$ such that $\psi(x)$ holds iff $x \in f(\mathbb N)$. So as $f$ is computable, it is given by some set of recursive equations (the axioms), and by totality we can successively "derive" the equations $f(1) = ..., f(2) = ..., f(3) = ...$ and so on, and if we find some equation of the form $f(k) = x$ we know that $\psi(x)$ is true, and if not than we will not find such an equation (or a "proof" of this equation).
But now to his other characterisation: A property $\psi$ is axiomatic iff there is a computable property $\phi$ of two positive integers, such that $\psi(x)$ is true if and only if there is a positive integer $y$ such that $\phi(x,y)$ is true. For one direction, I guess what he means is the property that $\phi(x,y)$ is true iff $f(x) = y$, and this surely is computable if $f$ is computable. But just given such a property, how can $f : \mathbb N \to \mathbb N$ look like? Maybe he meant partial computable functions, then for each $x$ we can search for an $y$ which makes $\phi(x,y)$ true, and take some as an image, but then my first interpretation would not make any sense...
So, could someone explain what Turing meant here?