Timeline for Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 2, 2020 at 15:10 | vote | accept | Jori | ||
| Aug 2, 2020 at 11:38 | answer | added | Emil Jeřábek | timeline score: 8 | |
| Aug 1, 2020 at 14:01 | comment | added | Jori | Another point: it leaves open the question of a "natural" example. | |
| Aug 1, 2020 at 14:00 | comment | added | Jori | @Emil That sounds pretty concrete, although I cannot really follow the argument (I'm just starting out in proof theory). I've only come across reflection in the case of Con(PA) is equivalent to $\Pi_1$ reflection. | |
| Jul 29, 2020 at 15:38 | comment | added | Emil Jeřábek | Ok. (The single axiom equivalent to) $I\Sigma_2$ is not provable in $I\Sigma_1+{}$ bounded $\epsilon_0$-induction (as the latter is a consistent $\Pi_3$ theory, while the former implies the uniform $\Sigma_3$-reflection principle). Is that concrete enough? | |
| Jul 29, 2020 at 15:28 | comment | added | Jori | @EmilJeřábek Oh, yes, sorry: on bounded formulas. And yes, thanks for pointing that out, I meant: essentially because $I\Sigma_1$ is finitely axiomatizable. I hope it is good now :) | |
| Jul 29, 2020 at 15:22 | history | edited | Jori | CC BY-SA 4.0 |
added 20 characters in body
|
| Jul 29, 2020 at 15:20 | comment | added | Emil Jeřábek | What exactly do you mean by “$\epsilon_0$-induction”? The schema of $\epsilon_0$-induction for all formulas most definitely proves the schema of $\omega$-induction for all formulas, i.e., PA. The schema is not finitely axiomatizable unless it is restricted to formulas of complexity $\Sigma_n$, or something. (PRA is also not finitely axiomatizable, by the way.) | |
| Jul 29, 2020 at 15:07 | review | First posts | |||
| Jul 29, 2020 at 15:12 | |||||
| Jul 29, 2020 at 15:02 | history | asked | Jori | CC BY-SA 4.0 |