Is infinitary logic a logic in the sense of Gurevich?

Question

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?

Answer 1

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