Guarded Quantification

Guarded quantification can be regarded as a modification of the quantification rules of the game programs. Here we have a new relation P (or perhaps several relations P_i) (perhaps defined in some special way from given relations), which can be used to constrain quantification as follows. If the game is currently at a state (s; x), where x = x₁, ..., x_l, then an appropriate player may be permitted to choose some y satisfying

P(x₁', ..., x_l''; y) and the game continues from (s''; x'', y), where x'' = x₁'', ..., x_l''' consists of elements from x. This gives us an image of moving a marker along P-arcs. The relation(s) P is the "guard(s)".

The quantification rules become:

(s; x) :- (Qy: P(x'; y)) (s'; x'',y) and assert that from a state (s; x), the appropriate player can choose any y satisfying P(x'; y), and the game continues from (s''; x'', y).

This approach appeared in a 1983 JSL paper by Kevin Compton, motivated by classical model-theoretic concerns. It appears again in a series of recent papers by Hajnal Andreka, Johan van Benthem, and Istvan Nemeti, which were motivated by concerns in modal logic. (Since then, Erich Graedel has developed an interest in the decidability issues involved.)

First Order Logic with Guards

Most of the pre-Graedel work is on fragments of "guarded first order logic", i.e., there is no recursion. There is one immediate problem: for formulas of quantifier depth r, vertices of distance > r from constants are inaccessible. There are two ways to finesse this:

Require that there exists R such that in the guard structures, all vertices are within R steps of some constants. In this case we say that the guard structures are of "bounded extent".
Permit transitive closures of formulas of 2k free variables. We will still need the guard structures to be of "finite extent": every vertex is accessible from {\it somewhere}.

In this page, we will look at the first option.

Let's look at simulation (for unguarded simulation, see the bisimulation page. One detail: given a structure D, we will add guard relation P, on the same domain as the structure D, to get an "expansion" (D, P).

The Fraisse-Ehrenfeucht games for guarded FO are straightforward: you have two structures (D₁, P₁) and (D₂, P₂), where D_i is the structure and P_i the guard relation (on the same domain as D_i). The game of r pairs of moves consists, as usual, of a Spoiler placing a pebble on a structure, and a Duplicator responding on the other. The Duplicator wins iff the map from pebbled vertices of (D₁, P₁) to the pebbled vertices of (D₂, P₂) is a partial isomorphism. Let "(D₁, P₁) =_r (D₂, P₂)" mean that the Duplicator has a winning strategy for the r-pairs-of-moves game.

Theorem. (Andreka, van Benthem, Nemeti) If (D₁, P₁) =_r (D₂, P₂), then for any guarded FO formula THETA of quantifier depth <= r, (D₁, P₁) |= THETA iff (D₂, P₂) |= THETA. Conversely, the equivalence classes of =_r are guarded FO-expressible.

Hence, guarded FO has the same expressive power as FO itself iff the guard is of bounded extent.

Hidden Recursions

Yuri Gurevich has complained that unguarded quantification in relational database theory ignores significant computational complexity. Constrained quantification may provide a way to expose the complexities. Intuitively, the guarded quantifications seem to capture the steps that a computer might take in tracking down a datum via quantifiers. And yet we lose no expressive power:

Theorem. On the class of finite structures, where P is strongly connected, all FO + LFP queries are guarded FO + LFP expressible.

Idea of proof. All we have to do is show how unquarded quantification can be captured by recursions of guarded quantifications. For existential quantification, this is easy: Eloise simply goes out and finds the vertices that she claimed existed. The problem is representing universal quantification by having Abelard go off and finding a vertex to challenge. Remember that if the game goes on forever, Abelard wins, so we can't just let Abelard go out and spend all eternity finding his alleged counterexample.

To prevent Abelard from stalling, we enable Eloise to challenge a move Abelard makes, as follows. If Abelard started his search at a, and is at x, then if he was moving towards a vertex to challenge, his next vertex would be a y such that P(x; y) and P-dist(a, y) > P-dist(a, x). So after Abelard moves from x to y, Eloise could challenge him to a race: they race from x and y respectively, and if Abelard doesn't win, he was stalling, and so he should lose the game. QED

Notice that this will NOT work on an infinite structure.

Incidentally we can get some parametrization results about guarded FO + LFP using the game view of this logic. For example, the Dimension or Arity is the maximum number of variables for any formula in an LFP recursion: there is a matroidish characterization of dimension in my 1995 MLQ paper. So we could get a variant of the dimension result of Martin Grohe (see APAL 82 (1996)):

Theorem Suppose that we were on a class of finite structures such that:

The guard was connected.
On each structure, every tuple had an outdegree of order o(ln^k n) for each fixed k > 0, where n is the cardinality of the structure.
There was an unbounded guarded FO + LFP induction.

Then Dimension is nontrivial.

We would like to get this result for result for any class of structures admitting an unbounded FO induction.