Page 33 - Textos de Matemática Vol. 40

1.3. The theory BON 21
(18) W(x)→(c⊆xε↔x=ε),
(19) W(x)∧W(y)∧y̸=ε→(c⊆xy↔c⊆x(pWy)∨x=y), (20) W(x)∧W(y)∧W(z)∧c⊆xy∧c⊆yz→c⊆xz.
VII. Tally length of binary words.
(21) (lW :W→W)∧lWε=ε,
(22) W(x)→lW(s0x)=s1(lWx)∧lW(s1x)=s1(lWx), (23) W(x)∧lWx=x→lW(slx)=s1x,
(24) W(x)∧lWx̸=x→lW(slx)=lWx,
(25) W(x)∧W(y)→c⊆(lWx)(lWy)∨c⊆(lWy)(lWx).
VIII. Word concatenation.
(26) (∗:W2 →W),
(27) W(x)→x∗ε=x,
(28) W(x)∧W(y)→x∗(s0y)=s0(x∗y)∧x∗(s1y)=s1(x∗y).
IX. Word multiplication.
(29) (×:W2 →W),
(30) W(x)→x×ε=ε,
(31) W(x)∧W(y)→x×(s0y)=(x×y)∗x∧x×(s1y)=(x×y)∗x.
This axiomatization of binary words forms the basis for applicative theories which characterize different classes of computational complexity depending on different forms of induction and the presence or absence of word multiplication, cf. [Str01, Str03]; see also [Str97, Can00, Str04, Can05a].
Totality. The total version BON is called TON and introduced and stud- ied in [JS95b], see also [Can96, Str96a, Can05b]. TON is formally introduced in the language where the definedness predicate is dropped; it is based on classi- cal logic with equality instead of the logic of partial terms; the axiom I.(2) for the s combinator is replaced by its total version and the axiom II.(3) is, obvi- ously, omitted. However, it is an easy exercise to check that TON is equivalent to BON + (Tot). It is shown in [JS95b] that the presence of (Tot) does not change the proof-theoretic strength of BON and of several of its extensions in the presence of natural forms of induction.
The theory PRON. In analogy to BON one can define a theory comprising natural numbers, definition by cases, and primitive recursion over the primitive- recursive application relation given by the combinators k, i, a, b, p0, and p1 and the binary operation expressed by ⟨·, ·⟩ described above, cf. [Sch95, Def. 5.3] and [Ste01, SS06]. The resulting theory was called PEA+ + (r) by Schlu¨ter and renamed PRON in [Ste01, SS06].