Fixed-point logics, descriptive complexity, and random satisfiability

We study the expressive power and the computational aspects of fixed-point logics on finite structures. Fixed-point logics is the generic name for the several known extensions of first-order logic with a mechanism to incorporate recursion through inductive definitions.; In the first part of the thesis, we compare the expressive power of least fixed-point logic UP with that of first-order logic FO on structures that are equipped with the powerful built-in predicate known as BIT, or equivalently, the set-membership relation when the elements of the universe are interpreted as hereditarily finite sets. The power and importance of this built-in predicate stems from the fact that it provides logics with the ability to simulate low-level computations. Moreover, its set-theoretic interpretation allows us to use methods and techniques from set theory. We consider natural fragments of UP syntactically defined in terms of the bounded formulas of set theory. The goal is to identify the boundary between the fragments of UP that collapse to FO and those whose collapse is unlikely or will be hard to settle. First, we show that certain large natural fragments of UP collapse to FO. The proofs of these collapsing results are based on the absoluteness properties that the bounded formulas of set theory enjoy. Second, we prove that the collapse of essentially the next fragment would imply unexpected results in complexity theory. For these fragments, we focus on their computational aspects and identify the complexity classes they capture.; In the second part of the thesis, we obtain inexpressibility results for Datalog and use them to derive consequences for computational complexity. Datalog is a pure fixed-point logic without built-in predicates capable of expressing many important properties, such as unsatisfiability of 2-CNF formulas, non 2-colorability of graphs, the monotone circuit value problem, and path systems, among others. We revisit the model for random 3-CNF formulas with a fixed density, and prove that every Datalog property that implies unsatisfiability of these formulas must have asymptotic probability zero, even when formulas are taken in the region in which most formulas are unsatisfiable. Then we observe that our negative result allows us re-derive the well-known lower bounds for Resolution refutations of random 3-CNF formulas, and the Pigeonhole Principle. Thus, our results establish precise connections between the areas of finite model theory and propositional proof complexity.