Ordinal analysis is a research program wherein recursive ordinals are assigned to axiomatic theories. According to conventional wisdom, ordinal analysis measures the strength of theories. Yet what is the attendant notion of strength? In this paper we present abstract characterizations of ordinal analysis that address this question. -/- First, we characterize ordinal analysis as a partition of $\Sigma^1_1$-definable and $\Pi^1_1$-sound theories, namely, the partition whereby two theories are equivalent if they have the same proof-theoretic ordinal. We show that no equivalence (...) relation $\equiv$ is finer than the ordinal analysis partition if both: (1) $T\equiv U$ whenever $T$ and $U$ prove the same $\Pi^1_1$ sentences; (2) $T\equiv T+U$ for every set $U$ of true $\Sigma^1_1$ sentences. In fact, no such equivalence relation makes a single distinction that the ordinal analysis partition does not make. -/- Second, we characterize ordinal analysis as an ordering on arithmetically-definable and $\Pi^1_1$-sound theories, namely, the ordering wherein $T\leq U$ if the proof-theoretic ordinal of $T$ is less than or equal to the proof-theoretic ordinal of $U$. The standard ways of measuring the strength of theories are consistency strength and inclusion of $\Pi^0_1$ theorems. We introduce analogues of these notions---$\Pi^1_1$-reflection strength and inclusion of $\Pi^1_1$ theorems---in the presence of an oracle for $\Sigma^1_1$ truths, and prove that they coincide with the ordering induced by ordinal analysis. (shrink)

We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...) and the axiom of choice both for arbitrary formulae; and $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO ; but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

We introduce a new axiom called inductive dichotomy, a weak variant of the axiom of inductive definition, and analyze the relationships with other variants of inductive definition and with related axioms, in the general second order framework, including second order arithmetic, second order set theory and higher order arithmetic. By applying these results to the investigations on the determinacy axioms, we show the following. (i) Clopen determinacy is consistency-wise strictly weaker than open determinacy in these frameworks, except second order arithmetic; (...) this is an enhancement of Schweber–Hachtman separation of open and clopen determinacy into the consistency-wise separation. (ii) Hausdorff–Kuratowski hierarchy of differences of opens is faithfully reflected by the hierarchy of consistency strengths of corresponding parameter-free determinacies in the aforementioned frameworks; this result is valid also in second order arithmetic only except clopen determinacy. (shrink)