First-order and counting theories of \(\omega\)-automatic structures. (English) Zbl 1141.03015

Kuske, Dietrich; Lohrey, Markus

J. Symb. Log. 73, No. 1, 129-150 (2008).

Let \(\mathcal A\) be a relational structure of finite signature with universe \(A\). This structure is said to be \(\omega\)- automatic if there is a triple \((\Gamma, L,h)\) where \(\Gamma\) is a finite alphabet, \(L\subseteq \Gamma^{\omega}\), and \(h\) is a surjection from \(L\) to \(A\) with the property that the “inverse image” under \(h\) of each \(n\)-ary relation of \(\mathcal A\) is a regular \(\omega\)-language, i.e., accepted by some \(n\)-dimensional Büchi automaton. If in addition \(h\) is injective, \(\mathcal A\) is said to be injectively \(\omega\)-automatic.
The authors state as their objective the extension of results for first-order logic with the addition of “counting” quantifiers from automatic structures to \(\omega\)-automatic structures. Initially they consider first-order logic extended by modulo-counting quantifiers and extended by exact counting quantifiers for infinite cardinalities. They show that any injectively \(\omega\)-automatic structure has a decidable theory in these logics. The proof uses Muller automata.
The authors then go on to study more powerful logics. The logic \(\mathcal L(\mathcal Q_u)\) has quantifiers of the form \(\mathcal Q_{\mathcal C}y: (\psi_1(y),\dots, \psi_n (y))\), where \(y\) is a first-order variable and \(\mathcal C\) is an \(n\)-ary relation on cardinals. Such a formula is true in \(\mathcal A\) if the \(n\)-tuple of the cardinalities of the sets defined in \(\mathcal A\) by the \(\psi_i (y)\) are in the relation \(\mathcal C\).
Let \(\mathcal L\) be a fragment of \(\mathcal L(\mathcal Q_u)\) that contains only countably many generalized quantifiers, and let \(\mathcal A\) be an injectively \(\omega\)-automatic structure whose Gaifman-graph has bounded degree. The authors prove that the \(\mathcal L\)-theory of \(\mathcal A\) can be decided by a Turing machine with oracle access to the relations \(\mathcal C\) appearing in the quantifiers of \(\mathcal A\). The authors show that both of the assumptions on \(\mathcal A\) are necessary for this result.

Reviewer: J. M. Plotkin (East Lansing)

MSC:

03C80	Logic with extra quantifiers and operators
03B25	Decidability of theories and sets of sentences
03D05	Automata and formal grammars in connection with logical questions

Keywords:

\(\omega\)-automatic structures; generalized quantifiers; decidability

References:

[1]	DOI: 10.1007/978-3-540-39813-4_24
[2]	DOI: 10.1007/11690634_22
[3]	Proceedings of the IEEE Symposium on Logic in Computer Science (LICS) pp 168– (2003)
[4]	DOI: 10.1016/0168-0072(90)90080-L · Zbl 0705.03017
[5]	DOI: 10.1016/S0022-0000(74)80051-6 · Zbl 0292.02033
[6]	DOI: 10.1002/malq.19600060105 · Zbl 0103.24705
[7]	DOI: 10.1007/s00224-004-1133-y · Zbl 1061.03038
[8]	Proceedings of the IEEE Symposium on Logic in Computer Science (LICS) pp 51– (2000)
[9]	Automatic structures (1999)
[10]	Undecidable extensions of Biichi arithmetic and Cobham-Semenov theorem 62 pp 1280– (1997)
[11]	DOI: 10.1145/876638.876642 · Zbl 1325.03031
[12]	Handbook of Theoretical Computer Science pp 133– (1990)
[13]	Journal of Automata, Languages and Combinatorics 6 pp 467– (2001)
[14]	LCC: International Workshop on Logic and Computational Complexity 960 pp 367– (1994)
[15]	DOI: 10.1002/malq.200410013 · Zbl 1060.03060
[16]	Proceedings of the IEEE Symposium on Logic in Computer Science (LICS) pp 235– (2002)
[17]	DOI: 10.1016/0304-3975(82)90042-1 · Zbl 0493.03002
[18]	Model Theory (1993)
[19]	Colloquium on the Foundations of Mathematics, Mathematical Machines and their Applications (Tihany, 1962) pp 31– (1965)
[20]	Logic Colloquium ’81 pp 105– (1982)
[21]	Word Processing in Groups (1992)
[22]	DOI: 10.1016/j.ipl.2006.06.011 · Zbl 1185.68400
[23]	Proceedings of the ACM Symposium on Theory of Computing (STOC) pp 1– (1973)
[24]	Infinite Words 141 (2004) · Zbl 1089.68082
[25]	Computational Complexity (1994) · Zbl 0833.68049
[26]	Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2850 pp 344– (2003)
[27]	Algebraische Codierungstheorie (1977) · Zbl 0363.94016
[28]	Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS) 2996 pp 440– (2004)