Die Unentscheidbarkeit der Existenz von Interpolanten für die Zwei-Variable-Logik Erster Ordnung mit zwei Äquivalenzrelationen

Core Concepts

Die Existenz von Interpolanten ist unentscheidbar für die Zwei-Variable-Logik Erster Ordnung mit zwei Äquivalenzrelationen.

Abstract

Der Artikel untersucht das Interpolantenexistenzproblem (IEP) für Fragmente der Logik Erster Ordnung, insbesondere für die Zwei-Variable-Logik Erster Ordnung mit zwei Äquivalenzrelationen (FO22E) und den gegürteten Zwei-Variable-Fragment mit Konstanten und zwei Äquivalenzrelationen (GF22Ec). Die Hauptergebnisse sind: Das IEP ist unentscheidbar für FO22E und GF22Ec. Dies widerlegt die Vermutung, dass das IEP für jede entscheidbare Logik L entscheidbar ist, wenn die Erfüllbarkeit in L entscheidbar ist. Als Konsequenz ist auch das Problem der expliziten Definierbarkeit (EDEP) für diese Logiken unentscheidbar. Für die Beschreibungslogik 𝒜ℒ𝒞∩,¬,id2E, die dem FO22E-Fragment entspricht, sind ebenfalls das IEP und EDEP unentscheidbar. Der Beweis erfolgt durch eine Reduktion des unentscheidbaren unendlichen Post-Korrespondenzproblems auf das IEP für FO22E. Dieser Beweis kann dann auf GF22Ec und geeignete Beschreibungslogiken übertragen werden.

Stats

Es gibt keine relevanten Statistiken oder Zahlen im Artikel.

Quotes

Es gibt keine hervorstechenden Zitate im Artikel.

Key Insights Distilled From

Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations

by Frank Wolter... at arxiv.org 04-04-2024

https://arxiv.org/pdf/2404.02683.pdf

Deeper Inquiries

Ist das IEP für FO21E, also FO2 mit einer Äquivalenzrelation, entscheidbar?

Für FO21E, das heißt First-Order-Logik mit einer Äquivalenzrelation, ist das IEP entscheidbar. Im Gegensatz zu FO22E ist die Entscheidbarkeit und die Komplexität von FO21E deutlich weniger kompliziert. Es stellt sich die Frage, ob die Entscheidbarkeit auch dann erhalten bleibt, wenn FO2 um eine einzelne transitive (anstatt Äquivalenz-)Relation erweitert wird. Diese Erweiterung könnte potenziell zu einer anderen Komplexität führen, die gesondert untersucht werden müsste.

Ist das FO22E-IEP immer noch unentscheidbar, wenn man Gleichheit aus FO2 weglässt?

Es ist eine interessante Frage, ob das FO22E-IEP auch dann unentscheidbar bleibt, wenn die Gleichheit aus FO2 entfernt wird. Es ist bekannt, dass für FO2 ohne Äquivalenzrelationen und ohne Gleichheit das IEP entscheidbar ist. Die Entscheidbarkeit und die bekannten Komplexitätsgrenzen sind in diesem Fall dieselben wie bei der Version mit Gleichheit. Eine genaue Untersuchung wäre erforderlich, um festzustellen, ob das Entfernen der Gleichheit die Unentscheidbarkeit des FO22E-IEP beeinflusst.

Ist das IEP für 𝒜ℒ𝒞𝒬ℐ𝒪 oder den Zählerfragment C2 entscheidbar?

Für 𝒜ℒ𝒞𝒬ℐ𝒪, das eine Erweiterung der grundlegenden Beschreibungssprache 𝒜ℒ𝒞 um die Operatoren ∩ und ¬ auf Rollen sowie die Identitätsrolle id ist, ist das IEP unentscheidbar. Ebenso ist das IEP für das Zählerfragment C2, das FO2 mit Zählung, unentscheidbar. Diese Ergebnisse zeigen, dass die Interpolantenexistenz in diesen komplexeren Beschreibungssprachen nicht entscheidbar ist. Die Unentscheidbarkeit des IEP in diesen Kontexten wirft interessante Fragen zur Komplexität und zur Anwendbarkeit von Interpolanten in komplexen logischen Systemen auf.