# Questions tagged [constructive-mathematics]

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

161 questions
Filter by
Sorted by
Tagged with
123 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 ...
105 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 ...
363 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 ...
50 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 ...
309 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 ...
480 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 ...
280 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 ...
351 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 ...
578 views

165 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. ...
492 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 ...
454 views

174 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 ...
362 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 ...
136 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 ...
135 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 ...
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"...
613 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 ...
352 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. ...
240 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 ...