7
votes
3answers
524 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
2answers
227 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 ...
12
votes
3answers
469 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 ...
11
votes
1answer
352 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 ...
6
votes
2answers
494 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 ...
17
votes
3answers
866 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 ...
36
votes
1answer
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
2answers
347 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
1answer
385 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
0answers
115 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
0answers
161 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
2answers
384 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 ...
4
votes
3answers
414 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
0answers
371 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 ...
4
votes
2answers
294 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 ...
23
votes
4answers
1k 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
1answer
222 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
3answers
320 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
1answer
175 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
1answer
304 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
6answers
239 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
0answers
165 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
0answers
200 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
2answers
268 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
1answer
370 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
1answer
490 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 ...
4
votes
1answer
562 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
3answers
791 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
1answer
727 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
1answer
277 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
2answers
481 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
1answer
451 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
0answers
209 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
0answers
948 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 ...
12
votes
8answers
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 ...
2
votes
0answers
288 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 ...
3
votes
3answers
3k 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 ...
26
votes
4answers
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 ...
18
votes
3answers
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 ...
48
votes
8answers
5k 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
4answers
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} ...
5
votes
3answers
732 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
4answers
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 ...
11
votes
7answers
1k views

What happens when we print the digits of a real number?

Here are two well known facts, which put together leave me confused. First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutionistic proof, you ...
4
votes
7answers
3k views

Are real numbers countable in constructive mathematics?

We are talking about ordinary reals in constructive mathematics. Let represent each real number by infinite converging series: $$r = [\;(a_0,b_0),(a_1,b_1),...,(a_i,b_i),...\;]$$ $$where\quad a_i ...
5
votes
2answers
2k views

Primitive element theorem without building field extensions

Is there are nice way to prove the primitive element theorem without using field extensions? The primitive element theorem says that if $x$ and $y$ are algebraic over $F$ and $y$ is separable over ...
10
votes
8answers
2k views

Direct construction of the integers

Is there a direct construction of the integers which does not involve taking any quotients? I am of course aware of the usual construction. I am also aware of the nice axiomatic characterization of ...
8
votes
2answers
847 views

Why do generic polynomials work in reality?

I understand that a generic $G$-polynomial $f(t_1,...,t_n)[X]$ over field $k$ has Galois group $G$ over $k(t_1,...,t_n)$. And basically any $G$ extension of $k$ should be generated by a realization of ...
7
votes
1answer
632 views

Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?

Background In constructive set theory (say based on CZF) there are inequivalent ways of stating the continuum hypothesis. Some of them are easily if not trivially refutable with common anti-classical ...
6
votes
4answers
782 views

Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...