The formalization of Bishop's constructive mathematics

1972 ◽  
pp. 83-96 ◽  
Author(s):  
Nicolas D. Goodman ◽  
John Myhill
Keyword(s):  
Constructive Mathematics ◽  
Bishop’S Constructive Mathematics

Co-quasiordered residuated systems: An introduction

2019 ◽  
Vol 12 (05) ◽  
pp. 1950073
Author(s):  
Daniel A. Romano
Keyword(s):  
Constructive Mathematics ◽  
Relational System ◽  
Philosophical Orientation ◽  
Relational Systems ◽  
Bishop’S Constructive Mathematics

In this paper, we introduce and discuss a concept of co-quasiordered residuated relational systems. The setting of this research is Bishop’s constructive mathematics — a mathematics based on the Intuitionisic logic and particular principle-philosophical orientation of this attitude. Moreover, we introduce the concept of co-filters in such relational system. Additionally, some of the fundamentals properties of these substructures we have been shown.

scholarly journals On co-Filters in Semigroups with Apartness

2021 ◽  
Vol 45 (4) ◽  
pp. 607-613
Author(s):  
DANIEL A. ROMANO ◽  
Keyword(s):  
Intuitionistic Logic ◽  
Constructive Mathematics ◽  
Ordered Semigroup ◽  
Philosophical Orientation ◽  
Semigroup With Apartness ◽  
Bishop’S Constructive Mathematics

The logical environment of this research is the Intuitionistic Logic and principled-philosophical orientation of the Bishop’s Constructive Mathematics. In this paper, basing our consideration on the sets with the apartness relation, we analyze the lattices of all co-filters of an ordered semigroup under a co-quasiorder as a continuation of our article [?]. We prove a number of results related to co-filters in a semigroup with apartness and the lattice of all co-filters of such semigroups.

scholarly journals On Weak Markov's Principle

2001 ◽  
Vol 8 (51) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Real Number ◽  
Positive Real Number ◽  
Constructive Mathematics ◽  
Positive Real ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle ◽  
Bishop’S Constructive Mathematics

We show that the so-called weak Markov's principle (WMP) which states that every pseudo-positive real number is positive is underivable in T^{omega}:= E-HA^{omega} + AC. Since T^{omega} allows to formalize (at least large parts of) Bishop's constructive mathematics this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics (which has been open for about 20 years). The underivability even holds if the ineffective schema of full comprehension (in all types) for negated formulas (in particular for $\exists$-free formulas) is added which allows to derive the law of excluded middle for such formulas.

scholarly journals BROUWER’S FAN THEOREM AND CONVEXITY

2018 ◽  
Vol 83 (04) ◽  
pp. 1363-1375 ◽  
Author(s):  
JOSEF BERGER ◽  
GREGOR SVINDLAND
Keyword(s):  
Continuous Functions ◽  
Unit Interval ◽  
Binary Sequences ◽  
Constructive Mathematics ◽  
Convexity Condition ◽  
Fan Theorem ◽  
Image Position ◽  
Uniformly Continuous ◽  
Bishop’S Constructive Mathematics

AbstractIn the framework of Bishop’s constructive mathematics we introduce co-convexity as a property of subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$, the set of finite binary sequences, and prove that co-convex bars are uniform. Moreover, we establish a canonical correspondence between detachable subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$ and uniformly continuous functions f defined on the unit interval such that B is a bar if and only if the corresponding function f is positive-valued, B is a uniform bar if and only if f has positive infimum, and B is co-convex if and only if f satisfies a weak convexity condition.

A constructive look at the completeness of the space (ℝ)

2002 ◽  
Vol 67 (4) ◽  
pp. 1511-1519 ◽  
Author(s):  
Hajime Ishihara ◽  
Satoru Yoshida
Keyword(s):  
Convex Space ◽  
Locally Convex Space ◽  
Constructive Mathematics ◽  
Test Functions ◽  
Sequential Completeness ◽  
Locally Convex ◽  
Bishop’S Constructive Mathematics

AbstractWe show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space (ℝ) of test functions is equivalent to the principle BD-ℕ which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

Sign in / Sign up

Export Citation Format

Share Document