[proofplan] We prove the theorem by structural induction on the primitive recursive construction of $f$. The initial functions are represented directly by equality formulas. The composition clause is handled by existentially quantifying the intermediate values supplied by the representing formulas for the component functions. The primitive recursion clause is handled by coding a finite computation history as one number and using PA-induction on the recursion variable to prove that the history exists and has a unique final value. [/proofplan]

[step:Represent the initial primitive recursive functions by equality formulas] The zero function $Z:\mathbb{N}^k \to \mathbb{N}$, defined by $Z(a_1,\dots,a_k)=0$, is represented by \begin{align*} F_Z(x_1,\dots,x_k,y) \;:\!\iff\; y = 0. \end{align*} For every tuple $a_1,\dots,a_k \in \mathbb{N}$, PA proves \begin{align*} F_Z(\overline{a_1},\dots,\overline{a_k},\overline{0}), \end{align*} and PA proves $\forall x_1 \cdots \forall x_k \exists! y\, y=0$ by the equality axioms. The successor function $S:\mathbb{N}\to\mathbb{N}$, defined by $S(a)=a+1$, is represented by \begin{align*} F_S(x,y) \;:\!\iff\; y = Sx. \end{align*} For each $a\in\mathbb{N}$, PA proves $F_S(\overline a,\overline{a+1})$, since $\overline{a+1}=S\overline a$. Also PA proves $\forall x\exists!y\, y=Sx$ by equality. For $1\le i\le k$, the projection function $P_{k,i}:\mathbb{N}^k\to\mathbb{N}$, defined by \begin{align*} P_{k,i}(a_1,\dots,a_k)=a_i, \end{align*} is represented by \begin{align*} F_{P_{k,i}}(x_1,\dots,x_k,y) \;:\!\iff\; y=x_i. \end{align*} PA proves the required numeral instance and proves \begin{align*} \forall x_1\cdots \forall x_k \exists!y\, y=x_i \end{align*} again by the equality axioms. [/step]

[step:Preserve functional representability under composition]Assume $g:\mathbb{N}^m\to\mathbb{N}$ is functionally represented in PA by $G(u_1,\dots,u_m,y)$, and for each $1\le j\le m$ assume $h_j:\mathbb{N}^k\to\mathbb{N}$ is functionally represented in PA by $H_j(x_1,\dots,x_k,z_j)$. Define \begin{align*} f:\mathbb{N}^k &\to \mathbb{N} \\ (a_1,\dots,a_k) &\mapsto g(h_1(a_1,\dots,a_k),\dots,h_m(a_1,\dots,a_k)). \end{align*} Define the formula \begin{align*} F_f(x_1,\dots,x_k,y) \;:\!\iff\; \exists z_1\cdots \exists z_m\, \left( \bigwedge_{j=1}^m H_j(x_1,\dots,x_k,z_j) \wedge G(z_1,\dots,z_m,y) \right). \end{align*} Fix $a_1,\dots,a_k\in\mathbb{N}$. For each $j$, let \begin{align*} b_j := h_j(a_1,\dots,a_k). \end{align*} By the induction hypothesis for $H_j$, \begin{align*} \mathrm{PA}\vdash H_j(\overline{a_1},\dots,\overline{a_k},\overline{b_j}). \end{align*} Let \begin{align*} c := g(b_1,\dots,b_m). \end{align*} By the induction hypothesis for $G$, \begin{align*} \mathrm{PA}\vdash G(\overline{b_1},\dots,\overline{b_m},\overline c). \end{align*} Introducing the existential quantifiers for $z_1,\dots,z_m$, PA proves \begin{align*} F_f(\overline{a_1},\dots,\overline{a_k},\overline c). \end{align*} Since $c=f(a_1,\dots,a_k)$, this proves the numeral correctness clause. It remains to prove functionality. PA proves that for every $x_1,\dots,x_k$, each $H_j(x_1,\dots,x_k,z_j)$ has a unique witness $z_j$, and then $G(z_1,\dots,z_m,y)$ has a unique witness $y$. Therefore PA proves \begin{align*} \forall x_1\cdots \forall x_k \exists! y\, F_f(x_1,\dots,x_k,y). \end{align*}[/step]

