Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [constructive-mathematics]

13
votes
1answer
246 views

Is there a constructive proof that in four dimensions, the PL and the smooth category are equivalent?

Summary Famously, the categories of 4-dimensional smooth manifolds and 4-dimensional piecewise linear manifolds are equivalent. Is there a constructive proof for this theorem or does it depend on the ...
8
votes
0answers
172 views

Reflection principle for intuitionistic Zermelo–Fraenkel?

The well-known reflection principle for classical Zermelo–Fraenkel states: For any formula $\varphi(x_1,\ldots,x_n)$ of the language of ZFC with free variables $x_1,\ldots,x_n$, ZFC proves $$ \...
2
votes
0answers
120 views

Infintely iterated and functional integration in constructive math

Looking for references on constructive derivations of (elements of) functional integration -- in particular, those used in the classical construction of the Wiener measure. It seems such ...
3
votes
1answer
413 views

Going beyond the strength of Peano arithmetic “without sets”

First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...
9
votes
2answers
570 views

What did the Intuitionists want to do with applied mathematics?

Oversimplification: Newton & Leibnitz &c build the calculus and other methods that solve a vast number of practical problems. Weierstrass, Dedekind, Cantor &c build a foundation under it ...
8
votes
3answers
304 views

Locales as spaces of ideal/imaginary points

I posted this question on MSE a few days ago, but got no response (despite a bounty). I hope it will get more answers here, but I'm afraid it might not be appropriate as I'm not sure it's actually ...
3
votes
1answer
136 views

Partitions of unity in constructive mathematics

Can someone point me to any substitutes for the partition of unity in Bishop's constructive mathematics? In particular, under what circumstances can we construct a partition of unity subordinate to ...
8
votes
1answer
289 views

Is every set smaller than a regular cardinal, constructively?

Constructively, my only interest in regular cardinals is in terms of the "$\Sigma$-universes" they generate. By a $\Sigma$-universe, I mean a collection of triples $(X,Y,f: X \to Y)$ closed under base ...
17
votes
4answers
1k views

Constructively, is the unit of the “free abelian group” monad on sets injective?

Classically, we can explicitly construct the free Abelian group $\newcommand{\Z}{\mathbb{Z}}\Z[X]$ on a set $X$ as the set of finitely-supported functions $X \to \Z$, and so easily see that the unit ...
19
votes
4answers
890 views

Mathematics without the principle of unique choice

The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...
16
votes
1answer
744 views

New articles by Errett Bishop on constructive type theory?

Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and ...
2
votes
1answer
198 views

Unorthodox constructive reasoning: The Kleene Getaway

KG (the Kleene Getaway) is the name I improvised (in my answer to a question on MO on constructive Perron-Frobenius) for a constructive principle which enables the direct constructive use of a ...
15
votes
2answers
721 views

Constructive proof of a rational version of Perron-Frobenius?

