# Tameness in least fixed-point logic and McColm’s conjecture

Siddharth Bhaskar and Alex Kruckman

###### Abstract

We investigate fundamental model-theoretic dividing lines (the order property,
the independence property, the strict order property, and the tree property 2)
in the context of least fixed-point ($LFP$) logic over families of finite
structures. We show that, unlike the first-order ($FO$) case, the order
property and the independence property are equivalent, but all of the other
natural implications are strict. We identify the $LFP$-strict order property
with _proficiency_ , a well-studied notion in finite model theory.

Gregory McColm conjectured in [14] that $FO$ and $LFP$ definability coincide
over a family $\mathcal{C}$ of finite structures exactly when $\mathcal{C}$ is
non-proficient. McColm’s conjecture is false in general, but as an application
of our results, we show that it holds under standard $FO$ tameness assumptions
adapted to families of finite structures.

##  1 Introduction

A central theme in finite model theory is the study of definability over
families of finite structures by first-order logic $FO$, finite variable
logics like $L^{k}$, fixed-point logics like $LFP$ and $PFP$, and infinitary
logics like $L_{\infty\omega}^{\omega}$. In his seminal work [16], Shelah
initiated the classification of theories according to which finite
combinatorial structures they encode in a first-order sense, such as linear
orders, boolean algebras, and various types of trees. These measures of
complexity provide dividing lines between theories which are _tame_ and _wild_
in precise senses. Several more recent papers [1, 12, 13] have shown that
these combinatorial dividing lines, adapted to $FO$-definability over families
of finite structures, are both robust and useful, often generalizing classical
properties in graph theory and combinatorics.

In the present paper, we initiate the study of these combinatorial dividing
lines, namely the _order property_ (OP), _independence property_ (IP), _strict
order property_ (sOP), and _tree property 2_ (TP2), in the context of
$LFP$-definability over families of finite structures. Our main results are
the following:

  1. 1.

$LFP$-sOP is equivalent to the classical notion of _proficiency_ , namely that
for some functional definable by a positive elementary formula $\varphi(x;S)$,
there is no bound on the number of iterations needed to reach a fixed point.

  2. 2.

$LFP$-sOP $\implies$$LFP$-TP2$\implies$($LFP$-IP$\iff$$LFP$-OP), and all the
implications are strict. (Contrast this with the first-order case, where
$FO$-TP2$\implies$$FO$-IP$\implies$$FO$-OP and $FO$-sOP$\implies$$FO$-OP, all
implications are strict, and $FO$-TP2 and $FO$-sOP are incomparable.)

These results allow us to give a purely first-order characterization of each
of the $LFP$ dividing lines, using a known first-order characterization for
$LFP$-sOP (see Section 2). Furthermore, the implications for $LFP$ hold for
any more expressive logic, in particular
$\mathcal{L}_{\omega\infty}^{\omega}$. Examining these combinatorial
properties in the context of
$\mathcal{L}_{\omega\infty}^{\omega}$-definability is a natural direction that
we do not pursue.

### McColm’s conjecture

We do, on the other hand, examine _McColm’s conjecture_ of Gregory McColm [14]
, which was an attempt to characterize exactly when $FO$ and $LFP$
definability coincide over a family of finite structures $\mathcal{C}$. In
1990, McColm posited that the following three properties were equivalent:

  1. 1.

$\mathcal{C}$ is __ proficient _._

  2. 2.

$FO\neq LFP$ over $\mathcal{C}$.

  3. 3.

$FO\neq L_{\infty\omega}^{\omega}$ over $\mathcal{C}$.

The first property easily implies the latter two, but the converses are not
clear. In 1992, Kolaitis and Vardi [10] proved the equivalence of 1 and 3. Two
years later, Gurevich, Immerman, and Shelah [8] constructed two examples of a
proficient family of structures for which $FO=LFP$, thus establishing that 2
does not imply 1.

By _McColm’s conjecture_ , we mean the equivalence of 1 and 2. Even though
McColm’s conjecture is false in general, we show that it holds under any
_first-order_ tameness assumption $FO$-NOP, $FO$-NIP, $FO$-NTP2, or $FO$-NsOP.

##  2 Proficiency and the strict order property

We briefly review some basic material on least fixed-point logic. See
Moschovakis [15] for a comprehensive treatment.

Least fixed-point ($LFP$) logic is obtained by extending the syntax of first-
order logic by second-order (relation) variables, as well as the following
quantification rule. Suppose $\varphi$ is a formula with a free $n$-ary
relation variable $S$ that occurs _positively_(within an even number of
negations), an $n$-tuple of free variables $x$, and suppose $u$ is a fresh
$n$-tuple. Then we may form the formula $[\mathbf{lfp}\ Sx.\varphi](u)$, where
$S$ and $x$ are bound and $u$ is free. When we speak of $LFP$ formulas, we
mean formulas in which all of the relation variables are bound.

The semantics of the lfp quantifier is defined by taking the least fixed-point
of the functional defined by $\varphi$. To be precise, write $\varphi(x;S)$
for $\varphi$, and for simplicity, assume there are no other free variables.
(Otherwise, we can fix these and proceed as before.) Given a structure
$\mathbf{A}$ in the same language as $\varphi$, $\varphi$ defines an operator
$\Gamma$ on the powerset of $A^{x}$ by

$\Gamma:X\mapsto\varphi(A^{x};X),$

where $\varphi(A^{x};X)=\\{b\in A^{x}:\mathbf{A}\models\varphi(b;X)\\}$. Since
$S$ occurs positively, $\Gamma$ is monotone, so if we define

$I_{\varphi}^{\xi}=\Gamma(\bigcup_{\eta<\xi}I_{\varphi}^{\eta}),$

then $I_{\varphi}^{\xi}$ is increasing in the ordinal parameter $\xi$ and has
some fixed point,

$I_{\varphi}=\bigcup_{\xi}I_{\varphi}^{\xi}.$

Then $I_{\varphi}$ is exactly the set defined by $[\mathbf{lfp}\
Sx.\varphi](u)$.

The _stages_ of $\varphi$ given a structure $\mathbf{A}$ are exactly the sets
$I_{\varphi}^{\xi}$. For $b\in A^{x}$, we define $\|b\|_{\varphi}$ to be the
least $\xi$ such that $b\in I_{\varphi}^{\xi}$. A fundamental result
(Moschovakis [15]) of $LFP$-definability is the _stage comparison theorem_ ,
which says that for any $\mathbf{A}$, the relation
$y\leq_{\varphi}z\iff\|y\|_{\varphi}\leq\|z\|_{\varphi}$ is $LFP$-definable,
and moreover its definition is independent of $\mathbf{A}$.

