Arithmetization, Incompleteness, and Relative Consistency

From the initial functions and parameter recursion in F1 define $a+0=a$, $a+Sn=S(a+n)$, $a\cdot 0=0$, $a\cdot Sn=a\cdot n+a$, $\mathrm{pred}(0)=0$, $\mathrm{pred}(Sn)=n$, and , . Set $z(0)=1,z(Sn)=0$. Then equality is and $a\le b$ has characteristic function . Products, complements and $rg+(1-r)h$ implement Boolean tests and case splits for a 0–1 test $r$. Bounded sums/products have initial values 0/1 and append one term, so are primitive recursive.

For a 0–1 predicate $r$, ${\sum }_{j<N}{\prod }_{i\le j}(1-r(i))$ counts the unsuccessful initial positions: it equals the least successful index, or $N$ if none succeeds. This explicitly proves bounded search, consistent with bounded closure F2. Powers satisfy $b^0=1,b^{n+1}=b\cdot b^n$. For $d>0$ put $q(a,d)={\sum }_{j=1}^a[dj\le a]$ and , and set both to 0 for $d=0$. The successful indices are exactly $1,\dots ,q$; thus $dq\le a<d(q+1)$, giving quotient and remainder. Every operation just defined is primitive recursive.

Put $P(u,v)=(u+v{)}^2+u$. For a fixed sum $t$, its values occupy $[t^2,t^2+t]$ with distinct offsets $u$; the next interval starts at $(t+1{)}^2>t^2+t$. Hence $P$ is injective. Both coordinates are at most $P(u,v)$, including $(0,0)$. Bounded search therefore gives its range test and inverses, with zero off-range. Nesting a fixed number of these pairs stores a fixed register tuple. Decode, apply the finitely many update functions, and encode again: ordinary primitive recursion on the one state code implements the simultaneous register recursion, regardless of how large the registers grow.

For $s>0$, its binary width is $\mathrm{\ell }(s)=1+{\sum }_{j=1}^s[2^j\le s]$, and $\mathrm{\ell }(0)=1$. Indeed the powers of two are strictly increasing and $2^s>s$ for $s\ge 1$ including s=1; induction proves this bound. Thus the counted indices give the largest exponent below $s$. The left-to-right bit at $j<\mathrm{\ell }(s)$ is the remainder modulo 2 of the quotient of $s$ by $2^{\mathrm{\ell }(s)-1-j}$; elsewhere return zero. Horner updating $v\mapsto 2v+b$ evaluates any specified payload. These are primitive-recursive register computations by steps 2.1–3.1.

Parse the canonical binary word of $s>0$. After the initial 1, count the consecutive 1s to the first 0; failure to find that delimiter is invalid. Their number is $k$. At each of $k$ block starts $p$, find the next zero below $\mathrm{\ell }(s)$ and let $m$ be its distance. Require $m\ge 1$, require $m$ payload bits after the delimiter to fit, and require their first bit to be 1 unless $m=1$. Evaluate those bits by Horner and advance by $2m+1$. Finally require the position to equal $\mathrm{\ell }(s)$. Each scan and block loop has at most $\mathrm{\ell }(s)+1$ iterations. A persistent error flag freezes invalid states. The counters, current position, flag and requested entry are finitely many registers, so step 3.1 proves primitive recursiveness. At the end reset length and coordinates to zero on failure, and coordinates to zero outside $0\le j<k$.

The header and every block delimiter determine their lengths uniquely. Each canonical payload therefore recovers its unique original natural number. Induction over the blocks proves that parsing an encoded list returns that list; conversely, a successful parse consumes the whole word and reconstruction reproduces it. Thus two lists with the same code have equal length and equal entries. The word 10 has k=0 and no payload, so parses successfully as the empty list.

For construction represent a word by value and width $(v,L)$; concatenating $(w,M)$ gives $(v{2}^M+w,L+M)$. The length-k header is $(2^{k+2}-2,k+2)$. For $m=\mathrm{\ell }(a)$ the entry block has width $2m+1$ and value $(2^m-1)2^{m+1}+a$. Fixed-arity encoders concatenate finitely many such blocks. Append and concatenation build the enlarged header and copy coordinates from the validated inputs, followed by the new entry or second list, using their lengths as bounds. Induction on the number copied gives exactly the required output list. Invalid inputs return 2. Finally a history recursion stores its current list code, computes the primitive-recursive next value from it and appends. This is one ordinary parameter recursion; retrieving a coordinate supplies the result.

