A new proof of Ajtai's completeness theorem for nonstandard finite structures
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.
- Forcing in Finite Structures
- Generalizations of the Compactness Theorem and Gödel’s Completeness Theorem for Nonstandard Finite Structures
- Arithmetical completeness versus relative completeness
- scientific article; zbMATH DE number 1072417
- A model-theoretic approach to proof theory. Edited by Zofia Adamowicz, Teresa Bigorajska and Konrad Zdanowski
- \(\Sigma_ 1^ 1\)-formulae on finite structures
- An introduction to recursively saturated and resplendent models
- Generalizations of the Compactness Theorem and Gödel’s Completeness Theorem for Nonstandard Finite Structures
- scientific article; zbMATH DE number 51556 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 227056 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Models with compactness properties relative to an admissible language
- Parity, circuits, and the polynomial-time hierarchy
- Saturated models and models that are generated by indiscernibles
- scientific article; zbMATH DE number 3557786 (Why is no real title available?)
- Forcing in Finite Structures
- Construction of models of bounded arithmetic by restricted reduced powers
- Generalizations of the Compactness Theorem and Gödel’s Completeness Theorem for Nonstandard Finite Structures
- Resplendent models and \({\Sigma_1^1}\)-definability with an oracle
This page was built for publication: A new proof of Ajtai's completeness theorem for nonstandard finite structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2339960)