Another important notion is the _closure ordinal_ $\|\varphi\|_{\mathbf{A}}$,
which is defined to be the least $\kappa$ such that
$I_{\varphi}=I_{\varphi}^{\kappa}$. (Of course, if $\mathbf{A}$ is finite,
then so is $\kappa$.) This allows us to introduce the following fundamental
notion, due to Gregory McColm [14].

######  Definition 2.1 (Proficiency).

A class $\mathcal{C}$ of finite structures is _proficient_ if
$\|\varphi\|_{\mathbf{A}}$ is unbounded as $\mathbf{A}$ ranges over
$\mathcal{C}$ for some $\varphi$.

######  Remark 2.2.

If $\mathcal{C}$ is not proficient, then $LFP=FO$ over $\mathcal{C}$. This
observation, made originally in [14], amounts to showing that if $S$ is first-
order definable, so is $\varphi(x;S)$, and hence any finite stage of $\varphi$
as well. (Moreover, the definition is independent of the specific structure.)

######  Remark 2.3.

In [9], Immerman showed that over a class of finite structures, any $LFP$
formula is equivalent to one with a single application of the $\mathbf{lfp}$
quantifier. We will not use this result directly, but it does shed some light
on the complexity of $LFP$ formulas relative to $FO$ formulas over finite
structures.

Next we present the main classification-theoretic definitions (all of which
are originally due to Shelah [16] in the setting of first-order logic on
infinite structures):

######  Definition 2.4 (OP, sOP, IP, TP2).

Let $\varphi(x;y)$ be any formula ($FO$ or $LFP$), where $x$ and $y$ are
tuples of variables.

  * •

We say $\varphi(x;y)$ has an $n$-instance of the _order property_(OP($n$)) in
a structure $\mathbf{M}$ if there are $a_{1},\dots,a_{n}\in M^{x}$, and
$b_{1},\dots,b_{n}\in M^{y}$ such that

$\mathbf{M}\models\varphi(a_{i};b_{j})\iff i<j.$

    * –

We say $\varphi(x;y)$ has an $n$-instance of the _strict order
property_(sOP($n$)) in a structure $\mathbf{M}$ if there are
$b_{1},\dots,b_{n}\in M^{y}$ such that

$\varphi(M^{x};b_{1})\subsetneq\dots\subsetneq\varphi(M^{x};b_{n}).$

    * –

We say $\varphi(x;y)$ has an $n$-instance of the _independence
property_(IP($n$)) in a structure $\mathbf{M}$ if there are
$a_{1},\dots,a_{n}\in M^{x}$, and $b_{1},\dots,b_{2^{n}}\in M^{y}$ such that

$\mathbf{M}\models\varphi(a_{i};b_{j})\iff i\in j,$

identifying $\\{1,\dots,2^{n}\\}$ with the powerset of $\\{1,\dots,n\\}$.

    * –

We say $\varphi(x;y)$ has an $n$-instance of the _tree property 2_(TP2($n$))
in a structure $\mathbf{M}$ if there are $b_{i,j}\in M^{y}$ for $1\leq i,j\leq
n$ such that $\varphi(x;b_{i,j})$ and $\varphi(x;b_{i,k})$ are not
simultaneously satisfied by any $a\in M^{x}$ for distinct $j$ and $k$, yet for
any function $f\colon\\{1,\dots,n\\}\to\\{1,\dots,n\\}$, there is an element
$a_{f}\in M^{x}$ such that

$\mathbf{M}\models\bigwedge_{i=1}^{n}\varphi(a_{f};b_{i,f(i)}).$

######  Definition 2.5.

For any property $P$ among (OP, sOP, IP, TP2), we say that $\varphi(x;y)$ has
$P$ relative to a family of structures $\mathcal{C}$ if for every $n<\omega$
there is some $\mathbf{M}\in\mathcal{C}$ such that $\varphi(x;y)$ has $P(n)$
in $\mathbf{M}$. And finally, we say that $\mathcal{C}$ itself has $FO$-$P$ if
some $FO$ formula $\varphi$ has $P$ relative to $\mathcal{C}$, and $LFP$-$P$
if some $LFP$ formula $\varphi$ has $P$ relative to $\mathcal{C}$.

######  Remark 2.6.

Let $P$ be any property among (OP, sOP, IP, TP2), and let $\varphi(x;y)$ be a
formula. Here are a few observations:

  * •

If $\varphi$ has $P(n)$ in a structure $\mathbf{M}$, then it also has $P(m)$
in $\mathbf{M}$ for all $m\leq n$.

  * •

For every $N<\omega$, there is an upper bound on the $n$ such that $\varphi$
has $P(n)$ in a finite structure of size $\leq N$.

  * •

For every $n<\omega$, there is a sentence $\psi_{n}$ such that a structure
$\mathbf{M}\models\psi_{n}$ if and only if $\varphi$ has $P(n)$ in
$\mathbf{M}$. We can take $\psi_{n}$ to be an $FO$ sentence or an $LFP$
sentence according to whether $\varphi$ is an $FO$ formula or an $LFP$
formula.

  * •

In the classical first-order context, thanks to compactness, if an $FO$
formula $\varphi(x;y)$ has $P(n)$ in some model of $T$ for every $n<\omega$,
then $\varphi(x;y)$ has $P(\omega)$ in some model of $T$ (where we extend the
definitions to $n=\omega$ in the obvious ways). As a consequence, these
properties are usually defined in their infinitary forms. The finitary forms
defined above are obviously more suitable for classes of finite structures.

######  Remark 2.7.

It is easy to see that sOP $\implies$ OP, and that TP2 $\implies$ IP
$\implies$ OP for any formula $\varphi(x;y)$ relative to any family of
structures $\mathcal{C}$. (In fact, these implications hold in the most
general possible context, namely abstract set systems.) For a visualization of
these and many other model-theoretic dividing lines and their relationships,
see [4].

######  Remark 2.8.

We write NOP, NsOP, NIP, and NTP2 for the negations of the properties OP, sOP,
IP, and TP2. Since the positive properties indicate the presence of
complicated combinatorial configurations in the definable subsets of
structures in $\mathcal{C}$, their negations are tameness assumptions on
$\mathcal{C}$.

We now state our first main theorem, relating proficiency to the $LFP$ strict
order property.

######  Theorem 2.9.

For any family of finite structures $\mathcal{C}$, the following are
equivalent:

  1. 1.

$\mathcal{C}$ is proficient.

  2. 2.

