Some specially formulated axiomizations for \(\mathrm{I}\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem
type: Item
instance of: scholarly article
title: Some specially formulated axiomizations for \(\mathrm{I}\Sigma _0\) manage to evade the Herbrandized version of the second incompleteness theorem
zbMATH Open document ID: 1191.03044
author: Dan E. Willard
published in: Information and Computation
publication date: 2009-10-09T00:00:00Z
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 th…
reviewed by: Saeed Salehi
Mathematics Subject Classification ID: 03F40
zbMATH DE Number: 5611736
zbMATH Keywords: Gödel's second incompleteness theorem
zbMATH Keywords: Herbrand consistency
MaRDI profile type: Publication
full work available at URL: j.ic.2008.11.007
OpenAlex ID: W2022687341
cites work: Herbrand consistency and bounded arithmetic
cites work: Existentially closed structures and Gödel's second incompleteness theorem
cites work: On Herbrand consistency in weak arithmetic
cites work: Gödel's Second incompleteness theorem for Q
cites work: Q3794177
cites work: Unprovability of consistency statements in fragments of bounded arithmetic
cites work: The decision problem for exponential diophantine equations
cites work: Arithmetization of metamathematics in a general setting
cites work: Q4001935
cites work: On the Herbrand notion of consistency for finitely axiomatizable fragments of bounded arithmetic theories
cites work: A note on proofs of falsehood
cites work: Q4856172
cites work: Q4103079
cites work: Solution of a problem of Leon Henkin
cites work: Q3992465
cites work: Q4726219
cites work: Q3931384
cites work: A note on the undefinability of cuts
cites work: Some Prime Elements in the Lattice of Interpretability Types
cites work: Q3755452
cites work: Cuts, consistency statements and interpretations
cites work: Q4885911
cites work: Modal analysis of generalized rosser sentences
cites work: Finite sets and Gödel's incompleteness theorems
cites work: Q5822068
cites work: Gödel sentences of bounded arithmetic
cites work: Undecidable theories
cites work: An inside view of EXP; or, The closed fragment of the provability logic of IΔ0 + Ω1 with a prepositional constant for EXP
cites work: The unprovability of small inconsistency. A study of local and global interpretability
cites work: Faith \& falsity
cites work: Q5181365
cites work: On the scheme of induction for bounded arithmetic formulas
cites work: Q4282618
cites work: Q2721211
cites work: Self-verifying axiom systems, the incompleteness theorem and related reflection principles
cites work: How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q
cites work: Q3367334
cites work: An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency
cites work: On the available partial respects in which an axiomatization for real valued arithmetic can recognize its consistency
cites work: A generalization of the second incompleteness theorem and some exceptions to it
cites work: Passive induction and a solution to a Paris-Wilkie open question
cites work: Rudimentary Predicates and Relative Computation
DOI: 10.1016/J.IC.2008.11.007
description: scientific article; zbMATH DE number 5611736