FORMAL SYSTEMS OF INTUITIONISTIC ANALYSIS, I,
Abstract
Various possible formalizations of existing intuitionistic mathematics (Heyting, Kleene, Kreisel) are compared. An axiomatization is presented that is obtained from Kreisel's by dropping the continuity axiom and adding Kripke's 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 Kreisel's 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1966
- Accession Number
- AD0647901
Entities
People
- John Myhill
Organizations
- Hughes Aircraft Company