Use the seven Q axioms F1. Externally inducting on $b$ gives Q proofs of $\bar{a}+\bar{b}=\overline{a+b}$ and $\bar{a}\cdot \bar{b}=\overline{ab}$, by substituting the previous equality into the respective recursion axiom. Structural induction reduces each closed term to a numeral. For distinct numerals cancel their common successor prefix using injectivity; a remaining successor cannot equal zero. Hence Q proves the correct equality or inequality between any two closed terms.

We prove the bounded-case scheme externally on $n$. If $z+x=0$ and $x\mathrm{\ne }0$, predecessor gives $x=Sy$, so $z+x=S(z+y)\mathrm{\ne }0$, a contradiction. Hence $x\le 0\to x=0$. For the next bound, either $x=0$ or $x=Sy$. In the second case $z+x=S\bar{n}$ implies $z+y=\bar{n}$ by injectivity, hence $y\le \bar{n}$ and the earlier finite case scheme makes $x$ one of $\bar{1},\dots ,\overline{n+1}$. This is a finite derivation for each n.

For every fixed $k$, external induction proves $z+\bar{k}=S^{k}z$ and $Sz+\bar{k}=z+\overline{k+1}$. Repeatedly applying the predecessor axiom $n+1$ times gives the finite disjunction: $x=0$, ..., $x=\bar{n}$, or $x=S^{n+1}z$ for some $z$. In a numeral case, a numeral left-addend witness proves $x\le \bar{n}$ by step 1.1. In the last case, $z+\overline{n+1}=x$ proves $\overline{n+1}\le x$. This gives the second scheme without internal induction. The same calculation shows $\overline{n+1}\le x\to \bar{n}\le x$ by replacing z with Sz.

A numeral instance of $\le$ is true exactly when its first numeral is among those allowed by step 2.1. If it is, a numeral witness proves it; otherwise the finite disjunction and the unequal-numeral proofs refute it. Thus closed order atoms are decided as well. For a closed bounded quantifier first reduce its bounding term to $\bar{n}$, then use step 2.1 to replace the bounded variable by the finite list of possible numerals. Induction on the formula gives a proof or a refutation for each substituted matrix. Existential introduction proves a true existential; the finite case disjunction refutes a false one. Negation handles universal quantifiers; Boolean truth tables combine the remaining cases. The zero bound yields either a singleton test for <= or no candidates for <.

For $d>0$, induction on $b$ gives unique division $b=qd+r$, $r<d$: at zero use $(0,0)$; from $(q,r)$ use $(q,r+1)$ if $r+1<d$, and $(q+1,0)$ if $r+1=d$. If two such expressions had $q<q\mathrm{\prime }$, then $qd+r<(q+1)d\le q\mathrm{\prime }d\le q\mathrm{\prime }d+r\mathrm{\prime }$, impossible; interchange them for the other inequality. Thus quotient and remainder are unique. These arguments use natural-number induction and elementary distributivity/order, each derivable in PA by induction from F1.

To derive the required congruence theorem, repeatedly replace $(u,v)$ with $(v,\mathrm{rem}(u,v))$ while $v>0$. The positive second coordinate strictly decreases, so strong induction on the second coordinate $v$ gives termination, uniformly in $u$ (also when $u<v$). Common divisors are unchanged because $u=qv+r$ iff $r=u-qv$. Maintaining integer linear combinations of the original pair (integers represented as differences of naturals) shows that the final positive divisor $g$ is $su+tv$. It divides both original numbers, and every common divisor divides it. Thus coprime $u,v$ have $su+tv=1$. For residues $A,B$ the integer $Avt+Bus$ is congruent to A modulo u and B modulo v. Taking its nonnegative residue modulo uv gives a simultaneous solution. Uniqueness modulo uv follows since a number divisible by u and v is divisible by uv: multiply $su+tv=1$ by the quotient after division by u. Iterating combines any finite pairwise coprime list.

Use the Q remainder graph $R(b,d,r):=(d=0\wedge r=0)\vee [d\mathrm{\ne }0\wedge r\le b\wedge r<d\wedge \mathrm{\exists }q\le b(b=q\cdot d+r)]$. At numeral b,d, F2 restricts r and q to finite lists of numerals. Step 1.1 identifies the one correct remainder; every other pair is refuted by closed calculations, and the correct pair supplies existence. If d=0 the first clause forces r=0. Substituting the term $1+(i+1)c$ into the divisor place gives the beta graph. At numeral inputs the divisor is a numeral by F2, so the same unique-value conclusion follows.

