The unprovability of small inconsistency. A study of local and global interpretability (Q688510)

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.