Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
340 questions
91
votes
10
answers
19k
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 ...
- 1,021
83
votes
4
answers
8k
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....
- 36.2k
60
votes
5
answers
9k
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-...
- 36.2k
53
votes
3
answers
9k
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 ...
- 36.2k
49
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 ...
- 601
46
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 ...
- 69.1k
44
votes
1
answer
5k
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 ...
- 6,235
42
votes
4
answers
5k
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 ...
- 4,603
42
votes
7
answers
4k
views
Precise meaning of "picking a basis"?
Some years ago, Kevin Buzzard wrote a blog post asking whether the trace of a linear map $\phi \colon V \to V$ on a vector space $V$ can be defined "without picking a basis." He had some ...
- 92.3k
39
votes
4
answers
4k
views
Is every real number the limit of a sequence of irrational numbers, constructively?
By $\mathbb{R}$ I mean Dedekind real numbers.
By $X \setminus Y$ I mean $\{x \in X: \neg(x \in Y)\}$.
Let $x \in \mathbb{R}$. Can we construct (without using the law of the excluded middle and the ...
- 1,391
35
votes
4
answers
6k
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 ...
- 20.2k
34
votes
5
answers
4k
views
What can be proven in Peano arithmetic but not Heyting arithmetic?
I'll confess from the start to not being a logician. In fact this question came up not from research but during a discussion with a friend about whether the classical proof that $\sqrt{2}$ is ...
- 2,291
34
votes
4
answers
4k
views
Why is it so difficult to define constructive cardinality?
Consider Frege's cardinality and HoTT set-truncation cardinality, both of which can be well-defined in constructive theory (as SetoidTT and CubicalTT, respectively). Why don’t we regard them as well ...
- 1,553
34
votes
7
answers
3k
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 ...
34
votes
3
answers
4k
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 ...
- 20k