- Diener, H. (2015). Variations on a theme by Ishihara. Mathematical Structures in Computer Science, 25, 1569–1577.
A preliminary version can be found here
- Lubarsky, R., & Diener, H. (2014). Principles weaker than BD-N. Journal of Symbolic Logic, 78, 873–885.
BD-N is a weak principle of constructive analysis. Several interesting principles implied by BD-N have already been identified, namely the Riemann Permutation Theorem, the closure of the anti-Specker spaces under product, and the Cauchyness of all partially Cauchy sequences. Here these are shown to be strictly weaker than BD-N, yet not provable in set theory alone under constructive logic. The implications among these principles are also discussed.
- Lubarsky, R., & Diener, H. (2013). Separating the Fan Theorem and Its Weakenings. In S. Artemov & A. Nerode (Eds.), Logical Foundations of Computer Science (Vol. 7734, pp. 280–295). Springer Berlin Heidelberg.
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 suffices to separate all of the as yet identified fan theorems.
- Diener, H. (2013). Weak König’s Lemma Implies the Uniform Continuity Theorem. Journal of Computability, 2, 9–13.
As the title suggests we are going to show that Weak König’s Lemma implies the uniform continuity theorem; to be more precise the uniform continuity theorem for functions [0, 1] → R. This improves upon a result by J. Berger who has proven this implication for functions [0, 1] → N
- Diener, H. (2012). Reclassifying the antithesis of Specker’s theorem. Archive for Mathematical Logic, 51, 687–693.
The anti-Specker property can be seen as a constructive substitute for sequential compactness. It is closely related to Brouwer’s fan theorem. We show that different spaces satisfying this property is equivalent to subtly different versions of Brouwer’s fan theorem(s).
- Diener, H., & Hedin, A. (2012). The Vitali covering theorem in constructive mathematics. Journal of Logic and Analysis, 4. Retrieved from http://logicandanalysis.org/index.php/jla/article/viewFile/143/54
This paper investigates the Vitali Covering Theorem from various constructive angles. A Vitali Cover of a metric space is a cover such that for every point there exists an arbitrarily small element of the cover containing this point. The Vitali Covering Theorem now states, that for any Vitali Cover one can find a finite family of pairwise disjoint sets in the Vitali Cover that cover the entire space up to a set of a given non-zero measure. We will show, by means of a recursive counterexample, that there cannot be a fully constructive proof, but that adding a very weak semi-constructive principle suffices to give such a proof. Lastly, we will show that with an appropriate formalization in formal topology the non-constructive problems can be avoided completely.
- Diener, H., & Schuster, P. (2011). Uniqueness, continuity and the existence of implicit functions in constructive analysis. LMS Journal of Computation and Mathematics, 14, 127–136.
- Diener, H., & Loeb, I. (2011). Constructive reverse investigations into differential equations. Journal of Logic and Analysis, 3. Retrieved from http://logicandanalysis.org/index.php/jla/article/view/114/41
We study Picard’s Theorem and Peano’s Theorem from a constructive reverse perspective. This means that we have to change our focus from global properties to local properties. We also extend the theory of pointwise continuously differentiable functions to include Rolle’s Theorem, the Mean Value Theorem, and the full Fundamental Theorem of Calculus.
- Bridges, D. S., & Diener, H. (2010). The anti-Specker property, positivity, and total boundedness. Mathematical Logic Quarterly, 56, 434–441.
- Diener, H., & Schuster, P. (2010). On Choice Principles and Fan Theorems. Journal of Universal Computer Science, 16, 2556–2562.
Veldman proved that the contrapositive of countable binary choice is a theorem of full-fledged intuitionism, to which end he used a principle of continuous choice and the fan theorem. It has turned out that continuous choice is unnecessary in this context, and that a weak form of the fan theorem suffices which holds in the presence of countable choice. In particular, the contrapositive of countable binary choice is valid in Bishop-style constructive mathematics. We further discuss a generalisation of this result and link it to Ishihara’s boundedness principle BD-N.
- Diener, H., & Loeb, I. (2009). Sequences of Real Functions on \( \lbrack 0, 1\rbrack \)in Constructive Reverse Mathematics. Annals of Pure and Applied Logic, 157, 50–61.
We give an overview of the role of equicontinuity of sequences of real-valued functions on \( \lbrack 0, 1\rbrack \)and related notions in classical mathematics, intuitionistic mathematics, Bishop’s constructive mathematics, and Russian recursive mathematics. We then study the logical strength of theorems concerning these notions within the programme of Constructive Reverse Mathematics. It appears that many of these theorems, like a version of Ascoli’s Lemma, are equivalent to fan-theoretic principles.
- Diener, H., & Schuster, P. (2009). Uniqueness, Continuity, and Existence of Implicit Functions in Constructive Analysis. In A. Bauer, P. Hertling, & K.-I. Ko (Eds.), 6th Int’l Conf. on Computability and Complexity in Analysis. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. Retrieved from http://drops.dagstuhl.de/opus/volltexte/2009/2265
- Diener, H. (2008). Generalising compactness. Mathematical Logic Quarterly, 54, 49–57.
Working within the framework of Bishop’s constructive mathematics, we will show that it is possible to define compactness in a more general setting than that of uniform spaces. It is also shown that it is not possible to do this in a topological space
- Bridges, D. S., & Diener, H. (2007). The pseudocompactness of \( \lbrack 0, 1\rbrack \)is equivalent to the uniform continuity theorem. J. Symbolic Logic, 72, 1379–1384.
We prove constructively that, in order to derive the uniform continuity theorem for pointwise continuous mappings from a compact metric space into a metric space, it is necessary and sufficient to prove any of a number of equivalent conditions, such as that every pointwise continuous mapping of \( \lbrack 0, 1\rbrack \)into ℝ is bounded. The proofs are analytic, making no use of, for example, fan-theoretic ideas.
- Bridges, D. S., & Diener, H. (2006). A constructive treatment of Urysohn’s Lemma in an apartness space. Math. Log. Quart., 52, 464–469.
At first (maybe even at second) sight it appears highly unlikely that Urysohn’s Lemma has any significant constructive content. However, working in the context of an apartness space and using functions whose values are a generalisation of the reals, rather than real numbers, enables us to produce a significant constructive version of that lemma.