Choice in applicative theories
Publication date
1989-09
Authors
Renardel de Lavalette, G.R.
Editors
Advisors
Supervisors
DOI
Document Type
Preprint
Metadata
Show full item recordCollections
License
Abstract
TAPP is a total applicative theory, conservative over intuitionistic arithmetic. In
this paper, we first show that the same holds for TAPP + the choice principle
EAC; then we generalize this to TAPP + inductive definitions. Finally, we use
TAPP to show that P.Martin-Löfs basic extensional theory MLp is conservative
over intuitionistic arithmetic.
Keywords
applicative theory, intuitionism, constructivism, metamathematics, Heyting's arithmetic, realizability, Skolem functions, forcing, inductive definitions, theory of types, extensional types, extensional realizability