In the following, we work with vectors and matrices whose entries are rational numbers. Inequalities between such vectors are understood to be coordinatewise: e.g., two vectors $a = \left(a_1,a_2,\...
3
votes
0answers
84 views

What's a completely computational/syntactical model for handle decompositions of manifolds?

Simplicial sets, CW complexes Simplicial sets can be described completely algebraically, by specifying a family of sets, and maps between them satisfying certain relations. This description can be ...
5
votes
1answer
354 views

Infinite-time Turing machines and the formal Church's thesis

Infinite-time Turing machines are known to either halt or loop in countable time. In the spirit of double-negation translation, is there a statement which is: classically equivalent to this; ...
14
votes
1answer
490 views

In what ways is ZF (without Choice) “somewhat constructive”

Let me summarize what I think I understand about constructivism: "Constructive mathematics" is generally understood to mean a variety of theories formulated in intuitionist logic (i.e., not assuming ...
10
votes
2answers
396 views

Is the existence of double complement of a set provable in Intuitionistic ZF?

In Powell's article [1] he introduces the axiom of double complement, which says a double complement $\{x : \lnot\lnot(x\in A)\}$ is a set for any set $A$. I can't find similar axiom from other ...
3
votes
1answer
150 views

Fixed-point property and $T_0$ separation property

Each topological space $A$ with fixed-point property is $T_0$ space. Proof: suppose, two different points $a_1$ and $a_2$ belong to the same open subsets of $A$. Then the function $$f(a)= \begin{cases}...
2
votes
2answers
88 views

Terminology: product on strict preorders corresponding to direct product of preorders?

I’ve had trouble finding a well-established term for the following very obvious and elementary construction on strict partial orders (i.e. transitive, irreflexive relations): Given two strict partial ...
2
votes
1answer
105 views

Constructive version of Hilbert Projection Theorem

I am looking at the Hilbert Projection Theorem, which states that every non-empty closed convex set in a Hilbert space admits a unique element that has the minimum norm in the set. The proof involves ...
9
votes
7answers
617 views

Constructive proof of existence of non-separable normed space

I am looking for a constructive proof of one of the following two statements. If they are not constructively provable, I would be very thankful for an explanation as to why that is so (i.e., at which ...
8
votes
4answers
744 views

Gödel's speed-up from constructive to classical logic?

Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano ...
15
votes
2answers
521 views

Cauchy real numbers with and without modulus

In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers ...
13
votes
2answers
324 views

Constructive proofs of existence in analysis using locales

There are several basic theorems in analysis asserting the existence of a point in some space such as the following results: The intermediate value theorem: for every continuous function $f : [0,1] \...
14
votes
1answer
426 views

Constructive homological algebra in HoTT

I'm curious how much of homological algebra carries over to a constructive setting, like say HoTT (or some other variety of intensional type theory) without AC or excluded middle. There doesn't seem ...
6
votes
4answers
372 views

Strict and non-strict orderings

Consider a set $A$ equipped with two binary relations $\le$ and $<$, related in the appropriate ways for the strict and non-strict version of an ordering. One might make different choices about ...
15
votes
1answer
1k views

In constructive mathematics, why does the category of abelian groups fail to be abelian?

I was reading the paper Towards Constructive Homological Algebra in Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...
9
votes
1answer
252 views

Constructive analysis and synthetic differential geometry

I am curious if (any of) the various inequivalent constructions of the real line in constructive mathematics can be used to build a model of Kock and Lawvere's synthetic differential geometry? In ...
30
votes
1answer
2k views

Constructive algebraic geometry

I was just watching Andrej Bauer's lecture Five Stages of Accepting Constructive Mathematics, and he mentioned that in the constructive setting we cannot guarantee that every ideal is contained in a ...
6
votes
1answer
707 views

Rice's theorem in type theory

From the formula $$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$ we can get the scheme $$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...
12
votes
0answers
402 views

Algebraic closure of a field in constructive mathematics

There is a short note by André Joyal called Les théorèmes de Chevalley-Tarski et remarque sur l'algèbre constructive (pp. 256-258). It is claimed there that there is a constructive version of the ...
5
votes
2answers
385 views

Sets in constructive mathematics

It is not completely clear how Bridges, Richman and Youchuan treated sets in their paper. Example is in the following lemma (Lemma 7 on p. 7): Let $U$ and $V$ be (inhabited to mean $\exists u \in U,...
3
votes
0answers
105 views

Constructive treatment of Jacobson rings

Which result is closest to the classical General Hilbert's Nullstellensatz: Finite type algebras over Jacobson rings are Jacobson. and constructively true at the same time? And where can I find a ...
13
votes
2answers
347 views

Locales in constructive mathematics

It is well known that locales are much more well behaved in a constructive setting than topological spaces. Nevertheless, many authors develop the theory of locales in classical mathematics. Are there ...
4
votes
3answers
341 views

Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete ...
6
votes
0answers
150 views

Constructive approach to complete intersections

Let $K$ be a field (probably of positive characteristic) and consider the ring $R=K[\![x_1,\dotsc,x_n]\!]$. Suppose we have an ideal $I=(f_1,\dotsc,f_n)$ (with the same $n$ as before). Suppose we ...
3
votes
0answers
96 views

Collapsing the Intuitionistic Bounded Arithmetics Hierarchy

Let $iT$ be the intuitionistic first order theory with non-logical axioms of classical first order theory $T$. Theorem1. If $\mathsf{T^i_2}\vdash \mathsf{T_2}$, then $\mathsf{T^i_2}$ proves that ...
5
votes
0answers
206 views

Uniqueness of localic analogue of Radon-Nikodym derivatives

In classical probability theory, Radon-Nikodym derivatives are unique up to measure-0 sets of the background measure. I am wondering whether the following statement, intended to state an analogue of ...
12
votes
1answer
860 views

Bishop quote stating that axiom of choice is constructively valid

This is about constructive mathematics, but it is not a research question. But since it may also be of interest for research mathematicians, I hope this question is appropriate for this forum. As ...
14
votes
1answer
1k views

Axioms of Choice in constructive mathematics

There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC) $$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...
5
votes
0answers
306 views

Did Kleene constructively prove Brouwer's axioms?

Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...
7
votes
2answers
252 views

Matrix diagonalization and eigenvector computation constructively

Assuming Bishop's constructive mathematics, is it true that any real-valued square matrix with distinct roots of the characteristic polynomial can be diagonalized? By distinct, I mean apart: $x \neq y ...
12
votes
2answers
307 views

Given a sequence of reals, we can find a dense sequence avoiding it, but can we find one continuously?

Let $S$ be the set of injective sequences in $\mathbb{R}$: $$S = \{s: \mathbb{N} \rightarrow \mathbb{R}: s(m) \neq s(n) \text{ if }m \neq n\}.$$ Consider $S$ with the topology of pointwise convergence,...
4
votes
0answers
126 views

Inductive generation of non-spatial locales

Is there an example of a locale/formal space which is not spatial (i.e., one can prove it is not spatial, rather than something like $\mathbb{R}$, where spatiality is independent in a constructive ...
9
votes
2answers
326 views

Admissibility of Harrop's rule, computationally

It is obvious that the following formula is not a theorem of intuitionistic propositional calculus (IPC). $$ (\neg A \; \to \; B \vee C) \;\; \to \;\; ((\neg A \; \to \; B) \vee (\neg A \; \to \; ...
10
votes
2answers
339 views

Why is the notion of algorithm a primitive one in Brouwer's intuitionism?

I've seen several times people mentioning that the notion of an algorithm / a computation is taken as a primitive notion in L. E. J. Brouwer's intuitionism. For instance, in Varieties of Constructive ...
6
votes
1answer
246 views

Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate: $\neg \neg \exists x P \to \...
18
votes
3answers
1k views

Approximate intermediate value theorem in pure constructive mathematics

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise ...
8
votes
3answers
429 views

What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...
32
votes
4answers
5k views

How Would an Intuitionist Prove This?

My question concerns the proof of the following: Let $a,b,n \in \mathbb{N}$. If $n \neq 1$ and $n$ divides both $a$ and $b$, then $b$ is a composite number or $b$ divides $a$. My proof: Suppose $b$ ...