# Is this proof of existence and uniqueness of recursive functions in ZF using recursive predicates valid?

$$\newcommand{\N}{\mathbb{N}}$$ $$\newcommand{\pp}{\texttt{++}}$$ $$\newcommand{\set}[1]{\{#1\}}$$ $$\newcommand{\tand}{\text{ and }}$$ $$\newcommand{\tor}{\text{ or }}$$ In Terrence Tao's analysis, he describes the Peano axioms and then then axioms of ZF set theory, and then gives the reader the following definition of a function:

Let $$X,Y$$ be sets, and let $$P(x,y)$$ be a property pertaining to an object $$x \in X$$ and an object $$y \in Y$$ , such that for every $$x \in X$$, there is exactly one $$y \in Y$$ for which $$P(x,y)$$ is true (this is sometimes known as the vertical line test). Then we define the function $$f : X \to Y$$ defined by $$P$$ on the domain $$X$$ and range $$Y$$ to be the object which, given any input $$x \in X$$, assigns an output $$f(x) \in Y$$, defined to be the unique object $$f(x)$$ for which $$P(x,f(x))$$ is true. Thus, for any $$x \in X$$ and $$y\in Y$$,

$$y=f(x) \iff P(x,y)\text{ is true}.$$

Later, after defining the Cartesian product, he gives the following exercise

Let $$f : \N \times \N \to \N$$ be a function, and let $$c$$ be a natural number. Show that there exists a function $$a : \N \to \N$$ such that

$$a(0) = c$$

and

$$a(n\pp) = f(n, a(n))\text{ for all }n \in \N$$

and furthermore that this function is unique.

I believe I was able to prove this in the way that he had in mind, by showing that, for all $$N \in \N$$, there exists a function $$a_N(n)$$ that has the desired properties for $$n < N$$

However, I also came up with another proof that uses the definition Tao gave more directly.

Let $$P(x, y) := (x = 0 \tand y = c) \tor (x = n\pp \tand \exists u, y = f(n, u) \tand P(n, u) )$$. We will show that, by induction on $$x$$, for every $$x \in \N$$ there is exactly one $$y \in \N$$ such that $$P( x, y)$$ is true.

First the base case. Let $$x = 0$$, and let $$y = c$$, then $$P(x, y)$$ is trivially true. Now suppose that $$x = 0$$ and $$y \neq c$$, then $$(x = 0 \tand y = c)$$ is false, and $$x = n\pp \tand y = f(n, a(n))$$ is false since there exists no $$n$$ such that $$0 = n\pp$$ by Axiom 2.3 in the book (0 is not the successor of any natural number). Therefore $$P(x, y)$$ is false if $$x = 0$$ and $$y \neq c$$, so $$y$$ is unique for $$x = 0$$.

Now suppose that, for some $$x$$, there is exactly one $$y$$ such that $$P(x, y)$$. Then let $$y' = f(x, y)$$ (this exists since $$f$$ exists by assumption) and $$x' = x\pp$$. Then $$P(x', y')$$ is true, since $$(x' = x\pp \tand y' = f(x, y) \tand P(x, y))$$ is true, and by the induction hypothesis, $$y$$ is the only $$y$$ such that $$P(x, y)$$ is true for that $$x$$.

To show that $$y'$$ is unique, assume that $$y' \neq f(x, y)$$; and assume for contradiction that $$P(x', y')$$ is true. Since $$x' \neq 0$$ by Axiom 2.3, we have $$(x' = n\pp \tand \exists u, y' = f(n, u) \tand P(n, u)$$. We have $$x' = x\pp$$, so $$y' = f(x, y)$$. But this is a contradiction, since we have assumed $$y' \neq f(x, y)$$. Therefore $$P(x', y')$$ is false if $$y' \neq f(x, y)$$, and so $$y'$$ is unique for $$x' = x\pp$$.

Since we have just shown that, for every $$x \in \N$$, there is exactly one $$y \in \N$$ such that $$P(x, y)$$ is true, we have by definition that there exists a function $$a : \N \to \N$$ such that $$a(x) = y$$ if and only if $$P(x, y)$$.

Let $$a$$ be the function given by $$P(x, y)$$ as defined above. Then $$a(0) = c$$, since we have shown that $$P(0, y) \implies y = c$$.

Furthermore, $$a(n\pp) = f(n, a(n))$$. This is because $$n\pp \neq 0$$, and so $$x = n\pp \tand \exists u, y = f(n, u) \tand P(n, u)$$ must be true. This implies $$P(n, u)$$, and so $$a(n) = u$$. Since also $$y = f(n, u)$$, we have $$y = f(n, a(n))$$.

So $$a$$ exists.

To prove uniqueness, assume that there exists an $$a$$ and $$a'$$ such that the definition is met. We will show by induction that $$a(n) = a'(n)$$ for all $$n$$.

If $$n = 0$$, then $$a'(0) = c = a(0)$$. Now assume $$a'(n) = a(n)$$ for some $$n$$, then $$a'(n\pp) = f(n, a'(n))$$ and by the induction hypothesis $$a'(n\pp) = f(n, a(n))$$. By definition, $$a(n\pp) = f(n, a(n))$$, so $$a'(n\pp) = a(n\pp)$$. So $$a'(n) = a(n)$$ for all $$n$$.

This second proof all depends on the predicate $$P(x, y)$$ being both well formed, and non circular. I am thinking that $$P(x, y)$$ is well formed, but that the proof is circular, however, I am not sure of either. Terrence Tao's book does not cover predicate logic in enough detail to decide (which feels kind of bad considering that functions are defined by them).

I am pretty sure that in type theory, the proof would be circular, but that the predicate would be well defined, because the predicate would itself be a function, and recursive functions do exist in type theory (I am not 100% positive about this though).

However, based on Tao's definition, a predicate is somehow separate from a function, so I am thinking that it's possible that the proof is non circular and that the predicate is well defined. However, I am not sure.

• @DerekElkins This isn't Tao's proof, this is mine. It was a typo, I fixed it in the edit. Sep 23, 2019 at 2:11

It is arguably a bit questionable to present a definition of $$P$$ in this manner, but there is a straightforward way to understand it that causes no issues. There are some minor issues with the proof and it's unnecessarily complicated, but the approach is fine.

Specifically, we assume $$P$$ is some binary predicate (i.e. add a binary predicate symbol to our theory called $$P$$) and the only thing we know about it is that the "definition" holds as an axiom (i.e. also add the "defining" equivalence as an axiom of our theory). This would be no different than how we handle any other predicate symbol, e.g. $$\in$$. However, what we don't get is any guarantee that this completely specifies the behavior of the predicate $$P$$. In particular, $$P$$ could fail to be eliminable, meaning that there is no set theoretic formula (not involving $$P$$) that is provably equivalent to $$P$$. This would be undesirable for many reasons but is not a problem in itself. (One undesirable property is without eliminability there is the possibility that the new axiom adds a contradiction.)

This turns out not to be an issue. First, the proof would go through even if we were just talking about some predicate that satisfied the given axiom. Second, the proof (more or less) shows that $$P$$ is eliminable. The proof shows that for all $$x\in\mathbb N$$, $$P(x,y)\iff y = a(x)$$ for a function $$a$$ which ultimately can be defined without reference to $$P$$. For $$x\notin\mathbb N$$, it's easy to see that $$P(x,y)$$ is false for any $$y$$, and this is implicit in the proof as well. Therefore, $$P$$ is, in fact, eliminable.

As you allude to, in many type theories, we would be able to directly define predicates (i.e. $$\mathsf{Prop}$$- or $$\mathcal U$$-valued functions) via recursion. This isn't possible (and doesn't really make sense) for first-order logic. What you can do, in the context of typical set theories, is define $$P(x,y)\equiv (x,y)\in X$$ and then define $$X$$ inductively, internally to the set theory. Indeed, this is what your proof is ultimately doing that implies the eliminability of $$P$$. It is showing that $$P(x,y)\iff (x,y)\in a$$ where $$a$$ is defined inductively.

