Page 20 - Textos de Matemática Vol. 40
P. 20
8
2.
3. 4.
5. 6. 7.
Chapter 1. Applicative theories
a set of maximal countably many (individual) constants
(to which at least the combinators k and s should belong, cf. the following Section 1.2, but also the remark in the Subsection 1.2.2),
a binary function symbol · for term application,
a set of maximal countably many relation symbols (with assigned arity),
to which at least the following ones belong:
(a) the unary relation symbol ↓ (definedness) and (b) the binary relation symbol = (equality),
the logical connectives ¬ and ∧,
the universal quantifier ∀, and
parentheses, point and comma as auxiliary symbols.
It is one of the characteristics of applicative theories that the language may, in principle, be arbitrarily extended by new constants and relation sym- bols. Normally, the language will comprise next to the combinators k and s also constants for pairing and axiomatized natural numbers, see below Section 1.3. However, sometimes it is more natural to replace the natural numbers by an- other datatype. This is done, for instance, in the analysis of theories with restricted computational complexity by Strahm, where binary words are used instead of natural numbers. It is essential for applicative theories that we do not add further function symbols besides the term application (of course, the logic of partial terms could be considered for arbitrary (countable) sets of function symbols, cf. e.g., [J¨ag97]). In fact, functions may be introduced only by use of new constants, such that the function application has to use the well-known method called Currying (going back to Frege and Scho¨nfinkel), where the arguments are successively given by use of the application operation. As a con- sequence, every constant introduced to represent a function may also appear as argument. In particular, each constant may be applied to itself. Therefore, self- application is always allowed in an applicative theory, see also Subsection 1.1.3 below.
Terms. As usual, terms (r, s, t, . . .) of a language L are built inductively from individual variables and individual constants by use of the function symbol for term application. As a rule, we write s t for ·(t, s) or the infix notation (s · t) with the convention of association to the left.
Formulae. The atomic formulae are built by use of relations symbols. For the definedness predicate we will use the postfix notation t ↓ and for the equality the infix notation t = s.
The formulae (φ,ψ,...) of a language L are built by closing the atomic formulae under ¬ (negation), ∧ (conjunction), and ∀ (universal quantification).