Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.20115

A Reflection Calculus for Bar Induction and the Linearity of Consistency Strength Ordering

Fedor Pakhomov·Vlad Lazar
View original source ↗Read source document ↗Export metadata ↓

Abstract

We introduce a novel extension of reflection calculus, $\mathsf{RC_{BI}}$, to analyze a family of extensions of $\mathsf{ACA}_0$ generated by uniform $ω$-model and syntactic reflection principles, together with several other related operators. The union of these theories coincides with the theory of Bar Induction ($\mathsf{BI}$). We prove that $\mathsf{RC_{BI}}$ is arithmetically sound, and that it is sound and complete with respect to a natural class of Kripke models. Leveraging these modal semantics, we demonstrate that the class of theories denoted by $\nabla$-free closed formulas is a pre-wellordering with respect to $Π^1_1$-soundness and consistency strength. This allows us to establish an ordinal analysis for $\mathsf{BI}$ and its fragments, analogous to Beklemishev's analysis of $\mathsf{PA}$. The structural properties of $\mathsf{RC_{BI}}$ naturally give rise to a novel ordinal notation system for the Bachmann-Howard ordinal which differs substantially from existing representations.

Explore related subjects

math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Fedor Pakhomov, Vlad Lazar. 2026-10-14. A Reflection Calculus for Bar Induction and the Linearity of Consistency Strength Ordering. https://arxiv.org/abs/2610.20115

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Convex Team Logics

We prove expressive completeness results for convex propositional and modal team logics, where a logic is convex if, for each formula, if it is true in two teams $t$ and $u$ and $t\subseteq s\subseteq u$, then it is also true in $s$. We introduce propositional/modal team logics which are expressively complete for the class of all convex propositional/modal team properties. We also answer an open question concerning the expressive power of classical propositional logic extended with the nonemptiness atom NE: we show that it is expressively complete for the class of all convex and union-closed properties. A modal analogue of this result additionally yields an expressive completeness theorem for Aloni's (2022) Bilateral State-Based Modal Logic. There is a specific sense in which one of the propositional convex logics we introduce extends propositional dependence logic; this sense corresponds to the existence of a compositional translation between the two logics. Another of the convex logics extends propositional inquisitive logic in the same manner. We generalize the notion of uniform definability, as considered in the team semantics literature, to formalize this notion of compositional extension.

math.LO↗
arXiv2026

Hindman and Owings-like theorems without the Axiom of Choice

We investigate Hindman- and Owings-type Ramsey-theoretic statements in Zermelo-Fraenkel set theory without the Axiom of Choice, with some occasional extra assumptions (such as the Axiom of Dependent Choice and/or the Axiom of Determinacy). We study several variations of Hindman's theorem on $\mathbb Q$-vector spaces; notably, we show that the uncountable analog of Hindman's theorem fails for the additive group of $\mathbb R$ (under ZF), and for $\mathbb Q$-vector spaces of uncountable dimension (under DC if such dimension is not well-orderable), among other results. In contrast, for Owings-type configurations, we obtain several positive results, especially when assuming AD. These results highlight the interaction between determinacy, algebraic structure, and dimension in the study of infinite Ramsey theory without the Axiom of Choice.

math.LO↗
arXiv2026

Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma

In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point theorem, the construction of a continuous function on the unit square without fixed points due to Orevkov [Soviet Math. Doklady (1963), 1253--1256] is generalised to yield a uniformly continuous function on the unit square whose fixed points encode information about infinite paths of a given infinite tree.

math.LO↗