For $a_0,\dots ,a_n$, choose $j>\max (n+1,a_0,\dots ,a_n)$ and $c=j!$. Let $d_i=1+(i+1)c$. If a prime p divided both $d_i,d_k$ with $i\mathrm{\ne }k$, it would divide $(i-k)c$. It cannot divide c, since it divides $1+(i+1)c$, so it divides $\mathrm{\mid }i-k\mathrm{\mid }\le n<j$, and then divides j!, a contradiction. Here every integer greater than one has a prime divisor by taking its least divisor greater than one; that divisor is prime by minimality. The prime-divides-product assertion follows from the Bezout identity when it does not divide one factor. Thus the moduli are pairwise coprime, and step 2.1 gives b with remainder $a_i<d_i$ at each modulus. The empty list requires no congruences.

For the PA assertion, division and the Euclidean argument above are inductions on naturals, with integer coefficients stored as pairs of naturals. For every j and bound B, PA proves there is C>B divisible by every positive t<=j: the induction starts with C=B+1 for j=0; from a witness C at j take C(j+1) at j+1. This uses a single existential induction invariant and does not presuppose sequence coding or a factorial function. PA bounds the old beta values by $1+nc$ for $i<n$. Choose $j>n+1,a,1+nc$ and such a C>j divisible by 1,...,j, and use new moduli $1+(i+1)C$. The coprimality argument of step 3.1 uses precisely this divisibility property. Induction on $k\le n+1$ combines the first k congruences as in step 2.1, keeping the running product of their moduli and the current residue as existential witnesses; the induction hypothesis is a formula asserting those witnesses exist. The first n residues are $\beta (b,c,i)$, whose existence and uniqueness follow from division, and the last is a. Thus the formal PA induction produces the new code and proves every specified coordinate equation. Repeating extension supplies any internally given finite history; for a fixed external list step 3.1 already supplies its code.

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.

By F1 list coordinates and lengths, comparisons, append, and fixed-register iterations are primitive recursive. For a token word of length l, compute expression status for every interval [i,j) in increasing interval length, using at most $(l+1{)}^2$ intervals. A constructor test checks its punctuation and tag, and splits the interior at commas of parenthesis depth zero using a stack or depth counter of at most l entries. At a function/relation node compare the actual number of children to the supplied primitive-recursive arity. The children have strictly shorter intervals; the stored table therefore decides their term/formula status before the parent. Induction on interval length proves the table recognizes exactly the prescribed constructors, including nullary symbols and rejecting ill-formed words.

At a variable leaf store its singleton free-variable list; at other leaves use the empty list. At a function, relation, equality or conjunction node take the union of the child lists; at negation retain its list; at $\mathrm{\exists }{v}_i$ delete i. These finite loops have bounds l or the stored child-list lengths. To test whether a term t is free for x, scan each free x occurrence in the formula and test that no binder above it has an index in FV(t). The parse stack lists exactly those binders. This proves correctness of the free-for test and supplies its primitive-recursive bound.

For capture-free substitution, first traverse the binder nodes and rename them to distinct indices above every index in the input formula and term. Updating their bound occurrences uses their scope intervals and excludes subscopes rebinding that variable. There are at most l binders. Rebuild the parsed expression, replacing free x leaves by t and leaving other leaves unchanged. The traversal performs at most l node updates; each update is a primitive-recursive list construction and may increase the code without increasing the number of nodes processed. Structural induction proves the result is substitution with no capture. When t was already free for x, also provide the exact unrenamed free-for substitution by the same rebuild without the preliminary renaming; this is the version tested in the Hilbert axiom annotations. Negation adds its constructor; numeral formation iterates the successor constructor n times from the zero term.

A proof line contains its formula, a scheme/rule tag and its finite annotation. For scheme 1, the annotation gives the Boolean skeleton and substituted formulas; check the rebuilt formula and all at most $2^l$ Boolean valuations of its l-or-fewer skeleton letters. For schemes 2 and 4, the annotation supplies formula, variable and term; check free-for and exact substitution, then the instantiation/introduction template. For scheme 3 check its distribution template and that x is absent from the antecedent free list. Scheme 5 is term reflexivity. Scheme 6 checks both free-for conditions and the two exact substituted formulas in equality substitution. Thus every one of the six schemes is checked by steps 1.1–3.1 and bounded finite tests. An axiom instance always has such finite annotation; annotations never replace a test of validity.

