Injecting inconsistencies into models of PA (Q5916455)

Paris and Dimitracopoulos have shown that there exist models M and N of PA such that for some nonstandard number n, M and N ``agree up to n'' but do not ``agree up to \(2^ n\)''. Solovay's paper presents a variant of this result. The main theorem says that if M is a countable nonstandard model of PA, n nonstandard element of M which is ``much larger'' than r, for a nonstandard r such that \(M\vDash Con(I\Sigma_ r)\), then there is a model N of PA such that the set of elements of M which are smaller than n is an initial segment of N, \(N\vDash Con(I\Sigma_{r-1})\), and there is a proof of \(0=1\) from \(I\Sigma_ r\) in N whose Gödel number is less than \(2^{2^ n}\). A similar result with a sharper bound for the size of the inconsistency proof was given by \textit{J. Krajiček} and \textit{P. Pudlak} [Arch. Math. Logic 28, No. 2, 91-98 (1989; Zbl 0678.03026)]. Solovay's paper is self-contained and gives a detailed proof involving finite two player games G(n,\(\phi)\) which, for a suitably chosen self-referential formula \(\phi\), provide, under the assumptions of the above result, construction of the desired model N.