# Questions tagged [constructive-mathematics]

Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.

143 questions
Filter by
Sorted by
Tagged with
151 views

### Does a map over subsingletons determine a subsingleton over maps?

I hope this question isn't too obfuscated (or easy)! Given a set $S$, let $S_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are subsingletons. In the ...
217 views

246 views

### Kleene realizability in Peano arithmetic

For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question ...
1k views

### Is there any physical or computational justification for non-constructive axioms such as AC or excluded middle?

I became interested in mathematics after studying physics because I wanted to better understand the mathematical foundations of various physical theories I had studied such as quantum mechanics, ...
607 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 ...
335 views

### Is there a constructive proof that in four dimensions, the PL and the smooth category are equivalent?

Summary Famously, the categories of 4-dimensional smooth manifolds and 4-dimensional piecewise linear manifolds are equivalent. Is there a constructive proof for this theorem or does it depend on the ...
259 views

102 views

### Terminology: product on strict preorders corresponding to direct product of preorders?

I’ve had trouble finding a well-established term for the following very obvious and elementary construction on strict partial orders (i.e. transitive, irreflexive relations): Given two strict partial ...
123 views

### Constructive version of Hilbert Projection Theorem

I am looking at the Hilbert Projection Theorem, which states that every non-empty closed convex set in a Hilbert space admits a unique element that has the minimum norm in the set. The proof involves ...
690 views

### Constructive proof of existence of non-separable normed space

I am looking for a constructive proof of one of the following two statements. If they are not constructively provable, I would be very thankful for an explanation as to why that is so (i.e., at which ...
788 views

### Gödel's speed-up from constructive to classical logic?

Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano ...
546 views

### Cauchy real numbers with and without modulus

In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers ...
358 views

132 views

### Constructive treatment of Jacobson rings

Which result is closest to the classical General Hilbert's Nullstellensatz: Finite type algebras over Jacobson rings are Jacobson. and constructively true at the same time? And where can I find a ...
386 views

### Locales in constructive mathematics

It is well known that locales are much more well behaved in a constructive setting than topological spaces. Nevertheless, many authors develop the theory of locales in classical mathematics. Are there ...
In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete ...
Let $K$ be a field (probably of positive characteristic) and consider the ring $R=K[\![x_1,\dotsc,x_n]\!]$. Suppose we have an ideal $I=(f_1,\dotsc,f_n)$ (with the same $n$ as before). Suppose we ...