For MP check the two earlier premise indices and the implication shape; for generalization check the earlier premise and bound variable; for restricted existential elimination check the earlier implication, the resulting quantified antecedent, and absence of the eliminated variable from the consequent free list. At a nonlogical axiom line check sentencehood and E(a,w) from the supplied certificate (F2), rather than searching for w. A loop over the decoded number of lines checks every line and the final conclusion; reject an empty derivation, malformed annotation or non-earlier premise. Induction on lines gives soundness of acceptance for the specified calculus, and conversely each certified derivation meets these tests. All bounds are input lengths, explicit exponentials for Boolean valuations, or bounds of already constructed primitive-recursive loops, proving the claim.

Under the guard on free inputs, induction on terms proves that $V_t$ has a value in D, is unique modulo E, and is invariant under E-equivalent inputs. The variable case uses E reflexivity and transitivity on D. At a function node, the finitely many argument values exist by induction; graph totality supplies the output. Congruence of the graph identifies outputs modulo E when the arguments are replaced, and graph uniqueness compares any two outputs. No guard asserts E-reflexivity outside D. These are precisely the obligations in F1.

Induction on formulas proves invariance under E-equivalent assignments: atoms use step 1.1 and relation congruence; negation and conjunction use Boolean reasoning; an existential retains its witness while changing the other parameters. Simultaneous substitution induction gives, for free-for t and fresh z, $(\varphi [t\mathrm{/}x]{)}^I\leftrightarrow \mathrm{\exists }z(V_t(z)\wedge {\varphi }^I[z\mathrm{/}x])$ under the free-input guard. At atoms substitute the argument graphs. At conjunction compare the two possible values modulo E and use formula invariance to place both conjuncts at one value. At negation, value existence and invariance imply every value has the same truth value, so $\mathrm{\neg }\mathrm{\exists }z(V_t(z)\wedge A(z))\leftrightarrow \mathrm{\exists }z(V_t(z)\wedge \mathrm{\neg }A(z))$. At quantifiers rename the binder away from t,z and commute independent existential witnesses using F2. Thus the substitution equivalence holds in both directions, including when x is absent.

Surplus guards can be removed. If x is absent from A and G and T proves $(G\wedge D(x))\to A$, rearrange it to $D(x)\to (G\to A)$ and apply restricted existential elimination to obtain $(\mathrm{\exists }xD(x))\to (G\to A)$. Domain nonemptiness from F1 yields $G\to A$. All temporary deductions can be discharged by F3: generalized or eliminated variables have been chosen absent from those open assumptions.

The six logical schemes of F4 translate as follows. A Boolean tautology remains a tautology under formula substitution. For universal instantiation take a value of t by step 1.1; the relativized universal supplies the matrix there and step 2.1 yields the substituted conclusion. Distribution sends $\mathrm{\forall }x(D(x)\to (A\to B))$ and A to $\mathrm{\forall }x(D(x)\to B)$ since x is absent from A. Existential introduction takes the value furnished by step 2.1 as its domain witness. Reflexivity follows from a term value and E-reflexivity. For equality substitution, interpreted equality relates the values of the two terms by E; formula invariance transports the substituted matrix, and step 2.1 translates back. Add required guards, remove surplus ones by step 3.1, and use F2 for universal abbreviations and quantified double negation. Every auxiliary witness variable is fresh.

Induct over source proof lines. Sentence axioms use their supplied translation proofs. For MP enlarge both guards to their union, apply propositional MP and remove surplus guards. For generalization in x, write the transformed premise as $G\to (D(x)\to A)$ with x absent from G, generalize and distribute to obtain $G\to \mathrm{\forall }x(D(x)\to A)$; F2 identifies the expanded universal translation. For existential elimination with x absent from the source consequent B, rearrange the premise to $(D(x)\wedge A)\to (G\to B)$ with x absent from G,B, eliminate x and rearrange back. Step 3.1 then removes surplus guards. These are exactly the three rules in F4.

The source contradiction is $\mathrm{\exists }x\mathrm{\neg }(x=x)$. Its translation is refuted in T by domain-guarded E-reflexivity and step 1.1. Hence its translated proof and that refutation give the fixed target contradiction by explosion F2. Finite support and concatenation F5 assemble the finitely many obligation and axiom proofs used by step 5.1; finite selection is provable in ZF by induction on their number. Effective certificate data makes every such substitution and assembly effective. Finally, if B verifies a total contradiction-code map r, a hypothetical source contradiction code maps to a target one; under Con(T) that is impossible. Quantifying over the source code inside B gives Con(S). The totality verification is a separate hypothesis.

