# Questions tagged [constructive-mathematics]

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

252
questions

6
votes

2
answers

542
views

### In the constructive theory of direct categories, is it decidable whether an arbitrary morphism is an identity or not?

I'm wondering what the legit definition of direct categories should be in constructive mathematics. I must admit I don't even know in what literature I should look for the definition. I would ...

12
votes

0
answers

116
views

### Limits in free cocompletion, constructively

Classically, if a locally small category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits.
But all proof I know of that result ...

20
votes

4
answers

2k
views

### Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He ...

3
votes

0
answers

117
views

### Does negative trichotomy hold for constructive ordinals?

I don't know if there is a standard term for this, but by "negative trichotomy" I mean ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴). This holds for constructive real numbers as an easy ...

7
votes

0
answers

199
views

### How strong is the Schröder–Bernstein theorem where one set is the natural numbers?

The full Schröder-Bernstein theorem states that given an injection from A to B and also one from B to A, there is a bijection between A and B. It is equivalent to excluded middle, as shown in the ...

4
votes

0
answers

122
views

### Do presheaf toposes satisfy the full fan theorem?

Presheaf toposes satisfy LPO and (edit: if over categories with binary products) PAx and countable choice internally, so they automatically satisfy the stable fan theorem (every bar which is the ...

7
votes

0
answers

151
views

### Constructive theory of Lie algebras

I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is ...

2
votes

0
answers

137
views

### Do Grothendieck topoi with enough points satisfy the fan theorem internally?

Fourman and Hylland proved in the 80s that all spatial topoi satisfy the full fan theorem internally, while there are examples of localic topoi that do not satisfy it.
This leads one to conjecture a ...

9
votes

0
answers

142
views

### Are there good criteria for the topological models where BD-N and BD hold?

A (non-empty/inhabited) subset $S$ of $\mathbb{N}$ is said to be pseudo-bounded if for every sequence $x_n$ in $S$ we have
$\lim_{n\to \infty} \frac{x_n}{n} = 0$
Clearly all bounded subsets are pseudo-...

6
votes

1
answer

232
views

### Does a tight apartness relation on a subobject classifier imply the elementary topos is Boolean?

Given a set $S$, a tight apartness relation on $S$ is a relation $\#$ which is tight, irreflexive, symmetric, and a comparison, or more specifically, a relation $\#$ such that
for all elements $a \in ...

4
votes

0
answers

72
views

### Constructively valid reference for the soberness of discrete spaces and points of a locale coproduct

I am looking for constructively valid references for the following two related facts:
discrete topological spaces are sober,
the points of a locale coproduct are the disjoint union of the points of ...

7
votes

0
answers

512
views

### A new and subtle order-theoretic fixed point theorem

Sometimes a very simple argument appears out of the blue and overturns a subject. It is not based on pre-existing theory and heavy involvement in such a theory is actually a handicap in finding such ...

5
votes

1
answer

131
views

### Constructive proof of univariate McCoy theorem without Dedekind-Mertens?

McCoy's theorem (one of them) says that for any commutative ring $A$, $f\in A[x]$ is a zero-divisor iff it's annihilated by a scalar in $A$.
There's a widespread proof by contradiction. There's also a ...

7
votes

2
answers

426
views

### Continuous nowhere differentiability and constructive mathematics

In some constructive systems, every function from $\mathbb{R}\to\mathbb{R}$ is continuous (roughly speaking from the classical fact that computable functions are continuous). More weakly, in Bishop's ...

5
votes

0
answers

152
views

### Moduli all the way down

The notion of modulus of continuity is well-known from constructive mathematics, reverse mathematics, and computability theory. Intuitively, such a modulus is a function that returns the '$\delta>...

8
votes

0
answers

303
views

### What is the relationship (if any) between constructivism, finitism and predicativism?

The terms “constructivism”, “finitism” and “predicativism” refer to ideas / currents in the philosophy of mathematics (or loosely defined conditions on a system of logic) that I think I understand ...

5
votes

0
answers

132
views

### Weaker versions of the Riemann series theorem in constructive mathematics

The classical Riemann series theorem states that given a sequence $(a_n)_{n \in \mathbb{N}}$ of real numbers such that the series $\sum_{n = 0}^\infty a_n$ is conditionally convergent, for all real ...

3
votes

0
answers

210
views

### Has an uncomputable variant of the Cantor staircase ever been used in constructive logic?

An open problem in choiceless constructivism is to prove that if a function $f:\mathbb R \to \mathbb R$ is pointwise differentiable everywhere, with $f'=0$, then $f$ is constant. See In choiceless ...

7
votes

0
answers

196
views

### New Foundations in a Homotopy/Intuitionistic Type Theory form?

New Foundations is a famously odd set theory suggested by Quine in the 1930s which:
Features a universal set.
Disproves the axiom of choice.
Proves the existence of an infinite set by a trivial ...

12
votes

2
answers

526
views

### Is the Intermediate Value Theorem strictly stronger than LLPO?

(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.)
By LLPO, I mean the statement that ...

7
votes

2
answers

436
views

### What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?

Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, ...

6
votes

0
answers

123
views

### Complexity of constructive arithmetical truth vs second order arithmetic

Let us say that an arithmetic statement is constructively true iff it is realized by a computable function under Kleene's function realizability. Does the set of constructively true (first order) ...

12
votes

1
answer

356
views

### Tarski-Seidenberg for strict inequalities and bounded quantification

This theorem says that quantifiers over real variables can be eliminated from classical first order formulae built from equations and inequalities between polynomials with rational coefficients, ie in ...

7
votes

1
answer

263
views

### For which Sheaf topoi is Brouwer's fan theorem true?

Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable ...

3
votes

1
answer

126
views

### Does CZF prove there is a minimal cauchy completion of the rationals?

In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields.
CZF can ...

7
votes

1
answer

273
views

### Status of the fundamental theorem of algebra for the locale of real numbers

In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed ...

7
votes

1
answer

123
views

### Invertibility and comparison to zero in the MacNeille sections (bounded extended reals)

(The following three paragraphs are given for context. Readers already aware of the terminology can skip to “the problem” below.)
In a spatial topos $\mathop{\textbf{Sh}}(X)$ the MacNeille sections (...

4
votes

3
answers

328
views

### The field structure on the locale of real numbers

It is well known how to derive the field operations from the construction of the real numbers as the Dedekind completion of the rational numbers and as the Cauchy completion of the rational numbers; ...

7
votes

0
answers

176
views

### Weakest theory over which "all sets are measurable" has consistency strength?

Some convention: $\textrm{DC}$ stands for axiom of dependent choice, $\text{LM}$ stands for the statement "all subsets of $\mathbb{R}$ are Lebesgue measurable", $\textrm{IC}$ for "there ...

5
votes

0
answers

149
views

### Do quasi-excellent rings have a good constructive definition?

$\DeclareMathOperator\Sh{Sh}$Informally, a quasi-excellent ring is a Noetherian ring with a few technical extra regularity conditions that make it turns out to be the largest class of rings that allow ...

9
votes

1
answer

266
views

### Are finitely enumerated and subfinite sets Dedekind-finite?

The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF.
Let us say that a set $X$ is:
finite when there exists a ...

8
votes

0
answers

315
views

### Why is the double negation of the axiom of choice rarely considered?

In constructive/intuitionistic mathematics, it is common to reject the axiom of choice, because it is highly nonconstructive and implies the law of the excluded middle by Diaconescu's theorem/Bishop's ...

3
votes

1
answer

148
views

### Using generating functions to construct or solve differential equations

I know that $T_n(x)$ is the solution of the differential equation $(1-x^2)y''-xy'+n^2y=0$, where
$$
T_n(x)=\begin{cases}
T_n(x)=1 & \text{if $n=0$}\\
T_n(x)=x & \text{if $n=1$}\\
T_{n}(x)=...

17
votes

0
answers

336
views

### Joyal's topos in which $[0,1]$ fails to be compact

Some time around 1977, André Joyal constructed a topos (actually a locale, i.e., a localic topos, necessarily non-spatial) in which the closed unit interval $[0,1]$ fails to be compact. There are ...

7
votes

3
answers

433
views

### Is there a constructive version of internal set theory?

Is there a theory T such that:
T includes all the axioms of CZF.
T includes the Idealization, Standardization, and Transfer schemas from IST.
Every axiom of T is a theorem of IST.
T has Church's rule....

0
votes

1
answer

365
views

### Did I find a few (small) errors in the Pradic and Brown 2021 paper that Schroeder-Bernstein implies excluded middle?

I'm looking at the https://arxiv.org/abs/1904.09193 paper (version 2, from 2021) and think it has a few errors. I think I found three small places where the paper needs to be corrected (in the sense ...

3
votes

0
answers

63
views

### Discreteness of the higher inductive-inductive Cauchy real numbers in real cohesive homotopy type theory

We work in cohesive homotopy type theory with propositional resizing, so that there is only one type of Dedekind real numbers $\mathbb{R}$ up to equivalence, and Mike Shulman's axiom $\mathbb{R}\flat$,...

4
votes

1
answer

230
views

### Equivalence of real numbers in terms of Dedekind cuts and Cauchy nets of rational numbers

We work in weakly predicatively constructive mathematics, in that we accept function sets but do not accept power sets or excluded middle. More specifically, we shall assume a sequential universe ...

3
votes

0
answers

244
views

### Principle of unique choice in homotopy type theory

In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be
if $R$ is a relation between two sets $A$, $B$, and for every $...

9
votes

2
answers

931
views

### Proof in constructive mathematics that the principal square root function exists in any Cauchy complete Archimedean ordered field

In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple ...

2
votes

1
answer

209
views

### Constructing ordered fields with lattice structure from ordered fields without lattice structure, and vice versa, in constructive mathematics

This post originated from my reference request for the definition of an ordered field in constructive mathematics: Proper definition of ordered field in constructive mathematics
We are working in ...

5
votes

1
answer

258
views

### Proper definition of ordered field in constructive mathematics

The nLab article on ordered fields defines ordered fields to be a field $K$ with a strict linear order $<$ such that $0 < 1$ and for all elements $a \in K$ and $b \in K$, if $a > 0$ and $b &...

4
votes

1
answer

249
views

### Construction of graphs of high girth and chromatic number

Are there any concrete constructions of graphs of both high girth and chromatic number?
Of course there is the seminal paper of Erdős which proves the existence of such graphs via the probabilistic ...

4
votes

0
answers

373
views

### Simple constructive proof for the hyperplane separating theorem (HST)?

The Hyperplane Separation Theorem (HST) is usually proved through the existence of a unique minimum-norm vector in a nonempty closed convex set. I think this is an existential proof which applies to ...

4
votes

1
answer

281
views

### For which "permutation groups" is the sign homomorphism well-defined constructively?

Let $X$ be a finite set. I now have a favorite construction of the sign homomorphism $Sym(X) \to C_2$. But perhaps it shouldn't be my favorite construction.
After discussion with the experts, I've ...

10
votes

2
answers

385
views

### Is there a purely constructive presentation of the HK integral?

Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...

6
votes

1
answer

397
views

### Is Solèr’s theorem true in constructive mathematics?

Solèr’s theorem says that for every star division ring $R$ and every $R$-module $H$ with an orthomodular Hermitian form $\langle (-),(-) \rangle:H \times H \to R$ such that there exists an infinite ...

17
votes

1
answer

611
views

### Is Hurwitz's theorem true in constructive mathematics?

Hurwitz's theorem says that the only division composition algebras over the real numbers $\mathbb{R}$ are the real numbers themselves $\mathbb{R}$, the complex numbers $\mathbb{C}$, the quaternions $\...

16
votes

1
answer

980
views

### Easiest proof of computability of homotopy groups of spheres

Has it gotten easier to prove all homotopy groups of spheres are computable? I don’t care if the computation is inefficient, what’s the easiest proof? Are we still stuck doing Postnikov towers?

9
votes

1
answer

405
views

### Is Heyting arithmetic sufficient to prove its own (formalized) existence property?

Let $\mathsf{HA}$ denote first-order Heyting arithmetic (viꝫ., Peano axioms with unrestricted recursion scheme, in first-order intuitionistic logic). It is known (e.g., Troelstra & van Dalen, ...