<p>Yes there is. In <a href="https://arxiv.org/abs/1405.1715" rel="nofollow noreferrer">https://arxiv.org/abs/1405.1715</a> the author introduced a Turing-complete logic which captures precisely the recursively enumerable languages.</p>
<p><strong>Edit:</strong> the same author considers in <a href="https://arxiv.org/abs/1408.4080" rel="nofollow noreferrer">https://arxiv.org/abs/1408.4080</a> a different, but closely related, Turing-complete logic. The basic idea is simple. First, we introduce a new operator <span class="math-container">$I$</span> which has the following semantics. Let <span class="math-container">$\varphi$</span> be a sentence (of same typical logic such as first-order logic or existential second-order logic), <span class="math-container">$Y$</span> a unary second-order variable and <span class="math-container">$\mathfrak{A}$</span> a <span class="math-container">$\tau$</span>-structure. We define that <span class="math-container">$\mathfrak{A} \models IY \varphi$</span> iff there exists a finite set <span class="math-container">$U$</span> such that the following two conditions hold.</p>
<ol>
<li><span class="math-container">$\mathrm{dom}(\mathfrak{A}) \cap U = \varnothing$</span>.</li>
<li>Let <span class="math-container">$\mathfrak{A}^+$</span> be the <span class="math-container">$(\tau \cup \{Y\})$</span>-structure which has <span class="math-container">$ \mathrm{dom}(\mathfrak{A}) \cup U$</span> as its domain, <span class="math-container">$Y^{\mathfrak{A}^+} := U$</span> and <span class="math-container">$R^{\mathfrak{A}^+} := R^{\mathfrak{A}}$</span> for every <span class="math-container">$R \in \tau$</span>. Now <span class="math-container">$\mathfrak{A}^+ \models \varphi$</span>.</li>
</ol>
<p>So basically <span class="math-container">$I$</span> just extends the domain of the underlying structure with a fresh finite set of elements. Now the logic consisting of sentences of the form <span class="math-container">$I\varphi$</span>, where <span class="math-container">$\varphi$</span> is a sentence of existential second-order logic, is Turing complete.</p>

CC BY-SA 4.0
2024-12-12T14:02:01.353Z
neat. i'd be interested to see Kuusisto's construction brought closer to BET (i.e., using a superset of MSO). i also wonder if the game-theoretic semantics are *necessary* for the jump to RE?
silly-little-guy
CC BY-SA 4.0
2024-12-12T14:34:53.787Z
@silly-little-guy I extended my post, hopefully answering your question.
Reijo Jaakkola
CC BY-SA 4.0
2024-12-12T09:54:51.890Z
2024-12-16T05:37:32.060Z
2024-12-16T05:37:32.060Z
Reijo Jaakkola
<p>There is a well known correspondence between automata and languages (e.g. <a href="https://en.wikipedia.org/wiki/Chomsky_hierarchy#The_hierarchy" rel="nofollow noreferrer">Chomsky heirarchy</a>).</p>
<p>The <a href="https://en.wikipedia.org/wiki/B%C3%BCchi-Elgot-Trakhtenbrot_theorem" rel="nofollow noreferrer">Büchi-Elgot-Trakhtenbrot (BET) theorem</a> characterizes regular languages as formalizable in <a href="https://en.wikipedia.org/wiki/Monadic_second-order_logic" rel="nofollow noreferrer">monadic second order (MSO) logic</a>. Presumably this also establishes a correspondence between MSO logic and finite automata, since they generate regular languages.</p>
<p>Is there a generalization of the BET theorem to recursively enumerable languages (hence presumably a correspondence between Turing machines and a particular type of logic)?</p>

<lo.logic><fl.formal-languages><automata-theory><turing-machines>
Generalization of Büchi-Elgot-Trakhtenbrot theorem
silly-little-guy
# Generalization of Büchi-Elgot-Trakhtenbrot theorem

(Asked by: username_0 on 2024-12-12)

There is a well known correspondence between automata and languages (e.g. [Chomsky heirarchy](https://en.wikipedia.org/wiki/Chomsky_hierarchy#The_hierarchy)).

The [Büchi-Elgot-Trakhtenbrot (BET) theorem](https://en.wikipedia.org/wiki/B%C3%BCchi-Elgot-Trakhtenbrot_theorem) characterizes regular languages as formalizable in [monadic second order (MSO) logic](https://en.wikipedia.org/wiki/Monadic_second-order_logic). Presumably this also establishes a correspondence between MSO logic and finite automata, since they generate regular languages.

Is there a generalization of the BET theorem to recursively enumerable languages (hence presumably a correspondence between Turing machines and a particular type of logic)?

**Tags:** lo.logic, fl.formal-languages, automata-theory, turing-machines


---

## 1 answers

### Answer by username_1 on 2024-12-12. Score: 5

Yes there is. In <https://arxiv.org/abs/1405.1715> the author introduced a Turing-complete logic which captures precisely the recursively enumerable languages.

**Edit:** the same author considers in <https://arxiv.org/abs/1408.4080> a different, but closely related, Turing-complete logic. The basic idea is simple. First, we introduce a new operator $I$ which has the following semantics. Let $\varphi$ be a sentence (of same typical logic such as first-order logic or existential second-order logic), $Y$ a unary second-order variable and $\mathfrak{A}$ a $\tau$-structure. We define that $\mathfrak{A} \models IY \varphi$ iff there exists a finite set $U$ such that the following two conditions hold.

1. $\mathrm{dom}(\mathfrak{A}) \cap U = \varnothing$.
2. Let $\mathfrak{A}^+$ be the $(\tau \cup \{Y\})$-structure which has $ \mathrm{dom}(\mathfrak{A}) \cup U$ as its domain, $Y^{\mathfrak{A}^+} := U$ and $R^{\mathfrak{A}^+} := R^{\mathfrak{A}}$ for every $R \in \tau$. Now $\mathfrak{A}^+ \models \varphi$.

So basically $I$ just extends the domain of the underlying structure with a fresh finite set of elements. Now the logic consisting of sentences of the form $I\varphi$, where $\varphi$ is a sentence of existential second-order logic, is Turing complete.

> **Comments:**
> **username_0**: neat. i'd be interested to see Kuusisto's construction brought closer to BET (i.e., using a superset of MSO). i also wonder if the game-theoretic semantics are *necessary* for the jump to RE?  
> **username_1**: @username_0 I extended my post, hopefully answering your question.  

---

