An ordinal analysis of CM and its extensions

TL;DR

This paper constructs a realisability model for Weaver's third-order arithmetic theory, providing an ordinal analysis and exploring the proof-theoretic impact of adding well-ordering axioms.

Contribution

It offers the first ordinal analysis of Weaver's formal theory and investigates the proof-theoretic strength of its extensions with well-ordering axioms.

Findings

Realisability model based on $\Sigma^1_1$-definable functions constructed.

Ordinal analysis of Weaver's theory achieved.

Extensions with well-ordering axioms increase proof-theoretic strength.

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 $\Sigma^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.