Page 42 - Textos de Matemática Vol. 40

30 Chapter 1. Applicative theories
in general by Barwise [Bar75], and its use for proof theory was elaborated first of all by Ja¨ger [J¨ag86]. As a theory for the constructible hierarchy L, Kripke- Platek is obtained from Zermelo-Fraenkel by leaving out the power set axiom and restricting Separation and Collection to ∆0 formulae.
Without giving more details about these theories—for the proof-theoretic analysis of several theories comparable with theories in explicit mathematics, cf. e.g., [J¨ag86, Poh96, Poh98, Rat91, Rat94, JS01]—we would like to mention only two crucial parallelisms to concepts considered here:
The first one is the axiom of foundation (or ∈-induction). It turned out that KP without foundations allows the definition of proof-theoretic weak the- ories. We have the analogous situation in explicit mathematics, where the ad- dition of induction principles—like inductive generation, name induction, or leastness of universes—shifts the theories from the (meta)predicative to the im- predicative “world”.
The second one is the concept of admissible sets which corresponds to universes in explicit mathematics as well as in the Truth Theories. In particular, the axiom which guarantees the existence of admissible sets in Kripke-Platek set theory, the limit axiom, is the heuristic origin of the limit axioms which we consider in explicit mathematics and in the truth theories.
1.6 Quantification operators
In the following we work in extensions of BON, which include the rN and the axiom for primitive recursion, and the following new constants for functionals of higher type:
• μ,E0,E#0 ,andE1.
Such operators are well-known from higher recursion theory, cf. e.g., [KM77].
1.6.1 The non-constructive μ and related operators
It has been convincingly argued in a series of articles, for example in Feferman [Fef75, Fef85, Fef88b], that strong operation existence axioms are needed for a smooth development of classical mathematics in applicative theories.
One of these higher type operators is the non-constructive μ operator. It allows to determine a zero of a total function. But in contrast to the recursion theoretic μ operator (for which we used the designation μrec) it returns also a value in N if the function is total but has no zero. Starting from investigations in [Fef75, Fef85] it is discussed in applicative theories in [FJ93, FJ96, GS96]. Here we use a slightly strengthened form of μ, like in [JS96], which involves also a test for total functions. It is axiomatized as follows: