A Logic for PTIME and a Parameterized Halting Problem
Yijia Chen, Jörg Flum · Lecture notes in computer science · 2009
In [9] Yuri Gurevich addresses the question whether there is a logic that captures polynomial time. He conjectures that there is no such logic. He considers a logic, we denote it by L ≤ , that allows to express precisely the polynomial time properties of structures; however, apparently, there is no algorithm “that given an L ≤ -sentence ϕ produces a polynomial time Turing machine that recognizes the class of models of ϕ.” In [12] Nash, Remmel, and Vianu have raised the question whether one can prove that there is no such algorithm. They give a reformulation of this question in terms of a parameterized halting problem $p\textsc{-Acc}_\le$ for nondeterministic Turing machines. We analyze the precise relationship between L ≤ and $p\textsc{-Acc}_\le$ . Moreover, we show that $p\textsc{-Acc}_\le$ is not fixed-parameter tractable if “P $ e NP$ holds for all time constructible and increasing functions.” A slightly stronger complexity theoretic hypothesis implies that L ≤ does not capture polynomial time. Furthermore, we analyze the complexity of various variants of $p\textsc{-Acc}_\le$ and address the construction problem associated with $p\textsc{-Acc}_\le$ .