A new proof of Ajtai’s completeness theorem for nonstandard finite structures

Ajtai's completeness theorem roughly states that a countable structure A coded in a model of arithmetic can be end-extended and expanded to a model of a given theory G if and only if a contradiction cannot be derived by a (possibly nonstandard) proof from G plus the diagram of A, provided that the proof is definable in A and contains only formulas of a standard length. The existence of such model extensions is closely related to questions in complexity theory. In this paper we give a new proof of Ajtai's theorem using basic techniques of model theory.