Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
54
questions
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-...
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 ...
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 ...
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 ...
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 $...
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$ ...
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 ...
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 ...
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. ...
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 $\...
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 ...
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,...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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....
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 ...
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 ...
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"...
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^...
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 ...
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,\...
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 . \...
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 ...
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 ...
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 $\{\...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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 ...
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 &...
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 ...
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,...
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 ...
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 ...