Questions tagged [constructive-mathematics]
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
324 questions
9 votes
2 answers
469 views
Does every reduced ring inject into a von Neumann regular one, constructively?
Classically, every commutative $R$ without nilpotents embeds into the product of its residue fields. Of course, the proof uses Zorn’s lemma in an essential way. Since a product of fields is von ...
- 66.5k
1 vote
1 answer
56 views
How to prove this construction of maximum distance 2-point logarithm for directed acyclic graph
Problem: Find the simple directed acyclic graph with $n$ vertices that maximizes the number of vertex pairs with distance 2. The ordered pair $(x,y)$ is defined to have distance 2 if there exists an ...
- 11
9 votes
0 answers
250 views
Characterization theorems for lambda calculus realizability
There are theorems characterizing Kleene's realizability$\def\realize{\mathbin{\textbf{r}}}$ in various systems. For example, $$\textsf{HA} \vdash \exists n,n \realize \varphi \iff \exists n. \textsf{...
- 2,166
2 votes
0 answers
130 views
Logical differences between Effective and Kleene-Vesley topos
The Kleene-Vesley topos $RT(\mathcal{K}_2,\mathcal{K}_2^{rec})$ and Effective topos $RT(\mathcal{K_1})$ share quite a few properties. They're evidently both constructive and reject LPO, and both have ...
- 313
8 votes
3 answers
752 views
Arithmetic of constructive Dedekind reals
The construction of Cauchy real numbers in Constructive mathematics is well known. We can define addition, subtraction, multiplication, and order as usual and prove that they form an ordered field. ...
2 votes
0 answers
171 views
What is known about realizability model of the real analysis?
What do "Realizability of the axiom of choice in HOL" and "Realizability and the Axiom of Choice" mean when they claim they realize a non extensional version of $\sf AC$? Can they ...
- 1,425
3 votes
0 answers
117 views
Is there a universal LCCB (locally compact, countably based) sober space?
By LC, I mean that every neighbourhood (of a point, or compact subspace) contains a compact neighbourhood. Every locally-closed (open $\cap$ closed) subspace of a LC space is LC. Similarly for locally-...
- 3,809
3 votes
0 answers
124 views
On the history of the “bb” propositional formula that characterizes finite Kripke frames of bounded branching
The intuitionistic propositional formula $\mathbf{bb}_n$ (in the $n+1$ variables $p_0,\ldots,p_n$) is: $$ \bigwedge_{i=0}^n \Big ( \big (p_i \Rightarrow \bigvee_{j\neq i} p_j\big) \,\Rightarrow \, \...
- 38k
33 votes
4 answers
4k views
Why is it so difficult to define constructive cardinality?
Consider Frege's cardinality and HoTT set-truncation cardinality, both of which can be well-defined in constructive theory (as SetoidTT and CubicalTT, respectively). Why don’t we regard them as well ...
- 1,425
6 votes
1 answer
272 views
$\mathit{RCA}_0$ without the law of the excluded middle
$\newcommand\name{\mathit}$In Classical Reverse Mathematics, the most famous base theory is $\name{RCA}_0$. I want to work in the area of formal Constructive Reverse Mathematics. I wonder if "$\...
8 votes
2 answers
641 views
Is there a more abstract or unified way to write the modulus condition in constructive definitions of real numbers?
I'm a beginner in constructive mathematics, and while studying different definitions of real numbers, I came across three sources that seem to describe equivalent notions of Cauchy reals: The first ...
- 83
7 votes
0 answers
219 views
Different forms of completeness of intuitionistic propositional logic for topological semantics
I've gotten myself very confused as to what “completeness” means in the context of intuitionistic logic. I'm aware of the following theorem (Alfred Tarski, “Der Aussagenkalkül und die Topologie”, Fund....
- 38k
39 votes
4 answers
4k views
Is every real number the limit of a sequence of irrational numbers, constructively?
By $\mathbb{R}$ I mean Dedekind real numbers. By $X \setminus Y$ I mean $\{x \in X: \neg(x \in Y)\}$. Let $x \in \mathbb{R}$. Can we construct (without using the law of the excluded middle and the ...
11 votes
1 answer
330 views
Does analytic WLLPO together with sequential LLPO imply analytic LLPO?
This question is about constructive mathematics, without any form of Choice except Unique Choice, such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the ...
- 38k
9 votes
0 answers
336 views
Does the decomposability of $\mathbb{R} \setminus \mathbb{Q}$ imply the decomposability of $\mathbb{R} \setminus \{0\}$?
By $\mathbb{R}$ I mean Dedekind real numbers. By $X \setminus Y$ I mean $\{x \in X: \neg (x \in Y)\}$. Let's assume the following statements: ($\bf WLLPO$) For all binary sequence $(\alpha_n)$ with at ...
14 votes
2 answers
2k views
Why are quotients so much trickier in constructive type theory than in constructive set theory?
Quotients in constructive type theory are a bit of a pain. My understanding is that the first type theory that supported them well was cubical type theory, and in previous type theories the ...
- 7,128
10 votes
2 answers
744 views
What's the deal with predicative foundations?
The working mathematician and layperson's reasons for caring about constructive foundations are well-documented. Topos theory, in particular, gives an abundance of examples in nature of settings where ...
- 551
8 votes
0 answers
335 views
Diaconescu's theorem in type theory without propositional extensionality
Diaconescu's theorem states that the axiom of choice implies excluded middle. It can be proven, e.g., in the internal logic of a topos, or in IZF. The usual proof is the following: Proof: Assume AC ...
- 1,433
4 votes
1 answer
225 views
What (if any) fragment of MLTT has the same proof theoretic strength as CZF + wREA
It seems to be fairly well known that MLTT (with W-types) and one universe has the same proof theoretic strength as CZF with the regular extension axiom (see section 5 of https://arxiv.org/pdf/1610....
- 453
3 votes
0 answers
176 views
Realizability model of the core models/inner models
Background According to A program for the full axiom of choice, forcing has a computational interpretation and a realizability models. However, this paper also mentions that it is not possible to ...
- 1,425
11 votes
1 answer
637 views
Does subsingleton choice imply LEM?
We know from Diaconescu's theorem that the axiom of choice over pairs implies the law of excluded middle. What about the axiom of choice over subsingletons. Recall that $S$ is a subsingleton if the ...
- 7,128
4 votes
0 answers
168 views
When does the disjunction property imply Church's rule?
A theory $T$ has the disjunction property when $(T \vdash \phi \lor \psi) \implies ((T \vdash \phi) \lor (T \vdash \psi))$. A theory $T$ has Church's rule when $T \vdash \forall x \in \mathbb N. \...
- 7,128
5 votes
1 answer
307 views
Does the axiom of countable choice constructively imply an omniscience principle?
$\newcommand\name{\mathrm}\newcommand\BISH{\name{BISH}}\newcommand\ACC{\name{ACC}}\newcommand\LPO{\name{LPO}}\newcommand\WLPO{\name{WLPO}}\newcommand\LLPO{\name{LLPO}}\newcommand\WLLPO{\name{WLLPO}}\...
7 votes
1 answer
342 views
Mathematical strength of the statement "Heyting Arithmetic admits Markov's rule"
Consider the following theorem about Heyting arithmetic (HA): For every arithmetical formula $\phi$ whose only free variable is $n$, if $\text{HA} \vdash \forall n. \phi \lor \lnot \phi$ and $\text{...
- 7,128
5 votes
2 answers
248 views
Construction of the smallest nucleus above a prenucleus: what does this proof tell us?
While reading Hyland's paper on the effective topos [retyped version here] in the L. E. J. Brouwer Centenary Symposium, specifically prop. 16.3, I realized that the following proposition is implicit: ...
- 38k
6 votes
1 answer
300 views
Does this weak omniscience principle have a name?
In constructive analysis, I'm looking at principles which follow both when there exists at least one discontinuous function from $\mathbb{R}$ to $\mathbb{R}$ (equivalent to WLPO i.e. $x > 0$ or $x \...
- 2,019
6 votes
2 answers
678 views
Can the real numbers be constructed as/from a Hom-object in a topos?
I've been reading through Greenblatt's Topoi and while I'm still definitely over my head I'm starting to get a feel for some of the concepts at play there. I see the definitions of $\mathbb{R}_c$ and $...
- 2,148
8 votes
1 answer
316 views
Examples of anti-classical theories in iFOL
An anti-classical axiom $\phi$ is one which is inconsistent with LEM Are there any sources for good examples of anti-classical theories in intuitionstic first-order logic? There are many examples of ...
- 313
7 votes
1 answer
372 views
Does a special property hold if the Archimedean property for reals doesn't hold?
Suppose $\mathbb{R}^e=A \cup B$ in which $A \cap B=\varnothing$ and there exist real numbers $a_0$ and $b_0$ such that $a_0 \in A$ and $b_0 \in B$. My question is, can we construct $a \in A$ and $b \...
4 votes
0 answers
344 views
What did Mirimanoff say about Intuitionism?
Dmitry Mirimanoff, "L'intuitionisme", Alma Mater n° 6, Geneva, 1945. Most of Mirimanoff's work was in number theory, but he wrote three papers about set theory that were way ahead of their ...
- 9,218
6 votes
2 answers
478 views
Weak Archimedean property instead of Archimedean property
We say that a sequence $(z_n)$ of real numbers is a modulated Cauchy sequence, whenever there exists a function $\alpha:\mathbb{N} \rightarrow \mathbb{N}$ such that: $$ |z_i-z_j| \le \frac{1}{k} \quad ...
9 votes
1 answer
446 views
Does the decomposability of $\mathbb{R}$ imply analytic LLPO?
By "BISH" I mean constructive mathematics without axiom of countable choice. By $\mathbb{R}^f$ I mean real numbers as fundamental sequences of rational numbers and by $\mathbb{R}^d$ I mean ...
4 votes
0 answers
311 views
Läuchli's "intermediate thing"
On page 230 of An abstract notion of realizability ..., Läuchli writes the following: If we drop the restrictions put on $\Theta$, then we get classical logic in one case and an intermediate thing in ...
- 19.5k
13 votes
1 answer
1k views
Consistency strength of HoTT
What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?
- 5,493
8 votes
0 answers
206 views
How to define Dedekind reals and Eudoxus reals such that they are equivalent to unmodulated Cauchy reals
In constructive mathematics without choice, we have three different versions of the real numbers (each embedding into the next). Regular Cauchy reals (functions $f : \mathbb N \to \mathbb Q$ such ...
- 7,128
7 votes
1 answer
649 views
Decimal expansion definition of real numbers, constructively
The two most common definitions of $\mathbb{R}$ are as Dedekind cuts or Cauchy sequences of rational numbers. A real analysis student of mine is working out of the book Real Analysis and Applications ...
- 10.4k
6 votes
0 answers
192 views
Constructive mathematics with different computational models
I am interested in understanding how the capabilities of constructive mathematics evolve when different computational models are considered. Specifically, if constructive mathematics traditionally ...
- 489
10 votes
2 answers
488 views
How big can function spaces get without extensionality?
In what follows we work in the usual formulation of Martin-Löf Type Theory including Axiom K [1]. Boldface numbers $\mathbf{n}$ denote the usual finite type with $n$ elements. Motivation Postulating ...
- 783
8 votes
1 answer
384 views
Equivalence of omniscience principles for natural numbers and analytic omniscience principles for Cauchy real numbers
In constructive mathematics, a proposition $P$ is decidable if $P \vee \neg P$, and a proposition is stable if $\neg \neg P \implies P$. We have the following principles of omniscience for the natural ...
user483446
2 votes
0 answers
181 views
Constructively, when do functions that agree on $[a, b] \cup [b, c]$ also agree on $[a,c]$?
Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be ...
- 7,128
3 votes
0 answers
247 views
Is the Tarski–Seidenberg theorem constructively provable?
The Tarski–Seidenberg theorem asserts that the projection of a semialgebraic set is also a semialgebraic set. My question is whether this is provable in constructive mathematics. First, let me ...
- 7,128
11 votes
0 answers
226 views
Closed sets versus closed sublocales in general topology in constructive math
This question is set in constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. Short version of the question: if $X$ is a sober ...
- 38k
8 votes
2 answers
682 views
Condition to guarantee that an inhabited and bounded set of reals has a supremum
This question is about constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the symbol $\mathbb{R}$) refer to ...
- 38k
15 votes
3 answers
2k views
Exponentials of truth values
I noticed that the exponentiation identity $$\exp(r + s) = \exp(r) \cdot \exp(s)~,$$ which is of course completely standard for real or complex numbers also holds in a Boolean setting. That is, when I ...
- 341
8 votes
0 answers
535 views
Can the p-adic be countable?
Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, The Countable Reals) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a ...
- 1,425
9 votes
1 answer
330 views
Does there exist a geometric morphism between the effective and topological topoi? Does one arise from synthetic topology?
I'm presenting in final projects for my computability and computational topology courses on the connections between computability, continuity, and logic. As a mathematician/unmentored baby logician ...
- 551
7 votes
0 answers
405 views
The constructive Eudoxus reals
Recently arxiv submitted a new paper (Andrej Bauer, James E. Hanson, The Countable Reals) claiming an incredible theorem that Dedekind reals are not sequence-avoiding, and furthermore obtaining a ...
- 1,425
7 votes
0 answers
335 views
Is it decidable whether a statement about reals (in the language of ordered rings) is constructively provable?
The language of ordered rings is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$. To decide whether such a ...
- 7,128
18 votes
3 answers
3k views
What's the earliest result (outside of logic) that cannot be proven constructively?
Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't). An obvious counter-example is the law ...
- 7,128
5 votes
0 answers
303 views
Are there Dedekind-infinite amorphous sets?
An amorphous set is an infinite set (i.e. cannot be put into bijection with any finite set $\{ 1, \dots, n \}$ for any $n$) that cannot be partitioned into two mutually disjoint infinite subsets. ...
- 151