Page 32 - Textos de Matemática Vol. 40

20 Chapter 1. Applicative theories
here, we do not have any such restrictions on the syntactic level. However, we can “reintroduce” types just as predicates or formulae, but now, the fact that a term belong to a certain type has to be proven within the framework, based on the axiomatization for the type in question. Later on, we will introduce an defined notion of “classes” in Section 1.8 which serves as types in this sense. Here, we can already refer to the predicate N axiomatized in BON.
Axiomatized natural numbers. The described treatment of types is ex- emplified in BON for the natural numbers. A term t belongs to “the natural numbers”—“is of type N”—if N(t) is provable in BON. The axioms may be read in the way, that 0 and sN are constructors, while pN and dN (with respect to its first two arguments) are functions defined on this datatype.
Binary words. As an alternative to the natural numbers, we like to present here how binary words can be axiomatized in an applicative theory as they were introduced by Strahm [Str01]. Therefore, we replace the predicate N by a pred- icate W (binary word) and the constants 0, sN, dN, and pN by ε (empty word), s0, s1 (binary successors), dW (definition by cases on W), pW (binary predecessor), sl, pl (lexicographic successor and predecessor), c⊆ (initial subword relation), lW (tally length), ∗ (word concatenation), and × (word multiplication). With the analogous abbreviations as for N, we have as axioms the following ones:
III. Definition by cases on W.
(5) W(v)∧W(w)∧v=w→dWxyvw=x,
(6) W(v)∧W(w)∧v̸=w→dWxyvw=y.
IV. Closure, binary successors and predecessor.
(7) W(ε) ∧ ∀x : W.W(s0 x) ∧ W(s1 x), (8) s0x̸=s1x∧s0x̸=ε∧s1x̸=ε, (9) (pW :W→W)∧pWε=ε,
(10) W(x)→pW(s0x)=x∧pW(s1x)=x,
(11) W(x)∧x̸=0→s0(pWx)=x∨s1(pWx)=x.
V. Lexicographic successor and predecessor.
(12) (sl :W→W)∧slε=s0ε,
(13) W(x)→sl(s0x)=s1x∧sl(s1x)=s0(slx), (14) (pl :W→W)∧pWε=ε,
(15) W(x)→pl(slx)=x,
(16) W(x)∧x̸=0→sl(plx)=x.
VI. Initial subword relation.
(17) W(x)∧W(y)→c⊆xy=s0ε∨c⊆xy=s1ε,