By F1 define d(e) to be the code obtained by substituting the numeral of e in the designated free variable of formula e, with a fixed default for invalid inputs. It is primitive recursive. F2 supplies a formula D(x,y) numeralwise representing d uniquely in Q. Choose auxiliary y fresh from psi and from the designated variable x.

Let $\eta (x)=\mathrm{\exists }y(D(x,y)\wedge \psi (y))$, $e=\mathrm{\#}\eta$ and $\theta =\eta (\bar{e})$. By definition of d, $d(e)=\mathrm{\#}\eta (\bar{e})=\mathrm{\#}\theta$. Thus Q proves $\mathrm{\forall }y(D(\bar{e},y)\leftrightarrow y=<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$ by F2. The code e is a natural number; its numeral is the term used in theta.

From theta a witness y satisfies D and psi; the uniqueness equation in step 2.1 gives $y=<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>$, hence $\psi (<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$. Conversely D holds at that numeral by the same equation; conjoin it with psi at that numeral and introduce the existential to obtain theta. All replacements use fresh variables and licensed equality substitution. These finite syntactic operations prove the biconditional in Q effectively.

F1 supplies the displayed fixed point, and F2 fixes a numeralwise correct proof predicate. If p were an actual T-proof of G, Q would prove ${\mathrm{Prf}}_T(\bar{p},<mi\; mathvariant="normal">⌜</mi>G<mi\; mathvariant="normal">⌝</mi>)$, hence T would prove Prov(G). Its proof of G and the fixed-point implication would also give not-Prov(G), contradicting consistency. Thus no such p exists.

For every actual natural p, the proof check therefore fails, and Q proves its negative numeral instance by F2. In the standard natural-number structure every element is such a numeral value, so $\mathrm{\neg }{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>G<mi\; mathvariant="normal">⌝</mi>)$ is true. The Q fixed-point theorem is true there: zero, successor, addition and multiplication satisfy each displayed Q axiom, and each logical proof rule preserves truth. Hence G is true. Additional signature symbols play no role in this proof predicate.

If T proved not-G, the fixed-point biconditional and classical logic would give $\mathrm{\exists }p{\mathrm{Prf}}_T(p,<mi\; mathvariant="normal">⌜</mi>G<mi\; mathvariant="normal">⌝</mi>)$. Step 2.1 gives a T-refutation of every numeral instance of its matrix, violating the stated omega-consistency condition. A sound theory cannot have that pattern, since any standard witness to the existential is one of those numeral values. Consistency alone was used only for the unprovability and truth of G.

In the extension case, apply F1 to obtain $R\leftrightarrow \mathrm{\forall }p({\mathrm{Prf}}_T(p,<mi\; mathvariant="normal">⌜</mi>R<mi\; mathvariant="normal">⌝</mi>)\to \mathrm{\exists }q\le p{\mathrm{Prf}}_T(q,<mi\; mathvariant="normal">⌜</mi>\mathrm{\neg }R<mi\; mathvariant="normal">⌝</mi>))$. The syntax and proof checks in F2 are numeralwise expressible in Q. If m proves R, consistency implies that no q proves not-R. In particular Q refutes the finitely many checks for $q\le m$; F3 combines them into a bounded universal. Q also proves the positive check at m. Therefore Q refutes the right side of the fixed point, giving not-R in T, a contradiction.

If n proves not-R, consistency implies that Q refutes every proof-of-R check for p at most n. F3 gives their bounded universal and splits arbitrary p into $p\le \bar{n}$ or $\overline{n+1}\le p$. The first case has false antecedent. In the second, the numeral order calculation in F3 gives $\bar{n}\le p$; the positive check at n witnesses the consequent. Q thus proves the right side for every p and hence proves R, again a contradiction. Neither R nor its negation is provable.

For an interpretation I, define arithmetic predicates P(p,e) and N(p,e) to check proofs of the translated sentence with code e and its translated negation. The formula translation itself is primitive recursive from its finite syntactic data, so these are primitive-recursive checks; the supplied effective axiom-proof certificates are used only when translating Q theorems. Diagonalize the Rosser formula in Q using P,N. An actual proof of $R^I$ gives by the finite argument of step 1.1 a Q proof of not-R; F4 translates it to a T proof of $\mathrm{\neg }{R}^I$. An actual proof of $\mathrm{\neg }{R}^I$ is a proof of $(\mathrm{\neg }R{)}^I$, since translation commutes with negation; step 2.1 gives a Q proof of R, which F4 translates. Thus both alternatives contradict consistency in this case as well.

Construct positive/negative proof-code functions simultaneously by external induction on the fixed bounded formula. The operations on codes and proof lists are primitive recursive by F1, and F2 makes their graphs PA-provably total; F3 fixes the actual certified proof predicate. Maintain the invariant in PA: when the formula has truth value e, the e-constructor is a Q certificate for the corresponding signed numeral instance. Off the relevant truth-value case return the fixed code of the proof of $0=0$; no correctness for a wrong-sign output is asserted. Each Boolean truth-value evaluator for a fixed bounded formula is primitive recursive by nested numerical bounded loops.

For terms, form an evaluation certificate $t(\overline{\stackrel{ˉ}{x}})=\overline{t(\stackrel{ˉ}{x})}$. At zero and variables this is reflexivity. At a successor append equality congruence. For addition, recursively define A(a,0) as the instance $\bar{a}+0=\bar{a}$; A(a,b+1) concatenates A(a,b), the axiom $\bar{a}+S\bar{b}=S(\bar{a}+\bar{b})$, and equality substitution to conclude $\bar{a}+\overline{b+1}=\overline{a+b+1}$. For multiplication, at zero use the zero axiom; at b+1 append the multiplication recursion axiom, the preceding multiplication certificate and A(ab,a). PA induction on b verifies these certificate recursions line by line, including shifted premise indices. For unequal values cancel the common successor prefix by repeated injectivity and finish with $Sx\mathrm{\ne }0$; the loop bound is the smaller value. Equal values use transitivity of the evaluation equalities. Thus atomic equalities have verified positive/negative certificate constructors.

For an order atom at values a,b, if a<=b insert the numeral b-a as left-addend witness and the addition certificate. If a>b use the finite bounded-case proof for bound b and refute each equality a=i. To generate that finite-case proof uniformly, start with the zero-bound derivation in F4 (predecessor, successor-not-zero); at the successor bound concatenate the preceding case proof with the fixed derivation taking $x=0$ or $x=Sy$ and cancelling a successor in the witness equation. The analogous repeated-predecessor proof generates the other order split. Each update substitutes numerals into fixed proof templates and concatenates lists, hence is primitive recursive. PA induction on the bound verifies the final formula and all annotations. Thus this is a proof generator for F4, not an assumption that a metatheoretic scheme is already uniform. Strict order adds a negated equality.

For negation exchange the two constructors and append double negation when needed. For conjunction, its true constructor concatenates the two positive certificates and conjunction introduction; its false constructor uses the first false conjunct and the tautological implication from its negation to the negated conjunction. Disjunction is its Boolean expansion. Since the truth test selects only among these finite cases, the induction hypotheses and checking of each fixed Boolean proof block establish the invariant in PA.

Consider $\mathrm{\exists }u\le t(\bar{x})ϵ(u,\bar{x})$ and let $b=t(\bar{x})$. On truth, bounded search below b+1 returns the first true matrix value k; concatenate its positive certificate, the bound certificate k<=b, the term-evaluation proof and existential introduction. On falsity, recursively concatenate negative matrix certificates for k=0,...,b. Combine them with the uniformly generated case theorem $u\le \bar{b}\to {\bigvee }_{k\le b}u=\bar{k}$ and equality substitution to derive $\mathrm{\forall }u\le \bar{b}\mathrm{\neg }ϵ(u,\overline{\stackrel{ˉ}{x}})$, then negate the existential. The list invariant after k iterations is that exactly the first k signed instances have valid certificates with earlier premise indices. PA induction on k proves it; at b+1 the finite case proof yields the desired formula. Bounded universals are handled by the negated existential of the negated matrix. At an empty strict bound the universal certificate is the zero-case bound proof and the existential is refuted with no matrix list.

For $\sigma =\mathrm{\exists }\bar{x}\delta (\bar{x})$, a witness tuple in PA satisfies the bounded matrix, so the invariant just proved supplies a Q certificate for its numeral instance. Append one existential introduction per witness coordinate to obtain a certificate ending with the fixed sentence sigma, and existentially quantify the certificate code. This proves the concluding implication. If another formula chi is only PA-equivalent to sigma, this conclusion gives Q proofs of sigma; a target extending PA must embed those proofs and append the fixed equivalence proof to get chi. No Q proof of that equivalence is inferred.