On the Decidability of Monadic Theories of Arithmetic Predicates

1. Problemstellung

Das Paper untersucht die Entscheidbarkeit der monadischen zweiten Ordnung (MSO) für Strukturen der Form $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$, wobei $\mathbb{N}$ die natürlichen Zahlen, $<$ die übliche Ordnung und $P_1, \dots, P_d$ unäre Prädikate (Teilmengen von $\mathbb{N}$) sind.

Der Fokus liegt auf sogenannten „arithmetischen Prädikaten", die aus der Theorie der linearen Rekurrenzfolgen (LRS) stammen. Konkret werden folgende Typen betrachtet:

• Feste Basen-Potenzen: $k^\mathbb{N} = \{k^n : n \in \mathbb{N}\}$.
• Potenzen mit variablem Exponenten: $\mathbb{N}^k = \{n^k : n \in \mathbb{N}\}$.
• Folgen linearer Rekurrenzen: Wie die Fibonacci-Folge $\text{Fib} = \{0, 1, 2, 3, 5, 8, \dots\}$, insbesondere solche mit einer einzigen, nicht-repetierten dominanten charakteristischen Wurzel.

Die zentrale Frage ist: Unter welchen Bedingungen ist die MSO-Theorie einer solchen Struktur entscheidbar? Während die MSO-Theorie von $\langle \mathbb{N}; < \rangle$ allein (Satz von Büchi) entscheidbar ist, führt die Hinzunahme von Prädikaten oft zu Undecidabilität (z. B. bei Primzahlen). Das Paper adressiert die Lücke im Verständnis der Wechselwirkung zwischen mehreren solchen Prädikaten gleichzeitig.

2. Methodik

Die Autoren entwickeln einen hybriden Ansatz, der Techniken aus der Automatentheorie, der Zahlentheorie und der Dynamischen Systemtheorie kombiniert. Der allgemeine Ablauf zur Entscheidungsfindung ist wie folgt:

1. Reduktion auf Automatenaufnahme:
   Gemäß dem Satz von Büchi wird die MSO-Formel $\varphi$ in einen endlichen Automaten $A$ über unendlichen Wörtern übersetzt. Die MSO-Theorie der Struktur ist genau dann entscheidbar, wenn das Aufnahme-Problem (Acceptance Problem) für das charakteristische Wort $\alpha$ der Prädikate entscheidbar ist. Das charakteristische Wort $\alpha \in \{0,1\}^d$ kodiert, zu welchem Zeitpunkt $n$ welche Prädikate erfüllt sind.

2. Kompression zu „Order Words":
   Da die Analyse des vollen charakteristischen Wortes bei mehreren Prädikaten komplex ist, führen die Autoren das Konzept des Order Word ($\beta$) ein. Dieses Wort enthält nur die Reihenfolge, in der die Elemente der Prädikate auftreten, und ignoriert die Abstände (die Nullen im charakteristischen Wort).

   • Unter bestimmten Bedingungen (effektive Procyclicität und Sparsamkeit der Prädikate) zeigen die Autoren, dass das Aufnahme-Problem für $\alpha$ äquivalent zu dem für $\beta$ ist (Theorem 3.12).

3. Modellierung durch Dynamische Systeme:
   Das Order Word $\beta$ wird durch dynamische Systeme generiert:

   • Für LRS mit einer dominanten Wurzel: Die Dynamik entspricht Translationen auf einem $d$-dimensionalen Torus $\mathbb{T}^d$ (additive Gruppe modulo 1). Dies führt zu Schneidsequenzen (Cutting Sequences) oder Billard-Wörtern.
   • Für gemischte Potenzen ($q^{n^d}$ und $p b^n$): Die Dynamik wird durch die Abbildung $x \mapsto \{b \cdot x\}$ (Bruchteil von $b \cdot x$) beschrieben, was zur Basis-$b$-Expansion von Zahlen führt.

4. Entscheidbarkeit durch Eigenschaften der Dynamik:
   Die Autoren nutzen Eigenschaften wie uniforme Rekurrenz und die Faktorkomplexität der erzeugten Wörter. Wenn das dynamische System gut verstanden ist (z. B. durch Kroneckers Theorem oder Schanuels Vermutung), kann entschieden werden, ob ein endliches Muster im unendlichen Wort vorkommt, was die MSO-Entscheidbarkeit impliziert.

3. Wichtige Beiträge und Ergebnisse

Das Paper liefert sowohl bedingte als auch unbedingte Entscheidbarkeitsresultate.

A. Lineare Rekurrenzfolgen mit einer dominanten Wurzel

Für Prädikate $P_i = \{a_i \rho_i^n : n \in \mathbb{N}\}$ (geometrische Folgen) oder allgemeinere LRS mit einer dominanten Wurzel $\rho_i$:

