Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
252
questions
6
votes
2
answers
542
views
In the constructive theory of direct categories, is it decidable whether an arbitrary morphism is an identity or not?
I'm wondering what the legit definition of direct categories should be in constructive mathematics. I must admit I don't even know in what literature I should look for the definition. I would ...
- 233
12
votes
0
answers
116
views
Limits in free cocompletion, constructively
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 ...
- 38.5k
20
votes
4
answers
2k
views
Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He ...
- 405
3
votes
0
answers
117
views
Does negative trichotomy hold for constructive ordinals?
I don't know if there is a standard term for this, but by "negative trichotomy" I mean ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴). This holds for constructive real numbers as an easy ...
- 163
7
votes
0
answers
199
views
How strong is the Schröder–Bernstein theorem where one set is the natural numbers?
The full Schröder-Bernstein theorem states that given an injection from A to B and also one from B to A, there is a bijection between A and B. It is equivalent to excluded middle, as shown in the ...
- 163
4
votes
0
answers
122
views
Do presheaf toposes satisfy the full fan theorem?
Presheaf toposes satisfy LPO and (edit: if over categories with binary products) PAx and countable choice internally, so they automatically satisfy the stable fan theorem (every bar which is the ...
- 1,783
7
votes
0
answers
151
views
Constructive theory of Lie algebras
I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is ...
- 5,753
2
votes
0
answers
137
views
Do Grothendieck topoi with enough points satisfy the fan theorem internally?
Fourman and Hylland proved in the 80s that all spatial topoi satisfy the full fan theorem internally, while there are examples of localic topoi that do not satisfy it.
This leads one to conjecture a ...
- 1,783
9
votes
0
answers
142
views
Are there good criteria for the topological models where BD-N and BD hold?
A (non-empty/inhabited) subset $S$ of $\mathbb{N}$ is said to be pseudo-bounded if for every sequence $x_n$ in $S$ we have
$\lim_{n\to \infty} \frac{x_n}{n} = 0$
Clearly all bounded subsets are pseudo-...
- 1,783
6
votes
1
answer
232
views
Does a tight apartness relation on a subobject classifier imply the elementary topos is Boolean?
Given a set $S$, a tight apartness relation on $S$ is a relation $\#$ which is tight, irreflexive, symmetric, and a comparison, or more specifically, a relation $\#$ such that
for all elements $a \in ...
- 1,826
4
votes
0
answers
72
views
Constructively valid reference for the soberness of discrete spaces and points of a locale coproduct
I am looking for constructively valid references for the following two related facts:
discrete topological spaces are sober,
the points of a locale coproduct are the disjoint union of the points of ...
- 27.8k
7
votes
0
answers
512
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,697
5
votes
1
answer
131
views
Constructive proof of univariate McCoy theorem without Dedekind-Mertens?
McCoy's theorem (one of them) says that for any commutative ring $A$, $f\in A[x]$ is a zero-divisor iff it's annihilated by a scalar in $A$.
There's a widespread proof by contradiction. There's also a ...
- 10.2k
7
votes
2
answers
426
views
Continuous nowhere differentiability and constructive mathematics
In some constructive systems, every function from $\mathbb{R}\to\mathbb{R}$ is continuous (roughly speaking from the classical fact that computable functions are continuous). More weakly, in Bishop's ...
- 620
5
votes
0
answers
152
views
Moduli all the way down
The notion of modulus of continuity is well-known from constructive mathematics, reverse mathematics, and computability theory. Intuitively, such a modulus is a function that returns the '$\delta>...
- 3,321
8
votes
0
answers
303
views
What is the relationship (if any) between constructivism, finitism and predicativism?
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 ...
- 27.8k
5
votes
0
answers
132
views
Weaker versions of the Riemann series theorem in constructive mathematics
The classical Riemann series theorem states that given a sequence $(a_n)_{n \in \mathbb{N}}$ of real numbers such that the series $\sum_{n = 0}^\infty a_n$ is conditionally convergent, for all real ...
- 1,826
3
votes
0
answers
210
views
Has an uncomputable variant of the Cantor staircase ever been used in constructive logic?
An open problem in choiceless constructivism is to prove that if a function $f:\mathbb R \to \mathbb R$ is pointwise differentiable everywhere, with $f'=0$, then $f$ is constant. See In choiceless ...
- 4,732
7
votes
0
answers
196
views
New Foundations in a Homotopy/Intuitionistic Type Theory form?
New Foundations is a famously odd set theory suggested by Quine in the 1930s which:
Features a universal set.
Disproves the axiom of choice.
Proves the existence of an infinite set by a trivial ...
- 4,732
12
votes
2
answers
526
views
Is the Intermediate Value Theorem strictly stronger than LLPO?
(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.)
By LLPO, I mean the statement that ...
- 4,732
7
votes
2
answers
436
views
What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?
Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, ...
- 27.8k
6
votes
0
answers
123
views
Complexity of constructive arithmetical truth vs second order arithmetic
Let us say that an arithmetic statement is constructively true iff it is realized by a computable function under Kleene's function realizability. Does the set of constructively true (first order) ...
- 5,742
12
votes
1
answer
356
views
Tarski-Seidenberg for strict inequalities and bounded quantification
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 ...
- 7,697
7
votes
1
answer
263
views
For which Sheaf topoi is Brouwer's fan theorem true?
Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable ...
- 1,783
3
votes
1
answer
126
views
Does CZF prove there is a minimal cauchy completion of the rationals?
In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields.
CZF can ...
- 4,675
7
votes
1
answer
273
views
Status of the fundamental theorem of algebra for the locale of real numbers
In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed ...
- 1,826
7
votes
1
answer
123
views
Invertibility and comparison to zero in the MacNeille sections (bounded extended reals)
(The following three paragraphs are given for context. Readers already aware of the terminology can skip to “the problem” below.)
In a spatial topos $\mathop{\textbf{Sh}}(X)$ the MacNeille sections (...
- 27.8k
4
votes
3
answers
328
views
The field structure on the locale of real numbers
It is well known how to derive the field operations from the construction of the real numbers as the Dedekind completion of the rational numbers and as the Cauchy completion of the rational numbers; ...
- 1,826
7
votes
0
answers
176
views
Weakest theory over which "all sets are measurable" has consistency strength?
Some convention: $\textrm{DC}$ stands for axiom of dependent choice, $\text{LM}$ stands for the statement "all subsets of $\mathbb{R}$ are Lebesgue measurable", $\textrm{IC}$ for "there ...
- 171
5
votes
0
answers
149
views
Do quasi-excellent rings have a good constructive definition?
$\DeclareMathOperator\Sh{Sh}$Informally, a quasi-excellent ring is a Noetherian ring with a few technical extra regularity conditions that make it turns out to be the largest class of rings that allow ...
- 1,783
9
votes
1
answer
266
views
Are finitely enumerated and subfinite sets Dedekind-finite?
The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF.
Let us say that a set $X$ is:
finite when there exists a ...
- 27.8k
8
votes
0
answers
315
views
Why is the double negation of the axiom of choice rarely considered?
In constructive/intuitionistic mathematics, it is common to reject the axiom of choice, because it is highly nonconstructive and implies the law of the excluded middle by Diaconescu's theorem/Bishop's ...
- 1,783
3
votes
1
answer
148
views
Using generating functions to construct or solve differential equations
I know that $T_n(x)$ is the solution of the differential equation $(1-x^2)y''-xy'+n^2y=0$, where
$$
T_n(x)=\begin{cases}
T_n(x)=1 & \text{if $n=0$}\\
T_n(x)=x & \text{if $n=1$}\\
T_{n}(x)=...
- 31
17
votes
0
answers
336
views
Joyal's topos in which $[0,1]$ fails to be compact
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 ...
- 27.8k
7
votes
3
answers
433
views
Is there a constructive version of internal set theory?
Is there a theory T such that:
T includes all the axioms of CZF.
T includes the Idealization, Standardization, and Transfer schemas from IST.
Every axiom of T is a theorem of IST.
T has Church's rule....
- 4,675
0
votes
1
answer
365
views
Did I find a few (small) errors in the Pradic and Brown 2021 paper that Schroeder-Bernstein implies excluded middle?
I'm looking at the https://arxiv.org/abs/1904.09193 paper (version 2, from 2021) and think it has a few errors. I think I found three small places where the paper needs to be corrected (in the sense ...
- 163
3
votes
0
answers
63
views
Discreteness of the higher inductive-inductive Cauchy real numbers in real cohesive homotopy type theory
We work in cohesive homotopy type theory with propositional resizing, so that there is only one type of Dedekind real numbers $\mathbb{R}$ up to equivalence, and Mike Shulman's axiom $\mathbb{R}\flat$,...
- 1,826
4
votes
1
answer
230
views
Equivalence of real numbers in terms of Dedekind cuts and Cauchy nets of rational numbers
We work in weakly predicatively constructive mathematics, in that we accept function sets but do not accept power sets or excluded middle. More specifically, we shall assume a sequential universe ...
- 1,826
3
votes
0
answers
244
views
Principle of unique choice in homotopy type theory
In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be
if $R$ is a relation between two sets $A$, $B$, and for every $...
- 1,826
9
votes
2
answers
931
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 ...
- 1,826
2
votes
1
answer
209
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 ...
- 1,826
5
votes
1
answer
258
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 &...
- 1,826
4
votes
1
answer
249
views
Construction of graphs of high girth and chromatic number
Are there any concrete constructions of graphs of both high girth and chromatic number?
Of course there is the seminal paper of Erdős which proves the existence of such graphs via the probabilistic ...
- 128
4
votes
0
answers
373
views
Simple constructive proof for the hyperplane separating theorem (HST)?
The Hyperplane Separation Theorem (HST) is usually proved through the existence of a unique minimum-norm vector in a nonempty closed convex set. I think this is an existential proof which applies to ...
- 579
4
votes
1
answer
281
views
For which "permutation groups" is the sign homomorphism well-defined constructively?
Let $X$ be a finite set. I now have a favorite construction of the sign homomorphism $Sym(X) \to C_2$. But perhaps it shouldn't be my favorite construction.
After discussion with the experts, I've ...
- 56.6k
10
votes
2
answers
385
views
Is there a purely constructive presentation of the HK integral?
Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...
- 1,783
6
votes
1
answer
397
views
Is Solèr’s theorem true in constructive mathematics?
Solèr’s theorem says that for every star division ring $R$ and every $R$-module $H$ with an orthomodular Hermitian form $\langle (-),(-) \rangle:H \times H \to R$ such that there exists an infinite ...
user173426
17
votes
1
answer
611
views
Is Hurwitz's theorem true in constructive mathematics?
Hurwitz's theorem says that the only division composition algebras over the real numbers $\mathbb{R}$ are the real numbers themselves $\mathbb{R}$, the complex numbers $\mathbb{C}$, the quaternions $\...
user173426
16
votes
1
answer
980
views
Easiest proof of computability of homotopy groups of spheres
Has it gotten easier to prove all homotopy groups of spheres are computable? I don’t care if the computation is inefficient, what’s the easiest proof? Are we still stuck doing Postnikov towers?
- 595
9
votes
1
answer
405
views
Is Heyting arithmetic sufficient to prove its own (formalized) existence property?
Let $\mathsf{HA}$ denote first-order Heyting arithmetic (viꝫ., Peano axioms with unrestricted recursion scheme, in first-order intuitionistic logic). It is known (e.g., Troelstra & van Dalen, ...
- 27.8k