Määriteltävyys modaalilogiikoissa

Abstract

Hakutermit: logiikka, modaalilogiikka, määriteltävyys, Goldblatt-Thomasonin lause

Tässä työssä tarkastellaan kehystason määriteltävyyttä erilaisissa modaalilogiikoissa. Lähtökohtana on Goldblatt-Thomasonin lause, jonka mukaan elementaarinen kehysluokka on modaalisesti määriteltävissä täsmälleen silloin, kun se on suljettu generoitujen alimallien, erillisten yhdisteiden ja p-morfisten kuvien suhteen sekä heijastaa ultrafiltterilaajennuksia.

Elementaariset kehysluokat ovat kompakteja tavallisen modaalilogiikan suhteen, minkä johdosta ensimmäisessä Goldblatt-Thomasonin lauseen analogiassa on siirrytty tarkastelemaan kompaktisuutta. Sen mukaan generoitujen alimallien, erillisten yhdisteiden ja p-morfisten kuvien suhteen suljettu L-kompakti kehysluokka on L-määriteltävissä kehysluokan C suhteen, kun oletetaan, että luokan C jokaista kehystä F ja sen pistettä w kohti on olemassa logiikan L sellainen kaavajoukko ∆, että ∆ toteutuu pisteessä w ja jos se toteutuu kehyksen G jossain pisteessä v, niin Fw on kehyksen Gv p-morfinen kuva.

Esimerkiksi äärellisesti haaratuvien kehysten luokka toteuttaa tämän ehdon, mistä seuraa, että ML[Φ, τ0]-kompakti kehysluokka K on määriteltävissä suhteessa äärellisesti haarautuvien kehysten luokkaan, kun K on suljettu mainittujen sulkeumaehtojen suhteen. Jos edellä voidaan olettaa, että p-morfisena kuvana olemisen välittämiseen riittää yksittäinen L-kaava, voidaan kompaktisuusoletuksesta luopua. Tällainen kaava löytyy modaalisessa μ-kalkyylissä, kun rajoitutaan äärellisten kehysten luokkaan. Äärellisyysrajoituksesta päästään eroon siirtymällä äärettömät disjunktiot ja konjunktiot sallivaan modaalilogiikkaan tai muuhun modaalilogiikkaan, jossa polkukvanttori on määriteltävissä ja propositiosymboleita on käytössä riittävän paljon erottelemaan tarkasteltavien kehysten kaikki pisteet toisistaan. Esimerkiksi äärettömien kielten avulla polkukvanttori A voidaan määritellä kaavalla ∧{[¯]nϕ | n ∈ N}. Tällöin tarkasteltavien kehysten kokoa täytyy kuitenkin rajoittaa tai vaihtoehtoisesti sallia, että propositiosymboleja on käytössä aito luokka.

Lopuksi tarkastellaan vielä laskentaoperaattoreita käyttävää GML-määriteltävyyttä, määritellään g-saturoituvat mallit ja osoitetaan, että GML-kompakti kehysluokka on GML-määriteltävissä äärellisesti haarautuvien kehysten luokassa täsmälleen silloin, kun se on suljettu g-morfisten kuvien, generoitujen alikehysten ja erillisten yhdisteiden suhteen. Myös laskentaoperaattoreita käyttävää modaalilogiikkaa laajennetaan polkukvanttorin avulla ja esitetään perinteiselle modaalilogiikalle analogiset tulokset μGML-määriteltävyydestä ja GML∞, ω-määriteltävyydestä.

----------------------------------------------------------------------------------------- This work is about definability on the level of frames in various modal logics. The starting point is the Goldblatt-Thomason Theorem, which states that an elementary class of frames is modally definable if and only if it is closed under generated submodels, disjoint unions and bounded morphic images and reflects ultrafilter extensions. Elementary frameclasses are ML[Φ, τ0]-compact.

Here we prove that an L-compact frameclass which is closed under generated submodels, disjoint unions and bounded morphic images, is L-definable with respect to a frameclass C, if we can assume that for each frame F ∈ C and its point w there exists a set of formulas ∆ such that ∆ is satisfied in a point w and if it is satisfied in a point v of a frame G, then Fw is a bounded morphic image of Gv.

For example the class of image finite frames fulfills this condition and therefore ML[Φ, τ0]-compact frameclass is definable with respect to the class of image finite frames, if the mentioned closure conditions are fulfilled.

If we can assume that being a bounded morphic image can be transferred by a single L-formula instead of a set of formulas, we can leave out the compactness condition. Such a formula can be written in modal μ-calculus, when we restrict ourselves to the class of finite frames. We get rid of finiteness by allowing infinite disjunctions and conjunctions and sufficiently large amount of proposition symbols (possibly a proper class) to separate each point of a frame to be considered. Then we do not need fixed points to define the path quantifier A, formula ∧{[¯]nϕ | n ∈ N} will do.

Thereby we get that, a class of frames ML∞,ω[Φ]-definable with respect to a frameclass in which the size of every frame is at most κ if it is closed under generated submodels, disjoint unions and bounded morphic images and the size of Φ is at least κ. In the last section we concider definability in graded modal logics.

We define the notion of g-saturated models and g-morphic images and prove that GML-compact frameclass is GML-definable with respect to the class of image finite frames if and only if it is closed under g-morphic images, generated subframes and disjoint unions. Then we add the path quantifier also to graded modal logics and prove that a class of frames K is definable with respect to the class of finite frames by simple μGML[Φ]-formulas, if K is closed under generated submodels, disjoint unions and bounded morphic images and the size of Φ is at least ω. Futhermore we show that a class of frames is definable with respect to a class of frames in which the size of every frame is at most κ by GML∞,ω[Φ]-formulas, if it is closed under the mentioned closure conditions and the size of Φ is at least κ.