Primitive-recursive syntax and certified proof checking

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.