# Questions tagged [constructive-mathematics]

The constructive-mathematics tag has no usage guidance.

**6**

votes

**2**answers

332 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

128 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

198 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

519 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

273 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

222 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

434 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

591 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 ...

**10**

votes

**5**answers

429 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

140 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

296 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 ...

**17**

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 ...

**19**

votes

**4**answers

910 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

760 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 ...