Anil Seth

The Institute of Mathematical Sciences, Madras, India.

Implicit Definability vs. Weak Implicit Definability in Finite Model Theory

DIMACS Center - Room 431
Busch Campus
Piscataway, New Jersey
June 7, 2:30 p.m.


We compare two similar definitions of implicit definability in the context of finite model theory. The first definition requires that there is -exactly- one relation in every finite structure satisfying a given formula implicitly defining a query. Whereas the second definition is more liberal and requires -at most- one relation in every finite structure satisfying the given formula implicitly defining a query. These two ways are sometimes referred to as implicit and weak implicit definition respectively, in the literature. For a logical language L, we denote weak implicit closure and implicit closure of L by WIMP(L) and IMP(L), respectively. We find that these two notions give rise to logics that behave quite differently on classes of finite structures. For instance, WIMP(FO) and IMP(FO), capture UP and UP \intersect Co-UP respectively, on ordered structures but there are PTIME queries on unordered structures in WIMP(FO) which do not appear to be in IMP(FO). Weak implicit definability is much easier to work with. Many results which have easy proofs for the weak implicit definability have either very difficult or no proofs for the implicit definability. For instance, we give an elementary proof of WIMP(FO) is not contained in the finite variable infinitary first-order logic, whereas the only known proof earlier is implied by the proof of the stronger result for IMP(FO), which uses a complex probabilistic construction due to Gurevich and shelah. As another example, we show that there is no 0-1 law for WIMP(FO) but the question is open for IMP(FO).

We strongly suspect that the implicit closure and weak implicit closure of least fixed point logic, (and similarly, of partial fixed point logic or of infinitary logic with finitely many variables) give rise to two different logics. In the absence of auxiliary queries, we can separate these logics. However, to show the same separation in the general case appears to be an interesting and intriguing problem.