Browsing by Subject "modaalinen riippuvuuslogiikka"

Logiikan alalla eräs kiinnostava kysymys on minkälaisia malleja saadaan määriteltyä eri logiikoiden kaavoilla. Tätä kutsutaan logiikan ilmaisuvoimaksi. Modaalilogiikoille ilmaisuvoiman rajoja osoittavia lauseita kutsutaan van Benthemin lauseiksi. Modaalilogiikoiden ilmaisuvoimalle keskeinen piirre on bisimulaatioinvarianssi. Tässä tutkielmassa osoitetaan van Benthemin lause kahdelle logiikalle: modaalilogiikalle ja laajennetulle modaaliselle riippuvuuslogiikalle. Työssä esitellään myös modaalilogiikan ja riippuvuuslogiikan perusteita lyhyesti ennen kunkin logiikan van Benthem lauseen todistusta. Tässä tutkielmassa modaalilogiikan van Benthemin lause todistetaan peliteorian keinoin, mikä mahdollistaa todistuksen pelkästään äärellisiä malleja käyttäen, toisin kuin alkuperäinen malliteoreettinen todistus. Lause sanoo, että modaalilogiikka on ilmaisuvoimaltaan sama kuin ensimmäisen kertaluvun logiikan bisimulaatioinvariantti fragmentti. Kaikille logiikoille van Benthemin lauseen suora todistaminen ei onnistu yhtä vaivattomasti. Tällöin käytetään hyväksi välituloksia. Esimerkkinä tästä toimii laajennettu modaalinen riippuvuuslogiikka, jolle lause osoitetaan todistamalla se eri logiikalle, joka puolestaan todistetaan loogisesti ekvivalentiksi laajennetun modaalisen riippuvuuslogiikan kanssa. Tässä työssä van Benthem lause osoitetaan aluksi modaalilogiikalle, jota on laajennettu intuitionistisella disjunktiolla. Tämä logiikka todistetaan loogisesti ekvivalentiksi laajennetun modaalisen riipuvuuslogiikan kanssa. Näille logiikoille van Benthemin lause rajaa logiikan kykenevän määrittelemään alaspäin suljettuja, tyhjän tiimin ominaisuuden omaavia malleja jotka ovat bisimulaation suhteen invariantteja.