Page 19 - Textos de Matemática Vol. 40

Chapter 1 Applicative theories
Under the name applicative theories several first order theories are collected, which have as common basis a specific partial logic and a term language built on combinators. Specific applicative theories are defined by adding new constants (combinators) and predicates together with characterizing axioms. These the- ories form the first order part of Feferman’s systems of explicit mathematics, introduced in [Fef75, Fef79]. The reference theory is called basic theory of opera- tions and numbers, BON, which was introduced in Feferman and Ja¨ger [FJ93] as the classical version of Beeson’s theory EON without induction, [Bee85]. It is based on Beeson’s logic of partial terms and the term language of BON is built on (partial) combinatory algebra. A short survey of results on applicative theories may be found in Ja¨ger, Kahle, and Strahm [JKS99].
1.1 The logic of partial terms
The logic of partial terms, LPT, was introduced by Beeson, [Bee85]. Its spe- cific feature is a definedness predicate ↓ (also called existence predicate). The quantifiers of LPT are restricted to objects which are defined in the sense of this predicate. The logic is strict, i.e., if a complex term is defined then all its subterms have to be defined. Intuitively the definedness predicate t ↓ could be interpreted, for instance, as termination of a computation given by t. For a philosophical motivation of the logic of partial terms, we refer to Feferman, [Fef95].
1.1.1 A language for applicative theories
A language L for an applicative theory is a first order language, comprising:
1. asetofcountablymany(individual)variables(x,y,z,u,v,f,g,h,...(pos- sibly with subscripts)),
7