[Proof Complexity] New paper: A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

[Yijia Chen]

Dear all,

We have posted a new paper online

https://basics.sjtu.edu.cn/~chen/papers/haltlics.pdf

Title: A parameterized halting problem, the linear time hierarchy, and
the MRDP theorem

Abstract:

The complexity of the parameterized halting problem for nondeterministic
Turing machines p-Halt is known to be related to the question of whether
there are logics capturing various complexity classes [Chen and Flum, 2012].
Among others, if  p-Halt is in para-AC^0, the parameterized version of the
circuit complexity class AC^0, then AC^0, or equivalently, (+, \times)-invariant
FO, has a logic. Although it is widely believed that p-Halt \notin para-AC^0,
we show that the problem is hard to settle by establishing a connection to
the question in classical complexity of whether NE\not\subseteq LINH.
Here, LINH denotes the linear time hierarchy.

On the other hand, we suggest an approach toward proving NE\not\subseteq
LINH using bounded arithmetic. More specifically, we demonstrate that if
the much celebrated MRDP (for Matiyasevich-Robinson-Davis-Putnam) theorem
can be proved in a certain fragment of arithmetic, then NE\not\subseteq
LINH. Interestingly, central to this result is a para-AC^0 lower bound
for the parameterized model-checking problem for FO on arithmetical
structures.


Any comments and suggestions will be greatly appreciated.


With best wishes,

Keita, Moritz, and Yijia