Page 29 - Textos de Matemática Vol. 40

1.3. The theory BON 17
elements are natural numbers, it is useful not to depend on a pairing function which works only for these numbers.
Many presentations of BON do not contain the axiom II.(3). It is added here, since it is technically needed in Section 1.8, when we study least fixed points, and it is fully justified from the conceptional construction of applicative theories.
1.3.2 Induction principles
It is natural to consider an induction principle together with the natural num- bers. In applicative theories, we not only consider induction for arbitrary for- mulae, but also for restricted classes of formulae. The formulae induction for arbitrary Lp formulae is given as follows:
(Lp-IN) φ(0) ∧ (∀x : N.φ(x) → φ(x′)) → ∀x : N.φ(x). for every φ of Lp.
It is obvious that this form of induction can be extended to any language L containing at least the natural numbers. In this case, the official designation is (L-IN) with L replaced by the considered language; however, if the language is clear from the context we also use the generic designation (F-IN) for formulae induction.
One may also consider the following weaker principles. This is done, for instance, in the presence of quantification operators, cf. Section 1.6.
(S-IN ) f ∈P(N)∧f0=0∧(∀x:N.fx=0→f(x′)=0)→∀x:N.fx=0.
Set induction on N. P(N) is the defined notion of sets in BON, where sets correspond to characteristic functions and with the intention that an object x belongs to the set t ∈ P(N) if and only if tx = 0, cf. [Fef75, FJ93].
(O-IN) f0=0∧(∀x:N.fx=0→f(x′)=0)→∀x:N.fx=0.
(N-IN )
Operation induction on N. This form of induction corresponds to the set induction but without the condition f ∈ P(N). For that reason it is also called semiset induction.
f ∈P(N)∧f0=0∧(∀x:N.fx=0→f(x′)=0)→∀x:N.fx=0. N-induction on N. In this case the class of formulae is restricted to the
formulae of the form N(t).
(Lp -IN ) and (S-IN ) were already considered in [FJ93]. The intermediate forms of operation induction and N-induction were introduced by Ja¨ger and Strahm in [JS96]. The logical relation of these forms of induction was investi- gated in [Kah97a, Kah00] and is presented below, in Section 1.7.