# Questions tagged [constructive-mathematics]

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

209 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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, ...
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 ... 550 views

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 ...
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 ...
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$ ...
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 ...
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 ...
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 ...
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 |\...
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 ...
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 ...
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 / ...
327 views

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