All Questions
Tagged with theories-of-arithmetic proof-theory
9 questions
13
votes
3
answers
1k
views
Reducing ACA₀ proof to First Order PA
According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA.
http://en.wikipedia.org/wiki/Reverse_Mathematics
First of all I have a few questions about the proof:
a - What ...
- 1,659
12
votes
1
answer
975
views
What metatheory proves $\mathsf{ACA}_0$ conservative over PA?
Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is ...
- 11.1k
13
votes
3
answers
1k
views
Which ordinals can be proof-theoretic ordinals of a reasonable theory?
When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended ...
- 28.2k
9
votes
1
answer
1k
views
ERA, PRA, PA, transfinite induction and equivalences
I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist.
For instance I'm ...
8
votes
2
answers
560
views
Models of PRA/EFA with induction on $X$ but not $\omega^X$
As I currently understand it, induction on formulas containing $N+1$ first-order quantifiers is required to prove the well-ordering of the ordinal $(\omega \uparrow\uparrow N) < \epsilon_0$, that ...
7
votes
1
answer
358
views
Proving short consistency: can we do better than brute force search?
This is a minor variation of a question originally asked on MSE by user779130 and bountied by me, without success. Throughout, "length" refers to the number of symbols, not lines, in a proof....
- 20.7k
5
votes
0
answers
109
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:\...
- 20.7k
4
votes
0
answers
292
views
the strength of saying "each sentence of true arithmetic has a recursive proof"
Let $PA_{\omega}$ be just like $PA$ except that $PA_{\omega}$-proofs can use any number of applications of the recursive $\omega$-rule.
The recursive $\omega$-rule allows the following:
For each ...
- 449
4
votes
1
answer
377
views
Does ACA prove categoricity of the reals?
$\def\f#1{\text{#1}}$Does $\f{ACA}$ prove that any two internally complete ordered fields are isomorphic?
Here internal completeness is expressed roughly as "every sequence of reals with an upper ...
- 2,912