Sahlqvistův vzorec - Sahlqvist formula

V modální logice jsou Sahlqvistovy vzorce určitým druhem modálních vzorců s pozoruhodnými vlastnostmi. Sahlqvist korespondence teorém říká, že každý Sahlqvist vzorec je kanonický , a odpovídá prvního řádu definovatelné třídy Kripkeho rámů .

Sahlqvistova definice charakterizuje rozhodnou sadu modálních vzorců s korespondenty prvního řádu. Protože podle Chagrovy věty je nerozhodné, zda má libovolný modální vzorec korespondenta prvního řádu, existují vzorce s rámcovými podmínkami prvního řádu, které nejsou Sahlqvist [Chagrova 1991] (viz příklady níže). Proto Sahlqvistovy vzorce definují pouze (rozhodnutelnou) podmnožinu modálních vzorců s korespondenty prvního řádu.

Definice

Sahlqvistické vzorce jsou sestaveny z implikací, kde důsledek je pozitivní a předchůdce má omezenou formu.

• Krabicová atom je atom výrokové předcházela řada (případně 0) krabic, tedy vzorec formě (často zkráceně k ).${\ displaystyle \ Box \ cdots \ Box p}$${\ displaystyle \ Box ^ {i} p}$${\ displaystyle 0 \ leq i <\ omega}$
• Sahlqvist prekurzor je vzorec konstruovány s použitím ∧, ∨, a z krabicových atomů, a negativních vzorcích (včetně konstant ⊥, ⊤).${\ displaystyle \ Diamond}$
• Sahlqvist implikace je vzorec → B , kde je Sahlqvist předchůdce, a B je pozitivní vzorec.
• Sahlqvist vzorec je vyroben z Sahlqvist důsledků použití ∧ a (neomezené), a za použití ∨ na vzorcích s žádné společné proměnných.${\ displaystyle \ Box}$

Příklady Sahlqvistových vzorců

${\ displaystyle p \ rightarrow \ Diamond p}$

Jeho odpovídající vzorec prvního řádu je a definuje všechny reflexivní rámce${\ displaystyle \ forall x \; Rxx}$

${\ displaystyle p \ rightarrow \ Box \ Diamond p}$

Jeho odpovídající vzorec prvního řádu je a definuje všechny symetrické rámce${\ displaystyle \ forall x \ forall y [Rxy \ rightarrow Ryx]}$

${\ displaystyle \ Diamond \ Diamond p \ rightarrow \ Diamond p}$ nebo ${\ displaystyle \ Box p \ rightarrow \ Box \ Box p}$

Jeho odpovídající vzorec prvního řádu je a definuje všechny tranzitivní rámce${\ displaystyle \ forall x \ forall y \ forall z [(Rxy \ land Ryz) \ rightarrow Rxz]}$

${\ displaystyle \ Diamond p \ rightarrow \ Diamond \ Diamond p}$ nebo ${\ displaystyle \ Box \ Box p \ rightarrow \ Box p}$

Jeho odpovídající vzorec prvního řádu je a definuje všechny husté rámce${\ displaystyle \ forall x \ forall y [Rxy \ rightarrow \ existuje z (Rxz \ land Rzy)]}$

${\ displaystyle \ Box p \ rightarrow \ Diamond p}$

Jeho odpovídající vzorec prvního řádu je a definuje všechny neohraničené snímky (nazývané také sériové)${\ displaystyle \ forall x \ existuje y \; Rxy}$

${\ displaystyle \ Diamond \ Box p \ rightarrow \ Box \ Diamond p}$

Jeho odpovídající vzorec prvního řádu je a je to vlastnost Church-Rosser .${\ displaystyle \ forall x \ forall x_ {1} \ forall z_ {0} [Rxx_ {1} \ land Rxz_ {0} \ rightarrow \ existuje z_ {1} (Rx_ {1} z_ {1} \ land Rz_ { 0} z_ {1})]}$

Příklady nesahlqvistických vzorců

${\ displaystyle \ Box \ Diamond p \ rightarrow \ Diamond \ Box p}$

Toto je McKinseyův vzorec ; nemá podmínku rámce prvního řádu.

${\ displaystyle \ Box (\ Box p \ rightarrow p) \ rightarrow \ Box p}$

Löb axiom není Sahlqvist; opět nemá podmínku rámce prvního řádu.

${\ displaystyle (\ Box \ Diamond p \ rightarrow \ Diamond \ Box p) \ land (\ Diamond \ Diamond q \ rightarrow \ Diamond q)}$

Spojení McKinseyova vzorce a (4) axiomu má podmínku rámce prvního řádu (spojení vlastnosti přechodnosti s vlastností ), ale není ekvivalentní žádnému Sahlqvistovu vzorci.${\ displaystyle \ forall x [\ forall y (Rxy \ rightarrow \ existuje z [Ryz]) \ rightarrow \ existuje y (Rxy \ wedge \ forall z [Ryz \ rightarrow z = y])]}$

Krachtova věta

Když je Sahlqvistův vzorec použit jako axiom v normální modální logice, je zaručeno, že logika bude úplná s ohledem na základní třídu rámců, které axiom definuje. Tento výsledek pochází z Sahlqvistovy věty o úplnosti [Modal Logic, Blackburn et al. , Věta 4.42]. Existuje však také věta o obrácení, konkrétně věta, která uvádí, které podmínky prvního řádu jsou korespondenty Sahlqvistických vzorců. Krachtova věta uvádí, že jakýkoli Sahlqvistův vzorec místně odpovídá Krachtově vzorci; a naopak, každá Krachtova formule je místním korespondentem prvního řádu nějakého Sahlqvistova vzorce, který lze účinně získat z Krachtova vzorce [Modal Logic, Blackburn et al. , Věta 3,59].

Reference

• LA Chagrova, 1991. Nerozhodnutelný problém v teorii korespondence. Journal of Symbolic Logic 56: 1261–1272.
• Marcus Kracht, 1993. Jak se vdala teorie úplnosti a korespondence. In de Rijke, editor, Diamonds and Defaults , strany 175–214. Kluwer.
• Henrik Sahlqvist, 1975. Korespondence a úplnost v sémantice prvního a druhého řádu pro modální logiku. In Proceedings of the Third Scandinavian Logic Symposium . Severní Holandsko, Amsterdam.