PA verifies proof certificates for bounded arithmetic truth

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.