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
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 ...
Madeleine Birchfield's user avatar
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 (...
Gro-Tsen's user avatar
  • 29.9k
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; ...
Madeleine Birchfield's user avatar
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 ...
Lxm's user avatar
  • 313
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 ...
saolof's user avatar
  • 1,823
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 ...
Gro-Tsen's user avatar
  • 29.9k
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 ...
saolof's user avatar
  • 1,823
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)=...
CACM6's user avatar
  • 31
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 ...
Gro-Tsen's user avatar
  • 29.9k
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....
Christopher King's user avatar
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 ...
Jim Kingdon's user avatar
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$,...
Madeleine Birchfield's user avatar
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 ...
Madeleine Birchfield's user avatar
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 $...
Madeleine Birchfield'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
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
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
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 ...
Felix Schröder's user avatar
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 ...
dodo's user avatar
  • 589
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 ...
Tim Campion's user avatar
  • 60.6k
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, ...
saolof's user avatar
  • 1,823
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 ...
user avatar
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 $\...
user avatar
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?
Joe Shipman's user avatar
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, ...
Gro-Tsen's user avatar
  • 29.9k
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 ...
Gro-Tsen's user avatar
  • 29.9k
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)) \...
ToucanIan's user avatar
  • 391
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 ...
ToucanIan's user avatar
  • 391
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 ...
ToucanIan's user avatar
  • 391
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$ ...
Arrow's user avatar
  • 10.3k
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$,...
Arshak Aivazian's user avatar
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 ...
wlad's user avatar
  • 4,823
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 \...
Jordan Mitchell Barrett's user avatar
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 ...
Gro-Tsen's user avatar
  • 29.9k
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 ...
ToucanIan's user avatar
  • 391
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 ...
saolof's user avatar
  • 1,823
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)) \...
ToucanIan's user avatar
  • 391
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 ...
Arrow's user avatar
  • 10.3k
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
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 ...
Jason Rute's user avatar
  • 6,237
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 $...
ToucanIan's user avatar
  • 391
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 ...
wlad's user avatar
  • 4,823
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 ...
BPP's user avatar
  • 665
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$ ...
wlad's user avatar
  • 4,823
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
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 ...
ToucanIan's user avatar
  • 391
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 ...
Mohsen Shahriari's user avatar
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 |\...
Motaka's user avatar
  • 291
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 ...
Léreau's user avatar
  • 211