An ordinal analysis of CM and its extensions
Shuwei Wang
TL;DR
This work develops a realizability-based ordinal analysis of Weaver's CM, a third-order intuitionistic arithmetic for mathematical conceptualism, by encoding $Σ^1_1$-definable partial functions and building a multilevel realizability model. It clarifies the CM axioms, the role of $Σ^1_1$-definable function codes, and how CM sits relative to $Σ^1_1$-$AC$/$DC$, yielding an exact strength bound $|CM| = φ_{ε_0}(0)$. The paper then introduces a global well-ordering extension (GWO) with axioms W1–W3 and proves a Zorn-like lemma within CM+GWO, analyzing the impact on strength and linking it to BI via an ATR/BI-based ordinal analysis. It shows that CM+GWO attains the Bachmann–Howard ordinal $θ_{ε_{Ω+1}}(0)$, and that removing the countable-initial-segments axiom (W3) reduces this strength, highlighting the indispensable role of W3 for maximal predicative reach. The discussion culminates in a nuanced treatment of impredicativity and the prospects for weaker, yet mathematically robust, fragments between CM and CM+GWO.
Abstract
In arXiv:0905.1675, Nik Weaver proposed a novel intuitionistic formal theory of third-order arithmetic as a formalisation of his philosophical position known as mathematical conceptualism. In this paper, we will construct a realisability model from the partial combinatory algebra of $Σ^1_1$-definable partial functions and use it to provide an ordinal analysis of this formal theory. Additionally, we will examine possible extensions to this system by adding well-ordering axioms, which are briefly mentioned but never thoroughly studied in Weaver's work. We aim to use the realisability arguments to discuss how much such extensions constitute an increase from the original theory's proof-theoretic strength.