Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
277
questions
7
votes
1
answer
310
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 ...
7
votes
1
answer
126
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 (...
4
votes
3
answers
430
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; ...
8
votes
1
answer
344
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 ...
5
votes
0
answers
156
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 ...
9
votes
1
answer
318
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 ...
9
votes
0
answers
345
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 ...
3
votes
1
answer
209
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)=...
17
votes
0
answers
350
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 ...
7
votes
3
answers
472
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....
0
votes
1
answer
377
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 ...
3
votes
0
answers
66
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$,...
4
votes
1
answer
286
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 ...
3
votes
0
answers
265
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 $...
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 ...
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 ...
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 &...
4
votes
1
answer
399
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 ...
4
votes
0
answers
551
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 ...
4
votes
1
answer
313
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 ...
10
votes
2
answers
412
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, ...
7
votes
1
answer
419
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 ...
17
votes
1
answer
648
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 $\...
16
votes
1
answer
1k
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?
9
votes
1
answer
447
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, ...
4
votes
1
answer
177
views
Does second-order Heyting arithmetic have the disjunction and existence properties?
Consider full second-order Heyting arithmetic, axiomatized in two-sorted first-order intuitionistic logic (with “number” and “class” variables) by the usual Peano axioms (with induction being stated ...
7
votes
1
answer
291
views
In CZF (w/ Subset Collection removed) the Powerset axiom Implies Subset Collection
The Subset Collection axiom:
$$ \forall a \forall b \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \...
5
votes
1
answer
359
views
Subcountability
In these slides of a talk Giovanni Curi shows that the generalized uniformity principle follows from Troesltra’s uniformity principle and from the subcountability of all sets, which are both claimed ...
2
votes
1
answer
301
views
Collection of proper classes with in CZF
In Aczel's Constructive Set Theory (CZF), no non-degenerate complete lattice can be proved to be a set. There are hallmark examples of complete lattices that are proper classes in CZF, including the ...
3
votes
1
answer
208
views
Alternative definitions of étale and formally unramified in Wraith
I have stumbled upon the following definitions in a paper by Gavin Wraith.
Definition 1. Say a ring morphism $A\overset \varphi \to B$ is formally unramified if every $b\in B$ admits:
$b_0\in B$ ...
8
votes
1
answer
511
views
What is the status of Jordan's theorem in constructive mathematics in the language of locales?
By constructive mathematics in this matter we mean intuitionistic ZF (*).
In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$,...
13
votes
1
answer
807
views
How to express in categorical language that in some toposes not all complex numbers have square roots
I'm trying to improve my ability to translate constructive logic into the category theoretical language of topos theory. So far, my understanding of constructive logic has been rather naive. I know ...
5
votes
1
answer
163
views
Possible values of "Kripke rank" for formulae in IPL
Fix a (countable) set $\mathcal{P}$ of atomic propositional variables. Recall a Kripke model $\mathcal{K}$ for intuitionistic propositional logic (IPL) consists of:
A preorder $(W,\leq)$
For each $w \...
4
votes
1
answer
326
views
Is there a correspondence between principles of omniscience and computability classes?
My question will be speculative and therefore a little vague.
I wonder if attempts have been made to define a correspondence between, on the one hand, limited principles of omniscience that can be ...
3
votes
2
answers
431
views
Constructive lattice completion
The Dedekind–MacNeille Completion is the generalized way of completing an arbitrary lattice $L$. We will call $C$ the Dedekind–MacNeille completion of $L$ (I will not go into the details of the ...
5
votes
4
answers
663
views
What does overtness mean for metric spaces?
Original question:
For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed as a property dual to compactness. So is there a similar ...
3
votes
1
answer
295
views
Subset Collection axiom
In Constructive Set Theory (CZF) the Power Set axiom is replaced with the Subset Collection axiom which I will state here:
$$ \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \...
8
votes
0
answers
295
views
Can you constructively prove a univariate polynomial algebra over a Jacobson ring is itself Jacobson?
Recall the Jacobson radical of a commutative ring $\mathrm J(A)=\lbrace a\in A\mid \forall b\in A:1-ba\in A^\times\rbrace$. The Jacobson radical of a quotient by an ideal $I\vartriangleleft A$ is ...
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 ...
18
votes
4
answers
3k
views
What is neutral constructive mathematics
In Mike Shulman's answer to Initiation to constructive mathematics, he discusses how "neutral constructive mathematics" is the fashionable topic in constructive mathematics. When ...
5
votes
1
answer
435
views
How do working constructivists get by with out the zero product property?
It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property:
If $x,y \in \mathbb{R}$ and $...
2
votes
1
answer
158
views
LLPO as constructivity/computability for dense subsets
LLPO is the statement $\forall x \in \mathbb R. x \leq 0 \vee x \geq 0.$ The statement should be understood as a fragment of the Law of Excluded Middle, rather than a statement about the ordering of ...
5
votes
1
answer
507
views
What is known about constructively irrational numbers?
Intuitively, a constructively irrational number is one for which we can effectively separate it from any rational number in terms of the latter's denominator. More formally, a constructively ...
5
votes
0
answers
162
views
Within pointless topology inside of choiceless constructivism, prove that division is possible
In Frank Waaldijk's paper on the foundations of constructive analysis, Waaldijk shows that various definitions of "continuous function" for functions of the form $f: \mathbb R \to \mathbb R$ ...
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 ...
2
votes
0
answers
139
views
In a constructive order/lattice theory are the arbitrary join and the weak suprema the same?
For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if
$(\forall a \in S (a \leq b)) \implies w \leq b$.
While a supremum is defined more carefully (in ...
7
votes
1
answer
448
views
Realizability for constructive Zermelo-Fraenkel set theory
$ \def \CZF {\mathbf {CZF}}
\def \IZF {\mathbf {IZF}}
\def \A {\mathcal A}
\def \then {\mathrel \rightarrow}
\def \r {\mathrel \Vdash}
\DeclareMathOperator \V V $
In "Realizability for ...
0
votes
1
answer
341
views
What's the condition to prove the equicontinuity?
Let $K: I\times I\rightarrow \mathbb{R}$ be a scalar kernel, where $I=[0,1]$, and $a: I \rightarrow (0,+\infty)$ an $L^1(I)$ function.
For $t_1,t_2\in I$, define
$$I_{t_1,t_2}=\int_{0}^{1} \left |\...
8
votes
1
answer
515
views
Exposition of concrete constructions
I am frequently interested to find less technical proofs of results which already appear in the literature, at least in some special cases of these results. Sometimes a published proof shows that an ...
6
votes
0
answers
410
views
Proof of Tennenbaum's Theorem by McCarty
Tennenbaum's Theorem in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or ...