$\mathcal{C}$ has $LFP$-sOP.

  3. 3.

There is some $n$ and a $2n$-ary $LFP$-formula that defines a partial preorder
over each $M^{n}$ with arbitrarily long chains as $\mathbf{M}$ varies over
$\mathcal{C}$.

  4. 4.

There is some $n$ and a $2n$-ary $LFP$-formula that defines a linear preorder
over each $M^{n}$ of arbitrarily large order type as $\mathbf{M}$ varies over
$\mathcal{C}$.

###### Proof.

$(1\iff 4\iff 3)$

$1\implies 4$. If $\varphi(x;S)$ is an $S$-positive formula, then its stage
comparison relation linearly preorders each $\mathbf{M}\in\mathcal{C}$, and
its order type is exactly $\|\varphi\|_{\mathbf{M}}$. Therefore, if $\varphi$
is proficient, $\psi$ defines arbitrarily long linear preorders.

$4\implies 3$. Trivially.

$3\implies 1$. Suppose $\lambda(y_{1};y_{2})$ is a partial preorder with
unbounded chains as $\mathbf{M}\in\mathcal{C}$. In a partial preorder we can
define the _height_ of an element to be one more than the height of its
(strict) predecessors or 0 if it has none. Since $\lambda$ has arbitrarily
long chains, elements in the preorder defined by $\lambda$ will have
arbitrarily large heights.

Let $\varphi(y;T)$ say that all of $y$’s strict predecessors are in $T$. In
other words,

$\varphi(y;T)\equiv\forall
y^{\prime}\,((\lambda(y^{\prime},y)\wedge\neg\lambda(y,y^{\prime}))\to
T(y^{\prime})).$

(Notice $T$ occurs positively in $\varphi$.) Then it is easy to show by
induction that the iterates $I_{\varphi}^{n}$ of $\varphi$ are exactly those
elements of height $<n$, and hence $\varphi$ is proficient. ∎

###### Proof.

$(2\iff 3)$

$2\implies 3$. For any partitioned formula $\varphi(x;y)$, if we define

$\psi(y_{1};y_{2})\equiv\forall x\ \varphi(x;y_{1})\to\varphi(x;y_{2}),$

then for each $\mathbf{M}\in\mathcal{C}$,

$\mathbf{M}\models\psi(y_{1};y_{2})\iff\varphi(M^{x};y_{1})\subseteq\varphi(M^{x};y_{2}),$

so $\psi$ defines a partial preorder on $M^{y}$. If in addition $\varphi$ has
the strict order property, then the partial preorder on $M^{y}$ defined by
$\psi$ has arbitrarily long chains as $\mathbf{M}$ varies over $\mathcal{C}$.

$3\implies 2$. If $\lambda(y_{1};y_{2})$ is a partial preorder with unbounded
chains as $\mathbf{M}\in\mathcal{C}$, then $\lambda$ itself witnesses the
strict order property: given $n$, pick $\mathbf{M}\in\mathcal{C}$ which
contains a chain $b_{1},\dots,b_{n}$. Then

$\lambda(M^{y_{1}};b_{1})\subsetneq\dots\subsetneq\lambda(M^{y_{1}};b_{n}).\qed$

Next, we show some nontrivial implications among the $LFP$-dividing lines that
are _not_ valid in the first-order context.

######  Lemma 2.10.

If $\mathcal{C}$ has $LFP$-sOP, then it also has $LFP$-IP and $LFP$-TP2.

###### Proof.

Since TP2$\implies$IP in the most general circumstances, it would suffice to
prove this lemma only for TP2, but but we do it for both.

Consider the family $\mathcal{N}$ of all finite linear orders in the language
$<$. Identify the unique linear order of size $n$ with the set
$n=\\{0,1,\dots,n-1\\}$ augmented by the natural ordering. It suffices to show
that $\mathcal{N}$ has $LFP$-IP and $LFP$-TP2; indeed, suppose that
$\mathcal{C}$ is a general family of structures which satisfies $LFP$-sOP.
Then $\mathcal{C}$ “interprets” $\mathcal{N}$ in the appropriate sense and
inherits the properties $LFP$-IP and $LFP$-TP2.

To be a little more concrete, by Theorem 2.9, there is some $n$ and a $2n$-ary
$LFP$-formula $\psi(u_{1};u_{2})$ that defines a linear preorder on $n$-tuples
of each element of $\mathcal{C}$ that grows arbitrarily large as we range over
$\mathcal{C}$. Suppose $\varphi(x;y)$ witnesses $LFP$-IP (resp. $LFP$-TP2)
over $\mathcal{N}$. Simply replace each variable $v$ of $\varphi$ by $n$
copies of that variable $v_{1},\dots,v_{n}$, replace $v<w$ by
$\psi(v_{1},\dots,v_{n};w_{1},\dots,w_{n})$, and proceed by induction on the
construction of $\varphi$ in the obvious way. This gives us a new formula
$\varphi^{\star}(x^{\star};y^{\star})$ witnessing $LFP$-IP (resp. $LFP$-TP2)
over $\mathcal{C}$.

So why does $\mathcal{N}$ satisfy both $LFP$-IP and $LFP$-TP2? Over
$\mathcal{N}$, the graphs of the addition, multiplication, _and_
exponentiation functions are $LFP$-definable. Hence, both of the relations

$\mathrm{bit}(x;y)\iff``\text{the $x$-th bit of $y$ base 2 is 1}"$

$\mathrm{factor}(x;y,z)\iff``y^{z}\text{ is the largest power of $y$ dividing
}x"$

are $LFP$-definable.

The relation $\text{bit}(x;y)$ has IP($n$) in $(m,<)$ for $m$ large enough by
$a_{i}=i$ for $1\leq i\leq n$ and $b_{j}=j-1$ for $1\leq j\leq 2^{n}$. The
relation $\text{factor}(x;y,z)$ has TP2($n$) in $(m,<)$ for $m$ large enough
by $b_{i,j}=(p_{i},j)$ for $(p_{i})_{i\in\omega}$ an enumeration of the
primes, and $a_{f}=\prod_{i=1}^{n}p_{i}^{f(i)}$. ∎

We are now in a position to state McColm’s conjecture for families of finite
structures that satisfy (first-order!) tameness properties.

######  Corollary 2.11.

If $\mathcal{C}$ has $FO$-_NOP_ , $FO$-_NIP_ , $FO$-_NTP2,_ or $FO$-_NsOP,_
then McColm’s Conjecture holds for $\mathcal{C}$ ($\mathcal{C}$ is proficient
iff $FO\neq LFP$ over $\mathcal{C}$).

