Herbrand Consistency of Some Arithmetical Theories

TL;DR

This paper extends G"odel's second incompleteness theorem to Herbrand consistency of certain bounded arithmetic theories, demonstrating unprovability results through witness shrinking techniques.

Contribution

It generalizes previous results to theories IΔ₀+Ω₁ and IΔ₀, establishing Herbrand G"odel's second incompleteness theorem for these theories.

Findings

Herbrand consistency unprovability for IΔ₀+Ω₁ and IΔ₀

Logarithmic witness shrinking applies to these theories

Generalization of previous results to broader theories

Abstract

G\"odel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness of a bounded formula logarithmically, but in the presence of Herbrand consistency, for theories ${\rm I\Delta_0+\Omega_m}$ with $m\geqslant 2$, any witness for any bounded formula can be shortened logarithmically. This immediately implies the unprovability of Herbrand consistency of a theory $T\supseteq {\rm I\Delta_0+\Omega_2}$ in $T$ itself. In this paper, the above results are generalized for ${\rm I\Delta_0+\Omega_1}$. Also after tailoring the definition of Herbrand consistency for ${\rm I\Delta_0}$ we prove the corresponding theorems for ${\rm I\Delta_0}$. Thus the Herbrand version of G\"odel's second incompleteness theorem follows for the theories ${\rm I\Delta_0+\Omega_1}$ and ${\rm I\Delta_0}$.