# Questions tagged [constructive-mathematics]

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

293
questions

4
votes

0
answers

242
views

### Läuchli's "intermediate thing"

On page 230 of An abstract notion of realizability ..., Läuchli writes the following:
If we drop the restrictions put on $\Theta$, then we get classical logic in one case and an intermediate thing in ...

13
votes

1
answer

830
views

### Consistency strength of HoTT

What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?

8
votes

0
answers

145
views

### How to define Dedekind reals and Eudoxus reals such that they are equivalent to unmodulated Cauchy reals

In constructive mathematics without choice, we have three different versions of the real numbers (each embedding into the next).
Regular Cauchy reals (functions $f : \mathbb N \to \mathbb Q$ such ...

6
votes

1
answer

310
views

### Decimal expansion definition of real numbers, constructively

The two most common definitions of $\mathbb{R}$ are as Dedekind cuts or Cauchy sequences of rational numbers.
A real analysis student of mine is working out of the book Real Analysis and Applications ...

6
votes

0
answers

135
views

### Constructive mathematics with different computational models

I am interested in understanding how the capabilities of constructive mathematics evolve when different computational models are considered. Specifically, if constructive mathematics traditionally ...

9
votes

2
answers

365
views

### How big can function spaces get without extensionality?

In what follows we work in the usual formulation of Martin-Löf Type Theory including Axiom K [1]. Boldface numbers $\mathbf{n}$ denote the usual finite type with $n$ elements.
Motivation
Postulating ...

7
votes

1
answer

276
views

### Equivalence of omniscience principles for natural numbers and analytic omniscience principles for Cauchy real numbers

In constructive mathematics, a proposition $P$ is decidable if $P \vee \neg P$, and a proposition is stable if $\neg \neg P \implies P$. We have the following principles of omniscience for the natural ...

2
votes

0
answers

137
views

### Constructively, when do functions that agree on $[a, b] \cup [b, c]$ also agree on $[a,c]$?

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be ...

3
votes

0
answers

153
views

### Is the Tarski–Seidenberg theorem constructively provable?

The Tarski–Seidenberg theorem asserts that the projection of a semialgebraic set is also a semialgebraic set. My question is whether this is provable in constructive mathematics.
First, let me ...

10
votes

0
answers

144
views

### Closed sets versus closed sublocales in general topology in constructive math

This question is set in constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF.
Short version of the question: if $X$ is a sober ...

7
votes

2
answers

489
views

### Condition to guarantee that an inhabited and bounded set of reals has a supremum

This question is about constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the symbol $\mathbb{R}$) refer to ...

14
votes

3
answers

2k
views

### Exponentials of truth values

I noticed that the exponentiation identity
$$\exp(r + s) = \exp(r) \cdot \exp(s)~,$$
which is of course completely standard for real or complex numbers also holds in a Boolean setting.
That is, when I ...

8
votes

0
answers

331
views

### Can the p-adic be countable?

Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, The Countable Reals) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a ...

9
votes

1
answer

241
views

### Does there exist a geometric morphism between the effective and topological topoi? Does one arise from synthetic topology?

I'm presenting in final projects for my computability and computational topology courses on the connections between computability, continuity, and logic. As a mathematician/unmentored baby logician ...

7
votes

0
answers

283
views

### The constructive Eudoxus reals

Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, The Countable Reals) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a ...

7
votes

0
answers

249
views

### Is it decidable whether a statement about reals (in the language of ordered rings) is constructively provable?

The language of ordered rings is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$.
To decide whether such a ...

18
votes

3
answers

3k
views

### What's the earliest result (outside of logic) that cannot be proven constructively?

Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't).
An obvious counter-example is the law ...

5
votes

0
answers

220
views

### Are there Dedekind-infinite amorphous sets?

An amorphous set is an infinite set (i.e. cannot be put into bijection with any finite set $\{ 1, \dots, n \}$ for any $n$) that cannot be partitioned into two mutually disjoint infinite subsets. ...

9
votes

1
answer

236
views

### What are these generalizations of the principles of omniscience called?