###### Proof.

One direction of McColm’s Conjecture always holds: if $\mathcal{C}$ is not
proficient, then $FO=LFP$ over $\mathcal{C}$ (Remark 2.2). Conversely, if
$\mathcal{C}$ is proficient, then $\mathcal{C}$ has $LFP$-sOP by Theorem 2.9,
and $LFP$-TP2 (hence also $LFP$-IP and $LFP$-OP) by Lemma 2.10, so $FO\neq
LFP$. ∎

######  Remark 2.12.

Another way of phrasing Corollary 2.11 is this: since any counterexample to
McColm’s conjecture is a proficient class of structures over which $FO=LFP$,
and any proficient class of structures uniformly interprets the class of
initial segments of arithmetic in $LFP$, it follows that any counterexample to
McColm’s conjecture uniformly interprets the class of initial segments of
arithmetic in $FO$. Now the intuition is that the initial segments of
arithmetic are “as bad as possible” from the point of view of combinatorial
tameness properties. So every class of structures which are $FO$-tame
according to some notion of tameness that excludes arithmetic (such as
$FO$-NTP2 or $FO$-NsOP) satisfies McColm’s conjecture.

######  Corollary 2.13.

We can express the $LFP$-dividing lines purely in terms of $FO$-properties
plus $LFP$-_sOP_. Specifically,

$LFP\text{-OP}\iff FO\text{-OP}\vee LFP\text{-sOP},$ $LFP\text{-IP}\iff
FO\text{-IP}\vee LFP\text{-sOP},$ $LFP\text{-TP2}\iff FO\text{-TP2}\vee
LFP\text{-sOP}.$

###### Proof.

Let P stand for OP, IP, or TP2. If $LFP$-P but $LFP$-NsOP, then $LFP=FO$ by
Remark 2.2, so $FO$-P. Conversely, suppose $FO$-P or $LFP$-sOP. If $FO$-P,
then certainly $LFP$-P. If $LFP$-sOP then the result follows from Lemma 2.10.
∎

### First-order characterizations of $LFP$ dividing lines

Corollary 2.13 gives us a way of characterizing each $LFP$ property without
reference to _any_ fixed points of monotone operators. It suffices to give
such a characterization of $LFP$-sOP, i.e. proficiency. This is done in Dawar,
Lindell and Weinstein [6], who show that proficiency is equivalent to having
infinitely many realized $k$-variable types for some $k$. (They call the
opposite of this property $k$-_compactness._)

##  3 Implications among the $LFP$-properties

In this section, we complete the chain of implications among the
$LFP$-properties, by showing $LFP$-IP$\iff$$LFP$-OP. To do this, we show that
the classical identity OP$\iff\text{sOP}\vee\text{IP}$ continues to hold in
the $LFP$ case. We restrict our attention to IP, OP, sOP, and TP2 in the
context of $LFP$ definability only, so for brevity we drop the prefix $LFP$-.
In subsequent sections we will compare $LFP$\- and $FO$\- properties and
reintroduce the prefix.

The usual proof [16] of OP$\iff$sOP$\vee$IP in classical model theory for
first-order logic uses infinite indiscernible sequences, and therefore
(implicitly) compactness, which does not hold in the setting of $LFP$ logic
over families of finite structures.

However, compactness is not essential; we can replicate essentially the same
proof in our setting by replacing the infinitary Ramsey theory by finitary
Ramsey theory at the cost of slightly more ink.

######  Definition 3.1.

Let $\mathbf{A}$ be any structure, $\Delta$ a family of formulas ($FO$ or
$LFP$) in $k$ variables, and $\\{a_{i}\\}_{i<R}$ a sequence of elements of
$A$. We say that $\\{a_{i}\\}_{i<R}$ is _$\Delta$ -indiscernible _in case for
any formula $\delta(\mathtt{x}_{0},\dots,\mathtt{x}_{k})$ in $\Delta$ and any
two increasing subsequences $i_{0}<\dots<i_{k-1}<R$ and
$j_{0}<\dots<j_{k-1}<R$ of length $k$, we have

$\mathbf{A}\models\delta(a_{i_{0}},\dots,a_{i_{k-1}})\iff\mathbf{A}\models\delta(a_{j_{0}},\dots,a_{j_{k-1}}).$

######  Remark 3.2.

If $\Delta$ is finite, then for any $R$, there exists $R^{\star}$, such that
for any sequence of elements $\\{a_{i}\\}_{i<R^{\star}}$, there exists a
$\Delta$-indiscernible subsequence of length $R$. (Proof: Ramsey’s theorem,
applied to a $2^{|\Delta|}$-coloring of increasing $k$-tuples, according to
which formulas in $\Delta$ they satisfy.)

We introduce certain “global variables” in this section, which will be used in
the statements of the results below without being declared each and every
time.

In particular, we fix a family of structures $\mathcal{C}$ without the strict
order property, but with the order property. Our goal is to prove that
$\mathcal{C}$ has the independence property. In fact, if $\varphi(x;y)$ has
the order property relative to $\mathcal{C}$, then we will show that
$\varphi(y;x)$ has the independence property.

Fix a number $k<\omega$. We must exhibit some $\mathbf{M}\in\mathcal{C}$,
$c_{0},\dots,c_{k-1}\in M^{y}$, and $d_{0},\dots,d_{2^{k}-1}\in M^{x}$ such
that

$\mathbf{M}\models\varphi(d_{j};c_{i})\iff i\in j.$ (1)

######  Definition 3.3.

For any $\eta\in 2^{k}$, let $\varphi_{\eta}(x;y_{1},\dots,y_{k})$ be the
statement that $\varphi$ holds of $(x;y_{i})$ for exactly those $i\in\eta$,
i.e.,

$\varphi_{\eta}(x;y_{1},\dots,y_{k})\equiv\bigwedge_{i\in\eta}\varphi(x;y_{i})\wedge\bigwedge_{i\notin\eta}\neg\varphi(x;y_{i}).$

Let $\Delta_{k}$ be the collection of formulas $\exists
x\,\varphi_{\eta}(x;\bar{y})$ as $\eta$ ranges over $2^{k}$.

######  Definition 3.4.

A partitioned formula $\chi(x;z)$ _defines a chain of length_ $\ell$ _on
$\mathbf{M}$_ in case there are $b_{0},\dots,b_{\ell-1}\in M^{z}$ such that

$\chi(M^{x};b_{0})\subsetneq\dots\subsetneq\chi(M^{x};b_{\ell-1}).$

