The constructive-mathematics tag has no wiki summary.

**7**

votes

**1**answer

91 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 ...

**1**

vote

**0**answers

158 views

### (Reference request) Unwinding the notion of local non-constancy in constructive analysis

In constructive mathematics, several authors, including Bishop himself, use the term "locally non-constant" function. That is:
A function $f: [a, b] \longrightarrow \mathbb{R}$ is called locally ...

**4**

votes

**0**answers

327 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

198 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

242 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

297 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

260 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 ...

**8**

votes

**3**answers

673 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

264 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

507 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

395 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

611 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 ...

**45**

votes

**1**answer

2k 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

369 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 ...

**4**

votes

**1**answer

452 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

123 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

172 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 ...

**4**

votes

**2**answers

401 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

425 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

396 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

376 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 ...

**24**

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 ...

**7**

votes

**1**answer

238 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

392 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

256 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

334 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

249 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

178 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

245 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

283 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

384 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

502 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

652 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

935 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

763 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

288 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

503 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

501 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

960 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

357 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 ...

**5**

votes

**4**answers

4k views

### About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”

What does the classical proof of the proposition "there exists irrational numbers a, b such that $a^b$ is rational" want to reveal? I know it has something to do with the difference between classical ...

**28**

votes

**4**answers

3k views

### How to make Ext and Tor constructive?

EDIT: This post was substantially modified with the help of the comments and answers. Thank you!
Judging by their definitions, the $\mathrm{Ext}$ and $\mathrm{Tor}$ functors are among the most ...

**19**

votes

**3**answers

1k views

### What facts in commutative algebra fail miserably for simplicial commutative rings, even up to homotopy?

Simplicial commutative rings are very easy to describe. They're just commutative monoids in the monoidal category of simplicial abelian groups. However, I just realized that a priori, it's not clear ...

**53**

votes

**9**answers

6k views

### Is there any formal foundation to ultrafinitism?

Ultrafinitism is (I believe) a philosophy of mathematics that is not only constructive, but does not admit the existence of arbitrarily large natural numbers. According to wikipedia, it has been ...

**6**

votes

**4**answers

3k views

### Does constructing non-measurable sets require the axiom of choice?

The classic example of a non-measurable set is described by wikipedia. However, this particular construction is reliant on the axiom of choice; in order to choose representatives of $\mathbb{R} ...

**6**

votes

**3**answers

755 views

### Are all group monomorphisms regular, constructively?

By "constructive" I mean something that would go through in CZF for example.
[added Oct 6]
A sketch of a standard proof (such as referenced in comment below), which is almost constructive: Let H be a ...

**17**

votes

**4**answers

2k views

### How constructive is Doyle-Conway's 'Division by three'?

In the (whimsically written) article Division by three, Doyle and Conway describe a proof, (apparently) not using Choice, that an isomorphism $A \times 3 \simeq B\times 3$ of sets (where $3$ is a ...