Effective theories and certified numerical proof codes

Fix an effectively presented countable finite-arity signature whose symbol-kind and arity tests are primitive recursive in the sense of Bounded arithmetic formulas. Fix a primitive-recursive certificate predicate $E(a,w)$; the nonlogical axioms are the sentences $a$ for which $\mathrm{\exists }wE(a,w)$. A certified proof is a derivation of Formal proofs from sentence theories together with an $E$-certificate at each nonlogical axiom line. A c.e. enumeration can be presented this way by including a finite computation history; no decision procedure for axiom membership is assumed.

For a binary word $w$, put $c(w)=1^{\mathrm{\mid }w\mathrm{\mid }}0w$. Let $\mathrm{bin}(0)=0$, and otherwise use the canonical binary numeral. The code of $(a_0,\dots ,a_{k-1})$ is the natural number whose binary word is

$11^{k}0c(\mathrm{bin}(a_0))\cdots c(\mathrm{bin}(a_{k-1}))\mathrm{.}$

The empty-list code is $2$. Tokens, annotations and lists of lines are encoded by iterating this list convention. Invalid codes have validity false, length zero and all coordinates zero. An out-of-range coordinate is zero. Append and concatenation return the empty code $2$ if an input list is invalid.

The initial sentinel prevents leading-zero ambiguity. The following well-definedness lemma proves unique decoding and primitive-recursive operations; these are not consequences of the bare phrase “effective coding.”