The constructive-mathematics tag has no usage guidance.

**8**

votes

**2**answers

480 views

### Did Bishop, Heyting or Brouwer take partial functions seriously?

The partial μ-recursive functions which may or may not be provably total seem to have some direct relation to the initial motivations for intuitionistic mathematics. (Following Kronecker, one ...

**5**

votes

**0**answers

166 views

### Constructive approximation of Lipschitz functions

There are a number of theorems in classical functional analysis about approximation of Lipschitz functions by smooth functions. I was wondering if there are any similar constructive and explicit ...

**3**

votes

**1**answer

104 views

### Analogy of $\omega$-models in constructive mathematics

I apologize that this question is a bit vague, however that is partially the point.
In subsystems of second order arithmetic, one considers $\omega$-models, these are models of $\mathsf{RCA}_0$ whose ...

**5**

votes

**0**answers

104 views

### Constructive Mathematics and Termination [closed]

In the book "The Universal Turing Machine A Half-Century Survey" there is a paper called "The Confluence of Ideas in 1936" by Robin Gandy. In section 4.2, Gandy writes:
"If one accepts, on whatever ...

**16**

votes

**3**answers

396 views

### Brouwer's theorem for the Cauchy reals

Brouwer famously proved, using principles motivated by intuitionistic choice sequences, that every function $\mathbb{R}\to \mathbb{R}$ is continuous. In Sheaves in geometry and logic (section VI.9), ...

**6**

votes

**1**answer

182 views

### Grothendieck toposes in (very) weak foundation

There is on the nLab page "Grothendieck topos" a part about the theory of Grothendieck toposes in weak foundation.
It claims that the equivalence for a category between the Giraud's axioms and being ...

**34**

votes

**2**answers

862 views

### The formal p-adic numbers

The real numbers can be defined in two ways (well, more than two, but let's stick to these for now): as the Cauchy completion of the metric space $\mathbb{Q}$ with its usual absolute value, or as the ...

**4**

votes

**1**answer

125 views

### Does this axiom (a weak form of class valued choice) has a name?

At some point in my work (which has nothing to do with set theoretics foundation) I need to consider the following axiom:
For any set $X$, any class $V$ with a surjective map $f : V ...

**8**

votes

**1**answer

122 views

### Detecting positive endomaps of the formal reals

A locale is a sort of "formal topological space", which "may not have enough points to separate its open sets". For instance, there is a "locale of all real numbers that are both rational and ...

**4**

votes

**0**answers

345 views

### Elementary treatment of elementary functions in constructive math

I would appreciate a reference to constructive math literature with elementary proofs that elementary functions are locally non-constant (i. e. densely apart from any real in any interval with ...

**0**

votes

**2**answers

224 views

### Propositional logic without negation

As part of a bigger project I am researching a propositional logic, without a negation. And I would like to know, whether this already exists, to avoid double work and have proper references.
In this ...

**6**

votes

**1**answer

267 views

### Ordinals in constructive mathematics ? (references)

I'm looking for references presenting a constructive treatment of the theory of ordinals. By constructive I mean valid in the internal logic of a topos (so no axiom of choice and no law of excluded ...

**8**

votes

**3**answers

347 views

### Model-theoretic accounts of feasibility in bounded arithmetic and related systems

Various weak theories of arithmetic have been partially motivated by a concern with numbers (or functions/proofs) that are feasible. This concern is sometimes connected to an interest in strictly ...

**7**

votes

**3**answers

285 views

### A well-founded relation on lists

Let $A$ be a set equipped with a well-founded relation $<$, let $LA$ be the set of finite lists of elements of $A$, and define a relation $\prec$ on $LA$ such that $\ell \prec m$ if $\ell$ is ...

**9**

votes

**3**answers

853 views

### In the category of sets epimorphisms are surjective - Constructive Proof?

The statement that surjective maps are epimorphisms in the category of sets can be shown in a constructive way.
What about the inverse?
Is it possible to show that every epimorphism in the category ...

**4**

votes

**2**answers

300 views

### What is the status of the extreme value theorem in forms of constructive mathematics, such as Smooth Infinitesimal Analysis?

In certain intuitionistic frameworks the extreme value theorem cannot be proved. Depending on the exact framework, counterexamples can be constructed as well; see for example pp. 294-295 in
...

**13**

votes

**3**answers

525 views

### Formal/rigorous treatment of (im)predicativity/predicativism

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...

**12**

votes

**1**answer

414 views

### Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...

**10**

votes

**2**answers

650 views

### Are all functions in Bishop's constructive mathematics continuous?

When I started to write this question I was really confused, but now I think I am starting to get it. Nonetheless I'd like some confirmation that my understanding is correct.
I have read, heard ...

**18**

votes

**3**answers

1k views

### Function extensionality: does it make a difference? why would one keep it out of the axioms?

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...

**46**

votes

**1**answer

3k views

### Wanted: a “Coq for the working mathematician”

Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar ...

**1**

vote

**2**answers

371 views

### Bishop's paradox of the countability of sequences

In 'Foundations of Constructive Analysis', in the notes at the end of the first chapter, Bishop poses an apparent paradox as an exercise for the reader:
Since every sequence of rational numbers ...

**5**

votes

**1**answer

480 views

### Why is adopting Russell's Axiom of Reducibility as strong as eliminating the Ramified Hierarchy?

In order to respond to concerns of impredicativity, Bertrand Russell developed a system of ramified second-order logic, which is like regular second-order logic except the comprehension schema is ...

**7**

votes

**0**answers

126 views

### Constructively correct notion of unique factorization domain

Recall the well-known proof that a unique factorization domain is a GCD domain:
Let $x, y \in R \setminus \{ 0 \}$. Factor $x$ and $y$ into pairwise non-associated irreducible elements: ...

**1**

vote

**0**answers

175 views

### Has the Ramified Theory of Types been applied to Predicative Set Theories?

Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles ...

**5**

votes

**2**answers

414 views

### Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...

**3**

votes

**3**answers

428 views

### Infinite Partitions of the Primes and Sums of Reciprocals (Revised)

I have revised my original post. The questions I asked there were not well-put or even thought through. I don't want to delete, however, since some of the comments may be of interest to other MO ...

**2**

votes

**0**answers

403 views

### Is there a notion of “predicative given the real numbers”?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...

**6**

votes

**3**answers

402 views

### Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...

**25**

votes

**4**answers

2k views

### Illustrating Edward Nelson's Worldview with Nonstandard Models of Arithmetic

Mathematician Edward Nelson is known for his extreme views on the foundations of mathematics, variously described as "ultrafintism" or "strict finitism" (Nelson's preferred term), which came into the ...

**8**

votes

**1**answer

256 views

### Barr's theorem and constructivity?

Barr's covering theorem assert that any Gorthendieck topos can be covered by a Grothendieck topos (even a locale) satisfying the axiom of choice (and hence also the law of excluded middle). Its ...

**8**

votes

**3**answers

419 views

### reference request : constructive measure theory

As the title said, I would like to know if constructive measure theory has been developed somewhere ?
I am more precisely interested in the (constructive) theory of completely continuous valuation on ...

**9**

votes

**1**answer

317 views

### How hard is Heyting satisfiability, i.e. the constructive version of SAT? In particular, is 2-HSAT NL-complete or is it harder?

First of all, is it clear what I mean by $k$-HSAT?
I'm assuming that for $k>2$, $k$-HSAT is NP-complete, but the details of the reductions between $k$-HSAT and $k$-SAT aren't obvious to me.
I'm ...

**7**

votes

**1**answer

348 views

### Constructing Metrics for specific Topological Spaces, and Refinements of the Cantor-Space in particular

I have a Problem in general, given some some Topological Space $(X, \tau)$ from which I know it is metrisable, how can I find a metric (that is at best in some sence constructive and easy, at the very ...

**5**

votes

**6**answers

255 views

### Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is
Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used ...

**5**

votes

**0**answers

181 views

### Feasible Type Theories

I am looking for references about efficient type theories,
efficiency in the sense of computational complexity,
and type theory in the sense of Martin-Lof's type theories.
Has there been any studies ...

**6**

votes

**0**answers

260 views

### constructive Serre classes

A Serre class (of abelian groups) is a class of abelian groups closed under subgroups, quotients, and extensions. For instance, finitely generated groups and finite groups are both Serre classes.
...

**3**

votes

**2**answers

291 views

### Understanding Troelstra's Uniformity Principle in Constructive Mathematics

I have seen Troelstra's Uniformity Principle stated as:
$\forall x \exists n R(x,n) \rightarrow \exists n \forall x R(x,n)$
where $x$ ranges over $\mathbb{P(N)}$ and $n$ ranges over $\mathbb{N}$.
...

**1**

vote

**1**answer

391 views

### Cardinal Arithmetic, foundations and constructive math

This is not my area but a question occurred to me that I can not find the answer to. There is a very strong axiom of constructibility which ironically gives us highly non-constructive math (GCH is one ...

**5**

votes

**1**answer

506 views

### Intuitionistic consistency of surjection from naturals to reals

Is it consistent intuitionistically (in the sense of topos theory) for there to be a surjection from the natural numbers to the (Dedekind, let us say) real numbers? [I've managed to convince myself ...

**5**

votes

**1**answer

724 views

### intensional equality in type theory

I want to know why we add an intensional equality in type theory to definitional equality ?
What is the aim with this intensional equality ?
thanks

**6**

votes

**3**answers

1k views

### What is the status of irrational numbers within finitism/ultrafinitism?

According to constructivism a mathematical object to prove that it exists". There are several formulas to calculate pi, such as:
so I take it ...

**4**

votes

**1**answer

781 views

### effective/constructive/algorithmic probability theory

What sort of "alternative" probability theories are out there in which the methods of proof are inherently constructive?
I know of a number of theorems that say that if you take an infinite sequence ...

**5**

votes

**1**answer

306 views

### Higher computability : Constructive ordinal and $\Delta^1_1$ predicates

Everything I know on this subject comes from Sacks book : "Higher recursion theory"
Let $\mathcal{O^Y}$ be the set of codes for ordinals constructive in $Y$.
We should have the result that $A ...

**1**

vote

**2**answers

516 views

### Axiom of choice and convergence

Hi fellows,
I was wondering. Is the axiom of choice used to show that $\mathbb{R}$ is complete? If yes, is there a way to construct monotonic bounded sequences that do not converge?
Thanks in ...

**0**

votes

**1**answer

532 views

### Maximum sum of 3 consecutive numbers in a permutation [closed]

Given that $X = \{0, 1, 2, ..., 7, 8, 9\}$, and $P$ is a permutation on $X$. Let $M(P)$ be the maximum sum of 3 consecutive elements. For example, if $P = (0, 2, 4, 1, 5, 7, 9, 3, 8, 6)$, then $M(P)$ ...

**3**

votes

**0**answers

210 views

### Non-Computational classical subterms

Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term ...

**6**

votes

**0**answers

964 views

### Is there a finite-dimensional vector space whose dimension cannot be found? [closed]

Is there a finite-dimensional vector space whose dimension cannot be found? Assume, we have somehow constructed a vector space whose dimension is finite, but yet unknown. Is there always an algorithm ...

**13**

votes

**8**answers

2k views

### Are there any mathematical objects that exist but have no concrete examples? [closed]

I am curious as to whether there exists a mathematical object in any field that can be proven to exist but has no concrete examples? I.e., something completely non-constructive. The closest example ...

**5**

votes

**2**answers

362 views

### Artin Jacobson-semisimple rings are semisimple. Constructively, too?

Notation. When I say "ring", I mean "ring with unity" (not necessarily commutative).
Definition. A ring $R$ is said to be left-Artinian if for every sequence $I_0\supseteq I_1\supseteq I_2\supseteq ...