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)

$\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$ 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
    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$ 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
    Aug 1, 2020 at 14:00
  • $\begingroup$ Another point: it leaves open the question of a "natural" example. $\endgroup$
    – Jori
    Aug 1, 2020 at 14:01

1 Answer 1

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.

$\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
    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
    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$ 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$ 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
    Aug 2, 2020 at 17:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.