topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
further
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.
Let denote the list of natural numbers. A bar is a subset such that for all sequences of natural numbers, there exists a natural number such that the list of all for all is in . A bar is inductive if for all lists and all natural numbers , if the concatenation of with is in , then is in . Finally, a bar is monotone if for all lists , if is in , then the concatenation of and is in .
The principle of decidable bar induction or decidable bar theorem states that every bar which is a detachable subset of is inductive.
The principle of monotone bar induction or monotone bar theorem states that every monotone bar is inductive.
The principle of bar induction or bar theorem states that every bar which is a semi-decidable subset of is inductive.
The principle of full bar induction or full bar theorem states that every bar is inductive.
bar induction and thus the full bar induction implies the limited principle of omniscience for the natural numbers .
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 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.