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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Simon Henry's user avatar
  • 39.9k
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 ...
Carl Mummert's user avatar
  • 9,603
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 ...
Andrej Bauer's user avatar
  • 47.6k
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 ...
Andrej Bauer's user avatar
  • 47.6k
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) ...
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 ...
James Hanson's user avatar
  • 10.3k
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. ...
Valery Isaev's user avatar
  • 4,390
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
François G. Dorais's user avatar
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 ...
aws's user avatar
  • 3,836
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 ...
Mitchell Spector's user avatar
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 ...
Andrej Bauer's user avatar
  • 47.6k
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,...
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 ...
Todd Trimble's user avatar
  • 52.2k
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 ...
Simon Henry's user avatar
  • 39.9k
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 ...
Emil Jeřábek's user avatar
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 ...
Emil Jeřábek's user avatar
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 ...
Peter LeFanu Lumsdaine's user avatar
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 ...
Ingo Blechschmidt's user avatar
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 ...
Valery Isaev's user avatar
  • 4,390
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 ...
Simon Henry's user avatar
  • 39.9k
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 ...
Andrej Bauer's user avatar
  • 47.6k
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.
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 ...
user48801's user avatar
  • 311
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 ...
Andrej Bauer's user avatar
  • 47.6k
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 ...
Mike Shulman's user avatar
  • 64.7k
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 ...
Rodrigo Freire's user avatar

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