Since $\mathcal{C}$ does not have the strict order property, there is a
constant $N$ depending only on $k$ that bounds the length of a chain that any
formula $\psi(x;\bar{y})$ defines over any $\mathbf{M}\in\mathcal{C}$, where
$\psi$ ranges over _subformulas_ of $\varphi_{\eta}$, for $\eta\in 2^{k}$.

Fix $\mathbf{M}\in\mathcal{C}$ in which $\varphi$ has OP($n$), witnessed by
$\\{u_{i},v_{i}\\}_{i<n}$, where $n$ is large enough to extract a
$\Delta_{k}$-indiscernible sequence of length $kN$ from the sequence
$\\{v_{i}\\}_{i<n}$. Let $\\{a_{i},b_{i}\\}_{i<kN}$ be a subsequence of
$\\{u_{i},v_{i}\\}_{i<n}$ such that $\\{b_{i}\\}_{i<kN}$ is
$\Delta_{k}$-indiscernible.

For $0\leq i<k$, let $c_{i}=b_{iN}$. Between $c_{i}$ and $c_{i+1}$ there are
$b_{iN+1}$ up to $b_{iN+N-1}$, a sequence of length $N-1$. We show that
equation (1) holds exactly for this $\mathbf{M}$ and these $c_{i}$. What about
the $d_{j}$? We make the following definition:

######  Definition 3.5.

Say that a set $\eta\in 2^{k}$ is _selected_ in case for some $d\in M^{x}$,

$\forall i<k\ \mathbf{M}\models\varphi(d,c_{i})\iff i\in\eta.$

Showing equation (1) holds amounts to showing that every __ such $\eta$ is
selected. This is what we now show.

It suffices to show that:

  * •

for each $0\leq n\leq k$, there is some set in $2^{k}$ of size $n$ that is
selected, and

  * •

if the symmetric difference of a pair of sets in $2^{k}$ is two consecutive
elements, then one is selected iff the other is selected.

(This is because any two sets in $2^{k}$ of the same size differ by a
permutation in $S_{k}$, and permutations in $S_{k}$ are generated by
transpositions of consecutive elements.)

######  Lemma 3.6.

For each $0\leq n\leq k$, there is some set in $2^{k}$ of size $n$ that is
selected.

###### Proof.

We show _final_ subsets of $k$ are selected. This is simply from the order
property. For fixed $0\leq i\leq k-1$,

$\varphi(a_{iN};c_{j})\iff\varphi(a_{iN};b_{jN})\iff iN<jN\iff i<j,$

so $a_{iN}$ selects $\\{i+1,\dots,k-1\\}$ when $0\leq i<k-1$ and $\emptyset$
when $i=k-1$. ∎

######  Lemma 3.7.

Suppose that there are $\eta,\eta^{\prime}\in 2^{k}$ such that
$\eta\Delta\eta^{\prime}=\\{j,j+1\\}$ for some $j<k-1$. Then $\eta$ is
selected iff $\eta^{\prime}$ is selected.

###### Proof.

By contradiction, suppose that $\eta$ is selected but $\eta^{\prime}$ is not.
(With minimal loss of generality, we may assume that
$j\in\eta^{\prime}\setminus\eta$ and $j+1\in\eta\setminus\eta^{\prime}$.)

Suppose that for some $d\in M^{x}$ we have

$\forall i<k\ \mathbf{M}\models\varphi(d;c_{i})\iff i\in\eta.$

In particular,

$\mathbf{M}\models\exists x\,\varphi_{\eta}(x;c_{0},\dots,c_{k-1}).$

On the other hand, for no $d\in M^{x}$ is it true that

$\forall i<k\ \mathbf{M}\models\varphi(d;c_{i})\iff i\in\eta^{\prime}.$

By definition of $\varphi_{\eta^{\prime}}$, that means exactly that

$\mathbf{M}\models\neg\exists
x\,\varphi_{\eta^{\prime}}(x;c_{0},\dots,c_{k-1}).$

As the formulas $\exists x\,\varphi_{\eta}$ and $\exists
x\,\varphi_{\eta^{\prime}}$ are in $\Delta_{k}$, they hold of _no_ length-$k$
subsequence of $\\{b_{i}\\}_{i<kN}$ by $\Delta_{k}$-indiscernibility of that
sequence. In particular, they hold of subsequences $\bar{c}_{n}$ obtained by
replacing the pair $(c_{j},c_{j+1})$ in the sequence $(c_{0},\dots,c_{k-1})$
by $(b_{jN+n},b_{jN+n+1})$ for some $0\leq n\leq N-1$. (This preserves the
relative order of the elements since $c_{j}=b_{jN}$ and $c_{j+1}=b_{jN+N}$.)

Let $\varphi_{\eta\wedge\eta^{\prime}}(x;\bar{y})$ be the formula which only
asserts the instances of $\varphi$ where $\eta$ and $\eta^{\prime}$ agree (so
does not contain $\pm\varphi(x;y_{j})$ or $\pm\varphi(x;y_{j+1})$). Notice
that $\varphi_{\eta\wedge\eta^{\prime}}(x;\bar{c}_{n})$ is independent of $n$.
Now consider the formula

$\psi(x;\bar{y})\equiv\varphi_{\eta\wedge\eta^{\prime}}(x;\bar{y})\wedge\varphi(x;y_{j}).$

Notice that it is a subformula of $\varphi_{\eta^{\prime}}$, which is
$\psi\wedge\neg\varphi(x;y_{j+1})$. We claim that $\psi$ has a chain of length
$N$, in particular that

$\psi(M^{x};\bar{c}_{0})\subsetneq\dots\subsetneq\psi(M^{x};\bar{c}_{N-1}).$

This would contradict the definition of $N$, thus concluding the proof.

It remains to show two things: that for every $0\leq i<N-1$,

$\psi(M^{x};\bar{c}_{i})\subseteq\psi(M^{x};\bar{c}_{i+1}),$ (2)

and

$\psi(M^{x};\bar{c}_{i+1})\not\subseteq\psi(M^{x};\bar{c}_{i}).$ (3)

Towards (2), suppose that for some $d\in M^{x}$ and $0\leq i<N-1$,

$\mathbf{M}\models\psi(d;\bar{c}_{i})\wedge\neg\psi(d;\bar{c}_{i+1}).$

In other words,

$\mathbf{M}\models(\varphi_{\eta\wedge\eta^{\prime}}(d;\bar{c}_{i})\wedge\varphi(d;b_{jN+i}))\wedge\neg(\varphi_{\eta\wedge\eta^{\prime}}(d;\bar{c}_{i+1})\wedge\varphi(d;b_{jN+i+1})).$

Since

