Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
340 questions
3
votes
1
answer
374
views
Injective envelopes, constructively?
Question 0:
How do injective envelopes work in constructive mathematics?
For example,
Question 1: How strong is it to assert internally that there are enough injectives (in the category of sets, say)? ...
- 68.1k
9
votes
0
answers
109
views
Does $\mathsf{IZF}_{\mathrm{Rep}}$ prove that $L_{\omega_1^{\mathrm{CK}}}$ is a model of $\mathsf{IKP}$ (with $\Sigma_0$-collection)?
Let $\def\IZF{\mathsf{IZF}_{\mathrm{Rep}}}\IZF$ be intuitionistic Zermelo-Fraenkel set theory with the replacement scheme. (See this SEP article for a definition of the replacement scheme.) Let $\def\...
- 21.4k
15
votes
0
answers
524
views
What is the relation between the constructive Hilbert basis theorem and the theory of Gröbner bases?
Gröbner bases are often praised for their effectiveness in providing algorithmic solutions to problems in commutative algebra which a priori don't have an obvious computational solution.
For example, ...
- 1,816
8
votes
0
answers
147
views
Constructive status of the meta-theory of intuitionistic propositional logic
Intuitionistic propositional logic has several kinds of models. Bezhanishvili and Holliday [1] showed that these models form a neat hierarchy:
Kripke
Beth
Topological
Dragalin
Heyting
in the order ...
- 180
8
votes
2
answers
238
views
On formal systems for $\mathsf{BISH}$, $\mathsf{INT}$, and $\mathsf{RUSS}$ in constructive reverse mathematics
In informal constructive reverse mathematics, one typically works in Bishop-style constructive mathematics ($\mathsf{BISH}$) as a base theory and studies the strength of various principles over it (...
- 1,391
5
votes
0
answers
205
views
What is known about the structure of cardinalities under Church's thesis?
In a previous discussion (Question 491454), we explored the inherent difficulties in having a well-defined cardinality within constructive models.
Given these subtleties, I am interested in how the ...
- 1,553
7
votes
2
answers
181
views
Reference request for uniform separation of closed sets
I am looking for a reference for the following separation principle.
Let $(C_n)_{n \in \mathbb{N}}$ and $(D_n)_{n \in \mathbb{N}}$ be
sequences of closed and non-empty sets in the unit interval ...
- 4,411
20
votes
1
answer
537
views
Which non-constructive principle is equivalent to the isomorphism between Dedekind reals and Cauchy reals?
When I say that $x$ is a Dedekind real, I mean that $x$ is a left Dedekind cut of the rational numbers; that is, $x \subseteq \mathbb{Q}$ satisfying the following properties:
$\exists r,s \in \mathbb{...
- 1,391
5
votes
1
answer
248
views
In a topos, the subobject classifier is a compact locale?
Constructively, it is true that for any distributive lattice $D$, its ideal completion $Idl(D)$ is a coherent locale (thus in particular compact). It is also well-known that $\Omega$ in a topos $\...
- 407
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
7
votes
2
answers
520
views
Cauchy completeness in ordered families of equivalences, constructively
An ordered family of equivalences (OFE) is a set $X$ equipped with an $\omega$ indexed family of equivalence relations $\approx_i$ that are increasingly fine-grained in that if $x \approx_{i+1} y$ ...
- 1,081
5
votes
1
answer
1k
views
Is there a natural topos where the Riemann hypothesis is provable or disprovable?
While constructive logic is compatible with classical logic and is sufficient to develop almost all important theorems from classical complex analysis, constructive is also compatible with axioms that ...
- 2,159
7
votes
1
answer
461
views
How to do this computation inside a free module over a connected ring constructively?
Let $k$ be a commutative ring. For a set $M$, denote by $k[M] = \bigoplus_{m \in M} k \cdot m$ the free $k$-module generated by the elements of $M$.
In the end, my question will be about constructive ...
- 1,816
24
votes
4
answers
2k
views
Why and how do (classical) reverse mathematics and intuitionistic reverse mathematics relate?
Broadly speaking, the idea of “reverse mathematics” is to find equivalents to various standard mathematical statements over a weak base theory, in order to gauge the strength of theories (sets of ...
- 41k
8
votes
1
answer
379
views
Is van Dalen’s “open problem” about $\bf{CT}$ and indecomposability actually open?
In the paper "How connected is the intuitionistic continuum", D. van Dalen proves that in intuitionistic mathematics, the set $\mathbb{R} \setminus \mathbb{Q}$ is indecomposable, which means ...
- 1,391