THE ITERATION OF THE MATHEMATICAL PROCESS

Source abstract

Abstract In the opening sections of Das Kontinuum , Hermann Weyl describes the formation of the mathematical universe as shaped by two generative procedures: the logical process and the mathematical process. These procedures can be iterated, providing a conceptual motivation for the ramified hierarchy. In this paper, we offer a detailed analysis of Weyl’s ideas and present a formalization of the theory resulting from the iteration of the logical–mathematical process. We explore not only the variant based on classical logic, explicitly considered in Das Kontinuum , but also a constructive counterpart. Furthermore, we show that a restricted version of Weyl’s procedure gives rise to a theory that is conservative over the system ACA 0 $\mathbf {ACA}_0$ bold upper A upper C upper A 0 , while the unrestricted version can be interpreted within a certain fragment of Homotopy Type Theory. This provides a precise analysis of the iteration of the mathematical process and establishes a robust link with modern formal systems. Philosophically, our work clarifies the notion of predicativity as conceived by Weyl in this context and highlights its relationship with the logic underlying the process. To this end, we study a version of the Axiom of Reducibility recently introduced by Palmgren.