Formuła Sahlqvista

W logice modalnej formuły Sahlqvista są pewnym rodzajem formuł modalnych o niezwykłych właściwościach. Twierdzenie o zgodności Sahlqvista stwierdza, że ​​każda formuła Sahlqvista jest kanoniczna i odpowiada definiowalnej klasie ramek Kripkego pierwszego rzędu .

Definicja Sahlqvista charakteryzuje rozstrzygalny zestaw formuł modalnych z odpowiednikami pierwszego rzędu. Ponieważ na podstawie twierdzenia Chagrovy nie można rozstrzygnąć, czy dowolna formuła modalna ma odpowiednika pierwszego rzędu, istnieją formuły z warunkami ramowymi pierwszego rzędu, które nie są Sahlqvistem [Chagrova 1991] (patrz przykłady poniżej). Stąd formuły Sahlqvista definiują tylko (rozstrzygalny) podzbiór formuł modalnych z odpowiednikami pierwszego rzędu.

Definicja

Formuły Sahlqvista są zbudowane z implikacji, gdzie następnik jest dodatni , a poprzednik ma ograniczoną formę.

• Atom w pudełku to atom zdaniowy poprzedzony liczbą (prawdopodobnie 0) pudełek, czyli formułą postaci ${\ Displaystyle \ Box \ cdots \ Box p}$ (często w skrócie ${\ displaystyle \ Pudełko ^ {i} p}$ dla ${\ Displaystyle 0 \ równoważnik i <\ omega}$ ).
• Poprzednik Sahlqvista to formuła skonstruowana przy użyciu atomów w $ramkach i wzorów$ (w tym stałych ⊥, ⊤).
• Implikacją Sahlqvista jest formuła A → B , gdzie A jest poprzednikiem Sahlqvista, a B jest formułą dodatnią.
• Formuła Sahlqvista jest skonstruowana z implikacji Sahlqvista przy użyciu ∧ i ${\ displaystyle \ Box}$ (nieograniczony) oraz przy użyciu ∨ we wzorach bez wspólnych zmiennych.

Przykłady formuł Sahlqvista

${\ Displaystyle p \ rightarrow \ Diamond p}$

Jego odpowiednia formuła pierwszego rzędu to ${\ Displaystyle \ forall x \; Rxx}$ i definiuje wszystkie klatki refleksyjne

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

Odpowiedni wzór pierwszego rzędu to ${\ Displaystyle \ forall x \ forall y [Rxy \ rightarrow Ryx]}$ i definiuje wszystkie symetryczne ramki

${\ Displaystyle \ Diament \ Diament p \ rightarrow \ Diament p}$ lub ${\ Displaystyle \ Box p \ rightarrow \ Box \ Box p}$

Odpowiedni wzór pierwszego rzędu to ${\ Displaystyle \ forall x \ forall y \ forall z [(Rxy \ land Ryz) \ rightarrow Rxz]}$ i definiuje wszystkie ramki przechodnie

${\ Displaystyle \ Diamond p \ rightarrow \ Diament \ Diament p}$ lub ${\ Displaystyle \ Box \ Box p \ rightarrow \ Box p}$

Odpowiedni wzór pierwszego rzędu to ${\ Displaystyle \ forall x \ forall y [Rxy \ rightarrow \ istnieje z (Rxz \ land Rzy)]}$ i definiuje wszystkie gęste ramki

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

Jego odpowiednia formuła pierwszego rzędu to ${\ Displaystyle \ forall x \ istnieje y \; Rxy}$ i definiuje wszystkie nieograniczone w prawo ramki (zwane także szeregowymi)

${\ Displaystyle \ Diament \ Box p \ rightarrow \ Box \ Diamond p}$

Odpowiedni wzór pierwszego rzędu to ${\ Displaystyle \ forall x \ forall x_ {1} \ forall z_ {0} [Rxx_ {1} \ ziemia Rxz_ {0} \ strzałka w prawo \ istnieje z_ {1} (Rx_ {1} z_ {1} \ ziemia Rz_ { 0}z_{1})]}$ i jest to właściwość Churcha-Rossera .

Przykłady formuł innych niż Sahlqvist

${\ Displaystyle \ pudełko \ diament p \ strzałka w prawo \ diament \ pudełko p}$

To jest formuła McKinseya ; nie ma warunku ramki pierwszego rzędu.

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

Aksjomat Löba nie jest Sahlqvistem; znowu nie ma warunku ramki pierwszego rzędu.

${\ Displaystyle (\ Box \ Diamond p \ rightarrow \ Diamond \ Box p) \ land (\ Diamond \ Diamond q \ rightarrow \ Diamond q)} Koniunkcja wzoru McKinseya$

i aksjomat (4) ma warunek ramowy pierwszego rzędu (koniunkcja własności przechodniości z właściwością ${\ Displaystyle \ forall x [\ forall y (Rxy \ rightarrow \ istnieje z [Ryz]) \ rightarrow \ istnieje y (Rxy \ klin \ forall z[Ryz\rightarrow z=y])]}$ ), ale nie jest równoważne z żadną formułą Sahlqvista.

Twierdzenie Krachta

Gdy formuła Sahlqvista jest używana jako aksjomat w normalnej logice modalnej, gwarantuje się, że logika jest kompletna w odniesieniu do elementarnej klasy ramek, które definiuje aksjomat. Wynik ten pochodzi z twierdzenia Sahlqvista o zupełności [Modal Logic, Blackburn et al. , Twierdzenie 4.42]. Ale istnieje również twierdzenie odwrotne, a mianowicie twierdzenie, które stwierdza, które warunki pierwszego rzędu są odpowiednikami formuł Sahlqvista. Twierdzenie Krachta o tym mówi każda formuła Sahlqvista lokalnie odpowiada formule Krachta; i odwrotnie, każda formuła Krachta jest lokalnym odpowiednikiem pierwszego rzędu jakiejś formuły Sahlqvista, którą można skutecznie uzyskać ze wzoru Krachta [Modal Logic, Blackburn i in. , Twierdzenie 3.59].

• LA Chagrova, 1991. Nierozstrzygalny problem w teorii korespondencji. Journal of Symbolic Logic 56: 1261–1272.
• Marcus Kracht, 1993. Jak połączyły się teoria kompletności i korespondencji. W de Rijke, redaktor, Diamonds and Defaults , strony 175–214. Kluwer.
• Henrik Sahlqvist, 1975. Zgodność i kompletność w semantyce pierwszego i drugiego rzędu dla logiki modalnej. W Proceedings of the Third Scandinavian Logic Symposium . Holandia Północna, Amsterdam.