The tag has no usage guidance.

learn more… | top users | synonyms (1)

5
votes
1answer
264 views

Constructive compactness for countable models?

The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted here, in the context of classical logic. The weak König's ...
3
votes
1answer
163 views

Compactness in Bishop's constructive mathematics

In Bishop's constructive mathematics, is there any literature on a possible version of the weak König's lemma, or of the compactness theorem for countable models? There is some related information ...
3
votes
0answers
163 views

Derandomization barriers in complexity theory applicable as barriers to constructive arguments replacing probabilistic method

The probabilistic method as first pioneered by Erdős (although others used this before) shows existence of a certain object while finding that object may take exponential time. (1) Is there any ...
27
votes
7answers
1k views

List of proofs where existence through probabilistic method has not been constructivised

Probabilistic method as first pioneered by Erdős (although others used this before) shows existence of a certain object. What are some of the most important objects for which we can show existence but ...
13
votes
2answers
1k views

How strong is Cantor-Bernstein-Schröder?

There are several questions here on MO about the Cantor-Bernstein-Schröder ((C)BS) theorem, but I could not find answers to what arose to me recently. Although I don't think I need to recall it here, ...
7
votes
0answers
118 views

Kripke models of $HA$

Let $K$ be a kripke model and $k$ be one of its node, then $\mathcal{M}_k$ is classical structure of $k$. What is the strongest theory of arithmetic like $T$ such that for every kripke model ...
8
votes
2answers
550 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
0answers
174 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 ...
4
votes
1answer
120 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
0answers
109 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
3answers
410 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
1answer
192 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 ...
35
votes
2answers
893 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
1answer
130 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
1answer
126 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
0answers
350 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
2answers
256 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 ...
7
votes
1answer
288 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
3answers
367 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 ...
10
votes
4answers
341 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
3answers
918 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
315 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
3answers
534 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
1answer
433 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
2answers
675 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 ...
21
votes
3answers
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
1answer
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
2answers
376 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
1answer
498 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 ...
8
votes
0answers
131 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: ...
2
votes
0answers
180 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
2answers
420 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
3answers
429 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
408 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 ...
7
votes
3answers
421 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
4answers
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 ...
9
votes
1answer
269 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
441 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
357 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
357 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 ...
7
votes
7answers
371 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
187 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 ...
7
votes
1answer
300 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
301 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
395 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
509 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
1answer
763 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
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
1answer
789 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
311 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 ...