Craig-Interpolation

In der mathematischen Logik ist Craigs Interpolationssatz ein Ergebnis über die Beziehung zwischen verschiedenen logischen Theorien . Vereinfacht ausgedrückt besagt er: Wenn eine Formel φ eine Formel ψ impliziert und beide mindestens ein atomares Variablensymbol gemeinsam haben, dann existiert eine Formel ρ, die sogenannte Interpolante, sodass jedes nichtlogische Symbol in ρ sowohl in φ als auch in ψ vorkommt, φ ρ impliziert und ρ ψ impliziert. Der Satz wurde 1957 von William Craig erstmals für die Prädikatenlogik erster Stufe bewiesen. Varianten des Satzes gelten auch für andere Logiken, wie beispielsweise die Aussagenlogik . Eine stärkere Form von Craigs Interpolationssatz für die Prädikatenlogik erster Stufe wurde 1959 von Roger Lyndon bewiesen; ^[¹^]^[²^] das Gesamtergebnis wird mitunter als Satz von Craig-Lyndon bezeichnet .

Beispiel

In der Aussagenlogik sei

\varphi =\lnot (P\land Q)\to (\lnot R\land Q)

\psi =(S\to P)\lor (S\to \lnot R)

Die

Dann folgt daraus tautologisch . Dies lässt sich überprüfen, indem man es in konjunktiver Normalform schreibt : $\varphi$ $\psi$ $\varphi$

\varphi \equiv (P\lor \lnot R)\land Q

Die

Wenn also gilt, dann gilt auch . $\varphi$ $P\lor \lnot R$

\rho =(P\lor \lnot R)

Die

Dies impliziert wiederum tautologisch . Da die beiden in vorkommenden Aussagenvariablen sowohl in als auch vorkommen , bedeutet dies, dass eine Interpolation für die Implikation ist . $P\lor \lnot R$ $\psi$ $P\lor \lnot R$ $\varphi$ $\psi$ $P\lor \lnot R$ $\varphi \to \psi$

Lyndons Interpolationssatz

Seien S und T zwei Theorien erster Stufe. Zur Notation bezeichne S ∪ T die kleinste Theorie, die sowohl S als auch T enthält ; die Signatur von S ∪ T ist die kleinste, die die Signaturen von S und T enthält . Weiterhin sei S ∩ T der Schnitt der Sprachen der beiden Theorien; die Signatur von S ∩ T ist der Schnitt der Signaturen der beiden Sprachen.

Lyndons Theorem besagt, dass, wenn S ∪ T unerfüllbar ist, es einen interpolierenden Satz ρ in der Sprache von S ∩ T gibt, der in allen Modellen von S wahr und in allen Modellen von T falsch ist . Darüber hinaus besitzt ρ die stärkere Eigenschaft, dass jedes Relationssymbol, das in ρ positiv vorkommt, auch in mindestens einer Formel von S positiv und in mindestens einer Formel von T negativ vorkommt , und dass jedes Relationssymbol, das in ρ negativ vorkommt, auch in mindestens einer Formel von S negativ und in mindestens einer Formel von T positiv vorkommt .

Beweis des Interpolationssatzes von Craig

Wir präsentieren hier einen konstruktiven Beweis des Craig-Interpolationssatzes für die Aussagenlogik . ^{[ 3 ]}

Satz – Wenn ⊨φ → ψ, dann existiert ein ρ (die Interpolante ), sodass ⊨φ → ρ und ⊨ρ → ψ, wobei atoms (ρ) ⊆ atoms (φ) ∩ atoms (ψ). Hierbei ist atoms (φ) die Menge der in φ vorkommenden Aussagenvariablen , und ⊨ ist die semantische Folgerungsrelation der Aussagenlogik.

Nachweisen

Es gelte ⊨φ → ψ. Der Beweis erfolgt durch Induktion über die Anzahl der in φ vorkommenden Aussagenvariablen, die nicht in ψ vorkommen, bezeichnet mit | Atome (φ) − Atome (ψ)|.

Basisfall | Atome (φ) − Atome (ψ)| = 0: Da | Atome (φ) − Atome (ψ)| = 0, gilt Atome (φ) ⊆ Atome (φ) ∩ Atome (ψ). Weiterhin gilt ⊨φ → φ und ⊨φ → ψ. Dies genügt, um zu zeigen, dass φ in diesem Fall ein geeigneter Interpolant ist.

Nehmen wir für den Induktionsschritt an, dass das Ergebnis für alle χ mit | atome (χ) − Atome (ψ)| = n bewiesen wurde . Nun nehmen wir an, dass | atome (φ) − Atome (ψ)| = n + 1. Wir wählen ein q ∈ Atome (φ), aber q ∉ Atome (ψ). Nun definieren wir:

φ′ := φ[⊤/ q ] ∨ φ[⊥/ q ]