[guided]The composition step says that if PA can already compute each intermediate function $h_j$, and PA can compute $g$ from the intermediate values, then PA can compute the composite function by first existentially naming the intermediate outputs. The formula \begin{align*} F_f(x_1,\dots,x_k,y) \;:\!\iff\; \exists z_1\cdots \exists z_m\, \left( \bigwedge_{j=1}^m H_j(x_1,\dots,x_k,z_j) \wedge G(z_1,\dots,z_m,y) \right) \end{align*} has exactly that meaning: the variables $z_1,\dots,z_m$ are the values of the component functions, and $y$ is the value obtained by applying $g$ to those values. For correctness on numerals, fix $a_1,\dots,a_k\in\mathbb{N}$. Define \begin{align*} b_j := h_j(a_1,\dots,a_k) \end{align*} for $1\le j\le m$, and define \begin{align*} c := g(b_1,\dots,b_m). \end{align*} The induction hypotheses give PA-proofs of \begin{align*} H_j(\overline{a_1},\dots,\overline{a_k},\overline{b_j}) \end{align*} for all $j$, and a PA-proof of \begin{align*} G(\overline{b_1},\dots,\overline{b_m},\overline c). \end{align*} By conjunction introduction and existential introduction, PA proves \begin{align*} F_f(\overline{a_1},\dots,\overline{a_k},\overline c). \end{align*} Since $c=f(a_1,\dots,a_k)$, this is exactly the desired numeral instance. For uniqueness, suppose PA proves both $F_f(x_1,\dots,x_k,y)$ and $F_f(x_1,\dots,x_k,y')$. Expanding the definition, there are intermediate witnesses $z_1,\dots,z_m$ and $z'_1,\dots,z'_m$. The uniqueness clauses for the formulas $H_j$ prove $z_j=z'_j$ for every $j$. Substituting these equalities into the two instances of $G$, the uniqueness clause for $G$ proves $y=y'$. The existence part is obtained by first using the existence clauses for the $H_j$ and then the existence clause for $G$. Hence PA proves \begin{align*} \forall x_1\cdots \forall x_k \exists! y\, F_f(x_1,\dots,x_k,y). \end{align*}[/guided]

[step:Use finite computation histories for the primitive recursion clause]Assume $g:\mathbb{N}^k\to\mathbb{N}$ is functionally represented in PA by $G(x_1,\dots,x_k,y)$, and assume $h:\mathbb{N}^{k+2}\to\mathbb{N}$ is functionally represented in PA by $H(x_1,\dots,x_k,n,z,w)$. Let $f:\mathbb{N}^{k+1}\to\mathbb{N}$ be defined by primitive recursion: \begin{align*} f(a_1,\dots,a_k,0) &= g(a_1,\dots,a_k),\\ f(a_1,\dots,a_k,n+1) &= h(a_1,\dots,a_k,n,f(a_1,\dots,a_k,n)). \end{align*} We use the standard PA finite-sequence coding package, obtained by primitive recursive coding of finite lists and by representability of the primitive recursive sequence operations already established in the closure clauses above. Concretely, fix $\mathcal{L}_{\mathrm{PA}}$-formulas \begin{align*} \operatorname{Seq}(c,\ell) \end{align*} and \begin{align*} \operatorname{Entry}(c,i,v) \end{align*} where $\operatorname{Seq}(c,\ell)$ states that $c$ codes a finite sequence of length $\ell$, and $\operatorname{Entry}(c,i,v)$ states that the $i$-th entry of the sequence coded by $c$ is $v$. These formulas are chosen so that PA proves the following uniform sentences, with $c,\ell,i,v,w,d$ arbitrary PA variables rather than numerals. First, entries below the length exist uniquely: \begin{align*} \mathrm{PA}\vdash \forall c\,\forall \ell\,\forall i\,\bigl(\operatorname{Seq}(c,\ell) \wedge i<\ell \to \exists!v\,\operatorname{Entry}(c,i,v)\bigr). \end{align*} Second, coded sequences can be extended by appending one prescribed final entry: \begin{align*} \mathrm{PA}\vdash \forall c\,\forall \ell\,\forall w\,\bigl(\operatorname{Seq}(c,\ell) \to \exists d\,(\operatorname{Seq}(d,S\ell) \wedge \operatorname{Entry}(d,\ell,w) \wedge \forall i\,\forall v\,(i<\ell \wedge \operatorname{Entry}(c,i,v) \to \operatorname{Entry}(d,i,v)))\bigr). \end{align*} Third, coded sequences admit initial segments: \begin{align*} \mathrm{PA}\vdash \forall c\,\forall \ell\,\bigl(\operatorname{Seq}(c,S\ell) \to \exists d\,(\operatorname{Seq}(d,\ell) \wedge \forall i\,\forall v\,(i<\ell \wedge \operatorname{Entry}(c,i,v) \to \operatorname{Entry}(d,i,v)))\bigr). \end{align*} For standard finite lists, the same coding package also gives the corresponding numeral instances: every particular finite list of natural numbers has a numeral code whose length and entries are PA-provable. These are the only sequence-coding facts used below. Define $\operatorname{Hist}_f(x_1,\dots,x_k,n,c)$ to be the formula saying that $c$ codes a computation history of length $n+1$: \begin{align*} \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \;:\!\iff\; &\operatorname{Seq}(c,S n) \\ &\wedge \exists v_0\, \left( \operatorname{Entry}(c,0,v_0) \wedge G(x_1,\dots,x_k,v_0) \right) \\ &\wedge \forall i\,\forall v\,\forall w\, \left( i<n \wedge \operatorname{Entry}(c,i,v) \wedge \operatorname{Entry}(c,S i,w) \to H(x_1,\dots,x_k,i,v,w) \right). \end{align*} Now define \begin{align*} F_f(x_1,\dots,x_k,n,y) \;:\!\iff\; \exists c\, \left( \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \wedge \operatorname{Entry}(c,n,y) \right). \end{align*} We prove in PA, by induction on $n$, that for every $x_1,\dots,x_k$ there exists a unique $y$ satisfying $F_f(x_1,\dots,x_k,n,y)$. For $n=0$, a history of length $1$ consists of exactly one entry $v_0$, and the defining condition requires $G(x_1,\dots,x_k,v_0)$. Since PA proves $\exists!v_0\,G(x_1,\dots,x_k,v_0)$, the final entry is unique, and PA proves \begin{align*} \forall x_1\cdots\forall x_k\exists!y\,F_f(x_1,\dots,x_k,0,y). \end{align*} For the induction step, assume PA proves \begin{align*} \forall x_1\cdots\forall x_k\exists!v\,F_f(x_1,\dots,x_k,n,v). \end{align*} The following argument is carried out in PA with $x_1,\dots,x_k$ arbitrary. By existential elimination applied to the induction hypothesis, choose a variable $v$ together with a proof of $F_f(x_1,\dots,x_k,n,v)$. Expanding $F_f$, choose a code $c$ such that \begin{align*} \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \wedge \operatorname{Entry}(c,n,v). \end{align*} Since $H$ functionally represents $h$, PA proves \begin{align*} \exists!w\,H(x_1,\dots,x_k,n,v,w). \end{align*} By existential elimination again, choose a variable $w$ satisfying $H(x_1,\dots,x_k,n,v,w)$. From $\operatorname{Hist}_f(x_1,\dots,x_k,n,c)$ PA has $\operatorname{Seq}(c,S n)$. Applying the sequence-extension property with $\ell=S n$, PA obtains a code $d$ such that $\operatorname{Seq}(d,S(S n))$, $\operatorname{Entry}(d,S n,w)$, and every entry of $c$ below $S n$ is copied to the corresponding entry of $d$. PA now verifies $\operatorname{Hist}_f(x_1,\dots,x_k,S n,d)$. The base entry is preserved from $c$ because $0<S n$, so the $G$-clause remains true. If $i<n$, then both entries at $i$ and $S i$ are copied from $c$, and the transition clause follows from $\operatorname{Hist}_f(x_1,\dots,x_k,n,c)$. If $i=n$, entry functionality for $d$ gives that the entry at $n$ is the copied value $v$ and the entry at $S n$ is $w$, so the transition clause is exactly $H(x_1,\dots,x_k,n,v,w)$. Therefore PA proves \begin{align*} \operatorname{Hist}_f(x_1,\dots,x_k,S n,d) \wedge \operatorname{Entry}(d,S n,w), \end{align*} and hence PA proves existence of a $y$ satisfying $F_f(x_1,\dots,x_k,S n,y)$. For uniqueness, suppose $F_f(x_1,\dots,x_k,S n,y)$ and $F_f(x_1,\dots,x_k,S n,y')$ hold, witnessed by codes $c$ and $c'$. By the initial-segment clause of the coding lemma, PA obtains codes for the first $n+1$ entries of $c$ and $c'$. Because these initial segments preserve all entries below $S n$, the base clause and all transition clauses with index $i<n$ are preserved, so the two initial segments satisfy $\operatorname{Hist}_f(x_1,\dots,x_k,n,\cdot)$. By the induction hypothesis, their stage-$n$ entries are equal. Calling this common entry $v$, both final entries $y$ and $y'$ satisfy \begin{align*} H(x_1,\dots,x_k,n,v,y) \end{align*} and \begin{align*} H(x_1,\dots,x_k,n,v,y'). \end{align*} The uniqueness clause for $H$ gives $y=y'$. Therefore PA proves \begin{align*} \forall x_1\cdots\forall x_k\exists!y\,F_f(x_1,\dots,x_k,S n,y). \end{align*} By PA-induction on $n$, PA proves \begin{align*} \forall x_1\cdots\forall x_k\forall n\exists!y\,F_f(x_1,\dots,x_k,n,y). \end{align*}[/step]

[guided]The primitive recursion case is the only non-immediate closure step. The difficulty is that the value at stage $n$ depends on all previous recursive updates. PA handles this by talking about a finite computation history rather than trying to quantify over an external sequence. The recursive definition is \begin{align*} f(a_1,\dots,a_k,0) &= g(a_1,\dots,a_k),\\ f(a_1,\dots,a_k,n+1) &= h(a_1,\dots,a_k,n,f(a_1,\dots,a_k,n)). \end{align*} We therefore want a formula saying: "$c$ codes the list of values \begin{align*} f(a_1,\dots,a_k,0),\dots,f(a_1,\dots,a_k,n). \end{align*} " PA has standard primitive recursive finite-sequence coding. We use formulas \begin{align*} \operatorname{Seq}(c,\ell) \end{align*} and \begin{align*} \operatorname{Entry}(c,i,v) \end{align*} where $\operatorname{Seq}(c,\ell)$ says that $c$ codes a finite sequence of length $\ell$, and $\operatorname{Entry}(c,i,v)$ says that the $i$-th entry of the coded sequence is $v$. What must be checked about this coding? Not merely that standard finite lists have codes, but that PA proves the sequence operations uniformly for arbitrary PA variables. We therefore use the following PA-provable sentences: if $\operatorname{Seq}(c,\ell)$ and $i<\ell$, then there is a unique $v$ with $\operatorname{Entry}(c,i,v)$; if $\operatorname{Seq}(c,\ell)$ and $w$ is any value, then PA proves that there is a code $d$ of length $S\ell$ copying all entries of $c$ below $\ell$ and satisfying $\operatorname{Entry}(d,\ell,w)$; and if $\operatorname{Seq}(c,S\ell)$, then PA proves that there is a code $d$ of length $\ell$ copying all entries of $c$ below $\ell$. These are primitive recursive sequence operations represented in PA, so the extension and initial-segment arguments below are formal PA arguments, not only metamathematical statements about standard lists. The extension property is what builds the next recursive history, and the initial-segment property is what lets PA compare two histories at the previous stage. Using this coding, define $\operatorname{Hist}_f(x_1,\dots,x_k,n,c)$ by \begin{align*} \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \;:\!\iff\; &\operatorname{Seq}(c,S n) \\ &\wedge \exists v_0\, \left( \operatorname{Entry}(c,0,v_0) \wedge G(x_1,\dots,x_k,v_0) \right) \\ &\wedge \forall i\,\forall v\,\forall w\, \left( i<n \wedge \operatorname{Entry}(c,i,v) \wedge \operatorname{Entry}(c,S i,w) \to H(x_1,\dots,x_k,i,v,w) \right). \end{align*} The first line says that $c$ has exactly enough entries to record stages $0,\dots,n$. The second line says that the first entry is the value supplied by $g$. The third line says that whenever $i<n$, the next entry is obtained from the previous one by the representing formula for $h$. Now define the representing formula for $f$ by declaring $y$ to be the final entry of such a history: \begin{align*} F_f(x_1,\dots,x_k,n,y) \;:\!\iff\; \exists c\, \left( \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \wedge \operatorname{Entry}(c,n,y) \right). \end{align*} We prove inside PA that this formula is functional by induction on $n$. For $n=0$, a history has length $1$, so its only entry must be a value $v_0$ satisfying \begin{align*} G(x_1,\dots,x_k,v_0). \end{align*} The induction hypothesis for $g$ says that PA proves \begin{align*} \exists!v_0\,G(x_1,\dots,x_k,v_0). \end{align*} Thus PA proves that there is exactly one possible final entry at stage $0$. For the induction step, assume PA has proved that the stage-$n$ value exists uniquely. Inside PA, with $x_1,\dots,x_k$ arbitrary, existential elimination gives a variable $v$ and a code $c$ such that \begin{align*} \operatorname{Hist}_f(x_1,\dots,x_k,n,c) \wedge \operatorname{Entry}(c,n,v). \end{align*} The uniqueness part of the induction hypothesis will be used later for uniqueness; existence gives the history to extend. Since $H$ functionally represents $h$, PA proves \begin{align*} \exists!w\,H(x_1,\dots,x_k,n,v,w). \end{align*} Existential elimination gives a variable $w$ with $H(x_1,\dots,x_k,n,v,w)$. Because $\operatorname{Hist}_f(x_1,\dots,x_k,n,c)$ includes $\operatorname{Seq}(c,S n)$, the extension property applies with $\ell=S n$: PA obtains a code $d$ of length $S(S n)$ that copies every entry of $c$ below $S n$ and has final entry $w$ at index $S n$. Now PA checks the definition of $\operatorname{Hist}_f(x_1,\dots,x_k,S n,d)$ line by line. The initial $G$-entry is preserved because it was copied from $c$. For a transition index $i<n$, both adjacent entries were copied from $c$, so the transition follows from the old history. For the new transition index $i=n$, entry functionality identifies the copied stage-$n$ entry with $v$ and the appended final entry with $w$, and the transition formula is exactly $H(x_1,\dots,x_k,n,v,w)$. Hence PA proves existence at stage $S n$. For uniqueness at stage $S n$, suppose two histories produce final entries $y$ and $y'$. The initial-segment property gives codes for their first $n+1$ entries. Since those initial segments preserve all entries below $S n$, they still satisfy the history condition for stage $n$. By the induction hypothesis, their stage-$n$ entries are equal; call this common value $v$. The last transition in each history is then governed by the same instance of $H$: \begin{align*} H(x_1,\dots,x_k,n,v,y) \end{align*} and \begin{align*} H(x_1,\dots,x_k,n,v,y'). \end{align*} The uniqueness clause for $H$ proves $y=y'$. Thus PA proves uniqueness at stage $S n$. PA-induction yields \begin{align*} \forall x_1\cdots\forall x_k\forall n\exists!y\,F_f(x_1,\dots,x_k,n,y). \end{align*} It remains, in the recursion case, to check numeral correctness. Fix $a_1,\dots,a_k,n\in\mathbb{N}$. We prove by ordinary induction on $n$ that PA proves \begin{align*} F_f(\overline{a_1},\dots,\overline{a_k},\overline n,\overline{f(a_1,\dots,a_k,n)}). \end{align*} For $n=0$, the induction hypothesis for the representing formula $G$ gives \begin{align*} \mathrm{PA}\vdash G(\overline{a_1},\dots,\overline{a_k},\overline{g(a_1,\dots,a_k)}). \end{align*} Since $f(a_1,\dots,a_k,0)=g(a_1,\dots,a_k)$, the finite-sequence coding lemma gives a one-entry code whose zeroth entry is $\overline{f(a_1,\dots,a_k,0)}$, and PA verifies that this code satisfies $\operatorname{Hist}_f(\overline{a_1},\dots,\overline{a_k},0,\cdot)$. Hence PA proves the required instance at $0$. Assume the required numeral instance has been proved at $n$. Define \begin{align*} v := f(a_1,\dots,a_k,n) \end{align*} and \begin{align*} w := f(a_1,\dots,a_k,n+1)=h(a_1,\dots,a_k,n,v). \end{align*} The induction hypothesis for the representing formula $H$ gives \begin{align*} \mathrm{PA}\vdash H(\overline{a_1},\dots,\overline{a_k},\overline n,\overline v,\overline w). \end{align*} By the ordinary induction hypothesis, PA has a coded history through stage $n$ with final entry $\overline v$. Appending the entry $\overline w$ and using the displayed instance of $H$, PA verifies the history condition through stage $n+1$. Therefore PA proves \begin{align*} F_f(\overline{a_1},\dots,\overline{a_k},\overline{n+1},\overline{f(a_1,\dots,a_k,n+1)}). \end{align*} Thus the primitive recursion clause gives both functionality and numeral correctness.[/guided]

[step:Verify numeral correctness for primitive recursion] Fix $a_1,\dots,a_k,n\in\mathbb{N}$. We prove by ordinary induction on $n$ that \begin{align*} \mathrm{PA}\vdash F_f(\overline{a_1},\dots,\overline{a_k},\overline n,\overline{f(a_1,\dots,a_k,n)}). \end{align*} For $n=0$, the induction hypothesis for $G$ gives \begin{align*} \mathrm{PA}\vdash G(\overline{a_1},\dots,\overline{a_k},\overline{g(a_1,\dots,a_k)}). \end{align*} Since $f(a_1,\dots,a_k,0)=g(a_1,\dots,a_k)$, the one-entry sequence with that value is a valid computation history, so PA proves \begin{align*} F_f(\overline{a_1},\dots,\overline{a_k},0,\overline{f(a_1,\dots,a_k,0)}). \end{align*} Assume the numeral correctness statement holds for $n$. Let \begin{align*} v := f(a_1,\dots,a_k,n) \end{align*} and \begin{align*} w := f(a_1,\dots,a_k,n+1)=h(a_1,\dots,a_k,n,v). \end{align*} By the induction hypothesis for $H$, \begin{align*} \mathrm{PA}\vdash H(\overline{a_1},\dots,\overline{a_k},\overline n,\overline v,\overline w). \end{align*} Appending $\overline w$ to the coded computation history for stage $n$, PA proves the existence of a computation history for stage $n+1$ whose final entry is $\overline w$. Therefore \begin{align*} \mathrm{PA}\vdash F_f(\overline{a_1},\dots,\overline{a_k},\overline{n+1},\overline{f(a_1,\dots,a_k,n+1)}). \end{align*} This completes the numeral correctness proof for the primitive recursion clause. [/step]

[step:Conclude by structural induction over primitive recursive definitions] Primitive recursive functions are exactly the smallest class of functions $\mathbb{N}^k\to\mathbb{N}$ containing the zero, successor, and projection functions and closed under composition and primitive recursion. The case $k=0$ is interpreted in the usual nullary way: a function $f:\mathbb{N}^0\to\mathbb{N}$ is a constant, the tuple $a_1,\dots,a_k$ is the unique empty tuple, and the quantifier prefix $\forall x_1\cdots\forall x_k$ is the empty prefix. In the initial-function step, there are no projection functions when $k=0$, while the zero and successor clauses and both closure clauses remain meaningful with this empty-prefix convention. The first step established functional representability for the initial functions. The second step established preservation under composition. The primitive recursion steps established preservation under primitive recursion. Therefore, by structural induction on the construction of the primitive recursive function $f$, there exists an $\mathcal{L}_{\mathrm{PA}}$-formula $F_f(x_1,\dots,x_k,y)$ such that for every $a_1,\dots,a_k\in\mathbb{N}$, \begin{align*} \mathrm{PA}\vdash F_f(\overline{a_1},\dots,\overline{a_k},\overline{f(a_1,\dots,a_k)}), \end{align*} and \begin{align*} \mathrm{PA}\vdash \forall x_1\cdots\forall x_k\exists!y\,F_f(x_1,\dots,x_k,y). \end{align*} Thus every primitive recursive function is functionally represented in PA. [/step]