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
17 votes
3 answers
2k 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 ...
Christopher King's user avatar
5 votes
0 answers
186 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. ...
Ahraman's user avatar
  • 51
9 votes
0 answers
115 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 (...
Christopher King's user avatar
9 votes
2 answers
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 ...
Student's user avatar
  • 4,978
10 votes
5 answers
885 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 ...
Christopher King's user avatar
3 votes
0 answers
72 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 ...
Christopher King's user avatar
2 votes
1 answer
108 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 ...
Christopher King's user avatar
6 votes
0 answers
93 views

Archimedean ordered field in which every function is smooth

In constructive mathematics, it is consistent that every function $\mathbb{R} \to \mathbb{R}$ on the Dedekind real numbers is continuous. However, it is not consistent that every function $\mathbb{R} \...
Madeleine Birchfield's user avatar
6 votes
1 answer
239 views

Archimedean ordered fields without maxima and minima in constructive mathematics

In constructive mathematics, let us define an ordered (Heyting) field $F$ to be a commutative ring with a binary relation $<$ which is irreflexive, where for all $x$, $\neg (x < x)$ asymmetric, ...
Madeleine Birchfield's user avatar
13 votes
1 answer
465 views

Is there a theory between HA and PA that doesn't have Markov's rule?

A theory $T$ admits Markov's rule when For every formula $\phi(n)$, if $$T \vdash \forall n \in \mathbb N. \phi(n) \lor \lnot \phi(n)$$ and $$T \vdash \lnot \lnot \exists n \in \mathbb N. \phi(n)$$ ...
Christopher King's user avatar
4 votes
1 answer
196 views

Is every compact, sober, second-countable space the image of $2^\omega$?

As a bonus, is every compact, $T_0$, second-countable space the image of $2^\omega \times \omega$? As a further bonus, can we strengthen "image" to "quotient"? My motivation for ...
Robin Saunders's user avatar
4 votes
1 answer
225 views

What is the theory of statements with a provably *bounded* realizer (according to PA)?

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic. We can summarize the results from Emil Jeřábek's answer as follows: \begin{gather*} T_1 = \{ ...
Christopher King's user avatar
5 votes
3 answers
1k views

Understanding $\forall p \, q .\, \sqrt{2} \neq p/q$ constructively

"By contradiction" or "of negation" is an old chestnut of constructive dispute. But taking apartness as primitive instead of equality yields a definition of irrationality without ...
Paul Taylor's user avatar
  • 7,986
3 votes
0 answers
170 views

In constructive set theory, is it consistent for there to be a ring that models smooth infinitesimal analysis?

In a constructive set theory such as CZF, it is consistent to assume that every function $f : \mathbb R \to \mathbb R$ is continuous. However, it is not consistent to assume that every such function ...
Christopher King's user avatar
5 votes
1 answer
229 views

Does weak countable choice imply that the Cauchy reals are Dedekind complete?

Assuming the axiom of weak countable choice, is the set of modulated Cauchy reals Dedekind complete? The second theorem on this ncatlab page claims something equivalent, but it doesn't contain a proof ...
Christopher King's user avatar
6 votes
0 answers
203 views

What are these non-classical versions of ZFC defined by realizability?

See Kleene realizability in Peano arithmetic for a similar question, but about PA instead of ZFC. In the context of constructive set theory, consider two ways of defining realizability. The first is $\...
Christopher King's user avatar
6 votes
1 answer
269 views

Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.) Background: I'm trying to understand ...
Gro-Tsen's user avatar
  • 29.7k
3 votes
0 answers
211 views

Uses of excluded middle on a conjecture that can be rewritten constructively with this trick

