Search

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, ID ^ 1 i , over Heyting arithmetic (HA ), originally proved in full generality by Arai (Ann Pure Appl Log 162:807–815, 2011. https://doi.org/10.1016/j.apal.2011.03.002). The proof embeds ID ^ 1 i into the corresponding theory over Beeson's logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, and a direct interpretation into Heyting arithmetic with partial terms using a hierarchy of satisfaction predicates for almost negative formulae. It concludes by applying van den Berg and van Slooten's result (Indag Math 29:260–275, 2018. https://doi.org/10.1016/j.indag.2017.07.009) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over HA . [ABSTRACT FROM AUTHOR]

The aim of this paper is solving an intuitionistic fuzzy multi-objective linear programming problem containing intuitionistic fuzzy parameters, intuitionistic fuzzy maximization/minimization, and intuitionistic fuzzy constraints. To do this, a linear ranking function is used to convert the intuitionistic fuzzy parameters to crisp ones first. Then, linear membership and non-membership functions are used to manipulate intuitionistic fuzzy maximization/minimization and intuitionistic fuzzy constraints. Then, a multi-objective optimization problem is formulated containing maximization of membership functions and minimization of non-membership functions. To solve this problem, the minimax and weighted sum methods are used. Then, the described procedure is summarized as an algorithm to solve the problem, and a numerical example is solved by the proposed method. Finally, to investigate the capability and performance of the model, a supplier selection problem, which is one of the important applications in supply chain management, is solved by the proposed algorithm. [ABSTRACT FROM AUTHOR]

In the context of a weak formal theory called Basic Intuitionistic Mathematics BIM\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\textsf{BIM}$$\end{document}, we study Brouwer’s Fan Theorem and a strong negation of the Fan Theorem, Kleene’s Alternative (to the Fan Theorem). We prove that the Fan Theorem is equivalent to contrapositions of a number of intuitionistically accepted axioms of countable choice and that Kleene’s Alternative is equivalent to strong negations of these statements. We discuss finite and infinite games and introduce a constructively useful notion of determinacy. We prove that the Fan Theorem is equivalent to the Intuitionistic Determinacy Theorem. This theorem says that every subset of Cantor space 2ω\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$2^\omega $$\end{document} is, in our constructively meaningful sense, determinate. Kleene’s Alternative is equivalent to a strong negation of a special case of this theorem. We also consider a uniform intermediate value theorem and a compactness theorem for classical propositional logic. The Fan Theorem is equivalent to each of these theorems and Kleene’s Alternative is equivalent to strong negations of them. We end with a note on ‘stronger’ Fan Theorems. The paper is a sequel to Veldman (Arch Math Logic 53:621–693, 2014). [ABSTRACT FROM AUTHOR]

Constructions are central to the methodology of geometry presented in the Elements. This theory therefore poses a unique challenge to those concerned with the practice of constructive mathematics: can the Elements be faithfully captured in a modern constructive framework? In this paper, we outline our implementation of Euclidean geometry based on straightedge and compass constructions in the intuitionistic type theory of the Nuprl proof assistant. A result of our intuitionistic treatment of Euclidean geometry is a proof of the second proposition from Book I of the Elements in its full generality; a result that differs from other formally constructive accounts of Euclidean geometry. Our formalization of the straightedge and compass utilizes a predicate for orientation, which enables a concise and intuitive expression of Euclid's constructions. [ABSTRACT FROM AUTHOR]

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]