I will give some principles that are slightly stronger versions of the principles of omniscience. Despite being about the natural numbers, they imply their analytic versions! Under countable choice (...

9
votes

2
answers

1k
views

### Truth in a different universe of sets?

I understand that provability and truth as different concepts.
Provability is syntactic, it only concerns whether the given
sentence can be derived by reiterating the inference rules over a
collection ...

11
votes

6
answers

1k
views

### When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f : [a, b] \cup [b, c] \to S$ be a function. When can we find a function $g : [a, c] \to S$ that meets the following ...

3
votes

0
answers

91
views

### What does the computation of irrationality and transcendentality via a fancy implementation of analytic Markov's property look like?

Proofs that various real numbers are not rational or not algebraic tend to be constructively valid as is. Examples include the proofs that $\sqrt 2$ and $\log_2(3)$ are not rational and that $e$ is ...

3
votes

1
answer

192
views

### Are the multi-valued Eudoxus reals constructively equivalent to the Dedekind reals?

Without LEM or the axiom of choice, we can prove that the Eudoxus reals are equivalent to the Cauchy reals but can't prove either of those equivalent to the Dedekind reals.
However, we can prove that ...

6
votes

0
answers

106
views

### Archimedean ordered field in which every function is smooth

In constructive mathematics, it is consistent that every function $\mathbb{R} \to \mathbb{R}$ on the Dedekind real numbers is continuous. However, it is not consistent that every function $\mathbb{R} \...

6
votes

1
answer

269
views

### Archimedean ordered fields without maxima and minima in constructive mathematics

In constructive mathematics, let us define an ordered (Heyting) field $F$ to be a commutative ring with a binary relation $<$ which is
irreflexive, where for all $x$, $\neg (x < x)$
asymmetric, ...

14
votes

1
answer

509
views

### Is there a theory between HA and PA that doesn't have Markov's rule?

A theory $T$ admits Markov's rule when
For every formula $\phi(n)$, if $$T \vdash \forall n \in \mathbb N. \phi(n) \lor \lnot \phi(n)$$ and $$T \vdash \lnot \lnot \exists n \in \mathbb N. \phi(n)$$ ...

4
votes

1
answer

213
views

### Is every compact, sober, second-countable space the image of $2^\omega$?

As a bonus, is every compact, $T_0$, second-countable space the image of $2^\omega \times \omega$?
As a further bonus, can we strengthen "image" to "quotient"?
My motivation for ...

4
votes

1
answer

252
views

### What is the theory of statements with a provably *bounded* realizer (according to PA)?

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.
We can summarize the results from Emil Jeřábek's answer as follows:
\begin{gather*}
T_1 = \{ ...

5
votes

3
answers

1k
views

### Understanding $\forall p \, q .\, \sqrt{2} \neq p/q$ constructively

"By contradiction" or "of negation" is an old chestnut of constructive dispute.
But taking apartness as primitive instead of equality yields a definition of irrationality without ...

3
votes

0
answers

181
views

### In constructive set theory, is it consistent for there to be a ring that models smooth infinitesimal analysis?

In a constructive set theory such as CZF, it is consistent to assume that every function $f : \mathbb R \to \mathbb R$ is continuous. However, it is not consistent to assume that every such function ...

5
votes

1
answer

275
views

### Does weak countable choice imply that the Cauchy reals are Dedekind complete?

Assuming the axiom of weak countable choice, is the set of modulated Cauchy reals Dedekind complete?
The second theorem on this ncatlab page claims something equivalent, but it doesn't contain a proof ...

6
votes

0
answers

292
views

### What are these non-classical versions of ZFC defined by realizability?

See Kleene realizability in Peano arithmetic for a similar question, but about PA instead of ZFC. (In particular, an answer as specific as Emil Jeřábek's answer would be great!)
In the context of ...

6
votes

1
answer

289
views

### Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.)
Background: I'm trying to understand ...

3
votes

0
answers

229
views

### Uses of excluded middle on a conjecture that can be rewritten constructively with this trick

An interesting proof technique is to use the law of excluded middle on a conjecture. There are proofs using LEM on the Riemann hypothesis for example.
Constructively this is disallowed (if you can ...

7
votes

0
answers

191
views

### Strengthening Determinacy in constructive set theory?

Recall how games work. Let $X$ be a set (the "game space") and $\alpha$ an ordinal (the "game clock"). Alice and Bob take turns naming elements of $X$. We write them down in order ...

1
vote

1
answer

69
views

### Constructing set-truncations of types from universes

This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could ...

4
votes

1
answer

161
views

### Constructing coproduct types and boolean types from universes

Suppose we have a dependent type theory which has dependent product types, dependent sum types, identity types, function extensionality, an empty type, and a universe $U$ which is closed under the ...

8
votes

0
answers

269
views

### The approximate mean value theorem / Rolle's theorem in pure constructive mathematics

In the replies of this very similar question, there is a fascinating answer that is beautiful in its simplicity. In particular, it seems to use perhaps the most minimal assumptions one can possibly ...

8
votes

1
answer

224
views

### Sequential colimit of iterated quotients of Cauchy sequences

We work in constructive mathematics.
The sets and functions in the foundations form a Grothendieck topos, which means that all colimits exist, and in particular, that all sequential colimits exist. ...

12
votes

0
answers

521
views

### Does Wedderburn's Little Theorem hold constructively?

Wedderburn's Little Theorem states that every finite division ring is commutative. Perhaps even more surprising, this implies that every finite reduced ring is commutative.
The proofs that I am aware ...

6
votes

1
answer

252
views

### Existence property for second-order propositional logic

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language.
Question: Assume that $\Gamma$ and $\Psi$ are ...

6
votes

2
answers

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

13
votes

0
answers

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

23
votes

4
answers

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

11
votes

3
answers

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

12
votes

1
answer

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

5
votes

0
answers

142
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

179
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

154
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

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