Reference for a proof of the recursion theorem, for a general case.

502 Views Asked by At

Herbert Enderton in his A Mathematical Introduction to Logic 2nd edition, proves a theorem (a "recursion theorem") in section 1.4, p. 39.

Using his example, the idea is the following: We have some set $C \subseteq U $ generated "recursively" from some subset $B\subseteq C$, using some functions: $\ f:U\times U\rightarrow U\ $and $\ g:U\rightarrow U\ $ (in this case meaning simply that $C$ is closed under $f$ and $g$).

(For example $C$ might be the set of formulas of propositional logic generated from $B$, the atomic formulas, using formula building operations $f$, $g$, etc.)

The theorem shows that when a function $\ \bar{h} :C\rightarrow V\ $ is defined (here $V$ is just some set), using functions
$h:B\rightarrow V\ $
$ F:V\times V\rightarrow V\ $
$ G:V\rightarrow V\ $

so that:
(i) For $x$ in $B$: $\ \bar{h}(x)=h(x)$
(ii)For $x, y$ in $C$:
$ \bar{h}(f(x,y))=F(\bar{h}(x),\bar{h}(y))$
$ \bar{h}(g(x))=G(\bar{h}(x))$

then under certain condition (i.e. when: $f$ and $g$ are one-to-one, and when their ranges and $B$ are pairwise disjoint), there exists a unique such function $\bar{h}$ on $C$ meeting the given requirements (i)&(ii) (see p. 39 for a precise statement of the theorem).

(So for example $\bar{h}$ might be a truth assignment function for the formulas of propositional logic.)

As Enderton himself implies, the theorem would hold if instead of $f$ and $g$, we would have some functions $f_{1},f_{2},..,f_{n}$ and corresponding rules for $\bar{h}$. But he only proves the theorem for the special case mentioned here.

My question is: Does the theorem generalize to a case where $C$ is generated by a countably infinite set of functions $f_{1},f_{2},...$ , and so we also have infinitely many rules for computing $\bar{h}$ ?

I assume it does generalize, but I'm looking for a reference. Does anyone have a reference where the general case is proved?

1

There are 1 best solutions below

2
On

This is a bit of a hack, but you might reinterpret the many functions $f_i:U\times U\to U$ as a single function $f:\omega\times U\times \omega\times U\to \{i\}\times U$, and correspondingly the many rules $h_i$ on $U$ as a single rule on $\omega\times U$.