Injecting inconsistencies into models of PA (Q5899768)

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''. 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)]. 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.