Questions tagged [constructive-mathematics]

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

Filter by
Sorted by
Tagged 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-...
darij grinberg's user avatar
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 ...
Keshav Srinivasan's user avatar
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 ...
coudy's user avatar
  • 18.5k
13 votes
1 answer
599 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 ...
Gro-Tsen's user avatar
  • 29.9k
12 votes
5 answers
5k 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 $...
darij grinberg's user avatar
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$ ...
Mike Shulman's user avatar
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 ...
Gro-Tsen's user avatar
  • 29.9k
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 ...
Simon Henry's user avatar
  • 39.9k
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. ...
HeinrichD's user avatar
  • 5,402
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 $\...
wlad's user avatar
  • 4,823
16 votes
1 answer
688 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 ...
Manuel Bärenz's user avatar
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,...
Jason Rute's user avatar
  • 6,237
10 votes
5 answers
2k 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, ...
ಠ_ಠ's user avatar
  • 5,933
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 ...
Monic Win's user avatar
8 votes
3 answers
2k views

Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
Keshav Srinivasan's user avatar
7 votes
2 answers
522 views

Artin Jacobson-semisimple rings are semisimple. Constructively, too?

Notation. When I say "ring", I mean "ring with unity" (not necessarily commutative). Definition. A ring $R$ is said to be left-Artinian if for every sequence $I_0\supseteq I_1\supseteq I_2\supseteq ...
darij grinberg's user avatar
7 votes
1 answer
379 views

Every complex number has a square root via LLPO without weak countable choice

Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed. (Analytic LLPO is the ...
wlad's user avatar
  • 4,823
3 votes
1 answer
369 views

Compactness in Bishop's constructive mathematics

In Bishop's constructive mathematics, is there any literature on a possible version of the weak König's lemma, or of the compactness theorem for countable models? There is some related information ...
Mikhail Katz's user avatar
  • 15.1k
89 votes
10 answers
16k 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 ...
Michael O'Connor's user avatar
82 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....
darij grinberg's user avatar
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 ...
ಠ_ಠ's user avatar
  • 5,933
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 ...
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 ...
Mike Shulman's user avatar
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"...
wlad's user avatar
  • 4,823
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^...
HeinrichD's user avatar
  • 5,402
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 ...
Peter LeFanu Lumsdaine's user avatar
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,\...
darij grinberg's user avatar
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 . \...
Rubi Shnol's user avatar
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 ...
Simon Henry's user avatar
  • 39.9k
14 votes
1 answer
1k views

Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...
Zhen Lin's user avatar
  • 14.9k
13 votes
0 answers
270 views

Ordinal-valued sheaves as internal ordinals

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
  • 29.9k
12 votes
1 answer
867 views

Are the “topologies” arising from constructive type theories with quotients actually condensed sets?

This is the second in a pair of questions. For the other see Are representations in computable analysis the equivalent to countably-generated condensed sets?. Dustin Clausen and Peter Scholze have a ...
Jason Rute's user avatar
  • 6,237
10 votes
3 answers
1k views

Is set-induction relatively consistent?

One way to state the axiom of foundation is that the $\in$ relation on any transitive set is well-founded in the following sense: A relation $(X,\prec)$ is well-founded if for any subset $S\subseteq ...
Mike Shulman's user avatar
10 votes
1 answer
409 views

A weak form of countable choice

Let $\Omega$ be the set/type of truth values. We're using constructive logic. Define $AC_{0, 0} = \forall P : \mathbb{N}^2 \to \Omega, (\forall n \in \mathbb{N}, \exists m \in \mathbb{N}, P(n, m)) \to ...
Mark Saving's user avatar
9 votes
1 answer
461 views

Is every set smaller than a regular cardinal, constructively?

Constructively, my only interest in regular cardinals is in terms of the “$\Sigma$-universes” they generate. By a $\Sigma$-universe, I mean a collection of triples $(X,Y,f: X \to Y)$ closed under base ...
Tim Campion's user avatar
  • 60.6k
9 votes
2 answers
563 views

Birkhoff's completeness theorem put into practice

Birkhoff's completeness theorem (see here, Theorem 14.19) states that an equation which is true in all models of an algebraic theory can be proven in equational logic. Question. Does the proof of ...
Martin Brandenburg's user avatar
9 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 ...
Madeleine Birchfield's user avatar
9 votes
3 answers
2k views

Initiation to constructive mathematics

What are some good introductory references to constructive mathematics for non-specialist mathematicians? I would like to learn more about constructive mathematics, just to improve my general ...
AGenevois's user avatar
  • 7,481
8 votes
1 answer
430 views

Reference request: proof-theoretic strength of $\mathsf{KP}$ with recursively large ordinals and $\mathsf{CZF}$ with large set axioms

Large set axioms are notions corresponding to large cardinals on constructive set theories like $\mathsf{IZF}$ or $\mathsf{CZF}$. The notion of inaccessible sets, Mahlo sets, and 2-strong sets ...
Hanul Jeon's user avatar
  • 2,774
8 votes
1 answer
257 views

What is known about these "explicitly represented" spaces?

Apologies if this is too low-level. A related question that I asked on the Math Stack Exchange got no answers after a year, so I thought it might be better to ask this one here. The standard approach ...
Robin Saunders's user avatar
7 votes
4 answers
2k views

Strict and non-strict orderings

Consider a set $A$ equipped with two binary relations $\le$ and $<$, related in the appropriate ways for the strict and non-strict version of an ordering. One might make different choices about ...
Mike Shulman's user avatar
7 votes
0 answers
582 views

A new and subtle order-theoretic fixed point theorem

Sometimes a very simple argument appears out of the blue and overturns a subject. It is not based on pre-existing theory and heavy involvement in such a theory is actually a handicap in finding such ...
Paul Taylor's user avatar
  • 7,986
7 votes
7 answers
627 views

Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used in ...
Jason Rute's user avatar
  • 6,237
6 votes
1 answer
243 views

Archimedean ordered fields without maxima and minima in constructive mathematics

In constructive mathematics, let us define an ordered (Heyting) field $F$ to be a commutative ring with a binary relation $<$ which is irreflexive, where for all $x$, $\neg (x < x)$ asymmetric, ...
Madeleine Birchfield's user avatar
6 votes
1 answer
276 views

Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.) Background: I'm trying to understand ...
Gro-Tsen's user avatar
  • 29.9k
6 votes
1 answer
316 views

Proper definition of ordered field in constructive mathematics

The nLab article on ordered fields defines ordered fields to be a field $K$ with a strict linear order $<$ such that $0 < 1$ and for all elements $a \in K$ and $b \in K$, if $a > 0$ and $b &...
Madeleine Birchfield's user avatar
5 votes
3 answers
832 views

Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...
Keshav Srinivasan's user avatar
5 votes
2 answers
881 views

What is the status of the extreme value theorem in forms of constructive mathematics, such as Smooth Infinitesimal Analysis?

In certain intuitionistic frameworks the extreme value theorem cannot be proved. Depending on the exact framework, counterexamples can be constructed as well; see for example pp. 294-295 in Troelstra,...
Mikhail Katz's user avatar
  • 15.1k
4 votes
0 answers
312 views

Is intuitionistic predicate logic (semantically) complete or incomplete?

According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc ...
ToucanIan's user avatar
  • 391
4 votes
1 answer
249 views

Constructing ordered fields with lattice structure from ordered fields without lattice structure, and vice versa, in constructive mathematics

This post originated from my reference request for the definition of an ordered field in constructive mathematics: Proper definition of ordered field in constructive mathematics We are working in ...
Madeleine Birchfield's user avatar