k variables are needed to define k-Clique in first-order logic

TL;DR

This paper proves that the number of variables needed to define the k-Clique problem in first-order logic on finite ordered graphs is exactly k, using a purely model-theoretic approach, confirming longstanding conjectures.

Contribution

It provides a purely model-theoretic, constructive proof that exactly k variables are necessary to define k-Clique in first-order logic, and extends the result to structures with arithmetic predicates.

Findings

Confirmed that k variables are necessary for k-Clique in first-order logic.

Provided a constructive, model-theoretic proof alternative to circuit complexity methods.

Extended results to structures with arbitrary arithmetic predicates.

Abstract

In an early paper, Immerman raised a proposal on developing model-theoretic techniques to prove lower bounds on ordered structures, which represents a long-standing challenge in finite model theory. An iconic question standing for such a challenge is how many variables are needed to define $k$-Clique in first-order logic on the class of finite ordered graphs? If $k$ variables are necessary, as widely believed, it would imply that the bounded (or finite) variable hierarchy in first-order logic is strict on the class of finite ordered graphs. In 2008, Rossman made a breakthrough by establishing an optimal average-case lower bound on the size of constant-depth unbounded fan-in circuits computing $k$-Clique. In terms of logic, this means that it needs greater than $\lfloor\frac{k} {4}\rfloor$ variables to describe the $k$-Clique problem in first-order logic on the class of finite ordered graphs, even in the presence of arbitrary arithmetic predicates. It follows, with an unpublished result of Immerman, that the bounded variable hierarchy in first-order logic is indeed strict. However, Rossman's methods come from circuit complexity and a novel notion of sensitivity by himself. And the challenge before finite model theory remains there. In this paper, we give an alternative proof for the strictness of bounded variable hierarchy in $\fo$ using pure model-theoretic toolkit, and anwser the question completely for first-order logic, i.e. $k$-variables are indeed needed to describe $k$-Clique in this logic. In contrast to Rossman's proof, our proof is purely constructive. Then we embed the main structures into a pure arithmetic structure to show a similar result where arbitrary arithmetic predicates are presented. Finally, we discuss its application in circuit complexity.