Kaavan pituuspeli modaalilogiikalle ja tiiviystuloksia

Abstract

Tämän tutkielman aiheena on kaavan pituuspeli modaalilogiikalle ja sen käyttäminen tiiviystulosten osoittamiseen. Aluksi määritellään modaalilogiikan syntaksi ja semantiikka sekä modaalilogiikkaan ja predikaattilogiikkaan liittyviä perusasioita. Lisäksi määritellään kaavan pituuden käsite molemmille logiikoille. Tämän jälkeen määritellään kaavan pituuspeli modaalilogiikalle. Pelissä on kaksi pelaajaa, I ja II. Osoitetaan, että pelaajalla I on peliin voittostrategia, jos ja vain jos annetut pistemalliluokat voidaan erottaa kaavalla, joka on korkeintaan annetun pituinen.

Kaavan pituuspelin sovelluksena osoitetaan ensin, että julkisen tiedon logiikka on eksponentiaalisesti tiiviimpi kuin modaalilogiikka. Annetaan siis parametrin n suhteen määritelty ominaisuus, joka voidaan ilmaista julkisen tiedon logiikassa luvun n suhteen lineaarisen mittaisella kaavalla, ja osoitetaan kaavan pituuspelin avulla, että saman ominaisuuden ilmaiseminen modaalilogiikassa vaatii kaavan, jonka pituus on vähintään 2 potenssiin n.

Lopuksi osoitetaan toisena kaavan pituuspelin sovelluksena, että predikaattilogiikka on epäelementaarisesti tiiviimpi kuin modaalilogiikka. Tässä määriteltävä pistemallien ominaisuus on predikaattilogiikassa ilmaistavissa kaavalla, jonka pituus on suuruusluokkaa 2 potenssiin n ja vastaavan modaalilogiikan kaavan pituuden osoitetaan olevan suurempi kuin eksponenttitorni, jonka korkeus on n-1. Sopivien malliluokkien konstruoinnissa käytetään joukko-opin kumulatiivista hierarkiaa ja pelin aikana säilyvä invariantti löydetään graafiteorian väritysluvun avulla.