A new proof of Ajtai's completeness theorem for nonstandard finite structures (Q2339960)

Ajtaji's completeness theorem is a tool for investigating problems in computational complexity theory by means of model theory [\textit{M. Ajtai}, Lect. Notes Comput. Sci. 4484, 13--33 (2007; Zbl 1198.03038)]. It is a statement about countably infinite structures that can be coded as finite elements of a nonstandard model of arithmetic, and a suitably formulated internal notion of consistency. The author proves a slightly modified version of Ajtai's theorem for a notion of a Hilbert style \(\mathbf H^{(A)}\)-proof allowing possibly infinite proof trees that are definable over a linearly ordered structure \(A\), and a notion of an expanded end-extension of \(A\). The theorem states that for linearly ordered \(A\) coded in a model of \(I\Delta_0+\exp\) and a theory \(G\) in an extension of the language of \(A\), satisfying some further conditions, the following statements are equivalent: (I) There exists a positive integer \(l\) and an \(\mathbf H^{(A)}\)-proof of a contradiction with formula length \(l\) from \(G\) and the atomic diagram of \(A\); (II) \(G\) does not have a model over \(A\). The proof of (I)\(\Longrightarrow\)(II) is essentially the same as Ajtai's. The author's simplification is in the (II)\(\Longrightarrow\)(I) direction. He replaces a lengthy explicit construction of a model of \(G\) by an argument using the ideas behind the proof of the theorem of \textit{J. Barwise} and \textit{J. Schlipf} [J. Symb. Log. 41, 531--536 (1976; Zbl 0343.02032)], and independently \textit{J. P. Ressayre} [Ann. Math. Logic 11, 31--55 (1977; Zbl 0376.02032)], stating that countable recursively saturated models are resplendent.