All Questions
Tagged with theories-of-arithmetic constructive-mathematics
7 questions
5
votes
0
answers
58
views
Mathematical strength of the statement "Heyting Arithmetic admits Markov's rule"
Consider the following theorem about Heyting arithmetic (HA)
For every arithmetical formula $\phi$ whose only free variable is $n$, if $\text{HA} \vdash \forall n. \phi \lor \lnot \phi$ and $\text{HA}...
- 6,403
14
votes
1
answer
525
views
Is there a theory between HA and PA that doesn't have Markov's rule?
A theory $T$ admits Markov's rule when
For every formula $\phi(n)$, if $$T \vdash \forall n \in \mathbb N. \phi(n) \lor \lnot \phi(n)$$ and $$T \vdash \lnot \lnot \exists n \in \mathbb N. \phi(n)$$ ...
- 6,403
4
votes
1
answer
258
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,403
6
votes
0
answers
428
views
Proof of Tennenbaum's Theorem by McCarty
Tennenbaum's Theorem in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or ...
- 211
8
votes
0
answers
198
views
Kripke models of $HA$
Let $K$ be a kripke model and $k$ be one of its node, then $\mathcal{M}_k$ is classical structure of $k$.
What is the strongest theory of arithmetic like $T$ such that for
every kripke model $K\...
- 1,689
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,597
13
votes
7
answers
7k
views
Are real numbers countable in constructive mathematics?
We are talking about ordinary reals in constructive mathematics.
Let represent each real number by infinite converging series:
$$r = [\;(a_0,b_0),(a_1,b_1),...,(a_i,b_i),...\;]$$
$$where\quad a_i \...