CHOICE AND UNIFORMITY IN WEAK APPLICATIVE THEORIES

We are concerned with first order theories of operations, based on combinatory logic and extended with the type W of binary words. The theories include forms of “positive” and “bounded” induction on W and naturally characterize primitive recursive and polytime functions (respectively). We prove that the recursive content of the theories under investigation (i.e. the associated class of provably total functions on W) is invariant under addition of 1. an axiom of choice for operations and a uniformity principle, restricted to positive conditions; 2. a (form of) self-referential truth, providing a fixed point theorem for predicates. As to the proof methods, we apply a kind of internal forcing semantics, non-standard variants of realizability and cut-elimination.