Functions, Ordinals, Species

摘要: Publisher Summary This chapter discusses the proof theory of formal classical analysis, formulated as a two-sorted axiomatic with variables for natural numbers and number theoretic functions basic relations equality function evaluation. The analyses notion free choice sequence in terms which continuous are defined have shown that evident axioms sequences unexpectedly weak ; particular, some theorems A, A’ cannot be derived from known axioms. purpose present is to summarize work past ten years on proposal put results perspective by comparing them other subsystems.