First-Order Logic vs. Fixed-Point Logic in Finite Set Theory

The ordered conjecture states that least fixed-point logic LFP is strictly more expressive than first-order logic FO on every infinite class of ordered finite structures. It has been established that either way of settling this conjecture would resolve open problems in complexity theory. In fact, this holds true even for the particular instance of the ordered conjecture on the class of BIT-structures, that is, ordered finite structures with a built-in BIT predicate. Using a well known isomorphism from the natural numbers to the hereditarily finite sets that maps BIT to the membership relation between sets, the ordered conjecture on BIT-structures can be translated to the problem of comparing the expressive power of FO and LFP in the context of finite set theory. The advantage of this approach is that we can use set-theoretic concepts and methods to identify certain fragments of LFP for which the restriction of the ordered conjecture is already hard to settle, as well as other restrict...

• Type: Conference
• Year: 1999
• Where: LICS
• Authors: Albert Atserias, Phokion G. Kolaitis
• Keywords: Automated Reasoning, Conjecture, Finite Structures, Fixed-point Logic Lfp, LICS 1999