3
$\begingroup$

Recursion Theorem:

Let $A$ be a set, $a\in A$, and $f \colon A\to A$ a mapping. Then there exists a unique mapping $g \colon \Bbb N\to A$ such that

1. $g(0)=a$

2. $g(n+1)=f(g(n))$

I formalize a proof based on the comments of Noah Schweber at here and here .

Fix $a\in A$. Let $Y=\{(n,x)\in\mathbb{N}\times A\mid \text{ there exist a sequence of length}$ $n$, in which first term is $a$, last term is $x$, and each term after the first is $f$ of the previous term$\}$.

Now we prove by induction: for each $n\in \mathbb{N}$, there exists a unique $y\in A$ such that $(n,y)\in\mathbb{N}\times A$.

For $n=0\implies$ only $y=a$ such that $(0,a)\in Y$. Assume that for $n=k$ there exists a unique $y\in A$ such that $(k,y)\in Y\implies$ for $n=k+1$, there exits a unique $f(y)$ such that $(k+1,f(y))\in Y$.

$\implies$ For all $n\in \mathbb{N}$, there exists a unique $y\in A$ such that $(n,y)\in Y$

$\implies$ Set $Y$ defines a function $g \colon \Bbb N\to A$ such that

1. $g(0)=a$

2. $g(n+1)=f(g(n))$

Please check my proof above! Many thanks!

$\endgroup$
6
  • $\begingroup$ Seems perfectly fine to me. You may note that not only does $Y$ define a function $g$ -- it is exactly this function (or the graph thereof -- depending on your definition of 'function'). $\endgroup$ Feb 24, 2018 at 10:08
  • $\begingroup$ Hi @StefanMesken, how do we know that "there exist a sequence of length $n$, in which first term is $a$, last term is $x$, and each term after the first is $f$ of the previous term" is a well-defined statement under Zermelo–Fraenkel set theory? $\endgroup$
    – Akira
    Feb 24, 2018 at 10:17
  • $\begingroup$ You can formalize it as follows: $\exists s \subseteq \mathbb N \times A \wedge \forall n \in \mathrm{dom}(s) \exists ! a \in A \colon (n,s) \in s \wedge 0 \in \mathrm{dom}(s) \wedge (0,a) \in s \wedge \forall n \in \mathrm{dom}(s) \forall m < n \colon m \in \mathrm{dom}(s) \wedge n + 1 \in \mathrm{dom}(s) \implies (n+1, f(s(n)) \in s \wedge \neg \exists n < m (m \in \mathrm{dom}(s) \implies s(n) = x)$. $\endgroup$ Feb 24, 2018 at 10:27
  • 2
    $\begingroup$ Mind you that I don't encourage you to use the formalization. You should aim to become sufficiently comfortable with these notions that you know how to formalize it without the need of actually doing it. Overly formalized mathematics is almost always a disservice to both the author and the reader. $\endgroup$ Feb 24, 2018 at 10:28
  • $\begingroup$ Your formalization seems to confuse me: for all $(n,x)$, $n$ is the length of the sequence $s\implies n$ is the fixed number. But the way you used $n$ in the expressions makes me feel like $n$ is a free variable. Please explain the meaning of $\neg \exists n < m (m \in \mathrm{dom}(s) \implies s(n) = x$ ! Furthermore, I think you meant $(n,a)\in s$, not $(n,s)\in s$. $\endgroup$
    – Akira
    Feb 26, 2018 at 3:17

0

You must log in to answer this question.