Before I start - I want to say sorry if this has been asked before, I have searched about for a question like this, but haven't been able to find what I am looking for.
To begin, there are a number of (only slightly) different definitions of what a computable function is, so for completeness the definition I am going to be using is:
- A computable function is a function $f \colon \mathbb{N} \to \mathbb{N}$, such that there exists an effective procedure $p$ where for all $n \in \mathbb{N}$ - if $p$ is given $n$ as input, then $p$ outputs $f(n)$.
I am only just starting to learn about computability as a hobby, so I am unsure if my definition of a computable function even makes sense (if not, please tell me why it doesn't work). Although I am not sure exactly how an effective procedure rigorously works, I understand the intuitive idea of what one does.
Moving on, if $g$ is any computable function then clearly $g \subseteq \mathbb{N} \times \mathbb{N}$ and so I feel I should be able to construct the set of computable functions using the power set axiom and the axiom scheme of separation as $C = \{x \in P(\mathbb{N} \times \mathbb{N}) : ``x$ is a computable function$" \}$. But my question is how exactly do I formulate $``x$ is a computable function$"$ as a logical formula? In other words, how do I show that $ZF \models \exists C$?
(As an extra question, I have been wondering if there is a nice way to make the notion of an effective procedure and the process of giving an output for a given input more rigorous - in the sense of defining them in terms of mathematical logic? I assume these two questions are linked, which is why I ask.)
Thank you in advance, and sorry if I sound like a dumbass - I'm new to computation.
Once you formulated the notion of being a computable function in the language of set theory, the set of all computable functions automatically exists, by the very fact that $\sf ZF$ proves that the set of all partial functions $f\colon\Bbb N\to\Bbb N$ exists, and therefore by Separation the set of computable functions exist.
Now, to formulate "$f$ is a computable function" in $\sf ZF$ you need to understand that you first need to formalize arithmetic, and then choose one of the many paths you can choose for defining "computable". This is a tedious task, which can be circumvented if one understand the basic principle of foundations of mathematics using set theory: If we can write in, we can write it in the language of set theory.
You need to break down the definition of a "computable function", and then show that each step along the way can be translated into $\{\in\}$, which means that the entire thing can also be translated.