Skip to main content
MathOverflow

Questions tagged [constructive-mathematics]

Ask Question

Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.

83 questions with no upvoted or accepted answers
Newest Active Bountied Unanswered
17 votes
0 answers
456 views

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 ...
Gro-Tsen's user avatar
  • 41k
16 votes
0 answers
780 views

Wedderburn's Little Theorem states that every finite division ring is commutative. Perhaps even more surprising, this implies that every finite reduced ring is commutative. The proofs that I am aware ...
Martin Brandenburg's user avatar
  • 67.4k
16 votes
1 answer
3k views

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 . \...
Rubi Shnol's user avatar
  • 811
15 votes
0 answers
524 views

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, ...
Jakob Werner's user avatar
  • 1,816
14 votes
0 answers
256 views

Classically, if a locally small category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits. But all proof I know of that result ...
Simon Henry's user avatar
  • 45.6k
14 votes
2 answers
1k views

This theorem says that quantifiers over real variables can be eliminated from classical first order formulae built from equations and inequalities between polynomials with rational coefficients, ie in ...
Paul Taylor's user avatar
  • 9,324
14 votes
0 answers
381 views

Let $X$ be a topological space (feel free to add some separation axioms like “completely regular” if they help in answering the questions). Let $\alpha$ be an ordinal, identified as usual with $\{\...
Gro-Tsen's user avatar
  • 41k
13 votes
0 answers
705 views

There is a short note by André Joyal called Les théorèmes de Chevalley-Tarski et remarque sur l'algèbre constructive (pp. 256-258). It is claimed there that there is a constructive version of the ...
Valery Isaev's user avatar
  • 4,699
11 votes
0 answers
251 views

This question is set in constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. Short version of the question: if $X$ is a sober ...
Gro-Tsen's user avatar
  • 41k
11 votes
1 answer
452 views

We work in constructive mathematics. The sets and functions in the foundations form a Grothendieck topos, which means that all colimits exist, and in particular, that all sequential colimits exist. ...
user avatar
11 votes
0 answers
662 views

In the talk Unimath - its present and its future, July 10, 2017. Video and slides of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. (abstract) Voevodsky mentioned that he was ...
David Roberts's user avatar
  • 37.3k
11 votes
0 answers
702 views

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement: $F(X) \cong F(Y)$ if and only if $|X|=|Y|$. The proofs (that I have seen) consist of turning the group isomorphism ...
Ali Caglayan's user avatar
  • 1,191
10 votes
0 answers
790 views

The terms “constructivism”, “finitism” and “predicativism” refer to ideas / currents in the philosophy of mathematics (or loosely defined conditions on a system of logic) that I think I understand ...
Gro-Tsen's user avatar
  • 41k
9 votes
0 answers
109 views

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\...
James E Hanson's user avatar
  • 21.4k
9 votes
0 answers
275 views

There are theorems characterizing Kleene's realizability$\def\realize{\mathbin{\textbf{r}}}$ in various systems. For example, $$\textsf{HA} \vdash \exists n,n \realize \varphi \iff \exists n. \textsf{...
Trebor's user avatar
  • 2,592

15 30 50 per page
1
2 3 4 5 6