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
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 ...
user avatar
  • 221
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 ...
user avatar
  • 49.2k
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, ...
user avatar
  • 1,015
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 ...
user avatar
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 $\...
user avatar
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?
user avatar
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, ...
user avatar
  • 21.7k
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 ...
user avatar
  • 21.7k
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)) \...
user avatar
  • 351
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 ...
user avatar
  • 351
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 ...
user avatar
  • 351
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$ ...
user avatar
  • 9,635
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$,...
user avatar
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 ...
user avatar
  • 3,321
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 \...
user avatar
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 ...
user avatar
  • 21.7k
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 ...
user avatar
  • 351
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 ...
user avatar
  • 1,015
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)) \...
user avatar
  • 351
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 ...
user avatar
  • 9,635
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 ...
user avatar
  • 351
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 ...
user avatar
  • 5,759
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 $...
user avatar
  • 351
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 ...
user avatar
  • 3,321
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 ...
user avatar
  • 615
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$ ...
user avatar
  • 3,321
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 ...
user avatar
  • 5,759
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 ...
user avatar
  • 351
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 ...
user avatar
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 |\...
user avatar
  • 301
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 ...
user avatar
  • 191
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 / ...
user avatar
  • 5,580
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 6,053
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 ...
user avatar
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 ...
user avatar
  • 39
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 ...
user avatar
  • 1,577
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 ...
user avatar
  • 16.5k
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 32.2k
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 ...
user avatar
  • 113
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 1,698
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 1,698

1
2 3 4 5