Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
281
questions
89
votes
10
answers
17k
views
Is there any formal foundation to ultrafinitism?
Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to Wikipedia, it has been ...
81
votes
4
answers
7k
views
Wanted: a "Coq for the working mathematician"
Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar with....
57
votes
5
answers
8k
views
How to make Ext and Tor constructive?
EDIT: This post was substantially modified with the help of the comments and answers. Thank you!
Judging by their definitions, the $\mathrm{Ext}$ and $\mathrm{Tor}$ functors are among the most non-...
52
votes
3
answers
7k
views
Function extensionality: does it make a difference? why would one keep it out of the axioms?
Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...
46
votes
4
answers
5k
views
How to rewrite mathematics constructively?
Many mathematical subfields often use the axiom of choice and proofs by contradiction. I heard from people supporting constructive mathematics that often one can rewrite the definitions and theorems ...
45
votes
2
answers
3k
views
The formal p-adic numbers
The real numbers can be defined in two ways (well, more than two, but let's stick to these for now): as the Cauchy completion of the metric space $\mathbb{Q}$ with its usual absolute value, or as the ...
43
votes
1
answer
4k
views
Constructive algebraic geometry
I was just watching Andrej Bauer's lecture Five Stages of Accepting Constructive Mathematics, and he mentioned that in the constructive setting we cannot guarantee that every ideal is contained in a ...
39
votes
4
answers
4k
views
Illustrating Edward Nelson's Worldview with Nonstandard Models of Arithmetic
Mathematician Edward Nelson is known for his extreme views on the foundations of mathematics, variously described as "ultrafintism" or "strict finitism" (Nelson's preferred term), which came into the ...
33
votes
7
answers
2k
views
List of proofs where existence through probabilistic method has not been constructivised
The probabilistic method as first pioneered by Erdős (although others have used this before) shows the existence of a certain object. What are some of the most important objects for which we can show ...
32
votes
4
answers
5k
views
Does the Brouwer fixed point theorem admit a constructive proof?
Wikipedia and a few websites (and a few mathoverflow answers) say there is a constructive proof of the Brouwer fixed point theorem, some others say no. The argument for a constructive proof is always ...
31
votes
4
answers
5k
views
How Would an Intuitionist Prove This?
My question concerns the proof of the following: Let $a,b,n \in \mathbb{N}$. If $n \neq 1$ and $n$ divides both $a$ and $b$, then $b$ is a composite number or $b$ divides $a$. My proof:
Suppose $b$ ...
29
votes
3
answers
3k
views
What facts in commutative algebra fail miserably for simplicial commutative rings, even up to homotopy?
Simplicial commutative rings are very easy to describe. They're just commutative monoids in the monoidal category of simplicial abelian groups. However, I just realized that a priori, it's not clear ...
27
votes
13
answers
3k
views
Are there any good nonconstructive "existential metatheorems"?
Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...
27
votes
4
answers
11k
views
Does constructing non-measurable sets require the axiom of choice?
The classic example of a non-measurable set is described by wikipedia. However, this particular construction is reliant on the axiom of choice; in order to choose representatives of $\mathbb{R} /\...
26
votes
6
answers
3k
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$ ...
24
votes
1
answer
2k
views
In what ways is ZF (without Choice) "somewhat constructive"
Let me summarize what I think I understand about constructivism:
"Constructive mathematics" is generally understood to mean a variety of theories formulated in intuitionist logic (i.e., not assuming ...
22
votes
6
answers
3k
views
How strong is Cantor-Bernstein-Schröder?
There are several questions here on MO about the Cantor-Bernstein-Schröder ((C)BS) theorem, but I could not find answers to what arose to me recently.
Although I don't think I need to recall it here, ...
21
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 ...
21
votes
4
answers
3k
views
In the category of sets epimorphisms are surjective - Constructive Proof?
The statement that surjective maps are epimorphisms in the category of sets can be shown in a constructive way.
What about the inverse?
Is it possible to show that every epimorphism in the category ...
21
votes
3
answers
3k
views
Approximate intermediate value theorem in pure constructive mathematics
The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise ...
20
votes
4
answers
3k
views
How constructive is Doyle-Conway's 'Division by three'?
In the (whimsically written) article Division by three, Doyle and Conway describe a proof, (apparently) not using Choice, that an isomorphism $A \times 3 \simeq B\times 3$ of sets (where $3$ is a ...
20
votes
2
answers
2k
views
Is it possible to constructively prove that every quaternion has a square root?
Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many"...
20
votes
3
answers
875
views
Brouwer's theorem for the Cauchy reals
Brouwer famously proved, using principles motivated by intuitionistic choice sequences, that every function $\mathbb{R}\to \mathbb{R}$ is continuous. In Sheaves in geometry and logic (section VI.9), ...
19
votes
5
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
2
answers
874
views
Constructive proof of existence of free algebras for infinitary equational theories
Is it constructively true that all (not necessarily finitary) equational theories $T = (\Sigma, E)$ have an initial model?
The usual proof for finitary equational theories I know constructs first ...
19
votes
3
answers
1k
views
How to construct a constructive proof from a non-constructive proof using prime ideals?
The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^...
18
votes
4
answers
3k
views
What is neutral constructive mathematics
In Mike Shulman's answer to Initiation to constructive mathematics, he discusses how "neutral constructive mathematics" is the fashionable topic in constructive mathematics. When ...
18
votes
3
answers
2k
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 ...
18
votes
2
answers
1k
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 ...
17
votes
9
answers
3k
views
Direct construction of the integers
Question. Is there a direct construction of the integers which does not involve taking any quotients?
I am of course aware of the usual construction. I am also aware of the nice axiomatic ...
17
votes
4
answers
2k
views
reference request : constructive measure theory
As the title said, I would like to know if constructive measure theory has been developed somewhere ?
I am more precisely interested in the (constructive) theory of completely continuous valuation on ...
17
votes
2
answers
1k
views
Constructive homological algebra in HoTT
I'm curious how much of homological algebra carries over to a constructive setting, like say HoTT (or some other variety of intensional type theory) without AC or excluded middle. There doesn't seem ...
17
votes
1
answer
1k
views
In constructive mathematics, why does the category of abelian groups fail to be abelian?
I was reading the paper Towards Constructive Homological Algebra in
Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...
17
votes
2
answers
640
views
Locales in constructive mathematics
It is well known that locales are much more well behaved in a constructive setting than topological spaces. Nevertheless, many authors develop the theory of locales in classical mathematics. Are there ...
17
votes
4
answers
2k
views
Constructive proof that a kernel consists of nilpotent elements
I am interested in the following innocent looking statement:
Let $A \leftarrow R \rightarrow B$ be two homomorphisms of commutative rings. Assume that their kernels consist of nilpotent elements. ...
17
votes
2
answers
1k
views
Constructive proof of a rational version of Perron-Frobenius?
In the following, we work with vectors and matrices whose entries are rational numbers. Inequalities between such vectors are understood to be coordinatewise: e.g., two vectors $a = \left(a_1,a_2,\...
17
votes
1
answer
698
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 ...
17
votes
4
answers
1k
views
In choiceless constructivism: If $f'=0$ then is $f$ constant?
Prove, without any Choice principles or Excluded Middle, that if a pointwise differentiable function has derivative $0$ everywhere, then it is constant. The function in this case maps $\mathbb R$ to $\...
17
votes
1
answer
652
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 $\...
17
votes
0
answers
352
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 ...
16
votes
1
answer
1k
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?
16
votes
2
answers
796
views
Cauchy real numbers with and without modulus
In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers ...
16
votes
1
answer
1k
views
Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?
Background
In constructive set theory (say based on CZF) there are inequivalent ways of stating the continuum hypothesis. Some of them are easily if not trivially refutable with common anti-classical ...
16
votes
1
answer
2k
views
Axioms of Choice in constructive mathematics
There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC)
$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...
15
votes
5
answers
1k
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 ...
15
votes
3
answers
2k
views
Are all functions in Bishop's constructive mathematics continuous?
When I started to write this question I was really confused, but now I think I am starting to get it. Nonetheless I'd like some confirmation that my understanding is correct.
I have read, heard said,...
15
votes
3
answers
1k
views
Ordinals in constructive mathematics ? (references)
I'm looking for references presenting a constructive treatment of the theory of ordinals. By constructive I mean valid in the internal logic of a topos (so no axiom of choice and no law of excluded ...
15
votes
1
answer
563
views
Constructive Mathematics and Termination
In the 1988 book The Universal Turing Machine A Half-Century Survey
there is the paper "The Confluence of Ideas in 1936" by Robin Gandy. In section 4.2, Gandy writes:
"If one accepts, on whatever ...
14
votes
8
answers
3k
views
Are there any mathematical objects that exist but have no concrete examples? [closed]
I am curious as to whether there exists a mathematical object in any field that can be proven to exist but has no concrete examples? I.e., something completely non-constructive. The closest example ...
14
votes
1
answer
2k
views
Bishop quote stating that axiom of choice is constructively valid
This is about constructive mathematics, but it is not a research question. But since it may also be of interest for research mathematicians, I hope this question is appropriate for this forum. As ...