# Questions tagged [constructive-mathematics]

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

179
questions

**8**

votes

**1**answer

396 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

279 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

606 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

253 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

136 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

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

**38**

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

144 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

274 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

500 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

50 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

173 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

443 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

98 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

203 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

113 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

219 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

145 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

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

**11**

votes

**0**answers

432 views

### Does Merkurjev's argument help Voevodsky's program?

In the talk
Unimath - its present and its future, July 10, 2017. Video and slides of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. (abstract)
Voevodsky mentioned that he was ...

**3**

votes

**0**answers

61 views

### Embedding abelian categories into abelian sheaves

The Yoneda functor from an abelian category into sheaves of abelian groups is shown to be exact in The Stacks Project, Lemma 19.9.2. I like this proof because it is constructive and it doesn't use ...

**11**

votes

**0**answers

331 views

### Isomorphic free groups have bijective generating sets

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:
$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.
The proofs (that I have seen) consist of turning the group ...

**2**

votes

**2**answers

695 views

### Monotonic and bounded sequences throughout mathematics [closed]

When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure ...

**3**

votes

**1**answer

338 views

### From a constructive perspective, what are the ordinal numbers?

From a constructive and computational perspective, what are the ordinal numbers?
On the one hand, it seems you can represent ordinal numbers symbolically using something like Cantor Normal Form ...

**13**

votes

**1**answer

394 views

### History of well founded relations

I have changed the title in the hope of attracting the attention of someone who knows about the history of set theory as well as intuitionistic logic:
Who was the first to state the definition of ...

**11**

votes

**3**answers

626 views

### The constancy principle in choiceless constructive foundations

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

**9**

votes

**1**answer

446 views

### Toposes in which countable choice is true but dependent choice isn't

I'd like examples of toposes in which Countable Choice is true but Dependent Choice isn't. I'd prefer examples without Excluded Middle. It's hard to find a natural example.

**13**

votes

**2**answers

892 views

### Contrasting theorems in classical logic and constructivism

Is it possible there are examples of where classical logic proves a theorem that provably is false within constructivism? Is so what are some examples?
What are some examples of most contrasting ...

**1**

vote

**1**answer

122 views

### Markov's principle from constant domain logic

I am looking for a proof of and/or a reference for the result that Markov's principle can be proved in the framework of constant domain logic. By constant domain logic, I mean intuitionistic logic ...

**8**

votes

**1**answer

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

**6**

votes

**1**answer

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

**6**

votes

**1**answer

193 views

### Tight apartness relations in toposes

A tight apartness relation on a set is a binary relation $\#$ such that the following conditions hold:
$x = y$ if and only if $\neg (x \# y)$.
If $x \# y$, then $y \# x$.
If $x \# z$, then either $x \...

**4**

votes

**0**answers

309 views

### Constructive contents of “the support of a sheaf is closed” or “the flat locus is open”

Out of curiosity I started to go through an introductory course on schemes and to convince myself that I could prove every result (after an appropriate reformulation if necessary) constructively, i.e. ...

**5**

votes

**2**answers

537 views

### Uncountability of the real numbers from LLPO without countable choice

Does there exist a proof of the uncountability of the real numbers that uses analytic LLPO (the statement that any real number $x$ satisfies either $x \leq 0$ or $x \geq 0$) but avoids Excluded Middle ...

**0**

votes

**1**answer

471 views

### On provability of false statements in constructive mathematics [closed]

Lagarias "elementary" reformulation of Robin's theorem is that $$\mathrm{RH}\iff\sigma(n)\leq H_n+e^{H_n}\log(H_n)$$
holds for every $n\geq 1$, where $\sigma(n)$ is the sum of divisors function and $...

**4**

votes

**1**answer

175 views

### Does a map over subsingletons determine a subsingleton over maps?

I hope this question isn't too obfuscated (or easy)!
Given a set $S$, let $S_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are subsingletons. In the ...

**6**

votes

**3**answers

439 views

### How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?

This is cross-posted from MSE at the suggestion of a comment after receiving no answers over a few weeks.
Suppose we have $f : A \to B$ and $g : B \to A$, as well as left inverses $f_r : B \to A$ of $...

**4**

votes

**0**answers

183 views

### An axiom that shows that the real numbers are weakly countable?

Is there a model of Intuitionistic Higher-Order Logic in which the following axiom is true?
Covering Axiom: Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to ...

**5**

votes

**1**answer

419 views

### BISH: If a function is pointwise positive, is its infimum positive?

Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH?
I believe that it is indeed the case if ...

**1**

vote

**1**answer

140 views

### Partial computability results on integrals over open intervals

It's well known in Type 2 Effectivity that integration over a compact interval is computable. So what about integration over an open interval? What rigorous computability results exist?
My thoughts ...

**3**

votes

**0**answers

236 views

### Is there a constructive proof of Baer's Criterion?

Baer's Criterion states than one can check injectivity of an $R$-module on inclusions of ideals. The proof, however, strikes me as very nonconstructive: it employs both Zorn's Lemma and LEM.
Does ...

**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"...

**18**

votes

**2**answers

667 views

### Constructive proof of existence of free algebras for infinitary equational theories

Is it constructively true that all (not necessarily finitary) equational theories $T = (\Sigma, E)$ have an initial model?
The usual proof for finitary equational theories I know constructs first ...

**7**

votes

**1**answer

502 views

### Differentiability of the distance function from a (variable) point to a (fixed) set

The distance of from a point $x$ to a set $A$ is defined by
$$ d(x,S) = \inf\{d(x,a)\mid a\in A\}, $$
where you may choose the setting to be $\mathbb R^n$,
a Banach space or a complete metric space.
...

**12**

votes

**1**answer

249 views

### Does this “mixable” property have a standard name in constructive mathematics?

While thinking about constructive mathematics, I stumbled on the following notion, and I would like to know if it has a standard name, a simpler equivalent, or has appeared in the literature:
Say ...

**9**

votes

**2**answers

518 views

### Constructivist defininition of linear subspaces of $\mathbb{Q}^n$?

Let me preface this by saying I'm not someone who has every studied mathematical logic or philosophy of math, so I may be mangling terminology here (and the title is a little tongue in cheek).
I (and ...

**12**

votes

**0**answers

221 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 $\{\...

**8**

votes

**1**answer

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

**8**

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