Search

This work presents a formalization of the discrete model of the continuum introduced by Harthong (1989), the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field (Reveillès and Richard, Ann. Math. Artif. Intell. Math. Inform. 16(14), 89-152 (1996)). The formalization is based on the work presented in Chollet et al. (2012, 2009) where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges (1999). Laugwitz-Schmieden numbers (Laugwitz 1983) are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated (Chollet et al., Theor. Comput. Sci. 466, 2-19 (2012)). In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems. [ABSTRACT FROM AUTHOR]

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 the task of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space $${\mathcal{N}}$$ and of the set $${\mathcal{R}}$$ of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space $${\mathcal{C}}$$ , or, equivalently, the unit interval [0, 1], is compact and Kleene's Alternative is the statement that $${\mathcal{C}}$$ , or, equivalently, [0, 1], is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene's Alternative is found. [ABSTRACT FROM AUTHOR]