# Questions tagged [constructive-mathematics]

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

209
questions

3
votes

0
answers

149
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

225
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 ...

7
votes

1
answer

116
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, ...

6
votes

1
answer

351
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

550
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

914
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

315
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

99
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

268
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

254
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

284
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 ...

2
votes

1
answer

183
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

439
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

773
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

139
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

223
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

259
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

563
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

227
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

254
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 ...

3
votes

0
answers

191
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 ...

17
votes

4
answers

2k
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 ...

4
votes

1
answer

370
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

131
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 ...

4
votes

1
answer

341
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

121
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$ ...

11
votes

1
answer

588
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

109
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 ...

6
votes

1
answer

360
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

279
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

470
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

343
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 ...

12
votes

1
answer

728
views

### So after all, what is this thing about topos theory and non-binary truth?

Disclaimer. The question below is necessarily vague. I understand neither the subject matter topos theory nor the object about which my question is (the construction of a fractional / non-binary / ...

8
votes

1
answer

327
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 ...

5
votes

0
answers

154
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 ...

8
votes

3
answers

1k
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 ...

43
votes

3
answers

4k
views

### How to rewrite mathematics constructively?

Many mathematical subfields often use the axiom of choice and proofs by contradiction. I heard from people supporting constructive mathematics that often one can rewrite the definitions and theorems ...

3
votes

0
answers

188
views

### Is there a non-constructive dependent type theory?

If I understand correctly constructivism is not the only difference between intensional Martin-Löf type theory and a first-order set theory (e.g. ZFC). Can we drop constructivism and yet have a ...

8
votes

1
answer

344
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 ...

6
votes

1
answer

527
views

### Do we have an algorithm for comparing $e^e$ with rationals?

Do we have an algorithm for comparing $e^e$ with rationals, with a known time to convergence?
In a non-constructive sense, there obviously is an algorithm.
If $e^e$ is some rational $q_0$, then we ...

1
vote

0
answers

60
views

### Approximation Rates for Multivariate Taylor Series

Let $k,n,m$ be positive integers and suppose that $f$ is $C^{k}(\mathbb{R}^n,\mathbb{R}^m)$ functions. For any given $\epsilon>0$ and $x_0\in \mathbb{R}^n$, are there known sharp approximation ...

1
vote

0
answers

70
views

### Constructive way to optimally cover a compact subset of Euclidean space

Let, $(X,d)$ be a simply connected compact subset of $\mathbb{R}^d$ with non-empty interiorn, let $d$ denote the Euclidean metric, and let $\varepsilon>0$. Is there a way to iteratively select ...

7
votes

1
answer

194
views

### Functions on Stone spaces as "enveloping algebra" of Boolean algebra

I'm looking for references for the following closely related facts:
Given a Boolean algebra $B$, I denote by $\mathbb{Z}[B]$ the free ring generated by symbols $e_b$ such that $e_b e_{b'} = e_{b \cap ...

10
votes

1
answer

469
views

### Does $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$ imply excluded middle?

Suppose that we take constructive set theory and add the axiom $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$. Does this imply excluded middle, or are there still some formulas $\varphi$ for ...

1
vote

0
answers

100
views

### Algorithm/iterative procedure for constructing hypercyclic vectors?

Let $B$ be a separable Banach space and let $L:B\rightarrow B$ be a hypercyclic operator; here I use the definition of hypercyclicity given implicitly by Birkhoff's Transitivity Theorem: continuous ...

6
votes

1
answer

219
views

### When do algebraic closures exist constructively?

The field of algebraic numbers exists constructively, since we can represent a number by an irreducible polynomial plus an estimate in rational coordinates that separates it from any other root.
More ...

2
votes

1
answer

122
views

### Constructivity of two problems on a standard simplex?

Maximizing a hyperplane $\sum_i a_ix_i$ where $a_i\in\mathbb R$ and each $a_i$ are fixed and non-negative and $x_i$ are variables over a standard simplex $\sum_i x_i\leq 1$ with $0\leq x_i$ always ...

7
votes

1
answer

248
views

### Constructive definition of noncommutative rational functions (aka free skew fields)

The question
Let $F$ be a field. (I am fine with assuming $F=\mathbb{Q}$, but I suspect
that a "right" answer will be independent of $F$.) Let $k$ be a nonnegative integer.
Question. Is ...

3
votes

0
answers

156
views

### Constructive proof of the approximate Brouwer's Fixed Point Theorem for $\Delta^n$

The approximate Brouwer Fixed Point Theorem (aBFPT) for the standard $n$-simplex is:
Let $f$ be a uniformly continuous function from $\Delta^n$ into itself.
Then for each $\varepsilon>0$ there ...

1
vote

0
answers

142
views

### Is there difference in notion of measurability in classical versus constructive?

Are there notions of measure and examples of sets measurable in that measure in classical logic but not in constructive logic (I think there cannot be counterexamples in other direction)? Are there ...