Recursive definition of relations (or predicates, or how we want to call them)

Question

I think I have found a subject that is not 100% covered by the literature. When talking about first-order logic, the textbooks give a definition of what it means for a term to be free for (or substitutable for) a variable. Normally, they take a formula $\varphi$, and they say that if $\varphi$ is atomic, then $t$ is free for $x$. Then, they provide a recursive definition by defining what happens when $\varphi$ is $(\neg \psi)$ and so on. At first sight, it looks like the recursion theorem was used and some textbooks even say that explicitly, but there's a catch. The recursion theorem is used to define functions, while the aforementioned definition defines a predicate: the property of $\alpha$ whereby "$t$ is free for $x$ in it". Does this make sense or am I missing something? What could be a way of providing a background for defining predicates (or perhaps I should say "relations") recursively?

Answer 1

The standard approach is to represent a predicate $\phi(x)$ by a function $f(x)$ such that $\phi(x)$ holds iff $f(x) = 0$ (or $1$ or any other fixed natural number).