Finitely unstable theories and computational complexity

TL;DR

This paper explores the logical encoding of Turing machine computations within first order logic, establishing lower bounds on model size and time complexity for SAT-solving machines based on finite model theory.

Contribution

It introduces a novel encoding of finite-time Turing machine computations in first order logic and derives exponential lower bounds on model size and complexity for SAT-solving DTMs.

Findings

Lower bounds on model size grow almost exponentially with input parameter M.

Lower bounds on deterministic time complexity for SAT-solving Turing machines.

Logical encodings relate finite model theory to computational complexity.

Abstract

The complexity class $NP$ can be logically characterized both through existential second order logic $SO\exists$, as proven by Fagin, and through simulating a Turing machine via the satisfiability problem of propositional logic SAT, as proven by Cook. Both theorems involve encoding a Turing machine by a formula in the corresponding logic and stating that a model of this formula exists if and only if the Turing machine halts, i.e. the formula is satisfiable iff the Turing machine accepts its input. Trakhtenbrot's theorem does the same in first order logic $FO$. Such different orders of encoding are possible because the set of all possible configurations of any Turing machine up to any given finite time instant can be defined by a finite set of propositional variables, or is locally represented by a model of fixed finite size. In the current paper, we first encode such time-limited computations of a deterministic Turing machine (DTM) in first order logic. We then take a closer look at DTMs that solve SAT. When the length of the input string to such a DTM that contains effectively encoded instances of SAT is parameterized by the natural number $M$, we proceed to show that the corresponding $FO$ theory $SAT_M$ has a lower bound on the size of its models that grows almost exponentially with $M$. This lower bound on model size also translates into a lower bound on the deterministic time complexity of SAT.