Some specially formulated axiomizations for \(\mathrm{I}\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem (Q731897): Difference between revisions

In two earlier papers of the author [``How to extend the semantic tableaux and cut-free versions of the second imcompleteness theorem almost to Robinson's arithmetic Q'', J. Symb. Log. 67, No.~1, 465--496 (2002; Zbl 1004.03050)] and [``Passive induction and a solution to a Paris-Wilkie open question'', Ann. Pure Appl. Logic 146, No.~2--3, 124--149 (2007; Zbl 1115.03083)] it was shown that Gödel's second incompleteness theorem holds for the Herbrand consistency of \(\text{I}\Delta_{0}\) when two different somehow standard axiomatizations of it are taken into account. In the paper under review, a third axiomatization of \(\text{I}\Delta_{0}\) (in a rather non-standard language -- with, e.g., a Max predicate) is considered, and it is shown that for this axiomatization Gödel's second incompleteness theorem may not hold for its Herbrand consistency. In other words, there exists a consistent extension of this axiom system which can prove its own Herbrand consistency. The heart of the proof is roughly as follows: for a consistent theory \(T\) let \({\mathtt F}\) be the fixed-point formula of \(\text{Con}(T+\bullet)\); i.e., \(T\vdash {\mathtt F}\Longleftrightarrow \text{Con}(T+{\mathtt F})\). Then \(T+{\mathtt F}\vdash \text{Con}(T+{\mathtt F})\). But then \(T\vdash \text{Pr}_T(\neg {\mathtt F})\Longrightarrow\neg {\mathtt F}\), and so by Löb's rule we must have \(T\vdash\neg {\mathtt F}\), or \(T+{\mathtt F}\) is inconsistent. But if the theory \(T\) is too weak to recognize Löb's rule, then \(T+{\mathtt F}\) could be consistent, and at the same time be able to prove its own consistency. The paper, with a slightly different title but mainly the same arguments, has been published in Electron. Notes Theor. Comput. Sci. (\url{http://dx.doi.org/10.1016/j.entcs.2006.05.047}) in 2006 but it is oddly not cited in the present paper, though many related and unrelated papers of the author are listed in the bibliography. Nevertheless, the present paper is more mature and polished than the 2006 version, which should go to say that the referee(s) of Information and Computation have done a good job.