Some specially formulated axiomizations for I _0 manage to evade the Herbrandized version of the second incompleteness theorem

DOI10.1016/J.IC.2008.11.007MaRDI QIDQ731897zbMATH OpenOpenAlexFDO

Authors Dan E. Willard

Publication date 9 October 2009

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2008.11.007

zbMATH Keywords

Gödel's second incompleteness theorem Herbrand consistency

Mathematics Subject Classification ID

Gödel numberings and issues of incompleteness (03F40)

Review text

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.

Recommendations

Cites work

Cited in

(3)

This page was built for publication: Some specially formulated axiomizations for \(\mathrm{I}\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q731897)