Bar Induction

Definition

Let ${\mathbb{N}}^{\ast }$ be the set of finite sequences of natural numbers. A subset $B\subseteq {\mathbb{N}}^{\ast }$ is a bar if for every infinite sequence $\alpha \in {\mathbb{N}}^{\mathbb{N}}$, there exists an initial segment $\alpha [n]\in B$. Let $P$ be a predicate on ${\mathbb{N}}^{\ast }$. The principle of Bar Induction asserts that if:

1. $B$ is a bar such that $\forall \sigma \in B,P(\sigma )$ (Base case), and
2. $\forall \sigma \in {\mathbb{N}}^{\ast },(\forall n\in \mathbb{N},P(\sigma \ast ⟨n⟩))\to P(\sigma )$ (Inductive step), then $P(⟨⟩)$ holds.

Context

This principle extends induction to well-founded tree that are not necessarily finitely branching. It validates reasoning about objects defined by such trees. The Fan Theorem is often derived from Bar Induction restricted to decidable bars on binary trees, combined with the observation that a finitely branching tree with no infinite path is finite (Kőnig’s Lemma), which holds intuitionistically only in specific forms.

References

• Kleene, S. C., & Vesley, R. E. (1965). The Foundations of Intuitionistic Mathematics.
• Troelstra, A. S., & van Dalen, D. (1988). Constructivism in Mathematics.
• Brouwer, L. E. J. (1927). Über Definitionsbereiche von Funktionen.
• dummett2000-intuitionism