NOTES TOWARDS AN AXIOMATIZATION OF INTUITIONISTIC ANALYSIS,
HUGHES AIRCRAFT CO FULLERTON CALIF
Pagination or Media Count:
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 Kreisels axiom system Lectures in Modern Mathematics, 1964 which makes explicit the distinction between free-choice sequences and computable functions that Kleenes 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. Kripkes 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 An,x,y with only three numerical free variables indicated.
- Theoretical Mathematics