Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
Questions tagged [constructive-mathematics]
277 questions
31
votes
4 answers
How Would an Intuitionist Prove This?
My question concerns the proof of the following: Let $a,b,n \in \mathbb{N}$. If $n \neq 1$ and $n$ divides both $a$ and $b$, then $b$ is a composite number or $b$ divides $a$. My proof:
Suppose $b$ is not composite. Then $b$ is prime. Since $n…
J126
- 535
14
votes
8 answers
Are there any mathematical objects that exist but have no concrete examples?
I am curious as to whether there exists a mathematical object in any field that can be proven to exist but has no concrete examples? I.e., something completely non-constructive. The closest example I know of are ultrafilters, which only have one…
Jon Paprocki
- 509
- 6
- 16
5
votes
3 answers
Understanding $\forall p \, q .\, \sqrt{2} \neq p/q$ constructively
"By contradiction" or "of negation" is an old chestnut of constructive dispute.
But taking apartness as primitive instead of equality yields a definition of irrationality without negation, making rationality a derived notion.
So can we give a neat…
Paul Taylor
- 7,996
4
votes
1 answer
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 following $Y_\perp^X$ means $(Y_\perp)^X$.
The…
wlad
- 4,823
2
votes
1 answer
Are the multi-valued Eudoxus reals constructively equivalent to the Dedekind reals?
Without LEM or the axiom of choice, we can prove that the Eudoxus reals are equivalent to the Cauchy reals but can't prove either of those equivalent to the Dedekind reals.
However, we can prove that the multi-valued Cauchy reals are equivalent to…
Christopher King
- 5,715