Tagged Questions

The tag has no usage guidance.

37 views

How to build C-Corn for Coq from source? [on hold]

Trying to install C-Corn via opam install. The problem is that since two weeks I do not see any progress, I see only Processing: make . I have i7 , 8 GB RAM. Is that normal or has something gone ...
320 views

Noetherian Rings in Constructive Mathematics

These definitions are largely from pages 92-93 of Ingo's notes. All rings are commutative with 1. I'm interested in understanding the extent to which discussion of Noetherian rings can be carried over ...
397 views

Difference between constructive Dedekind and Cauchy reals in computation

If the Axiom of Countable Choice (ACC) $$\forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \forall n \in \mathbb{N} . \varphi [n, f(n)]$$ ...
333 views

189 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 ...
445 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 ...
431 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 users....
422 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 ...
463 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 ...
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 ...
283 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 ...
483 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 ...
372 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 ...
372 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 ...
389 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 ...
196 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 ...
367 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. ...
311 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}$. ...