nLab bar induction

Redirected from "full bar theorem".

Context

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

Analysis

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

 Idea

A family of axioms in constructive mathematics which are provable from the principle of excluded middle. They imply their respective versions of the fan theorem, since bar induction is about Baire space while the fan theorem is about Cantor space, which is a subspace of Baire space.

This page should contain the classical proof of full bar induction, as well as Brouwer’s reasoning for why bar induction should hold.

Definition

Let *\mathbb{N}^* denote the list of natural numbers. A bar is a subset P *P \subseteq \mathbb{N}^* such that for all sequences α\alpha of natural numbers, there exists a natural number nn such that the list of all α(i)\alpha(i) for all i<ni \lt n is in PP. A bar PP is inductive if for all lists a *a \in \mathbb{N}^* and all natural numbers nn \in \mathbb{N}, if the concatenation of aa with nn is in PP, then aa is in PP. Finally, a bar PP is monotone if for all lists a,b *a, b \in \mathbb{N}^*, if aa is in PP, then the concatenation of aa and bb is in PP.

  • The principle of decidable bar induction or decidable bar theorem states that every bar which is a detachable subset of *\mathbb{N}^* is inductive.

  • The principle of monotone bar induction or monotone bar theorem states that every monotone bar is inductive.

  • The principle of Σ 1 0\Sigma_1^0 bar induction or Σ 1 0\Sigma_1^0 bar theorem states that every bar which is a semi-decidable subset of *\mathbb{N}^* is inductive.

  • The principle of full bar induction or full bar theorem states that every bar is inductive.

Properties

Σ 1 0\Sigma_1^0 bar induction and thus the full bar induction implies the limited principle of omniscience for the natural numbers LPO \mathrm{LPO}_\mathbb{N}.

 References

  • L. E. J. Brouwer. Uber Definitionsbereiche von Funktionen. Mathematische Annalen, 97:60–75, 1927.

  • W. A. Howard and G. Kreisel. Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Log., 31(3):325–358, 1966.

  • W. W. Tait. Constructive reasoning. In B. V. Rootselaar and J. Staal, editors, Logic, Methodology and Philosophy of Science III, Studies in Logic and the Foundations of Mathematics, pages 185–200, Amsterdam, 1968. North-Holland.

  • Michael Fourman, Martin Hyland, Sheaf Models for Analysis , pp.280-301 in Fourman, Mulvey, Scott (eds.), Applications of Sheaves , LNM 753 Springer Heidelberg 1979. (draft, 6.64 MB)

  • Benno van den Berg, Ieke Moerdijk, Derived rules for predicative set theory: an application of sheaves (arXiv:1009.3553)

  • Michael Rathjen, Pedro Francisco Valencia Vizcaino?, Well ordering principles and bar induction (arXiv:1405.4485)

  • Tatsuji Kawai?, Giovanni Sambin, The principle of pointfree continuity, Logical Methods in Computer Science, Volume 15, Issue 1 (March 5, 2019). (doi:10.23638/LMCS-15%281%3A22%292019, arXiv:1802.04512)

  • Tatsuji Kawai?, Principles of bar induction and continuity on Baire space (arXiv:1808.04082)

  • Tatsuji Kawai?, Representing definable functions of HA ω\mathrm{HA}^\omega by neighbourhood functions (arXiv:1901.11270)

  • Joan Rand Moschovakis?, Solovay’s Relative Consistency Proof for FIM and BI (arXiv:2101.05878)

  • Nuria Brede?, Hugo Herbelin, On the logical structure of choice and bar induction principles, LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy. (arXiv:2105.08951)

Last revised on July 26, 2024 at 23:45:21. See the history of this page for a list of all contributions to it.