An interesting proof technique is to use the law of excluded middle on a conjecture. There are proofs using LEM on the Riemann hypothesis for example. Constructively this is disallowed (if you can ...
Christopher King's user avatar
7 votes
0 answers
176 views

Strengthening Determinacy in constructive set theory?

Recall how games work. Let $X$ be a set (the "game space") and $\alpha$ an ordinal (the "game clock"). Alice and Bob take turns naming elements of $X$. We write them down in order ...
Tim Campion's user avatar
  • 60.2k
1 vote
1 answer
49 views

Constructing set-truncations of types from universes

This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could ...
Madeleine Birchfield's user avatar
4 votes
1 answer
135 views

Constructing coproduct types and boolean types from universes

Suppose we have a dependent type theory which has dependent product types, dependent sum types, identity types, function extensionality, an empty type, and a universe $U$ which is closed under the ...
Madeleine Birchfield's user avatar
8 votes
0 answers
215 views

The approximate mean value theorem / Rolle's theorem in pure constructive mathematics

In the replies of this very similar question, there is a fascinating answer that is beautiful in its simplicity. In particular, it seems to use perhaps the most minimal assumptions one can possibly ...
SpectreDNZ's user avatar
8 votes
1 answer
171 views

Sequential colimit of iterated quotients of Cauchy sequences

We work in constructive mathematics. The sets and functions in the foundations form a Grothendieck topos, which means that all colimits exist, and in particular, that all sequential colimits exist. ...
Madeleine Birchfield's user avatar
9 votes
0 answers
400 views

Does Wedderburn's Theorem hold constructively?

Wedderburn's Theorem states that every finite division ring is commutative. Perhaps even more surprising, this implies that every finite reduced ring is commutative. The proofs that I am aware of ...
Martin Brandenburg's user avatar
6 votes
1 answer
224 views

Existence property for second-order propositional logic

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language. Question: Assume that $\Gamma$ and $\Psi$ are ...
Z. A. K.'s user avatar
  • 333
6 votes
2 answers
677 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 ...
gksato's user avatar
  • 295
12 votes
0 answers
156 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 ...
Simon Henry's user avatar
  • 39.9k
20 votes
4 answers
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 ...
Anon's user avatar
  • 405
10 votes
2 answers
482 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 ...
Jim Kingdon's user avatar
7 votes
0 answers
232 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 ...
Jim Kingdon's user avatar
4 votes
0 answers
135 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 ...
saolof's user avatar
  • 1,823
7 votes
0 answers
166 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 ...
ಠ_ಠ's user avatar
  • 5,875
2 votes
0 answers
140 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 ...
saolof's user avatar
  • 1,823
9 votes
0 answers
143 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-...
saolof's user avatar
  • 1,823
7 votes
1 answer
288 views

Does a tight apartness relation on a subobject classifier imply the elementary topos is Boolean?

Given a set $S$, a tight apartness relation on $S$ is a relation $\#$ which is tight, irreflexive, symmetric, and weakly linear, or more specifically, a relation $\#$ such that for all elements $a \...
Madeleine Birchfield's user avatar
3 votes
0 answers
89 views

Constructively valid reference for the soberness of discrete spaces and points of a locale coproduct

I am looking for constructively valid references for the following two related facts: discrete topological spaces are sober, the points of a locale coproduct are the disjoint union of the points of ...
Gro-Tsen's user avatar
  • 29.7k
7 votes
0 answers
577 views

A new and subtle order-theoretic fixed point theorem

Sometimes a very simple argument appears out of the blue and overturns a subject. It is not based on pre-existing theory and heavy involvement in such a theory is actually a handicap in finding such ...
Paul Taylor's user avatar
  • 7,986
5 votes
1 answer
221 views

Constructive proof of univariate McCoy theorem without Dedekind-Mertens?

McCoy's theorem (one of them) says that for any commutative ring $A$, $f\in A[x]$ is a zero-divisor iff it's annihilated by a scalar in $A$. There's a widespread proof by contradiction. There's also a ...
Arrow's user avatar
  • 10.3k
7 votes
2 answers
485 views

Continuous nowhere differentiability and constructive mathematics

In some constructive systems, every function from $\mathbb{R}\to\mathbb{R}$ is continuous (roughly speaking from the classical fact that computable functions are continuous). More weakly, in Bishop's ...
Bruno Le Floch's user avatar
6 votes
0 answers
161 views

Moduli all the way down

The notion of modulus of continuity is well-known from constructive mathematics, reverse mathematics, and computability theory. Intuitively, such a modulus is a function that returns the '$\delta>...
Sam Sanders's user avatar
  • 3,851
8 votes
0 answers
358 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 ...
Gro-Tsen's user avatar
  • 29.7k
5 votes
0 answers
142 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 ...
Madeleine Birchfield's user avatar
3 votes
0 answers
220 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 ...
wlad's user avatar
  • 4,782
7 votes
0 answers
228 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 ...
wlad's user avatar
  • 4,782
12 votes
2 answers
565 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 ...
wlad's user avatar
  • 4,782
7 votes
2 answers
454 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, ...
Gro-Tsen's user avatar
  • 29.7k
6 votes
0 answers
137 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) ...
Dmytro Taranovsky's user avatar
12 votes
1 answer
402 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 ...
Paul Taylor's user avatar
  • 7,986
8 votes
1 answer
283 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 ...
saolof's user avatar
  • 1,823
3 votes
1 answer
147 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 ...
Christopher King's user avatar

1
2 3 4 5 6