
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 freechoice sequences and (computable) functions at the lowest type. The underlying logic is an (infinitely) manysorted 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