Josef Berger
Brouwer's fan theorem states that every bar is a uniform bar. We give an overview of the status of this axiom in Bishop's constructive mathematics. In particular, we describe the relationship between the fan theorem, the weak König lemma, and the uniform continuity theorem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic Mathematics BIM, and then search for statements that are, over BIM, equivalent to Brouwer's Fan Theorem or to its positive denial, Kleene's Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene's Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene's Alternative is, intuitionistically, a nontrivial extension of finding equivalents of th…
We discuss the position of intuitionistic mathematics within the field of constructive mathematics. We discuss some principles defended and used by Brouwer but rejected by Bishop, like the Coninuity Principle, the Fan Theorem and the Bar Theorem. We explain some of their consequences in the development of constructive mathematics, like the Borel Hierarchy Theorem and the Intuitionistic Ramsey Theorem. We go into the theory of measure and integration as Bishop followed in this field a path different from Brouwer's.
We present a constructive proof of Brouwer's fixed point theorem for uniformly continuous and sequentially locally non-constant functions based on the existence of approximate fixed points. And we will show that Brouwer's fixed point theorem for uniformly continuous and sequentially locally non-constant functions implies Sperner's lemma for a simplex. Since the existence of approximate fixed points is derived from Sperner's lemma, our Brouwer's fixed point theorem is equivalent to Sperner's lemma.
In this paper using Sperner's lemma for modified partition of a simplex we will constructively prove Brouwer's fixed point theorem for sequentially locally non-constant and uniformly sequentially continuous functions.
In his book, John Stillwell wrote "finding the exact strength of the Brouwer invariance theorems seems to me one of the most interesting open problems in reverse mathematics." In this article, we solve Stillwell's problem by showing that (some forms of) the Brouwer invariance theorems are equivalent to weak König's lemma over the base system ${\sf RCA}_0$. In particular, there exists an explicit algorithm which, whenever weak König's lemma is false, constructs a topological embedding of $\mathbb{R}^4$ into $\mathbb{R}^3$.
Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma
该研究在构造性反数学中证明布劳威尔不动点定理与弱柯尼希引理等价，通过推广Orevkov的构造实现推导，明确二者的构造性等价关系。
The Fan Theorem, its strong negation, and the determinacy of games
在基本直觉主义数学中，证明扇形定理等价于可数选择公理逆否命题及直觉主义决定性定理等，而克莱尼替代等价于其强否定。
It is investigated in what sense the Brouwer fixed point theorem may be viewed as a corollary of the Lawvere fixed point theorem. A suitable generalisation of the Lawvere fixed point theorem is found and a means is identified by which the Brouwer fixed point theorem can be shown to be a corollary, once an appropriate continuous surjective mapping $A' \rightarrow X^{A''}$ has been constructed for each space $X$ in a certain class of "nice" spaces for each one of which the exponential topology on $X^{A''}$ exists, and here $A'$ and $A''$ have the same carrier set and the topology on $A'$ is fine…
We present a constructive proof of Brouwer's fixed point theorem with sequentially at most one fixed point, and apply it to the mini-max theorem of zero-sum games.
In intuitionistic mathematics, the Brouwer Continuity Theorem states that all total real functions are (uniformly) continuous on the unit interval. We study this theorem and related principles from the point of view of Reverse Mathematics over a base theory accommodating higher types and Nonstandard Analysis. With regard to the bigger picture, Reverse Mathematics provides a classification of theorems of ordinary mathematics based on computability. Our aim is to provide an alternative classification of theorems based on the central tenet of Feferman's Explicit Mathematics}, namely that a proof …
We prove intuitionistic versions of the classical theorems saying that all countable closed subsets of $[-π,π]$ and even all countable subsets of $[-π,π]$ are sets of uniqueness.
In this paper we consider Kakutani's extension of the Brouwer fixed point theorem within the framework of Bishop's constructive mathematics. Kakutani's fixed point theorem is classically equivalent to Brouwer's fixed point theorem. The constructive proof of (an approximate) Brouwer's fixed point theorem relies on a finite combinatorial argument; consequently we must restrict our attention to uniformly continuous functions. Since Brouwer's fixed point theorem is a special case of Kakutani's, the mappings in any constructive version of Kakutani's fixed point theorem must also satisfy some form o…
The Principle of Open Induction on Cantor space and the Approximate-Fan Theorem
本文在直觉主义逆数学框架中研究康托空间上的开归纳原理与近似扇定理，证明前者蕴含扇定理但不可逆推，并给出两者的若干等价命题。
We study the computational content of the Brouwer Fixed Point Theorem in the Weihrauch lattice. Connected choice is the operation that finds a point in a non-empty connected closed set given by negative information. One of our main results is that for any fixed dimension the Brouwer Fixed Point Theorem of that dimension is computably equivalent to connected choice of the Euclidean unit cube of the same dimension. Another main result is that connected choice is complete for dimension greater than or equal to two in the sense that it is computably equivalent to Weak Kőnig's Lemma. While we can p…
Extending Martín Escardó's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a functional of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ in Gödel's System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name $λ$-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue tree…
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of "adjoint logic" in which the discretization and codiscretization modalities are characterized using a judgmental formalism of "crisp variables". This yields type theories that we call "spatial" and "cohesive", in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the "fundamental $\infty$-groupoid" or "shape"), disentangling the "iden…
Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which separates all of the as yet identified fan theorems.
The strong continuity principle reads "every pointwise continuous function from a complete separable metric space to a metric space is uniformly continuous near each compact image." We show that this principle is equivalent to the fan theorem for monotone $Π^{0}_{1}$ bars. We work in the context of constructive reverse mathematics.
We develop a realizability model in which the realizers are the reals not just Turing computable in a fixed real but rather the reals in a countable ideal of Turing degrees. This is then applied to prove several separation results involving variants of the Fan Theorem.
The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is stronger than the decidable fan theorem (DFT); however, Loeb [Ann. Pure Appl. Logic, 132(1):51-66, 2005] has shown that the two principles become equivalent with a suitable coding of "continuous functions" as type-one objects. The question remains whether DFT can be characterised by a weaker version of UCT using a natural subclass of pointwise continuous functions without such a coding. We show that when "pointwise co…
We generalize the finite version of Gowers' Ramsey theorem to multiple tetris-like operations and apply it to show that a group of homeomorphisms that preserve a "typical" linear order of branches of the Lelek fan, a compact connected metric space with many symmetries, is extremely amenable.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。