All Questions
Tagged with foundations constructive-mathematics
18 questions
13
votes
1
answer
932
views
Consistency strength of HoTT
What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?
- 4,985
8
votes
0
answers
157
views
How to define Dedekind reals and Eudoxus reals such that they are equivalent to unmodulated Cauchy reals
In constructive mathematics without choice, we have three different versions of the real numbers (each embedding into the next).
Regular Cauchy reals (functions $f : \mathbb N \to \mathbb Q$ such ...
- 6,353
9
votes
2
answers
380
views
How big can function spaces get without extensionality?
In what follows we work in the usual formulation of Martin-Löf Type Theory including Axiom K [1]. Boldface numbers $\mathbf{n}$ denote the usual finite type with $n$ elements.
Motivation
Postulating ...
- 756
18
votes
3
answers
3k
views
What's the earliest result (outside of logic) that cannot be proven constructively?
Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't).
An obvious counter-example is the law ...
- 6,353
9
votes
1
answer
301
views
For which Sheaf topoi is Brouwer's fan theorem true?
Brouwer's fan theorem is the standard result that the Cantor space is compact, or equivalently that the Cantor space viewed as a locale is spatial. Since it is a compactness result for a countable ...
- 1,947
3
votes
0
answers
292
views
Principle of unique choice in homotopy type theory
In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be
if $R$ is a relation between two sets $A$, $B$, and for every $...
- 2,624
10
votes
2
answers
513
views
Is there a purely constructive presentation of the HK integral?
Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...
- 1,947
7
votes
2
answers
1k
views
Explaining the consistency of PRA and ZF from predicative foundations
Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.
From the point of view of a predicative foundation to ...
- 3,302
30
votes
6
answers
3k
views
Mathematics without the principle of unique choice
The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...
- 66.7k
5
votes
0
answers
386
views
Did Kleene constructively prove Brouwer's axioms?
Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...
- 1,616
5
votes
1
answer
868
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 ...
- 4,587
12
votes
3
answers
648
views
Has the Ramified Theory of Types been applied to NBG?
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,587
5
votes
3
answers
897
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,587
4
votes
0
answers
702
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,587
8
votes
3
answers
2k
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 ...
- 4,587
38
votes
4
answers
4k
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 ...
- 4,587
1
vote
1
answer
591
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 ...
- 741
7
votes
0
answers
1k
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 ...
- 441