We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends the set-theoretic version introduced in the mentioned paper with collections. The other level is given by an extensional set theory which is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the "proofs-as-programs" paradigm and acts as a programming language.
We introduce extensions by rules of the extensional level of the Minimalist Foundation which turn out to be equivalent to constructive and classical axiomatic set theories.
To be or not to be constructive, that is not the question
在20世纪初，L. E. J.布劳威尔开创了一种新的数学哲学，称为直觉主义。直觉主义在许多方面都是革命性的，但从数学上讲，它的突出之处在于它挑战了希尔伯特的形式主义数学哲学，并拒绝了主流数学中使用的“经典”逻辑中的排中律。从直觉主义中产生了直觉主义逻辑和相关的布劳威尔-海廷-柯尔莫哥洛夫解释，其中“存在x”直观地意味着“给出了计算x的算法”。许多建构性数学的学派受到布劳威尔的直觉主义的启发而发展起来，这些学派都是以直觉主义逻辑为基础的，但对算法的构成有不同的解释。本文讨论的二分法之间的建设性和非建设性的数学，或者更确切地说，没有这样一个“排除中间”。特别是，我们挑战的“二元”的观点，数学是建设性的或没有。为此，我们确定了经典数学的一部分，即经典非标准分析，并表明它栖息在建设性和非建设性之间的黄昏地带。直觉上，非标准分析中典型的谓词“x是标准的”可以解释为“x是可计算的”，从而产生了直接从经典非标准分析中获得的可计算（有时是构造性的）数学。我们的结果正式Osswald的长期猜想，经典的非标准分析是本地建设性的。最后，我们的结果提供了另一种解释布劳威尔的论文，逻辑依赖于数学。
We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically "constructivize" classi…
Mathematicians like Markov and Bishop made an effort to develop constructive mathematics and extended many theorems in classical mathematical analysis. Heine Borel theorem tells us that a closed bounded subset of Euclidean space R is compact, but in constructive mathematics, Tseitin and Zaslavskii showed that the set of all constructive real numbers between 0 and 1 is not compact. We are going to show that when giving certain restriction to the open cover on [0,1], we can however always choose a finite sub-cover.
Using a recent alternative to Tarskian semantics for first-order logic, known as $\textit{possibility semantics}$, I introduce an alternative approach to nonstandard analysis that remains within the bounds of \textit{semi-constructive} mathematics, i.e., does not assume any fragment of the Axiom of Choice beyond the Axiom of Dependent Choices. I define the $F\it{-hyperreal}$ $\it{line}$ ${^\dagger\!\mathcal{R}}$ as a possibility structure and show that it shares many fundamental properties of the classical hyperreal line, such as a Transfer Principle and a Saturation Principle. I discuss the t…
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.
In this paper we analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.
Proposed initially from a practical circumstance, the traveling salesman problem caught the attention of numerous economists, computer scientists, and mathematicians. These theorists were instead intrigued by seeking a systemic way to find the optimal route. Many attempts have been made along the way and all concluded the nonexistence of a general algorithm that determines optimal solution to all traveling salesman problems alike. In this study, we present proof for the nonexistence of such an algorithm for both asymmetric (with oriented roads) and symmetric (with unoriented roads) traveling s…
It is well known that the R, the set of real numbers, is an abstract set, where almost all its elements cannot be described in any finite language. We investigate possible approaches to what might be called an epi-constructionist approach to mathematics. While most constructive mathematics is concerned with constructive proofs, the agenda here is that the objects that we study, specifically the class of numbers that we study, should be an enumerable set of finite symbol strings. These might also be called decidable constructive real numbers, that is our class of numbers should be a computable …
本文经François Apéry许可转载。它最初是由弗朗索瓦·盖纳德和吉尔伯特·勒利弗尔为《思考数学》一书编辑的。它是以前作为Séminaire de philosophie et mathématiques de l 'École normale supérière（1976年4月26日会议）出现的文本的修改和删节版本，巴黎，IREM Paris-Nord，1980年，15页，http://www.numdam.org/item? id= SPHM_1976_1_A1_0，以及Langage et pensée mathématiques：actes du colloque international（Luxembourg，9-11 juin 1976），Luxembourg，Centre universaire de Luxembourg，1976，pp. 391--410.在导言中，阿佩里写道：“在缺乏说服力的情况下，这篇文章可以澄清事实：我们表明，构造性概念并没有破坏，相反，它丰富了经典数学。"
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Löf type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness. Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical o…
