Models and Interpretations of (Intuitionistic) "Analysis"
Joan Rand Moschovakis · 2011
Historically, intuitionistic analysis (INT) was Brouwer’s effort to understand constructively the structure of the continuum. He represented real numbers by Cauchy sequences of rationals, rejected arbitrary use of the law of excluded middle in logical reasoning, accepted full induction on the natural numbers ω and monotone bar induction on the “universal spread ” ω ω of all choice sequences, accepted countable and dependent choice... and then asserted that every total function on the universe of choice sequences must be continuous. This last step forced Brouwer to reject his own fixed point theorem and led to other bizarre conclusions, such as that the relation of inequality between real numbers does not satisfy the law of comparability. On the other hand, Brouwer was able to give a constructive proof of e.g. the Jordan Curve Theorem, he had no problem using reductio ad absurdum to derive negative conclusions, and his proofs of existential assertions always provided (constructive approximations to) witnesses. This last property was given primary importance by Errett Bishop, who developed a cautious constructivism (BISH) which neither condones nor violates Brouwer’s continuity principle. Separately, the classical continuum, the intuitionistic continuum, and even the recursive continuum satisfy BISH, which has been described as “mathematics using intuitionistic logic. ” Brouwer and Bishop worked informally, leaving natural questions about consistency and relative independence for logicians to answer if they cared. The point of this talk is to show how some of these consistency and independence questions have been answered for theories between two-sorted intuitionistic arithmetic IA1 and the intuitionistic formal system I of [Kleene and Vesley 1965], with some consequences for constructive analysis. The tools which have been used for this purpose include ◮ classical models,