Questions tagged [theories-of-arithmetic]
Theories of arithmetic in first-order logic, such as Peano arithmetic, second-order arithmetic, Heyting arithmetic, and their subsystems and extensions. Models of Peano arithmetic.
127
questions
-1
votes
2
answers
212
views
Heuristic interpretations of the PA-unprovability of Goodstein's Theorem
I've relatively recently learned about Goodstein's Theorem and its unprovability in Peano arithmetic (the Kirby-Paris Theorem). I do not have any real knowledge of formal logic; but I think I've seen ...
4
votes
1
answer
625
views
Which part(s) of this proof of Goodstein's Theorem are not expressible in Peano arithmetic?
EDIT: Noah Schweber helpfully points out that $\mathsf{ACA}_0$ is a conservative extension of Peano arithmetic in which certain aspects of my proof not expressible in Peano arithmetic are expressible. ...
4
votes
0
answers
87
views
Computational complexity of arithmetic sentences over classical theories
Below, I use the term "tracker" rather than "realizer" since I'm not requiring the relevant objects to be computable.
Define the relation "$f$ tracks $\varphi$" for $f:\...
4
votes
1
answer
212
views
Does Peano's axioms prove $\alpha$-induction for primitive recursive sequences for every concrete $\alpha < \varepsilon_0$?
It is well-known that Peano's axioms (PA) cannot prove $\varepsilon_0$-induction for primitive recursive sequences (PRWO($\varepsilon_0$)), because PA + PRWO($\varepsilon_0$) proves the consistency of ...
23
votes
1
answer
2k
views
What is known about the theory of natural numbers with only 0, successor and max?
Consider the first-order theory whose intended/standard model is the natural numbers $\mathbb{N}$, with constant $0\in \mathbb{N}$, with an injective successor operation $s$ such that $0$ is not a ...
4
votes
1
answer
165
views
Further research on relevant realizability etc
I just read Dunn's 1979 paper Relevant Robinson's Arithmetic, and the end especially caught my interest. Following the surprising role of constant functions in collapsing "relevant Q with zero&...
1
vote
0
answers
109
views
Is possibile to define transfinite sum and product recursively? [closed]
On mathstackexchange a few days ago I published the following question where I asked about "transfinite" sum and products but actually nobody answered or gave an opinion with a comment: thus ...
3
votes
1
answer
110
views
$\Pi^0_1$ sentences modulo "schematic entailment"
Let $\mathfrak{P}$ be the preorder of $\Delta^0_0$ (= only bounded quantifiers) formulas with one free variable in the language of arithmetic, under the relation $\alpha(x)\le\beta(x)$ iff there is a ...
4
votes
1
answer
118
views
Does this hierarchy of fragments of $I \Sigma_1$ collapse?
Does anyone know whether the following hierarchy of fragments of
$\mathrm{I} \Sigma_1$ (or rather
$\mathrm{I} \Pi_1$) collapses or not?
Let $\Sigma^b_n$ denote formulas in the language of arithmetic ...
7
votes
4
answers
485
views
A conservative extension of Peano Arithmetic
Ulrich Kohlenbach makes the following intriguing comment here:
"In the 70s S. Feferman introduced a mathematically strong system S=restricted(PA^omega)+QF-AC+mu for classical mathematics (and in ...
4
votes
1
answer
479
views
Truth Values of Statements in non-standard models
Excuse me, if the question sounds too naive.
Non-standard models of PA will have statements of non-standard lengths, basically infinite. And it is also true that every statement of a theory will have ...
14
votes
1
answer
502
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)$$ ...
5
votes
2
answers
416
views
Models of second-order arithmetic closed under relative constructibility
I know little to nothing about second-order arithmetic and its subsystems. However, I would like to understand when a model of (a subsystem of) second-order arithmetic ($\mathsf{Z}_2$) is downward ...
4
votes
1
answer
246
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 = \{ ...
5
votes
1
answer
267
views
Why include $0$ and $1$ in the signature of Presburger arithmetic?
I recently became interested in some problems concerning decidability of extensions of Presburger arithmetic. However, being a number-theorist rather than a logician, I am confused by some notational ...