<p><strong>First question:</strong> 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$.</p>

<p>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.</p>

<p><strong>Second question:</strong> 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</p>

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

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

<p>Hence,</p>

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

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

CC BY-SA 3.0
2014-03-05T15:34:18.120Z
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
CC BY-SA 3.0
2014-03-05T15:45:50.620Z
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
CC BY-SA 3.0
2014-03-05T15:49:07.233Z
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
CC BY-SA 3.0
2014-03-05T15:54:26.057Z
Or FO[log n], see [Immerman's page](http://people.cs.umass.edu/~immerman/descriptive_complexity.html).
Kaveh
CC BY-SA 3.0
2014-03-05T16:04:00.853Z
@Kaveh: now that pointer would make a great answer :)
Sylvain
CC BY-SA 3.0
2014-03-05T15:20:06.017Z
2014-03-05T15:20:06.017Z
Joachim
<p>Gurevich provides an exact definition of what <em>Logic capturing PTIME</em> is.</p>

<p>An abstract logic $L$ consists of</p>

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

<p>An abstract logic $L$ captures polynomial time on $\mathcal{C}$ if</p>

<ul>
<li>for every $\tau$, $L[\tau]$ is decidable,</li>
<li>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}$,</li>
<li>for every vocabulary $\tau$, we can compute an algorithm which decides $\mathcal{P}_\varphi$ for every $\varphi \in L[\tau]$.</li>
</ul>

<blockquote>
  <p>Infinitary logic $\mathcal{L}_{\infty \omega}$ is an extension of
  First-Order Logic s.t. if $X$ is set then  both</p>
  
  <p>$$ \bigvee_{\phi \in X} \phi \textrm{ and } \bigwedge_{\phi \in X} \phi$$</p>
  
  <p>are formulars. $\mathcal{L}^k_{\infty \omega}$ is infinitary logic
  with only $k$ distinct variables.</p>
</blockquote>

<p>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.</p>

<p><strong>First Question:</strong> 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$?</p>

<p><em>Problem:</em> 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$. <em>Approach:</em> 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])| &gt; |\{0,1\}^*|$. Hence, there can be no bijective mapping from $\mathcal{P}(\mathsf{FO}[\tau])$ to $\{0,1\}^*$ (or any code with finite alphabet).</p>

<p><strong>Second Question:</strong> 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.</p>

<p>Any ideas? Any references?</p>

CC BY-SA 3.0
2014-03-03T19:38:48.540Z
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
CC BY-SA 3.0
2014-03-03T22:47:26.883Z
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
CC BY-SA 3.0
2014-03-03T23:12:15.287Z
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
CC BY-SA 3.0
2014-03-04T16:45:27.293Z
@Kaveh: maybe you should turn that into an answer.
cody
CC BY-SA 3.0
2014-03-05T15:56:53.223Z
@Sylvain was first to answer, I just expanded his comment a bit.
Kaveh
<lo.logic><descriptive-complexity><model-checking><finite-model-theory>
Is infinitary logic a logic in the sense of Gurevich?
Joachim
# Is infinitary logic a logic in the sense of Gurevich?

(Asked by: username_0 on 2014-03-03)

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?

**Tags:** lo.logic, descriptive-complexity, model-checking, finite-model-theory
> **Comments:**
> **username_1**: 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$.  
> **username_0**: 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 ...  
> **username_2**: 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).  
> **username_3**: @Kaveh: maybe you should turn that into an answer.  
> **username_2**: @Sylvain was first to answer, I just expanded his comment a bit.  

---

## 1 answers

### Answer by username_0 on 2014-03-05. Score: 2 | Accepted answer

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

> **Comments:**
> **username_1**: 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$.  
> **username_1**: 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$.  
> **username_2**: 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.  
> **username_2**: Or FO[log n], see [Immerman's page](http://people.cs.umass.edu/~immerman/descriptive_complexity.html).  
> **username_1**: @Kaveh: now that pointer would make a great answer :)  

---

