# Questions tagged [constructive-mathematics]

Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.

143
questions

**3**

votes

**1**answer

151 views

### Does a map over subsingletons determine a subsingleton over maps?

I hope this question isn't too obfuscated (or easy)!
Given a set $S$, let $S_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are subsingletons. In the ...

**6**

votes

**2**answers

217 views

### How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?

This is cross-posted from MSE at the suggestion of a comment after receiving no answers over a few weeks.
Suppose we have $f : A \to B$ and $g : B \to A$, as well as left inverses $f_r : B \to A$ of $...

**4**

votes

**0**answers

158 views

### An axiom that shows that the real numbers are weakly countable?

Is there a model of Intuitionistic Higher-Order Logic in which the following axiom is true?
Covering Axiom: Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to ...

**5**

votes

**1**answer

327 views

### BISH: If a function is pointwise positive, is its infimum positive?

Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH?
I believe that it is indeed the case if ...

**1**

vote

**1**answer

130 views

### Partial computability results on integrals over open intervals

It's well known in Type 2 Effectivity that integration over a compact interval is computable. So what about integration over an open interval? What rigorous computability results exist?
My thoughts ...

**3**

votes

**0**answers

86 views

### Is there a constructive proof of Baer's Criterion?

Baer's Criterion states than one can check injectivity of an $R$-module on inclusions of ideals. The proof, however, strikes me as very nonconstructive: it employs both Zorn's Lemma and LEM.
Does ...

**20**

votes

**2**answers

1k views

### Is it possible to constructively prove that every quaternion has a square root?

Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many"...

**17**

votes

**2**answers

588 views

### Constructive proof of existence of free algebras for infinitary equational theories

Is it constructively true that all (not necessarily finitary) equational theories $T = (\Sigma, E)$ have an initial model?
The usual proof for finitary equational theories I know constructs first ...

**6**

votes

**1**answer

227 views

### Differentiability of the distance function from a (variable) point to a (fixed) set

The distance of from a point $x$ to a set $A$ is defined by
$$ d(x,S) = \inf\{d(x,a)\mid a\in A\}, $$
where you may choose the setting to be $\mathbb R^n$,
a Banach space or a complete metric space.
...

**12**

votes

**1**answer

230 views

### Does this “mixable” property have a standard name in constructive mathematics?

While thinking about constructive mathematics, I stumbled on the following notion, and I would like to know if it has a standard name, a simpler equivalent, or has appeared in the literature:
Say ...

**8**

votes

**2**answers

468 views

### Constructivist defininition of linear subspaces of $\mathbb{Q}^n$?

