The complexity of first-order and monadic second-order logic revisited (Q1886318)

The model-checking problem for a logic \(L\) is defined as follows. The inputs are (1) \(\phi\), a sentence in \(L\), and (2) a structure \(A\), and the goal is to determine whether \(\phi\) holds in \(A\). It was known that for first-order logic and for monadic second-order logic the model-checking problem is fixed-parameter tractable when the structure \(A\) is restricted to be a word. This means that for each of the two logics there exists a computable function \(f\) so that the problem is solvable in \(f(k) \cdot n\) time, where \(k\) is the length of \(\phi\) and \(n\) is the length of the word \(A\). This paper shows that, unless some implausible facts hold (such as P = NP), the function \(f\) is larger than any elementary function, in particular larger than any \(h\)-fold exponential function for any fixed \(h\). Some related hardness results are established for other types of structures (e.g., trees).