# Is infinitary logic a logic in the sense of Gurevich?

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?

• 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$. – Sylvain Mar 3 '14 at 19:38
• 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 ... – Joachim Mar 3 '14 at 22:47
• 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). – Kaveh Mar 3 '14 at 23:12
• @Kaveh: maybe you should turn that into an answer. – cody Mar 4 '14 at 16:45
• @Sylvain was first to answer, I just expanded his comment a bit. – Kaveh Mar 5 '14 at 15:56

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$.

• 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$. – Sylvain Mar 5 '14 at 15:34
• 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$. – Sylvain Mar 5 '14 at 15:45
• 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. – Kaveh Mar 5 '14 at 15:49
• Or FO[log n], see Immerman's page. – Kaveh Mar 5 '14 at 15:54
• @Kaveh: now that pointer would make a great answer :) – Sylvain Mar 5 '14 at 16:04