-
(Seemingly) Impossible Theorems in Constructive Mathematics
Authors:
Hannes Diener,
Matthew Hendtlass
Abstract:
We prove some constructive results that on first and maybe even on second glance seem impossible.
We prove some constructive results that on first and maybe even on second glance seem impossible.
△ Less
Submitted 11 April, 2019;
originally announced April 2019.
-
Rectifiability and finite variation
Authors:
Matthew Hendtlass
Abstract:
We show that the length of a path in $ \mathbf{R}^2 $ can be computed if and only if its variation in every direction can.
We show that the length of a path in $ \mathbf{R}^2 $ can be computed if and only if its variation in every direction can.
△ Less
Submitted 29 May, 2018;
originally announced June 2018.
-
The Third Trick
Authors:
Hannes Diener,
Matthew Hendtlass
Abstract:
We prove a result, similar to the ones known as Ishihara's First and Second Trick, for sequences of functions.
We prove a result, similar to the ones known as Ishihara's First and Second Trick, for sequences of functions.
△ Less
Submitted 8 August, 2022; v1 submitted 30 January, 2018;
originally announced January 2018.
-
Equivalents of disjunctive Markov's principle
Authors:
Matthew Hendtlass
Abstract:
The purpose of this short note is to point out a rich source of natural equivalents of the weak semi-intuitionistic principle MP$^\vee$ in reverse constructive mathematics: many simple theorems from Euclidean geometry when read classically (for example with $<$ interpreted as $\leqslant$ and $\neq$) are equivalent to disjunctive Markov's principle MP$^\vee$. We give an example of this phenomenon.
The purpose of this short note is to point out a rich source of natural equivalents of the weak semi-intuitionistic principle MP$^\vee$ in reverse constructive mathematics: many simple theorems from Euclidean geometry when read classically (for example with $<$ interpreted as $\leqslant$ and $\neq$) are equivalent to disjunctive Markov's principle MP$^\vee$. We give an example of this phenomenon.
△ Less
Submitted 8 November, 2016;
originally announced November 2016.
-
Constructing the demand function of a strictly convex preference relation
Authors:
Matthew Hendtlass
Abstract:
We give conditions under which the demand function of a strictly convex preference relation can be constructed.
We give conditions under which the demand function of a strictly convex preference relation can be constructed.
△ Less
Submitted 8 November, 2016;
originally announced November 2016.
-
On the construction of general equilibria in a competitive economy
Authors:
Matthew Hendtlass,
Nazar Miheisi
Abstract:
This paper gives a constructive treatment of McKenzie's theorem on the existence of general equilibria. While the full theorem does not admit a constructive proof, and hence does not admit a computational realisation, we show that if we strengthen the conditions on our preference relation---we require $\succ$ to be uniformly rotund in the sense of Bridges [5]---then we can find `approximate equili…
▽ More
This paper gives a constructive treatment of McKenzie's theorem on the existence of general equilibria. While the full theorem does not admit a constructive proof, and hence does not admit a computational realisation, we show that if we strengthen the conditions on our preference relation---we require $\succ$ to be uniformly rotund in the sense of Bridges [5]---then we can find `approximate equilibrium points,' points at which the collective profit may not be maximal, but can be made arbitrarily close to being maximal.
△ Less
Submitted 8 November, 2016;
originally announced November 2016.
-
Kakutani's fixed point theorem in constructive mathematics
Authors:
Matthew Hendtlass
Abstract:
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 unifo…
▽ More
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 of uniform continuity. We discuss the difficulties involved in finding an appropriate notion of uniform continuity, before giving a constructive version of Kakutani's fixed point theorem which is classically equivalent to the standard formulation. We also consider the reverse constructive mathematics of Kakutani's fixed point theorem, and provide a constructive proof of Kakutani's first application of his theorem---a generalisation of von Neumann's minimax theorem.
△ Less
Submitted 8 November, 2016;
originally announced November 2016.
-
Weak König's lemma implies the uniform continuity theorem: a direct proof
Authors:
Matthew Hendtlass
Abstract:
We show in Bishop's constructive mathematics---in particular, using countable choice---that weak König's lemma implies the uniform continuity theorem.
We show in Bishop's constructive mathematics---in particular, using countable choice---that weak König's lemma implies the uniform continuity theorem.
△ Less
Submitted 8 November, 2016;
originally announced November 2016.
-
On the Uniform Computational Content of the Baire Category Theorem
Authors:
Vasco Brattka,
Matthew Hendtlass,
Alexander P. Kreuzer
Abstract:
We study the uniform computational content of different versions of the Baire Category Theorem in the Weihrauch lattice. The Baire Category Theorem can be seen as a pigeonhole principle that states that a complete (i.e., "large") metric space cannot be decomposed into countably many nowhere dense (i.e., "small") pieces. The Baire Category Theorem is an illuminating example of a theorem that can be…
▽ More
We study the uniform computational content of different versions of the Baire Category Theorem in the Weihrauch lattice. The Baire Category Theorem can be seen as a pigeonhole principle that states that a complete (i.e., "large") metric space cannot be decomposed into countably many nowhere dense (i.e., "small") pieces. The Baire Category Theorem is an illuminating example of a theorem that can be used to demonstrate that one classical theorem can have several different computational interpretations. For one, we distinguish two different logical versions of the theorem, where one can be seen as the contrapositive form of the other one. The first version aims to find an uncovered point in the space, given a sequence of nowhere dense closed sets. The second version aims to find the index of a closed set that is somewhere dense, given a sequence of closed sets that cover the space. Even though the two statements behind these versions are equivalent to each other in classical logic, they are not equivalent in intuitionistic logic and likewise they exhibit different computational behavior in the Weihrauch lattice. Besides this logical distinction, we also consider different ways how the sequence of closed sets is "given". Essentially, we can distinguish between positive and negative information on closed sets. We discuss all the four resulting versions of the Baire Category Theorem. Somewhat surprisingly it turns out that the difference in providing the input information can also be expressed with the jump operation. Finally, we also relate the Baire Category Theorem to notions of genericity and computably comeager sets.
△ Less
Submitted 24 August, 2016; v1 submitted 7 October, 2015;
originally announced October 2015.
-
Reverse mathematics, well-quasi-orders, and Noetherian spaces
Authors:
Emanuele Frittaion,
Matt Hendtlass,
Alberto Marcone,
Paul Shafer,
Jeroen Van der Meeren
Abstract:
A quasi-order $Q$ induces two natural quasi-orders on $P(Q)$, but if $Q$ is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq showed that moving from a well-quasi-order $Q$ to the quasi-orders on $P(Q)$ preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the i…
▽ More
A quasi-order $Q$ induces two natural quasi-orders on $P(Q)$, but if $Q$ is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq showed that moving from a well-quasi-order $Q$ to the quasi-orders on $P(Q)$ preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the induced quasi-orders on $P(Q)$ are Noetherian, which means that they contain no infinite strictly descending sequences of closed sets. We analyze various theorems of the form "if $Q$ is a well-quasi-order then a certain topology on (a subset of) $P(Q)$ is Noetherian" in the style of reverse mathematics, proving that these theorems are equivalent to ACA_0 over RCA_0. To state these theorems in RCA_0 we introduce a new framework for dealing with second-countable topological spaces.
△ Less
Submitted 26 November, 2015; v1 submitted 28 April, 2015;
originally announced April 2015.
-
On the Uniform Computational Content of Computability Theory
Authors:
Vasco Brattka,
Matthew Hendtlass,
Alexander P. Kreuzer
Abstract:
We demonstrate that the Weihrauch lattice can be used to classify the uniform computational content of computability-theoretic properties as well as the computational content of theorems in one common setting. The properties that we study include diagonal non-computability, hyperimmunity, complete consistent extensions of Peano arithmetic, 1-genericity, Martin-Löf randomness, and cohesiveness. The…
▽ More
We demonstrate that the Weihrauch lattice can be used to classify the uniform computational content of computability-theoretic properties as well as the computational content of theorems in one common setting. The properties that we study include diagonal non-computability, hyperimmunity, complete consistent extensions of Peano arithmetic, 1-genericity, Martin-Löf randomness, and cohesiveness. The theorems that we include in our case study are the low basis theorem of Jockusch and Soare, the Kleene-Post theorem, and Friedberg's jump inversion theorem. It turns out that all the aforementioned properties and many theorems in computability theory, including all theorems that claim the existence of some Turing degree, have very little uniform computational content: they are located outside of the upper cone of binary choice (also known as LLPO); we call problems with this property indiscriminative. Since practically all theorems from classical analysis whose computational content has been classified are discriminative, our observation could yield an explanation for why theorems and results in computability theory typically have very few direct consequences in other disciplines such as analysis. A notable exception in our case study is the low basis theorem which is discriminative. This is perhaps why it is considered to be one of the most applicable theorems in computability theory. In some cases a bridge between the indiscriminative world and the discriminative world of classical mathematics can be established via a suitable residual operation and we demonstrate this in the case of the cohesiveness problem and the problem of consistent complete extensions of Peano arithmetic. Both turn out to be the quotient of two discriminative problems.
△ Less
Submitted 27 June, 2017; v1 submitted 2 January, 2015;
originally announced January 2015.
