61
votes

Accepted

### How to rewrite mathematics constructively?

If you want a "general method" that "always works" to turn a classical theorem into a constructive one, there are double-negation translations: if you add enough $\neg\neg$s to a ...

54
votes

Accepted

### Constructive algebraic geometry

Let me wrote a quick introduction to this idea:
1) Locales
I do not know if you are already familiar with the notion of locale that Andrej is referring to in his talk: They are a small variation on ...

42
votes

Accepted

### How Would an Intuitionist Prove This?

In general, when working in constructive mathematics, the strategy for proving $Q \lor R$ is to prove $Q$ or to prove $R$. In this case, just knowing abstractly that "there is an $n \not = 1$ that ...

30
votes

Accepted

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

Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.
Which ...

28
votes

### Bishop quote stating that axiom of choice is constructively valid

According to the BHK interpretation of intuitionistic logic we have that:
A proof of $\exists x \in A . \phi(x)$ consists of a pair $(a, p)$ where $a \in A$ and $p$ is a proof of $\phi(a)$.
A proof ...

26
votes

### List of proofs where existence through probabilistic method has not been constructivised

There is an example of this which is important in machine learning: finding linear maps with the restricted isometry property. Given a set $S$ of $m$ points in $\mathbb{R}^N$ (with $N$ very large) ...

Community wiki

25
votes

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

In the topos we construct in our paper there is a surjection/epimorphism from the natural numbers to the Dedekind reals. In the model of CZF you mention (and in the effective topos) the Dedekind reals ...

22
votes

Accepted

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

There are many different flavors of constructive mathematics. The theory that was used in this paper is weak, it lacks some useful constructions from the usual set theory such as quotient sets. ...

22
votes

Accepted

### Constructive homological algebra in HoTT

As regards HoTT, my own current opinion is that the best way to do "homological algebra" therein is by working directly with spectra.
With only a working mathematician's knowledge of homological ...

21
votes

### How Would an Intuitionist Prove This?

To add a few details to Carl's answer...
Assuming your system includes full induction, your system can prove that any bounded arithmetic formula is decidable (i.e., $P \lor \lnot P$ is provable for ...

20
votes

Accepted

### Does $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$ imply excluded middle?

It depends how much separation is available. If you can construct the set $\{ z \in \{ \emptyset \} \;|\; \varphi \}$ then you can show $\varphi \vee \neg \varphi$. So for theories with full ...

19
votes

### How Would an Intuitionist Prove This?

The question was about intuitionism specifically, not some variant of constructivism, nor about some particular formalization of intuitionism (I don't think an intuitionist would recognize any ...

19
votes

### How Would an Intuitionist Prove This?

You ask how a constructive mathematician would prove the theorem. Just like you did! We only need to verify that every number is either composite or prime, see below. But Carl Mummert gave the "proof ...

19
votes

### Contrasting theorems in classical logic and constructivism

There are several ways one could interpret the word "constructivism" here, and the answer depends on what you meant by it.
Bishop-style constructivism is a generalization of Brouwerian intuitionistim,...

Community wiki

18
votes

### What is neutral constructive mathematics

You'll probably have better luck with the phrase "intuitionistic higher-order logic" (IHOL). A good place to start is the book by Lambek and Scott, Introduction to Higher Order Categorical ...

18
votes

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

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF ...

17
votes

Accepted

### Kleene realizability in Peano arithmetic

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$Let me first answer a slightly modified question:
Proposition: For any sentence $\phi$, the following are equivalent:
There exists $n\in\mathbb N$ such ...

17
votes

Accepted

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

$\def\prf{\mathrm{Prf}}\def\pr{\mathrm{Pr}}\def\con{\mathrm{Con}}\def\f{\ulcorner\bot\urcorner}\def\ha{\mathsf{HA}}$Let $\prf(x,y)$ be the formalized proof predicate for either HA or PA (it doesn’t ...

16
votes

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

Yes! In fact, more generally, for any rig $R$ in which $0 \neq 1$, the map $X \mapsto R[X]$ is injective (where $R[X]$ denotes the free $R$-module on a set $X$).
Specifically: I claim we can ...

16
votes

Accepted

### Locales as spaces of ideal/imaginary points

I can only answer some of your questions.
Yes, the Zariski locale is extensively studied. It's one of the ways of setting up scheme theory in a constructive context: Don't define schemes as locally ...

16
votes

Accepted

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

It was proved by Andreas Blass in Words, free algebras, and coequalizers that free infinitary algebras are not constructible neither in topoi nor in ZF. It is easy to see that the existence of free ...

16
votes

### How to express in categorical language that in some toposes not all complex numbers have square roots

No the problem isn't quite choosing an element from an unordered pair, even if I agree with you that it somehow feel like it is. The map you are talking about is indeed always an epimorphism.
One way ...

16
votes

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

According to Wikipedia, in 5th century BCE, Bryson of Heraclea spoke of a special case of the intermediate value theorem. If we're very generous, that would be an early occurrence of a constructively ...

15
votes

### List of proofs where existence through probabilistic method has not been constructivised

Lower bounds for Ramsey numbers might fit the bill. See for instance this question.

Community wiki

15
votes

### Wanted: a "Coq for the working mathematician"

I might suggest the book devised for the library on GitHub, Mathematical Components (the author of the question is acknowledged within actually). It makes no assumptions on the reader in terms of ...

15
votes

Accepted

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

This question is about type theory in general and is not specific to homotopy type theory. $\newcommand{\Type}{\mathtt{Type}}$
The thing you are missing is that a universe $\Type_k$ contains very ...

15
votes

Accepted

### Initiation to constructive mathematics

I have a soft spot for Constructivism in Mathematics: An Introduction (2 volumes) by Troelstra and van Dalen as an overview. And for what one loses compared to classical mathematics (as well as its ...

14
votes

Accepted

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

As I have said in a comment, Levy proves a weak form of the existential property for $ZF$ and $\Pi_2$ sentences. He also proves that his results are best possible. Let me state a simple fact that is ...

Only top scored, non community-wiki answers of a minimum length are eligible

#### Related Tags

constructive-mathematics × 277lo.logic × 137

set-theory × 35

topos-theory × 33

reference-request × 30

ct.category-theory × 26

intuitionism × 20

real-analysis × 19

computability-theory × 19

ac.commutative-algebra × 18

type-theory × 17

proof-theory × 16

foundations × 15

gn.general-topology × 14

reverse-math × 14

locales × 14

model-theory × 11

ag.algebraic-geometry × 10

axiom-of-choice × 10

mathematical-philosophy × 10

ra.rings-and-algebras × 7

homotopy-type-theory × 7

realizability × 7

co.combinatorics × 6

fa.functional-analysis × 6