Hereditariness in the finite and prefix classes of first order logic

Abhisekh Sankaran ( University of Cambridge )

The Los-Tarski theorem is a result from classical model theory that states that over arbitrary (finite or infinite) structures, a first order (FO) sentence is hereditary if, and only if, it is equivalent to a universal sentence. This theorem however fails when restricted to finite structures. Tait (1959) and independently Gurevich and Shelah (1984) showed that in the finite (i.e. over the class of all finite structures), there is an FO sentence that is hereditary but that is not equivalent to any universal sentence.

In a recent paper [2], a strengthening of the above failure was shown: in the finite, for every k, there is a hereditary FO sentence that is not equivalent to any \Sigma^0_2 sentence that contains k existential quantifiers. We generalize this result by showing in the finite, that for every n, there is a hereditary FO sentence \varphi_n that is not equivalent to any \Sigma^0_n sentence. In short, (FO-)hereditariness over all finite structures is not capturable by any prefix class of FO. We show further that \neg \varphi_n is expressible in Datalog(\neq, \neg), thus answering in the negative an open question posed by Rosen and Weinstein [1], that asks whether FO \cap Datalog(\neq, \neg) is contained (semantically) inside some prefix class of FO. The methods used to show our result extend the ideas from [2] in a significant way, and involve the construction of structures that exhibit self-similarity.

This is joint work with Anuj Dawar.

[1] Eric Rosen and Scott Weinstein. Preservation theorems in finite model theory. In International Workshop on Logic and Computational Complexity, pages 480–502. Springer, 1994.

[2] Abhisekh Sankaran. Revisiting the generalized Los-Tarski theorem. In Logic and Its Applications - 8th Indian Conference, ICLA 2019, Delhi, India, March 1-5, 2019, Proceedings, pages 76–88, 2019.