# Questions tagged [constructive-mathematics]

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

293 questions
Filter by
Sorted by
Tagged with
242 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 ...
• 20.7k
830 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?
• 4,393
145 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 ...
• 6,288
310 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 ...
• 9,881
135 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 ...
• 441
365 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 ...
• 706
276 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 ...
• 2,574
137 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 ...
• 6,288
153 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 ...
• 6,288
144 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 ...
• 31.8k
489 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 ...
• 31.8k
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 ...
• 309
331 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 ...
• 685
241 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 ...
283 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 ...
• 685
249 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 ...
• 6,288
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 ...
• 6,288
220 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. ...
• 51
236 views

### What are these generalizations of the principles of omniscience called?

I will give some principles that are slightly stronger versions of the principles of omniscience. Despite being about the natural numbers, they imply their analytic versions! Under countable choice (...
• 6,288
1k views

### Truth in a different universe of sets?

I understand that provability and truth as different concepts. Provability is syntactic, it only concerns whether the given sentence can be derived by reiterating the inference rules over a collection ...
• 5,088
1k views

### When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?

Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f : [a, b] \cup [b, c] \to S$ be a function. When can we find a function $g : [a, c] \to S$ that meets the following ...
• 6,288
91 views

### What does the computation of irrationality and transcendentality via a fancy implementation of analytic Markov's property look like?

Proofs that various real numbers are not rational or not algebraic tend to be constructively valid as is. Examples include the proofs that $\sqrt 2$ and $\log_2(3)$ are not rational and that $e$ is ...
• 6,288
192 views

### Are the multi-valued Eudoxus reals constructively equivalent to the Dedekind reals?

Without LEM or the axiom of choice, we can prove that the Eudoxus reals are equivalent to the Cauchy reals but can't prove either of those equivalent to the Dedekind reals. However, we can prove that ...
• 6,288