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.
Abstract:
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.