It doesn't really make sense to talk about the proof being "circular" in type theory. The theorem and the proof are in a totally different language than type theory. It may still require work to show that a type-theoretic predicate $$\mathbb N \to \mathbb N \to \mathsf{Prop}$$ satisfying the analogues of being a total, functional relation gives rise to a function $$\mathbb N\to\mathbb N$$. It's possible that this isn't even true depending on exactly how it's stated and the exact details of the type theory.

• Thank you, just out of curiosity, since I am still learning how to do proofs correctly, what are the minor issues with the proof, and how is it unnecessarily complicated? (I think I know the answer to the second question, but I would like to verify). Sep 23, 2019 at 12:13
• Probably the biggest issue is the "so $a$ exists". We already know $a$ exists; you defined it a couple paragraphs before. What you mean is that the $a$ you defined satisfies the desired equations. Superficially similarly, there's no need (or point) to reminding us that $f$ exists. As for unnecessary things, the induction at the end is the most egregious. You can prove generically that the function induced by the total functional predicate is unique. The proof of this is simple and short and clearly can't rely on induction over the naturals. None of your uses of proof by contradiction... Sep 24, 2019 at 22:45
• ... are either necessary or helpful. For example, here's a direct proof that $y$ is uniquely determined when $P(0,y)$ holds. "Assume we have $y$ and $z$ such that $P(0,y)$ and $P(0,z)$ hold. Since $0\neq n++$ for any $n$, $P(0,y)\equiv y=c$. Therefore, $y=c=z$." This is overblown for an informal proof, though. Better would be: "Since $0\neq n++$ for any $n$, $P(0,y)$ simplifies to $y=c$ which clearly uniquely determines $y$." I would strongly recommend avoiding proof by contradiction (or equivalents) unless necessary or at least as a matter of last resort when you can't think of another way. Sep 24, 2019 at 22:45
• Just for completeness, here are two alternate, high-level approaches which are fundamentally different from each other. First, you could define a sequence of sets via $a_0=\{(0,c)\}$ and $a_{n\mathtt{++}}=\{(n\mathtt{++},f(n,u))\mid u\in a_n\}$. Then define $a=\bigcup_{n\in\mathbb N}a_n$. You can then use induction to prove that $a$ is a (set-theoretic) function which satisfies your desired equations. The other approach is to consider the $a$ in $\{g\in\mathcal P(\mathbb N\times\mathbb N)\mid(0,c)\in g\land\forall n\in\mathbb N.\forall y.(n,y)\in g\to(n\mathtt{++},f(n,y))\in g\}$. Sep 24, 2019 at 23:29
• This can be interpreted as $a$ being the intersection of the latter set. Both of these descriptions require showing the set is non-empty, but $g=\mathbb N\times\mathbb N$ shows that. You then need to establish that $a$ is a (set-theoretic) function $\mathbb N\to\mathbb N$. This approach is more or less the "rationalized" version of your approach. The above gives an explicit description of $a$, and we can then just choose $P(x,y)\equiv(x,y)\in a$ and go through your proof. Sep 24, 2019 at 23:29