Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
79 questions
14
votes
1
answer
911
views
Kleene realizability in Peano arithmetic
For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question ...
- 41k
13
votes
5
answers
6k
views
reduced ⊗ reduced = reduced; what about connected?
Several questions actually.
All rings and algebras are supposed to be commutative and with $1$ here.
(1) Let $k$ be a field, and let $A$ and $B$ be two $k$-algebras. I need a proof that if $A$ and $...
- 36.2k
8
votes
4
answers
2k
views
Are all group monomorphisms regular, constructively?
Are all group monomorphisms regular, constructively?
By "constructive" I mean something that would go through in CZF for example.
[added Oct 6]
A sketch of a standard proof (such as referenced in ...
- 91
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
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
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
31
votes
6
answers
4k
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$ ...
- 69.1k
21
votes
6
answers
2k
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
1
answer
1k
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 ...
- 5,757
11
votes
5
answers
4k
views
Is there any physical or computational justification for non-constructive axioms such as AC or excluded middle?
I became interested in mathematics after studying physics because I wanted to better understand the mathematical foundations of various physical theories I had studied such as quantum mechanics, ...
- 6,235
10
votes
2
answers
1k
views
Proof in constructive mathematics that the principal square root function exists in any Cauchy complete Archimedean ordered field
In classical mathematics, there exists only one Cauchy complete Archimedean ordered field, the Dedekind complete Archimedean ordered field. However, in constructive mathematics, there are multiple ...
user483446
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
27
votes
1
answer
3k
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 ...
- 41k
23
votes
3
answers
4k
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 ...
- 69.1k
20
votes
5
answers
2k
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 $\...
- 5,063