All Questions
Tagged with peano-axioms proof-theory
36
questions
1
vote
1
answer
74
views
Why doesn't $RCA_0$ prove $\Sigma^0_1$-comprehension?
Answer: because that's $ACA_0$, alright, but:
Friedman et al.'s 1983 "Countable algebra and set existence axioms" has [verbatim, including old terminology and dubious notation]:
Lemma 1.6 ($...
- 1,084
3
votes
1
answer
97
views
Are there examples of statements not provable in PA that do not require fast growing (not prf) functions?
Goodstein's theorem is an example of a statement that is not provable in PA. The Goodstein function, $\mathcal {G}:\mathbb {N} \to \mathbb {N}$, defined such that $\mathcal {G}(n)$ is the length of ...
- 1,027
3
votes
0
answers
219
views
Which sentences are irreducibly self-referential?
Below, all sentences/formulas are in the language of arithmetic, and for simplicity we conflate numbers with numerals and sentences with Godel numbers.
Now asked at MO.
Say that a sentence $\varphi$ ...
- 249k
2
votes
1
answer
118
views
How exactly are you allowed to use free set/predicate variables in first-order arithmetic?
In first-order arithmetic, you can't quantify over sets of numbers. However, you can include sets as free variables. I don't think this is just a meta-linguistic thing, as I've read papers about Peano ...
- 21
5
votes
0
answers
154
views
Can ZFC decide more values of the Busy Beaver function than PA?
This is related to a previous question. In that question, I asked whether ZFC can define the Busy Beaver function. I was told even Peano Arithmetic(PA) can define it, and also that PA can't decide ...
- 21.4k
4
votes
1
answer
448
views
Provably total functions in $\mathsf{Q}$
I was interested in the relations between induction and recursion, and so a natural question (to my mind, anyway), was how much we can prove without appealing to induction, i.e. which functions are ...
- 5,537
6
votes
1
answer
211
views
Kaye-Wong paper Theorem 6.5
In the paper On Interpretations of Arithmetic and Set Theory of Kaye and Wong they say that Theorem 6.5 (that PA can be interpreted in ZF-Inf*, that is, ZF plus every set is contained in a transitive ...
- 1,718
6
votes
1
answer
218
views
Epsilon recursion and ZF-Inf+TC in the Inverse Ackermann Interpretation
In the paper On Interpretations of Arithmetic and Set Theory of Kaye and Wong they write:
Equipped with $\in$-induction, we obtain an inverse interpretation of
PA in ZF−Inf*. The plan is to define a ...
- 1,718
5
votes
1
answer
230
views
Interpreting $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$
How does one interpret $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$, and what is the significance of such an aberrant interpretation?
I'm interested in the following: $\textbf{ZF} - \...
- 1,718
3
votes
0
answers
109
views
Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?
It is well-known that $\mathbf{PRA}$ plus $\epsilon_0$-induction on bounded formulas cannot prove all $\mathbf{PA}$ theorems (essentially because $I\Sigma_1$ plus $\epsilon_0$-induction on bounded ...
- 1,718
4
votes
0
answers
102
views
Every provably recursive function in PA is bounded by a Hardy function
The following lemma and proof are from Takeuti's Proof Theory (2nd edition, pp. 126-127), I've highlighted the problematic part in blue:
How does Takeuti get this inequality? If the proof $x$ is not ...
- 1,718
4
votes
0
answers
102
views
Characterization of provably recursive functions in PA
This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, ...
- 1,718
4
votes
1
answer
568
views
While using the method of proof by contradiction, are we "assuming" consistency?
I am aware of threads here and here which asks something similar. However, I had something very specific to ask under the same context.
I have a very elementary question about the connection between ...
2
votes
1
answer
156
views
Developing model theory in the language of PA
Is it possible to develop model theory for models of $PA$, inside $PA$ itself (augmented with consistency raising assumptions such as $Con(ZFC)$ if necessary, but still in the language of $PA$)? What ...
- 27.7k
0
votes
1
answer
66
views
Does $n^\prime\ne n^{\prime\prime}$ require proof by contradiction? $n^\prime$ is the successor of $n$.
This is the statement of Peano's axioms I will assume for this discussion:
$1$ is a number.
To every number $n$ there corresponds exactly one number $n^\prime.$
$n^\prime=m^\prime\implies n=m.$
$n^\...
- 3,349