Primitive-recursive functions are representable in Q

Induct externally on the finite primitive-recursive construction. Zero, successor and projections have the graphs $y=0$, $y=Sx$, $y=x_i$. Their unique-value proofs are equality calculations. For composition use $\mathrm{\exists }{u}_1\cdots u_k({\bigwedge }_i{G}_i(\bar{x},u_i)\wedge H(\bar{u},y))$. At numeral inputs the G graphs force numeral intermediate values, and H then forces the correct output; conversely those values witness existence. The same argument with variables proves totality and uniqueness in PA when the component graphs have them.

Before using a graph A as a history component replace it by $A^{\ast }(\bar{x},y):=A(\bar{x},y)\wedge \mathrm{\forall }z<y\mathrm{\neg }A(\bar{x},z)$. At numeral inputs with output r, uniqueness for A gives the positive instance of this strengthening and the same unique output. More strongly, for each external r, Q proves, uniformly in the other inputs, that $A^{\ast }(\bar{x},\bar{r})\wedge A^{\ast }(\bar{x},y)\to y=\bar{r}$. Indeed F1 splits y into the numerals at most r or the case $\overline{r+1}\le y$. Below r the least-output clause at r refutes A at y; above r the least-output clause at y refutes A at r, since the numeral order calculation gives $\bar{r}<y$. The remaining case is equality. This does not require functionality at arbitrary nonnumeral inputs.

For $f(0,\bar{x})=g(\bar{x})$ and $f(t+1,\bar{x})=h(t,f(t,\bar{x}),\bar{x})$, let G,H and B be the strengthened graphs for g,h and beta from F2. Define the raw recursion graph by $\mathrm{\exists }b,c[\mathrm{\exists }u(G(\bar{x},u)\wedge B(b,c,0,u))\wedge \mathrm{\forall }i<t\mathrm{\exists }u,v(B(b,c,i,u)\wedge B(b,c,Si,v)\wedge H(i,u,\bar{x},v))\wedge B(b,c,t,y)]$. All free variables here have the indicated roles, and auxiliary variables are fresh. For numeral t and inputs, F2 codes the actual finite sequence $f(0,\bar{n}),\dots ,f(t,\bar{n})$. Positive numeral instances of G,H,B and the finite case scheme F1 verify every clause, giving existence.

For uniqueness, take any b,c satisfying the raw graph at those numeral inputs. G forces the initial witness to the numeral $f(0,\bar{n})$, so B at coordinate zero holds with that numeral. Instantiate the successor clause at external i=0. Its occurrence of coordinate zero equals that numeral by the uniform property of strengthened B in step 2.1, even though b,c are arbitrary. H now forces v to the next computed numeral; consequently B at coordinate one holds with it. Repeat this finite argument for i=1,...,t-1. The terminal B occurrence then forces y to the computed numeral f(t,n), again by step 2.1. For t=0 the initial and terminal B occurrences alone suffice. This proves numeralwise uniqueness without assuming arbitrary Q history codes are functional.

In PA the beta graph is total and unique by F2. Induction on t proves existence of the raw history: start with the g value and a one-entry beta code; extend its code by the uniquely determined h value using F2. A second induction shows any two histories have the same value at each coordinate, first at zero by G and then at the successor by H. Thus PA proves the raw graph total and unique. It follows in PA that A and its strengthening A* are equivalent whenever A is any constructed graph: uniqueness excludes all smaller competing outputs. Also $\mathrm{\neg }A(\bar{x},y)\leftrightarrow \mathrm{\exists }z(A(\bar{x},z)\wedge z\mathrm{\ne }y)$, by totality and uniqueness.

We prove the complexity claim simultaneously with construction. The beta and initial graphs are bounded. At later stages replace earlier graphs by their PA-equivalent existential bounded forms, and replace negative occurrences by the distinct-output existential formula of step 5.1. Positive Boolean combinations and existential prefixes combine by fresh-variable prenexing. For bounded universal closure PA proves $\mathrm{\forall }i<t\mathrm{\exists }w\delta (i,w)\leftrightarrow \mathrm{\exists }B\mathrm{\forall }i<t\mathrm{\exists }w\le B\delta (i,w)$: induction on t starts with B=0, and adjoining the next witness replaces B by its maximum with that witness. Repeating this for a fixed finite witness tuple supplies a common bound. The remaining matrix is bounded. Therefore every constructed graph is PA-equivalent to a syntactic Sigma1 graph, while its original strengthened form retains the Q assertion.

For a primitive-recursive relation use the representing graph of its 0–1 characteristic function at output 1. The numeralwise unique-value theorem proves the instance when the value is 1, and proves its negation when the value is 0 since Q proves $0\mathrm{\ne }1$ by F1. This completes the function and relation assertions.