Hierbei ist φ[⊤/ q ] dasselbe wie φ, wobei jedes Vorkommen von q durch ⊤ ersetzt wird, und φ[⊥/ q ] ersetzt analog q durch ⊥. Aus dieser Definition lassen sich zwei Dinge ableiten:

| Atome (φ') − Atome (ψ) | = n

1

⊨ φ ↔ φ′

2

Aus ⊨ φ′ → φ folgt auch ⊨ φ′ → ψ. Daher können wir die Induktionsvoraussetzung mit χ := φ′ anwenden, um eine Interpolationsfunktion φ′′ für φ′ und ψ zu erhalten. Da ⊨ φ → φ′ gilt, schließen wir, dass φ′′ ebenfalls eine geeignete Interpolationsfunktion für φ und ψ ist.

Da der obige Beweis konstruktiv ist , lässt sich ein Algorithmus zur Berechnung von Interpolanten ableiten. Mit diesem Algorithmus erhält man, dass, falls n = | atome (φ') − atomaren (ψ)|, der Interpolant ρ O (exp( n )) mehr logische Verknüpfungen besitzt als φ (siehe Big-O-Notation für Details zu dieser Aussage). Ähnliche konstruktive Beweise lassen sich für die grundlegende Modallogik K, die intuitionistische Logik und den μ-Kalkül mit vergleichbaren Komplexitätsmaßen liefern.

Die Craig-Interpolation lässt sich auch mit anderen Methoden beweisen. Diese Beweise sind jedoch im Allgemeinen nicht konstruktiv .

Modelltheoretisch , mittels Robinsons gemeinsamem Konsistenzsatz : Bei Vorhandensein von Kompaktheit , Negation und Konjunktion sind Robinsons gemeinsamer Konsistenzsatz und Craig-Interpolation äquivalent.
Beweistheoretisch mittels Sequenzenkalkül . Wenn Schnitteliminierung möglich ist und folglich die Subformula-Eigenschaft gilt, dann ist die Craig-Interpolation durch Induktion über die Derivationen beweisbar.
algebraisch , unter Verwendung von Amalgamationssätzen für die Varietät der Algebren, die die Logik repräsentieren.
durch Übersetzung in andere Logiken, die Craig-Interpolation nutzen.

Anwendungen

Die Craig-Interpolation hat viele Anwendungsgebiete, darunter Konsistenzbeweise , Modellprüfung , ^{[ 4 ]} Beweise in modularen Spezifikationen und modularen Ontologien .

Referenzen

^ Lyndon, Roger (1959), „Ein Interpolationssatz im Prädikatenkalkül“, Pacific Journal of Mathematics , 9 : 129–142 , doi : 10.2140/pjm.1959.9.129Die
^ Troelstra, Anne Sjerp ; Schwichtenberg, Helmut (2000), Basic Proof Theory , Cambridge Tracts in Theoretical Computer Science, Bd. 43 (2. Aufl.), Cambridge University Press, S. 141, ISBN 978-0-521-77911-1Die
^ Harrison, S. 426–427
^ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). „Boolesche Erfüllbarkeitslöser und ihre Anwendungen im Modellprüfen“. Proceedings of the IEEE . 103 (11): 2021–2035 . doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .

Weiterführende Literatur

John Harrison (2009). Handbuch der praktischen Logik und des automatisierten Schließens . Cambridge, New York: Cambridge University Press . ISBN 978-0-521-89957-4Die
Hinman, P. (2005). Grundlagen der mathematischen Logik . AK Peters. ISBN 1-56881-262-0Die
Dov M. Gabbay ; Larisa Maksimova (2006). Interpolation und Definierbarkeit: Modale und intuitionistische Logiken (Oxford Logic Guides) . Oxford Science Publications, Clarendon Press . ISBN 978-0-19-851174-8Die
Eva Hoogland, Definierbarkeit und Interpolation. Modelltheoretische Untersuchungen . Dissertation, Amsterdam 2001.
W. Craig, Drei Anwendungen des Herbrand-Gentzen-Theorems zur Verknüpfung von Modelltheorie und Beweistheorie , The Journal of Symbolic Logic 22 (1957), Nr. 3, 269–285.

[1] Lyndon, Roger (1959), „Ein Interpolationssatz im Prädikatenkalkül“, Pacific Journal of Mathematics , 9 : 129–142 , doi : 10.2140/pjm.1959.9.129Die

[2] Troelstra, Anne Sjerp ; Schwichtenberg, Helmut (2000), Basic Proof Theory , Cambridge Tracts in Theoretical Computer Science, Bd. 43 (2. Aufl.), Cambridge University Press, S. 141, ISBN 978-0-521-77911-1Die

[3] Harrison, S. 426–427

[4] Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). „Boolesche Erfüllbarkeitslöser und ihre Anwendungen im Modellprüfen“. Proceedings of the IEEE . 103 (11): 2021–2035 . doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .

[

[

[ 3 ]

[ 4 ]