NOTES TOWARDS AN AXIOMATIZATION OF INTUITIONISTIC ANALYSIS,
Abstract
Assuming the formalization of intuitionistic number theory to be completed and known (Kleene), this paper discusses the formalization of intuitionistic analysis (theory of free-choice sequences). Each of the two new central notions of intuitionistic analysis over and above those of intuitionistic number theory corresponds to the classical notion of number-theoretic function. Axioms to be postulated for these objects are considered. Attention is given to Kreisel's axiom system (Lectures in Modern Mathematics, 1964) which makes explicit the distinction between free-choice sequences and (computable) functions that Kleene's does not. It is shown that the argument leading to the 'purified' sequence is not valid because there is no such (Brouwer) free-choice sequence as alpha'. Kripke's scheme is shown to have as a consequence that the species of computable functions cannot be enumerated by a formula, i.e., for any formula A(n,x,y) with only three (numerical) free variables indicated.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1966
- Accession Number
- AD0647899
Entities
People
- John Myhill
Organizations
- Hughes Aircraft Company