$\mathbf{M}\models\varphi_{\eta\wedge\eta^{\prime}}(d;\bar{c}_{i})\leftrightarrow\varphi_{\eta\wedge\eta^{\prime}}(d;\bar{c}_{i+1}),$

we have by propositional logic that

$\mathbf{M}\models\varphi_{\eta\wedge\eta^{\prime}}(d;\bar{c}_{i})\wedge\varphi(d;b_{jN+i})\wedge\neg\varphi(d;b_{jN+i+1}).$

But the right hand side is exactly $\varphi_{\eta^{\prime}}(d;\bar{c}_{i})$,
so

$\mathbf{M}\models\exists x\,\varphi_{\eta^{\prime}}(x;\bar{c}_{i}),$

which contradicts the fact that $\exists x\varphi_{\eta^{\prime}}$ holds of no
$\bar{c}_{i}$.

Towards (3), suppose for some $0\leq i<N-1$ that

$\mathbf{M}\models\forall x\ \psi(x;\bar{c}_{i+1})\to\psi(x;\bar{c}_{i}).$

Again by using the definitions of $\psi$ and $\varphi_{\eta}$, it follows by
pure propositional logic that

$\mathbf{M}\models\neg\exists x\,\varphi_{\eta}(x;\bar{c}_{i}).\qed$

This concludes the proof of the following theorem.

######  Theorem 3.8.

The family of structures $\mathcal{C}$ has OP iff it has sOP or IP.

######  Corollary 3.9.

For any family of finite structures $\mathcal{C}$, $\mathcal{C}$ has IP if and
only if it has OP.

###### Proof.

It is always the case that IP implies OP. Conversely, suppose $\mathcal{C}$
has OP. By Theorem 3.8, $\mathcal{C}$ has IP or sOP. In the second case, by
Lemma 2.10, $\mathcal{C}$ also has IP. ∎

######  Corollary 3.10.

For classes of finite structures, $LFP$-sOP $\implies$ $LFP$-TP2 $\implies$
$LFP$-IP $\iff$ $LFP$-OP.

###### Proof.

Lemma 2.10 and Corollary 3.9. ∎

##  4 Non-collapse for classes without sOP

Gurevich [7, Appendix 3] observed that in the context of models of a countably
categorical first-order theory, $LFP$ has no more expressive power than $FO$.
Blass, Gurevich, and Kozen [3] later used this observation to establish a
zero-one law for $LFP$ on random $L$-structures. In this section, we use the
same idea to give examples separating the properties $LFP$-sOP, $LFP$-TP2, and
$LFP$-IP, showing that the implications established in Corollary 3.10 are
strict. We essentially repeat Gurevich’s argument in Lemma 4.2 below.

When we say that a theory is countably categorical, we mean in particular that
it has infinite models.

######  Definition 4.1.

Let $\mathcal{C}$ be a class of finite structures. The (logical) limit theory
$T_{\mathcal{C}}$ is the set of all first-order sentences $\varphi$ such that
$\\{\mathbf{M}\in\mathcal{C}\mid\mathbf{M}\not\models\varphi\\}$ is finite.
Equivalently, $T_{\mathcal{C}}$ is the set of all sentences which are true in
every ultraproduct $\prod_{\mathcal{C}}\mathbf{M}/U$ by a non-principal
ultrafilter $U$. Note that $T_{\mathcal{C}}$ is consistent, as long as
$\mathcal{C}$ is infinite.

######  Lemma 4.2.

Suppose $\mathcal{C}$ is a class of finite structures such that
$T_{\mathcal{C}}$ is a complete and countably categorical first-order theory.
Then for every $LFP$ formula $\varphi(x)$, there is an $FO$ formula $\psi(x)$
such that $\varphi(x)$ is equivalent to $\psi(x)$ in all models of
$T_{\mathcal{C}}$ and in all structures $\mathbf{M}\in\mathcal{C}$.

###### Proof.

By induction on the depth of nesting of the lfp quantifier. We may assume that
$\varphi(x)$ has the form $[\textbf{lfp}\,Sy.\theta](x)$, where $S$ occurs
positively in $\theta(y;S)$.

Although the depth of nesting of the lfp quantifier is one less in $\theta$,
we cannot apply induction directly to $\theta$, since $S$ appears free in
$\theta$ (so $\theta$ is not an $LFP$ formula). Instead, we use the inductive
hypothesis to define a sequence of first-order formulas $\theta_{n}$ such that
$\theta_{n}$ defines the set $I_{\theta}^{n}$ for all $n\in\omega$, in all
models of $T_{\mathcal{C}}$ and all structures in $\mathcal{C}$.

Let $\theta_{0}$ be $\bot$. Given $\theta_{n}$, consider the formula
$\theta(\theta_{n};y)$ obtained by substituting $\theta_{n}$ for $S$ in
$\theta(S;y)$. This $LFP$ formula defines $I_{\theta}^{n+1}$. By the induction
hypothesis, there is a first-order formula $\theta_{n+1}$ which is equivalent
to $\theta(\theta_{n};y)$ in all models of $T_{\mathcal{C}}$ and in all
structures in $\mathcal{C}$.

Since (by the Ryll-Nardzewski theorem) there are only finitely many formulas
in variable context $y$ up to equivalence modulo $T_{\mathcal{C}}$, there is
some $n$ such that $\theta_{n}(y)$ is equivalent to $\theta_{n+1}(y)$ modulo
$T_{\mathcal{C}}$. The least such $n$ is the closure ordinal for $\theta$, and
$\theta_{n}(x)$ is equivalent to $\varphi(x)$ in models of $T_{\mathcal{C}}$.

Since $T_{\mathcal{C}}$ is the limit theory of $\mathcal{C}$, the first-order
sentence $\forall y\,(\theta_{n}(y)\leftrightarrow\theta_{n+1}(y))$ is also
true in all but finitely many structures in $\mathcal{C}$, and hence
$\theta_{n}$ is also equivalent to $\varphi(x)$ in these structures.

Now consider the exceptional structures $\mathbf{M}_{1},\dots,\mathbf{M}_{m}$
which fail to satisfy the equivalence of $\theta_{n}$ and $\theta_{n+1}$. Any
particular $\mathbf{M}_{j}$ can be picked out uniquely up to isomorphism by a
first-order sentence, and any isomorphism-invariant relation on
$\mathbf{M}_{j}$ is definable in $\mathbf{M}_{j}$ by a first-order formula. So
we can adjust the formula $\theta_{n}$ to handle the $\mathbf{M}_{j}$
individually by cases. ∎

The next step is to find classes of finite structures with complete and
countably categorical limit theories.

