10
$\begingroup$

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 formulas is finitely axiomatizable while the latter isn't). Are there any concrete examples known (preferable "natural")?

(This is an exact copy of my question on MSE, but I expect I won't get any answer there, so I hope I'm allowed to cross-post it here)

Improve this question
$\endgroup$
5
  • $\begingroup$ 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.) $\endgroup$
    – Emil Jeřábek
    Commented Jul 29, 2020 at 15:20
  • 1
    $\begingroup$ @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 :) $\endgroup$
    – Jori
    Commented Jul 29, 2020 at 15:28
  • 6
    $\begingroup$ 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? $\endgroup$
    – Emil Jeřábek
    Commented Jul 29, 2020 at 15:38
  • $\begingroup$ @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. $\endgroup$
    – Jori
    Commented Aug 1, 2020 at 14:00
  • $\begingroup$ Another point: it leaves open the question of a "natural" example. $\endgroup$
    – Jori
    Commented Aug 1, 2020 at 14:01

1 Answer 1

Reset to default
8
$\begingroup$

One example is $I\Sigma_2$ (or rather, the conjunction of its finite axiomatization).

Notice that the theory $I\Sigma_1+\epsilon_0$-induction for bounded formulas is axiomatized by $\Pi_3$ sentences: in particular, the $\epsilon_0$-induction schema can be written in prenex form as $$\forall u\,\forall x\,\exists y\,\forall z\,\bigl[\bigl(\neg\theta(u,y)\land(z\prec y\to\theta(u,z))\bigr)\lor\theta(u,x)\bigr],$$ where $\theta\in\Delta_0$ and $\prec$ is the order representing $\epsilon_0$. By a theorem of Leivant [1], $I\Sigma_2$ is not provable from any set of $\Pi_3$ (or even $\Sigma_4$) sentences consistent with $Q$. More generally, for $n\ge1$, $I\Sigma_n$ is not provable from any set of $\Sigma_{n+2}$ sentences consistent with $Q$.

The reason is that $I\Sigma_n$ proves the uniform $\Sigma_{n+1}$-reflection schema for $Q$: $$\mathrm\forall x\,\bigl(\mathrm{Pr}_Q(\ulcorner\phi(\dot x)\urcorner)\to\phi(x)\bigr),\qquad\phi\in\Sigma_{n+1},$$ where $\mathrm{Pr}_Q$ denotes the formalized provability predicate for $Q$. This schema is equivalent to the single sentence $$\def\rfn{\mathrm{RFN}}\rfn_Q(\Sigma_{n+1})=\forall x\,\bigl(\mathrm{Pr}_Q(x)\to\mathrm{Tr}_{n+1}(x)\bigr),$$ where $\mathrm{Tr}_{n+1}$ is the truth definition for $\Sigma_{n+1}$-formulas (defined so that it is vacuously true for non-$\Sigma_{n+1}$-formulas). Moreover, it is easy to see that $$\rfn_Q(\Sigma_{n+1})\equiv\rfn_Q(\Pi_{n+2}).$$ Now, if we assume for contradiction that $\rfn_Q(\Pi_{n+2})$ is provable from a consistent extension of $Q$ by $\Sigma_{n+2}$ sentences, there is a single $\Sigma_{n+2}$ sentence $\phi$ consistent with $Q$ such that $$Q+\phi\vdash\rfn_Q(\Pi_{n+2})\vdash\mathrm{Pr}_Q(\ulcorner\neg\phi\urcorner)\to\neg\phi,$$ that is, $$Q+\phi\vdash\mathrm{Con}_{Q+\phi},$$ contradicting the second incompleteness theorem.

Reference:

[1] Daniel Leivant: The optimality of induction as an axiomatization of arithmetic, Journal of Symbolic Logic 48 (1983), no. 1, pp. 182–184, doi: 10.2307/2273332.

Improve this answer
$\endgroup$
19
  • $\begingroup$ Yes! Thanks! And this only uses the consistency of PRA + $\epsilon_0$-induction, but you need that anyway, otherwise the result is of course false. A few short questions: 1) what do you mean with "uniform"? 2) is it hard to show that $I\Sigma_n$ proves the uniform $I\Sigma_{n+1}$-reflection schema for $Q$? 3) What is the complexity of the truth predicate of up to $n$ quantifiers ($\text{Tr}_n$); I think $\Delta_n$? $\endgroup$
    – Jori
    Commented Aug 2, 2020 at 15:08
  • $\begingroup$ I've accepted your answer; but I remind that the question of a natural example is still open. Or are there such that imply $I\Sigma_2$ easily? $\endgroup$
    – Jori
    Commented Aug 2, 2020 at 15:12
  • $\begingroup$ (1) What I presented above are called uniform (or global) reflection principles, as opposed to local reflection principles, which are the schemata $\mathrm{Pr}_Q(\ulcorner\phi\urcorner)\to\phi$ for sentences $\phi$. (2) It’s not that easy, as it relies on cut elimination. But basically, you convert a proof of a $\Sigma_{n+1}$ sentence into a cut-free sequent refutation of its negation $\psi$, which is $\Pi_{n+1}$; assuming for contradiction that $\psi$ is true, you prove by induction that all the sequents in the proof with $\psi$ removed are true. This is $\Pi_n$-induction, ... $\endgroup$
    – Emil Jeřábek
    Commented Aug 2, 2020 at 16:55
  • $\begingroup$ ... as apart from $\psi$, all the sequents have $\Sigma_n$ antecedents and $\Pi_n$ succedents. (3) The truth definition for $\Sigma_n$ formulas is $\Sigma_n$. $\endgroup$
    – Emil Jeřábek
    Commented Aug 2, 2020 at 16:56
  • $\begingroup$ I know about cut elimination, but I don't understand what you mean by "a cut-free sequent refutation of its negation $\psi$". $\endgroup$
    – Jori
    Commented Aug 2, 2020 at 17:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .