Accession Number : AD0647901

Title :   FORMAL SYSTEMS OF INTUITIONISTIC ANALYSIS, I,

Corporate Author : HUGHES AIRCRAFT CO FULLERTON CALIF

Personal Author(s) : Myhill,John

Report Date : NOV 1966

Pagination or Media Count : 19

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.

Descriptors :   (*MATHEMATICAL LOGIC, *SEQUENCES(MATHEMATICS)), NUMBER THEORY, FUNCTIONAL ANALYSIS, IDENTITIES, METAMATHEMATICS

Subject Categories : Theoretical Mathematics

Distribution Statement : APPROVED FOR PUBLIC RELEASE