• Unbedingte Resultate (Theorem 4.4):
  Die MSO-Theorie ist entscheidbar, wenn die Zahlen $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ linear unabhängig über $\mathbb{Q}$ sind.

  • Beispiel: Die Theorie von $\langle \mathbb{N}; <, 2^\mathbb{N}, 3^\mathbb{N} \rangle$ ist entscheidbar, da $1/\log(2)$ und $1/\log(3)$ linear unabhängig sind.
  • Beispiel: Die Theorie von $\langle \mathbb{N}; <, 2^\mathbb{N}, \text{Fib} \rangle$ ist entscheidbar.

• Bedingte Resultate unter Schanuels Vermutung (Theorem 4.5, 4.6):
  Falls die lineare Unabhängigkeitsbedingung nicht gegeben ist (z. B. bei $2^\mathbb{N}, 3^\mathbb{N}, 6^\mathbb{N}$, da $\log(6) = \log(2) + \log(3)$), wird die Vermutung von Schanuel herangezogen.

  • Unter Annahme von Schanuels Vermutung ist die MSO-Theorie für beliebige solche Prädikate entscheidbar.
  • Wichtig: Die Vermutung wird nur für die Terminierung des Algorithmus benötigt; die Korrektheit der Ausgabe ist bedingungslos garantiert.

• Nicht-uniforme Entscheidbarkeit (Theorem 4.9):
  Für eine feste Menge von Prädikaten (z. B. festes $2^\mathbb{N}, 3^\mathbb{N}, 5^\mathbb{N}$) existiert ein Algorithmus, der die MSO-Theorie entscheidet. Dieser Algorithmus ist jedoch nicht-uniform, da er das Ideal aller polynomialen Relationen zwischen den Logarithmen der Parameter „hartcodiert" enthält.

B. Gemischte Prädikate: Potenzen und Basis-Expansionen

Für Strukturen der Form $\langle \mathbb{N}; <, \{q^{n^d}\}, \{p b^n\} \rangle$:

• Turing-Äquivalenz zu Basis-Expansionen (Theorem 5.1):
  Die MSO-Theorie dieser Strukturen ist Turing-äquivalent zur MSO-Theorie der Basis-$b$-Expansionen bestimmter algebraischer Zahlen (insbesondere $\eta = \sqrt[d]{p/q}$ und seiner Potenzen).

  • Beispiel: Die MSO-Theorie von $\langle \mathbb{N}; <, \mathbb{N}^2, 2^\mathbb{N} \rangle$ ist Turing-äquivalent zur Theorie der binären Expansion von $\sqrt{2}-1$.
  • Konsequenz: Wenn die binäre Expansion von $\sqrt{2}-1$ disjunktiv ist (jede endliche Ziffernfolge kommt unendlich oft vor), was allgemein vermutet wird (da $\sqrt{2}$ als normal angenommen wird), dann ist die MSO-Theorie entscheidbar.

• Spezialfälle:

  • Die Theorie von $\langle \mathbb{N}; <, \mathbb{N}^4, 2^\mathbb{N} \rangle$ ist unbedingbar entscheidbar (da hier die Expansionen periodisch sind).
  • Die Theorie von $\langle \mathbb{N}; <, 2^\mathbb{N}, 3^\mathbb{N}, 5^\mathbb{N} \rangle$ ist unter Schanuels Vermutung entscheidbar.

4. Signifikanz und Bedeutung

• Überwindung der „Einzel-Prädikat"-Grenze: Bisherige Arbeiten konzentrierten sich oft auf einzelne Prädikate. Dieses Paper löst das Problem der Interaktion mehrerer arithmetischer Prädikate, was zu komplexen Mustern führt, die mit reinen Automatentechniken nicht behandelbar waren.
• Verknüpfung von Disziplinen: Es demonstriert eine tiefe Verbindung zwischen logischer Entscheidbarkeit, der Theorie dynamischer Systeme (Torus-Translationen, Billard-Wörter) und transzendenter Zahlentheorie (Bakers Theorem, Schanuels Vermutung).
• Grenzen der aktuellen Mathematik: Die Ergebnisse zeigen, dass die vollständige Entscheidbarkeit für bestimmte Fälle (wie $2^\mathbb{N}, 3^\mathbb{N}, 5^\mathbb{N}$) an offenen Problemen der Zahlentheorie hängt. Ein Beweis der Entscheidbarkeit ohne Annahmen würde tiefgreifende neue Erkenntnisse über die algebraische Unabhängigkeit von Logarithmen erfordern.
• Praktische Implikationen: Die Arbeit liefert Algorithmen (oft bedingt), die es ermöglichen, komplexe Eigenschaften von Folgen wie Fibonacci oder Potenzen in logischen Formeln zu verifizieren, was für die formale Verifikation von Systemen relevant sein könnte, die solche Sequenzen modellieren.

Zusammenfassend stellt das Paper einen Meilenstein in der Untersuchung der MSO-Theorien arithmetischer Strukturen dar, indem es zeigt, dass die Kombination aus dynamischen Systemen und moderner Zahlentheorie neue Wege zur Entscheidungsfindung eröffnet, auch wenn einige Resultate noch auf tiefen Vermutungen wie der von Schanuel beruhen.