Let me preface this by saying I'm not someone who has every studied mathematical logic or philosophy of math, so I may be mangling terminology here (and the title is a little tongue in cheek).
I (and ...

**11**

votes

**0**answers

178 views

### Ordinal-valued sheaves as internal ordinals

Let $X$ be a topological space (feel free to add some separation axioms like “completely regular” if they help in answering the questions). Let $\alpha$ be an ordinal, identified as usual with $\{\...

**8**

votes

**1**answer

246 views

### Kleene realizability in Peano arithmetic

For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question ...

**7**

votes

**5**answers

1k views

### Is there any physical or computational justification for non-constructive axioms such as AC or excluded middle?

I became interested in mathematics after studying physics because I wanted to better understand the mathematical foundations of various physical theories I had studied such as quantum mechanics, ...

**7**

votes

**1**answer

607 views

### Explaining the consistency of PRA and ZF from predicative foundations

Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.
From the point of view of a predicative foundation to ...

**13**

votes

**1**answer

335 views

### Is there a constructive proof that in four dimensions, the PL and the smooth category are equivalent?

Summary
Famously, the categories of 4-dimensional smooth manifolds and 4-dimensional piecewise linear manifolds are equivalent. Is there a constructive proof for this theorem or does it depend on the ...

**9**

votes

**0**answers

259 views

### Reflection principle for intuitionistic Zermelo–Fraenkel?

The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $\varphi(x_1,\ldots,x_n)$ of the language of ZFC with free variables $x_1,\ldots,x_n$, ZFC proves
$$ \...

**3**

votes

**1**answer

493 views

### Going beyond the strength of Peano arithmetic “without sets”

First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...

**9**

votes

**2**answers

630 views

### What did the Intuitionists want to do with applied mathematics?

Oversimplification: Newton & Leibnitz &c build the calculus and other methods that solve a vast number of practical problems. Weierstrass, Dedekind, Cantor &c build a foundation under it ...

**11**

votes

**5**answers

634 views

### Locales as spaces of ideal/imaginary points

I posted this question on MSE a few days ago, but got no response (despite a bounty). I hope it will get more answers here, but I'm afraid it might not be appropriate as I'm not sure it's actually ...

**3**

votes

**1**answer

150 views

### Partitions of unity in constructive mathematics

Can someone point me to any substitutes for the partition of unity in Bishop's constructive mathematics?
In particular, under what circumstances can we construct a partition of unity subordinate to ...

**8**

votes

**1**answer

311 views

### Is every set smaller than a regular cardinal, constructively?

Constructively, my only interest in regular cardinals is in terms of the "$\Sigma$-universes" they generate. By a $\Sigma$-universe, I mean a collection of triples $(X,Y,f: X \to Y)$ closed under base ...

**18**

votes

**4**answers

1k views

### Constructively, is the unit of the “free abelian group” monad on sets injective?

Classically, we can explicitly construct the free Abelian group $\newcommand{\Z}{\mathbb{Z}}\Z[X]$ on a set $X$ as the set of finitely-supported functions $X \to \Z$, and so easily see that the unit ...

**20**

votes

**4**answers

1k views

### Mathematics without the principle of unique choice

The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...

**16**

votes

**1**answer

781 views

### New articles by Errett Bishop on constructive type theory?

Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and ...

**3**

votes

**1**answer

224 views

### Unorthodox constructive reasoning: The Kleene Getaway

KG (the Kleene Getaway) is the name I improvised (in my answer to a question on MO on constructive Perron-Frobenius) for a constructive principle which enables the direct constructive use of a ...

**15**

votes

**2**answers

776 views

### Constructive proof of a rational version of Perron-Frobenius?

In the following, we work with vectors and matrices whose entries are rational numbers. Inequalities between such vectors are understood to be coordinatewise: e.g., two vectors $a = \left(a_1,a_2,\...

**3**

votes

**0**answers

88 views

### What's a completely computational/syntactical model for handle decompositions of manifolds?

Simplicial sets, CW complexes
Simplicial sets can be described completely algebraically, by specifying a family of sets, and maps between them satisfying certain relations. This description can be ...

**5**

votes

**1**answer

373 views

### Infinite-time Turing machines and the formal Church's thesis

Infinite-time Turing machines are known to either halt or loop in countable time.
In the spirit of double-negation translation, is there a statement which is: classically equivalent to this; ...

**16**

votes

**1**answer

740 views

### In what ways is ZF (without Choice) “somewhat constructive”

Let me summarize what I think I understand about constructivism:
"Constructive mathematics" is generally understood to mean a variety of theories formulated in intuitionist logic (i.e., not assuming ...

**11**

votes

**2**answers

731 views

### Is the existence of double complement of a set provable in Intuitionistic ZF?

In Powell's article [1] he introduces the axiom of double complement, which says a double complement $\{x : \lnot\lnot(x\in A)\}$ is a set for any set $A$.
I can't find similar axiom from other ...

**3**

votes

**1**answer

164 views

### Fixed-point property and $T_0$ separation property

Each topological space $A$ with fixed-point property is $T_0$ space. Proof: suppose, two different points $a_1$ and $a_2$ belong to the same open subsets of $A$. Then the function
$$f(a)=
\begin{cases}...

**2**

votes

**2**answers

102 views

### Terminology: product on strict preorders corresponding to direct product of preorders?

I’ve had trouble finding a well-established term for the following very obvious and elementary construction on strict partial orders (i.e. transitive, irreflexive relations):
Given two strict partial ...

**2**

votes

**1**answer

123 views

### Constructive version of Hilbert Projection Theorem

I am looking at the Hilbert Projection Theorem, which states that every non-empty closed convex set in a Hilbert space admits a unique element that has the minimum norm in the set.
The proof involves ...

**9**

votes

**7**answers

690 views

### Constructive proof of existence of non-separable normed space

I am looking for a constructive proof of one of the following two statements. If they are not constructively provable, I would be very thankful for an explanation as to why that is so (i.e., at which ...

**8**

votes

**4**answers

788 views

### Gödel's speed-up from constructive to classical logic?

Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano ...

**15**

votes

**2**answers

546 views

### Cauchy real numbers with and without modulus

In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers ...

**13**

votes

**2**answers

358 views

### Constructive proofs of existence in analysis using locales

There are several basic theorems in analysis asserting the existence of a point in some space such as the following results:
The intermediate value theorem: for every continuous function $f : [0,1] \...

**13**

votes

**1**answer

507 views

### Constructive homological algebra in HoTT

I'm curious how much of homological algebra carries over to a constructive setting, like say HoTT (or some other variety of intensional type theory) without AC or excluded middle. There doesn't seem ...

**6**

votes

**4**answers

476 views

### Strict and non-strict orderings

Consider a set $A$ equipped with two binary relations $\le$ and $<$, related in the appropriate ways for the strict and non-strict version of an ordering. One might make different choices about ...

**15**

votes

**1**answer

1k views

### In constructive mathematics, why does the category of abelian groups fail to be abelian?

I was reading the paper Towards Constructive Homological Algebra in
Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...

**9**

votes

**1**answer

324 views

### Constructive analysis and synthetic differential geometry

I am curious if (any of) the various inequivalent constructions of the real line in constructive mathematics can be used to build a model of Kock and Lawvere's synthetic differential geometry? In ...

**30**

votes

**1**answer

2k views

### Constructive algebraic geometry

I was just watching Andrej Bauer's lecture Five Stages of Accepting Constructive Mathematics, and he mentioned that in the constructive setting we cannot guarantee that every ideal is contained in a ...

**6**

votes

**1**answer

739 views

### Rice's theorem in type theory

From the formula
$$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$
we can get the scheme
$$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...

**12**

votes

**0**answers

439 views

### Algebraic closure of a field in constructive mathematics

There is a short note by André Joyal called Les théorèmes de Chevalley-Tarski et remarque sur l'algèbre constructive (pp. 256-258). It is claimed there that there is a constructive version of the ...

**5**

votes

**2**answers

404 views

### Sets in constructive mathematics

It is not completely clear how Bridges, Richman and Youchuan treated sets in their paper. Example is in the following lemma (Lemma 7 on p. 7):
Let $U$ and $V$ be (inhabited to mean $\exists u \in U,...

**3**

votes

**0**answers

132 views

### Constructive treatment of Jacobson rings

Which result is closest to the classical
General Hilbert's Nullstellensatz: Finite type algebras over Jacobson rings are Jacobson.
and constructively true at the same time? And where can I find a ...

**13**

votes

**2**answers

386 views

### Locales in constructive mathematics

It is well known that locales are much more well behaved in a constructive setting than topological spaces. Nevertheless, many authors develop the theory of locales in classical mathematics. Are there ...

**4**

votes

**3**answers

372 views

### Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete ...

**6**

votes

**0**answers

165 views

### Constructive approach to complete intersections

Let $K$ be a field (probably of positive characteristic) and consider the ring $R=K[\![x_1,\dotsc,x_n]\!]$. Suppose we have an ideal $I=(f_1,\dotsc,f_n)$ (with the same $n$ as before). Suppose we ...