Substitution of Arithmetically Definable Functions is Arithmetically Definable

Theorem

Let $f: \N^t \to \N$ and $g_1, g_2, \dotsc, g_t: \N^k \to \N$ be partial functions.

Let $h: \N^k \to \N$ be defined by substitution as:

$\map h {x_1, \dotsc, x_k} \approx \map f {\map {g_1} {x_1, \dotsc, x_k}, \dotsc, \map {g_t} {x_1, \dotsc, x_k} }$

Suppose that there exists a $\Sigma_1$ WFF of $t + 1$ free variables:

$\map {\phi_f} {y, x_1, \dotsc, x_t}$

such that:

$y = \map f {x_1, \dotsc, x_t} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_t} }$

where $\sqbrk a$ denotes the unary representation of $a \in \N$.

Suppose also that there exist $\Sigma_1$ WFFs of $k + 1$ free variables:

$\map {\phi_{g_1} } {y, x_1, \dotsc, x_k}$

$\dots$

$\map {\phi_{g_t} } {y, x_1, \dotsc, x_k}$

such that:

$y = \map {g_i} {x_1, \dotsc, x_k} \iff \N \models \map {\phi_{g_i} } {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$

for each $1 \le i \le t$.

Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:

$\map {\phi_h} {y, x_1, \dotsc, x_k}$

such that:

$y = \map h {x_1, \dotsc, x_k} \iff \N \models \map {\phi_h} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$

Proof

Define:

$\map {\phi_h} {y, x_1, \dotsc, x_k} := \exists s_1: \dotsm \exists s_t: \map {\phi_f} {y, s_1, \dotsc, s_t} \land \map {\phi_{g_1} } {s_1, x_1, \dotsc, x_k} \land \dotso \land \map {\phi_{g_t} } {s_t, x_1, \dotsc, x_k}$

Correctness is apparent.

A particular theorem is missing. In particular: $\paren {\exists x: \map \phi x} \land \psi \vdash \exists x: \paren {\map \phi x \land \psi}$ You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding the theorem. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{TheoremWanted}} from the code.

That $\phi_h$ is $\Sigma_1$ follows from Conjunction of Existential Quantifier.

$\blacksquare$