The unprovability of small inconsistency. A study of local and global interpretability
type: Item
instance of: scholarly article
title: The unprovability of small inconsistency. A study of local and global interpretability
zbMATH Open document ID: 0795.03080
DOI: 10.1007/BF01387407
author: Albert Visser
published in: Archive for Mathematical Logic
publication date: 1993-12-09T00:00:00Z
review text: Some consistent theories, like PA+incon(PA), prove a sentence expressing their own inconsistency. Of course, (the Gödel number of) such a proof must be large, for otherwise the theory must be, indeed, inconsistent. The author shows that a consistent, finitely axiomatized, sequential theory cannot prove its own inconsistency in few steps, in the sense that there is a definable cut that does not contain any inconsistency proof. This follows from the main result (which the author labels the Tunneling Theorem) that relates one cut to another. [Here, a theory is called sequential if it can handle finite sequences adequately; and a cut is, by definition, an initial segment closed under a mild form of exponentiation.] Another theme of this paper is the interpretability of one theory, \(V\), into another, \(U\). When the set of axioms of \(V\), \(\alpha_ V\), is infinite, proofs in \(U\) of \(I(\alpha_ V)\) -- interpretations of \(\alpha_ V\) -- may become unbounded. So, one considers a local interpretability that requires \(I(\alpha_ V\restriction x)\) for each \(x\), as well as a global one \(I(\alpha_ V)\). Let \(\| V\|\) be the global degree of \(V\) (i.e. the class of theories mutually interpretable with \(V\), globally), and let \(\text{LOC}(U)=\{\| V\|/\) \(V\) and \(U\) are mutually interpretable locally\}. For a sequential, finitely axiomatized theory \(U\), the author exhibits maximal elements of \(\text{LOC}(U)\), and shows that \(\| U\|\) is not maximal (previously shown by Pudlak) and that \(\text{LOC}(U)\) has at least three elements.
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 444896
zbMATH Keywords: length of proof
zbMATH Keywords: sequential theory
zbMATH Keywords: inconsistency
zbMATH Keywords: Tunneling Theorem
zbMATH Keywords: interpretability
zbMATH Keywords: finitely axiomatized theory
MaRDI profile type: Publication
cites work: Q3794177
cites work: The computational complexity of logical theories
cites work: A note on proofs of falsehood
cites work: Existence and feasibility in arithmetic
cites work: On the scheme of induction for bounded arithmetic formulas
cites work: Some Prime Elements in the Lattice of Interpretability Types
cites work: Cuts, consistency statements and interpretations
cites work: Q4694229
description: scientific article; zbMATH DE number 444896