# Questions tagged [constructive-mathematics]

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

252 questions
Filter by
Sorted by
Tagged with
542 views

### In the constructive theory of direct categories, is it decidable whether an arbitrary morphism is an identity or not?

I'm wondering what the legit definition of direct categories should be in constructive mathematics. I must admit I don't even know in what literature I should look for the definition. I would ...
116 views

### Limits in free cocompletion, constructively

Classically, if a locally small category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits. But all proof I know of that result ...
2k views

### Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He ...
117 views

### Does negative trichotomy hold for constructive ordinals?

I don't know if there is a standard term for this, but by "negative trichotomy" I mean ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴). This holds for constructive real numbers as an easy ...
199 views

### How strong is the Schröder–Bernstein theorem where one set is the natural numbers?

The full Schröder-Bernstein theorem states that given an injection from A to B and also one from B to A, there is a bijection between A and B. It is equivalent to excluded middle, as shown in the ...
122 views

### Do presheaf toposes satisfy the full fan theorem?

Presheaf toposes satisfy LPO and (edit: if over categories with binary products) PAx and countable choice internally, so they automatically satisfy the stable fan theorem (every bar which is the ...
151 views

### Constructive theory of Lie algebras

I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is ...
137 views

### Do Grothendieck topoi with enough points satisfy the fan theorem internally?

Fourman and Hylland proved in the 80s that all spatial topoi satisfy the full fan theorem internally, while there are examples of localic topoi that do not satisfy it. This leads one to conjecture a ...
142 views

### Are there good criteria for the topological models where BD-N and BD hold?

A (non-empty/inhabited) subset $S$ of $\mathbb{N}$ is said to be pseudo-bounded if for every sequence $x_n$ in $S$ we have $\lim_{n\to \infty} \frac{x_n}{n} = 0$ Clearly all bounded subsets are pseudo-...
232 views

303 views

### What is the relationship (if any) between constructivism, finitism and predicativism?

The terms “constructivism”, “finitism” and “predicativism” refer to ideas / currents in the philosophy of mathematics (or loosely defined conditions on a system of logic) that I think I understand ...
132 views

### Weaker versions of the Riemann series theorem in constructive mathematics

The classical Riemann series theorem states that given a sequence $(a_n)_{n \in \mathbb{N}}$ of real numbers such that the series $\sum_{n = 0}^\infty a_n$ is conditionally convergent, for all real ...
210 views

### Has an uncomputable variant of the Cantor staircase ever been used in constructive logic?

An open problem in choiceless constructivism is to prove that if a function $f:\mathbb R \to \mathbb R$ is pointwise differentiable everywhere, with $f'=0$, then $f$ is constant. See In choiceless ...
196 views

### New Foundations in a Homotopy/Intuitionistic Type Theory form?

New Foundations is a famously odd set theory suggested by Quine in the 1930s which: Features a universal set. Disproves the axiom of choice. Proves the existence of an infinite set by a trivial ...
526 views

### Is the Intermediate Value Theorem strictly stronger than LLPO?

(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.) By LLPO, I mean the statement that ...
436 views

### What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?

Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, ...
123 views

### Complexity of constructive arithmetical truth vs second order arithmetic

Let us say that an arithmetic statement is constructively true iff it is realized by a computable function under Kleene's function realizability. Does the set of constructively true (first order) ...
356 views

### Tarski-Seidenberg for strict inequalities and bounded quantification

This theorem says that quantifiers over real variables can be eliminated from classical first order formulae built from equations and inequalities between polynomials with rational coefficients, ie in ...
263 views

### For which Sheaf topoi is Brouwer's fan theorem true?

Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable ...
126 views

### Does CZF prove there is a minimal cauchy completion of the rationals?

In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields. CZF can ...
273 views

### Status of the fundamental theorem of algebra for the locale of real numbers

In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed ...
123 views

### Invertibility and comparison to zero in the MacNeille sections (bounded extended reals)

(The following three paragraphs are given for context. Readers already aware of the terminology can skip to “the problem” below.) In a spatial topos $\mathop{\textbf{Sh}}(X)$ the MacNeille sections (...
328 views

### The field structure on the locale of real numbers

It is well known how to derive the field operations from the construction of the real numbers as the Dedekind completion of the rational numbers and as the Cauchy completion of the rational numbers; ...
176 views

### Weakest theory over which "all sets are measurable" has consistency strength?

Some convention: $\textrm{DC}$ stands for axiom of dependent choice, $\text{LM}$ stands for the statement "all subsets of $\mathbb{R}$ are Lebesgue measurable", $\textrm{IC}$ for "there ...
149 views

### Do quasi-excellent rings have a good constructive definition?

$\DeclareMathOperator\Sh{Sh}$Informally, a quasi-excellent ring is a Noetherian ring with a few technical extra regularity conditions that make it turns out to be the largest class of rings that allow ...
266 views

### Are finitely enumerated and subfinite sets Dedekind-finite?

The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. Let us say that a set $X$ is: finite when there exists a ...
315 views

### Why is the double negation of the axiom of choice rarely considered?

In constructive/intuitionistic mathematics, it is common to reject the axiom of choice, because it is highly nonconstructive and implies the law of the excluded middle by Diaconescu's theorem/Bishop's ...
148 views

### Using generating functions to construct or solve differential equations

I know that $T_n(x)$ is the solution of the differential equation $(1-x^2)y''-xy'+n^2y=0$, where  T_n(x)=\begin{cases} T_n(x)=1 & \text{if $n=0$}\\ T_n(x)=x & \text{if $n=1$}\\ T_{n}(x)=...
336 views

### Joyal's topos in which $[0,1]$ fails to be compact

Some time around 1977, André Joyal constructed a topos (actually a locale, i.e., a localic topos, necessarily non-spatial) in which the closed unit interval $[0,1]$ fails to be compact. There are ...
433 views

### Is there a constructive version of internal set theory?

Is there a theory T such that: T includes all the axioms of CZF. T includes the Idealization, Standardization, and Transfer schemas from IST. Every axiom of T is a theorem of IST. T has Church's rule....
365 views

### Did I find a few (small) errors in the Pradic and Brown 2021 paper that Schroeder-Bernstein implies excluded middle?

I'm looking at the https://arxiv.org/abs/1904.09193 paper (version 2, from 2021) and think it has a few errors. I think I found three small places where the paper needs to be corrected (in the sense ...
63 views

### Discreteness of the higher inductive-inductive Cauchy real numbers in real cohesive homotopy type theory

We work in cohesive homotopy type theory with propositional resizing, so that there is only one type of Dedekind real numbers $\mathbb{R}$ up to equivalence, and Mike Shulman's axiom $\mathbb{R}\flat$,...
230 views

### Equivalence of real numbers in terms of Dedekind cuts and Cauchy nets of rational numbers

We work in weakly predicatively constructive mathematics, in that we accept function sets but do not accept power sets or excluded middle. More specifically, we shall assume a sequential universe ...
244 views

249 views

### Construction of graphs of high girth and chromatic number

Are there any concrete constructions of graphs of both high girth and chromatic number? Of course there is the seminal paper of Erdős which proves the existence of such graphs via the probabilistic ...
373 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 ...
281 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 ...
385 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, ...
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 ... 