######  Definition 4.3.

A first-order theory $T$ has the finite model property if for every sentence
$\varphi$ such that $T\models\varphi$, $\varphi$ has a finite model.

######  Lemma 4.4.

Suppose $T$ is a countable first-order theory with the finite model property.
Then there is an infinite class $\mathcal{C}$ of finite structures such that
$T\subseteq T_{\mathcal{C}}$.

###### Proof.

Enumerate $T$ as $\\{\varphi_{i}\mid i<\omega\\}$. For each $n<\omega$, let
$\mathbf{M}_{n}$ be a finite model of $\bigwedge_{i=0}^{n}\varphi_{i}$, and
let $\mathcal{C}=\\{\mathbf{M}_{n}\mid n<\omega\\}$. Then for every
$\varphi_{i}\in T$,
$\\{\mathbf{M}\in\mathcal{C}\mid\mathbf{M}\not\models\varphi_{i}\\}\subseteq\\{\mathbf{M}_{j}\mid
j<i\\}$, so $T\subseteq T_{\mathcal{C}}$. ∎

######  Theorem 4.5.

Suppose $T$ is a complete countably categorical first-order theory with the
finite model property. Then there is an infinite class $\mathcal{C}$ of finite
structures such that $T\subseteq T_{\mathcal{C}}$, $FO=LFP$ over
$\mathcal{C}$, and for any property $P$ among (OP, sOP, IP, TP2),
$\mathcal{C}$ has $LFP$-$P$ if and only if $T$ has $FO$-$P$.

###### Proof.

By Lemma 4.4, let $\mathcal{C}$ be an infinite class of finite structures with
limit theory containing $T$ (hence equal to $T$, since $T$ is complete). Let
$P$ be a property among (OP, sOP, IP, TP2), and suppose first that $T$ has
$FO$-$P$, witnessed by the formula $\varphi(x;y)$. As noted in Remark 2.6,
there is an $FO$ sentence $\psi_{n}$ such that a structure $M\models\psi_{n}$
if and only if $\varphi$ has $P(n)$ in $M$. Since $\varphi$ has $P(n)$ in some
model of $T$, $\psi_{n}$ is in $T$ and hence is true in all but finitely many
structures $\mathbf{M}\in\mathcal{C}$. So $\mathcal{C}$ has $FO$-$P$, and
hence $LFP$-$P$.

Conversely, suppose $\mathcal{C}$ has $LFP$-$P$, witnessed by the formula
$\theta(x;y)$. By Lemma 4.2, there is an $FO$ formula $\varphi(x;y)$ which is
equivalent to $\theta(x;y)$ on all structures in $\mathcal{C}$, so $\varphi$
also witnesses $P$. As above, let $\psi_{n}$ be the $FO$ sentence asserting
that $\varphi$ has $P(n)$.

We claim that for all $n<\omega$, $\psi_{n}$ is true in infinitely many
structures $\mathbf{M}\in\mathcal{C}$. It suffices to show that for every
$\mathbf{M}$ such that $\mathbf{M}\models\psi_{n}$, we can find a larger
structure $\mathbf{M}^{\prime}\in\mathcal{C}$ such that
$\mathbf{M}^{\prime}\models\psi_{n}$. Indeed, as in Remark 2.6, let $N$ be the
upper bound on the $n$ such that $\varphi$ has $P(n)$ in a structure of size
$\leq|\mathbf{M}|$, and pick $\mathbf{M}^{\prime}$ such that $\varphi$ has
$P(N+1)$ in $\mathbf{M}^{\prime}$. Then $|\mathbf{M}^{\prime}|>|\mathbf{M}|$,
and $\varphi$ also has $P(n)$ in $\mathbf{M}^{\prime}$, since $n<N+1$, so
$\mathbf{M}^{\prime}\models\psi_{n}$. This shows that $\lnot\psi_{n}$ is not
in the limit theory $T_{\mathcal{C}}$, and since $T_{\mathcal{C}}$ is
complete, $\psi_{n}$ is in $T_{\mathcal{C}}$ for all $n$. We conclude that
$\varphi$ witnesses that $T_{\mathcal{C}}$ has $FO$-$P$. ∎

######  Corollary 4.6.

There exists a class of finite structures with $LFP$-IP but without $LFP$-TP2
and a class of finite structures with $LFP$-TP2 but without $LFP$-sOP.

###### Proof.

By Theorem 4.5, we only need to exhibit certain complete countably categorical
first-order theories with the finite model property, satisfying the $FO$
analogues of these properties. In the proof, we drop the prefix $FO$-.

For IP but not TP2, consider $T_{\text{RG}}$, the theory of the random graph.
This is well-known to be countably categorical with the finite model property,
to have IP, and to be simple; a first-order theory is simple if it does not
have the tree property (TP), which implies that it does not have TP2.

For TP2 but not sOP, consider $T_{\text{feq}}^{*}$, the generic theory of
parameterized equivalence relations. For discussions of this theory, see [5]
and [11]. In [5], Chernikov and Ramsey establish (Corollary 6.20) that
$T_{\text{feq}}^{*}$ does not have SOP1, which implies that it does not have
sOP, and (Corollary 6.18) that $T_{\text{feq}}^{*}$ is not simple by
witnessing TP2 directly. A proof that $T_{\text{feq}}^{*}$ has the finite
model property is given in [11]. ∎

######  Remark 4.7.

The proof of Corollary 4.6 mentions the combinatorial properties SOP1 and TP.
We have chosen not to define these in this paper, in order to keep to a
minimum the number of acronyms one must remember while reading. The reader can
find definitions in [4] or [5].

These properties, and indeed a plethora of other combinatorial properties
identified by model theorists, have the same form as the properties considered
in this paper, and can be finitized in the same way. In particular, they
satisfy the observations made in Remark 2.6, and Theorem 4.5 applies just as
well to them, so we have actually exhibited classes of finite structures with
IP but not TP and with TP2 but not SOP1. One might naturally ask whether it is
possible to go further and separate TP from TP2 or SOP1 from sOP.

But at present, we cannot use Theorem 4.5 to produce such examples, because of
open problems in model theory:

  * •

The question of whether a countably categorical theory has the finite model
property is very hard in general. Indeed, it is unknown whether any countably
categorical first-order theory with SOP1 has the finite model property.

  * •

No countably categorical theory with the finite model property has sOP [11,
Proposition 1.3], and it is unknown whether there is any first order theory
with TP but without TP2 and sOP.

We conclude with a list of some simple examples satisfying the various
combinations of properties we have discussed in this paper: see Figure 1.

