FORMAL SYSTEMS OF INTUITIONISTIC ANALYSIS, I,
HUGHES AIRCRAFT CO FULLERTON CALIF
Pagination or Media Count:
Various possible formalizations of existing intuitionistic mathematics Heyting, Kleene, Kreisel are compared. An axiomatization is presented that is obtained from Kreisels by dropping the continuity axiom and adding Kripkes schema with several other innovations, the most important of which is the introduction of a new primitive idea of lawfulness symbolized by D. Roughly, Dt, where t is any kind of term, says that t is determined by a law rather than a free choice or choices. This extends to arbitrary finite types Kreisels distinction between free-choice sequences and computable functions at the lowest type. The underlying logic is an infinitely many-sorted intuitionistic functional calculus with identity. Modifications of the formalization of impredicative intuitionism are given for a formalization of predicative intuitionism.
- Theoretical Mathematics