Herbrand consistency of some finite fragments of bounded arithmetical theories (Q2377353)

A theory \(T\) is Herbrand consistent if every finite set of instances of its Skolemized form is propositionally satisfiable. The author presents a formalization of Herbrand consistency suitable for bounded arithmetic and exhibits a finite fragment of \(I\Delta_0\) whose Herbrand consistency is not provable in \(I\Delta_0\). This improves a previous result of the author that \(I\Delta_0\) does not prove a form of its own Herbrand consistency [the author, J. Symb. Log. 77, No. 3, 807--827 (2012; Zbl 1256.03065)] building on related results by \textit{Z. Adamowicz} [Fundam. Math. 171, No. 3, 279--292 (2002; Zbl 0995.03044)], \textit{D. E. Willard} [J. Symb. Log. 67, No. 1, 465--496 (2002; Zbl 1004.03050)], and \textit{L. A. Kołodziejczyk} [J. Symb. Log. 71, No. 2, 624--638 (2006; Zbl 1099.03050)].