6
$\begingroup$

Gurevich provides an exact definition of what Logic capturing PTIME is.

An abstract logic $L$ consists of

  • a set of $L[\tau]$-sentences for each vocabulary $\tau$,
  • and a mapping that maps a property $\mathcal{P}_\varphi$ to each $L[\tau]$-sentence $\varphi$.

An abstract logic $L$ captures polynomial time on $\mathcal{C}$ if

  • for every $\tau$, $L[\tau]$ is decidable,
  • for every property $\mathcal{P}$ of $\tau$-structures that is decidable in polynomial time, there is a $\varphi \in L[\tau]$ which defines $\mathcal{P}$ on $\mathcal{C}$,
  • for every vocabulary $\tau$, we can compute an algorithm which decides $\mathcal{P}_\varphi$ for every $\varphi \in L[\tau]$.

Infinitary logic $\mathcal{L}_{\infty \omega}$ is an extension of First-Order Logic s.t. if $X$ is set then both

$$ \bigvee_{\phi \in X} \phi \textrm{ and } \bigwedge_{\phi \in X} \phi$$

are formulars. $\mathcal{L}^k_{\infty \omega}$ is infinitary logic with only $k$ distinct variables.

Apart from the question for which classes $\mathcal{C}$ of finite(!) structures, $\mathcal{L}_{\infty \omega}^k$ describes all polynomial time decidable properties, I want to know if $\mathcal{L}_{\infty \omega}^k$ is a logic in that sense.

First Question: Is $\mathcal{L}_{\infty \omega}^k[\tau]$ decidable for each $\tau$? We need an encoding for each $\varphi \in \mathcal{L}_{\infty \omega}^k[\tau]$ and a Turing Machine to decide whether $X$ is a set. Is it possible to provide a finite encoding for each $\varphi$?

Problem: If we want to define a Turing Machine which decides whether $\varphi \in \mathcal{L}_{\infty \omega}^k[\tau]$ we need a finite representation of $\varphi$. Approach: Let $\mathsf{FO}[\tau]$ be the set of all first order sentences over $\tau$. It is not possible to define a finite code for each $X \subset \mathsf{FO}[\tau]$ over a finite alphabet like $\{0,1\}$. $X$ is countable. However, $|\mathcal{P}(\mathsf{FO}[\tau])| > |\{0,1\}^*|$. Hence, there can be no bijective mapping from $\mathcal{P}(\mathsf{FO}[\tau])$ to $\{0,1\}^*$ (or any code with finite alphabet).

Second Question: The other thing is a model checking algorithm. Is there a model checking algorithm for $\mathcal{L}_{\infty \omega}^k[\tau]$ on each finite $\tau$ for classes $\mathcal{C}$ of finite structures? Can we make assertions regarding the run time? The basic ideas that on a finite structure it is sufficient to model check a finite $X' \subset X$ to decide.

Any ideas? Any references?

$\endgroup$
  • 4
    $\begingroup$ How do you finitely represent a formula in $\mathcal{L}_{\infty\omega}$? Without further restriction, I can define $X$ as the set of accepted words of a Turing machine, and ask about the validity of $\bigvee_{\phi\in X}\phi$. $\endgroup$ – Sylvain Mar 3 '14 at 19:38
  • 1
    $\begingroup$ The syntax is that $X$ has to be a set. Turing Machine Acceptance would require $X$ to be computable, right? I do not know if this is relevant ... $\endgroup$ – Joachim Mar 3 '14 at 22:47
  • 3
    $\begingroup$ An arbitrary set is not a syntactic object that you can give a computer. You have to represent it as a finite object, e.g. computable sets represented by TMs. Now what Sylvain is saying is that even that is not enough because it is easy to encode the halting problem using a single disjunction of a computable set of formulas (and you can restrict even more and make the set $AC^0$ decidable but it won't help as you can still get the halting problem). $\endgroup$ – Kaveh Mar 3 '14 at 23:12
  • 1
    $\begingroup$ @Kaveh: maybe you should turn that into an answer. $\endgroup$ – cody Mar 4 '14 at 16:45
  • $\begingroup$ @Sylvain was first to answer, I just expanded his comment a bit. $\endgroup$ – Kaveh Mar 5 '14 at 15:56
2
$\begingroup$

First question: A set $M$ is decidable if there is a Turing Machine which halts on all inputs and accepts all inputs $x$ with $x \in M$.

We try to encode $\bigwedge_{\phi \in X} \phi$ for arbitrary sets of $\mathsf{FO}[\tau]$-formulars $X$. Since, $\mathcal{P}(X)$ is uncountable there can be no code with finite alphabet. Hence, there can be no Turing Machine recognizing $\mathcal{L}_{\infty\omega}[\tau]$ for each $\tau$ (even for empty $\tau$). Hence, the syntax is undecidable.

Second question: Given a code which translates a Deterministic Turing Machine (DTM) $T$ into a $\tau$-Structure $\mathcal{T}$. We can write a $\mathsf{FO}$-formular $\varphi_k$ with

$$ \mathcal{T} \models \varphi_k \Leftrightarrow \textrm{ The DTM $T$ holds after $k$ steps on $\varepsilon$.}$$

If we reassign variables (forgot the previous states of the Turing Machine) we can modell this $\varphi_k$ with constant, finite number $m$ of variables which does not depend on $k$.

Hence,

$$ T \in H_\varepsilon \Leftrightarrow \mathcal{T} \models \bigvee_{k \in \omega} \varphi_k \in \mathcal{L}_{\infty \omega}^m.$$

Where $H_\varepsilon$ is the special Halting Problem. Consequently, the Model Checking Problem for $\mathcal{L}_{\infty \omega}^m$ is undecidable for sufficiently large $m$.

$\endgroup$
  • 1
    $\begingroup$ Both problems are meaningless until you provide us with a finite presentation for formulae (which of course entails a restriction on the class of sets over which you can do conjunctions or disjunctions). The questions can only start to make sense if you restrict the class of sets $X$. $\endgroup$ – Sylvain Mar 5 '14 at 15:34
  • 1
    $\begingroup$ PS: As pointed out by Kaveh above, the answer is going to be "No, it's undecidable", already for highly restricted classes of sets $X$. PPS: In fact, it's probably highly undecidable, i.e. outside the arithmetical hierarchy, already for very restricted classes for $X$. $\endgroup$ – Sylvain Mar 5 '14 at 15:45
  • 1
    $\begingroup$ The issue is that it is easy to convert a first-order formula in arithmetic to quantifier free formula using infinite disjunctions and conjunctions and we know first order arithmetic is not decidable. A more reasonable thing might be to allow the size of the disjunctions/conjunctions to grow with the size of the structure but remain polynomially bounded in it. That would probably give one of the known descriptive complexity classes like FO[poly(n)] or something like that. $\endgroup$ – Kaveh Mar 5 '14 at 15:49
  • $\begingroup$ Or FO[log n], see Immerman's page. $\endgroup$ – Kaveh Mar 5 '14 at 15:54
  • $\begingroup$ @Kaveh: now that pointer would make a great answer :) $\endgroup$ – Sylvain Mar 5 '14 at 16:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.