Continuous Truth II: Reflections

In the late 1960s, Dana Scott first showed how the Stone-Tarski topological interpretation of Heyting's calculus could be extended to model intuitionistic analysis; in particular Brouwer's continuity principle. In the early '80s we and others outlined a general treatment of non-constructive objects, using sheaf models--constructions from topos theory--to model not only Brouwer's non-classical conclusions, but also his creation of "new mathematical entities". These categorical models are intimately related to, but more general than Scott's topological model. The primary goal of this paper is to consider the question of iterated extensions. Can we derive new insights by repeating the second act? In Continuous Truth I, presented at Logic Colloquium '82 in Florence, we showed that general principles of continuity, local choice and local compactness hold in the gros topos of sheaves over the category of separable locales equipped with the open cover topology. We touched on the question of iteration. Here we develop a more general analysis of iterated categorical extensions, that leads to a reflection schema for statements of predicative analysis. We also take the opportunity to revisit some aspects of both Continuous Truth I and Formal Spaces Fourman & Grayson 1982, and correct two long-standing errors therein.