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 ove …

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 wikiped …

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-construct …

According to constructivism a mathematical object to prove that it exists". There are several formulas to calculate pi, such as: so I take it pi exists according to constructiv …

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 t …

Hi, 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

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 r …

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 a …

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 pr …

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 …

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 …

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). Th …

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 differenc …

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 …

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\sup …