Note that $LFP\neq FO$ implies proficiency and $LFP$-sOP (Remark 2.2 and
Theorem 2.9). So which $LFP$-properties a class has is determined by whether
$LFP=FO$ and by which $FO$-properties it has. Also, we have established that
there are no classes satisfying (NIP and sOP and $LFP=FO$) or (IP and NTP2 and
sOP and $LFP=FO$), since $LFP$-sOP implies $LFP$-IP and $LFP$-TP2 (Lemma
2.10).

Figure 1: Examples

$\begin{array}[]{|c||c|c|}\hline\cr FO\text{-properties}&LFP=FO&LFP\neq FO\\\
\hline\cr\hline\cr\text{NOP}=(\text{NIP and NsOP})&[n]&([n],S)\\\
\hline\cr\text{NIP and sOP}&\text{---}&([n],<)\\\ \hline\cr\text{IP and NTP2
and NsOP}&\text{RG}&\text{RG}+([n],S)\\\ \hline\cr\text{IP and NTP2 and
sOP}&\text{---}&\text{RG}+([n],<)\\\ \hline\cr\text{TP2 and
NsOP}&\text{PEQ}&\text{PEQ}+([n],S)\\\ \hline\cr\text{TP2 and
sOP}&\text{GIS}&\text{PEQ}+([n],<)\\\ \hline\cr\end{array}$

Here are the definitions of the classes appearing in Figure 1:

  * •

$[n]$ is the class of initial segments of $\mathbb{N}$ with no extra
structure. $([n],S)$ and $([n],<)$ are the classes of structures with the same
domains, but equipped with the successor relation and the order relation,
respectively.

  * •

RG is any class of finite structures with limit theory $T_{\mathrm{RG}}$, the
theory of the random graph. Such a class exists by Lemma 4.4, and the Paley
graphs provide an explicit example (see [2]).

  * •

PEQ is any class of finite structures with limit theory
$T_{\mathrm{feq}}^{*}$, the generic theory of parameterized equivalence
relations. Such a class exists by Lemma 4.4.

  * •

GIS is any counterexample to McColm’s conjecture. For example, one of the
classes of finite structures devised by Gurevich, Immerman, and Shelah in [8].

  * •

Given classes of finite structures $\mathcal{C}=\\{\mathbf{M}_{i}\mid
i\in\omega\\}$ and $\mathcal{C}^{\prime}=\\{\mathbf{M}^{\prime}_{i}\mid
i\in\omega\\}$ in disjoint languages $L$ and $L^{\prime}$, respectively, we
denote by $\mathcal{C}+\mathcal{C}^{\prime}$ the family
$\\{\mathbf{M}_{i}\sqcup\mathbf{M}_{i}^{\prime}\mid i\in\omega\\}$, where
$\mathbf{M}_{i}\sqcup\mathbf{M}_{i}^{\prime}$ is the disjoint union of
$\mathbf{M}_{i}$ and $\mathbf{M}_{i}^{\prime}$. We use the fact that for any
property $P$ among $(\text{sOP},\text{TP2},\text{IP},\text{OP})$,
$\mathcal{C}+\mathcal{C}^{\prime}$ has $FO$-$P$ if and only if $\mathcal{C}$
has $FO$-$P$ or $\mathcal{C}^{\prime}$ has $FO$-$P$.

## Acknowledgements

We would like to thank Cameron Hill for his comments on the first draft of
this paper. We would also like to thank Steve Lindell, Scott Weinstein, and
Greg McColm for many helpful conversations about the topics surrounding this
paper.

## References

  * [1] Hans Adler and Isolde Adler, _Nowhere dense graph classes, stability, and the independence property_. arXiv:1011.4016 [math.LO] (2010).
  * [2] Andreas, Blass, Geoffrey Exoo, and Frank Harary, _Paley graphs satisfy all first-order adjacency axioms_. J. Graph Theory 5 (1981) 435–439.
  * [3] Andreas Blass, Yuri Gurevich, and Dexter Kozen, _A zero-one law for logic with a fixed-point operator_. Information and Control 67 (1985), Issue 1, 70–90.
  * [4] Gabriel Conant, _Map of the universe_. Website (retrieved January 2018). http://forkinganddividing.com/.
  * [5] Artem Chernikov and Nicholas Ramsey, _On model-theoretic tree properties_. J. Math. Log. 16, 1650009 (2016).
  * [6] Anuj Dawar, Steven Lindell, and Scott Weinstein, _First order logic, fixed point logic and linear order_. In: International Workshop on Computer Science Logic. Springer, Berlin, Heidelberg, 1995.
  * [7] Yuri Gurevich, _Toward logic tailored for computational complexity_. In: Börger E., Oberschelp W., Richter M.M., Schinzel B., Thomas W. (eds) Computation and Proof Theory. Lecture Notes in Mathematics, vol 1104. Springer, Berlin, Heidelberg, 1984. http://web.eecs.umich.edu/~gurevich/Opera/60.pdf.
  * [8] Yuri Gurevich, Neil Immerman, and Saharon Shelah, _McColm’s conjecture [positive elementary inductions]_. In: Proc. IEEE Symp. on Logic in Computer Science (1994), 10–19.
  * [9] Neil Immerman, _Relational Queries Computable in Polynomial Time_. Information and Control 68.1–3 (1986), 86–104.
  * [10] Phokion Kolaitis and Moshe Vardi, _Fixpoint logic vs. infinitary logic in finite model theory_. In: Proc. IEEE Symp. on Logic in Computer Science (1992), 46–57.
  * [11] Alex Kruckman, _Disjoint $n$-amalgamation and pseudofinite countably categorical theories_. arXiv:1510.03539 [math.LO] (2015).
  * [12] Maryanthe Malliaris and Saharon Shelah, _Regularity lemmas for stable graphs_. Trans. Amer. Math. Soc. 366 (2014), 1551-1585.
  * [13] Maryanthe Malliaris and Caroline Terry. _On unavoidable induced subgraphs in large prime graphs_. arXiv:1511.02544 [math.LO] (2015).
  * [14] Gregory McColm, _When is Arithmetic Possible?_ Annals of Pure and Applied Logic 50 (1990), 29–51.
  * [15] Yiannis Moschovakis, _Elementary Induction on Abstract Structures_. Studies in Logic and the Foundations of Mathematics, Vol. 77. North-Holland, Amsterdam, 1974.
  * [16] Saharon Shelah, _Classification theory: and the number of non-isomorphic models_. Second edition. Studies in Logic and the Foundations of Mathematics, Vol. 92. North-Holland, Amsterdam, 1990.