All Questions
Tagged with computability-theory constructive-mathematics
20 questions
9
votes
1
answer
261
views
Does there exist a geometric morphism between the effective and topological topoi? Does one arise from synthetic topology?
I'm presenting in final projects for my computability and computational topology courses on the connections between computability, continuity, and logic. As a mathematician/unmentored baby logician ...
- 433
7
votes
0
answers
255
views
Is it decidable whether a statement about reals (in the language of ordered rings) is constructively provable?
The language of ordered rings is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$.
To decide whether such a ...
- 6,353
4
votes
1
answer
223
views
Is every compact, sober, second-countable space the image of $2^\omega$?
As a bonus, is every compact, $T_0$, second-countable space the image of $2^\omega \times \omega$?
As a further bonus, can we strengthen "image" to "quotient"?
My motivation for ...
- 3,612
4
votes
1
answer
257
views
What is the theory of statements with a provably *bounded* realizer (according to PA)?
$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.
We can summarize the results from Emil Jeřábek's answer as follows:
\begin{gather*}
T_1 = \{ ...
- 6,353
6
votes
0
answers
297
views
What are these non-classical versions of ZFC defined by realizability?
See Kleene realizability in Peano arithmetic for a similar question, but about PA instead of ZFC. (In particular, an answer as specific as Emil Jeřábek's answer would be great!)
In the context of ...
- 6,353
6
votes
1
answer
293
views
Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom
(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.)
Background: I'm trying to understand ...
- 32.5k
3
votes
0
answers
225
views
Has an uncomputable variant of the Cantor staircase ever been used in constructive logic?
An open problem in choiceless constructivism is to prove that if a function $f:\mathbb R \to \mathbb R$ is pointwise differentiable everywhere, with $f'=0$, then $f$ is constant. See In choiceless ...
- 4,943
6
votes
0
answers
151
views
Complexity of constructive arithmetical truth vs second order arithmetic
Let us say that an arithmetic statement is constructively true iff it is realized by a computable function under Kleene's function realizability. Does the set of constructively true (first order) ...
- 7,545
4
votes
1
answer
360
views
Is there a correspondence between principles of omniscience and computability classes?
My question will be speculative and therefore a little vague.
I wonder if attempts have been made to define a correspondence between, on the one hand, limited principles of omniscience that can be ...
- 32.5k
8
votes
1
answer
278
views
What is known about these "explicitly represented" spaces?
Apologies if this is too low-level. A related question that I asked on the Math Stack Exchange got no answers after a year, so I thought it might be better to ask this one here.
The standard approach ...
- 3,612
13
votes
1
answer
648
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 ...
- 32.5k
6
votes
1
answer
839
views
Rice's theorem in type theory
From the formula
$$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$
we can get the scheme
$$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...
16
votes
1
answer
2k
views
Axioms of Choice in constructive mathematics
There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC)
$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...
- 791
12
votes
5
answers
3k
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)] $$
...
- 791
7
votes
1
answer
531
views
Current status of computable spectral theorem and interpretation of quantum mechanics
The spectral theorem states if $A$ is a Hermitian operator acting on an $n-$dimensional Hilbert space space $H$, and $\lambda_1, ... \lambda_m$ are $m \leq n$ distinct eigenvalues of $A$, then
$$ H=\...
- 791
8
votes
2
answers
901
views
Did Bishop, Heyting or Brouwer take partial functions seriously?
The partial μ-recursive functions which may or may not be provably total seem to have some direct relation to the initial motivations for intuitionistic mathematics. (Following Kronecker, one ...
- 2,464
4
votes
1
answer
297
views
Analogy of $\omega$-models in constructive mathematics
I apologize that this question is a bit vague, however that is partially the point.
In subsystems of second order arithmetic, one considers $\omega$-models, these are models of $\mathsf{RCA}_0$ whose ...
- 6,287
3
votes
3
answers
575
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....
- 971
5
votes
1
answer
416
views
Higher computability : Constructive ordinal and $\Delta^1_1$ predicates
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 result that $A \...
- 764
13
votes
7
answers
2k
views
What happens when we print the digits of a real number?
Here are two well known facts, which put together leave me confused.
First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutionistic proof, you ...
- 9,201