Bûchin lause ja transitiivisen sulkeuman logiikat

Abstract

Büchin lauseen merkittävin tulos on, että äärellisellä automaatilla tunnistettavat säännölliset kielet ovat määriteltävissä monadisessa toisen kertaluvun logiikassa. Tässä tutkielmassa todistamme lisäksi, että monadisen toisen kertaluvun logiikan rinnalle Büchin lauseeseen voimme nostaa transitiivisen sulkeuman ja deterministisen transitiivisen sulkeuman logiikat.

Tutkielman päälähdeteoksena on käytetty Heinz-Dieter Ebbinghausin ja Jörg Flumin kirjaa Finite Model Theory. Pitkälti tämän kirjan pohjalta esittelemme ensin säännölliset kielet, äärelliset automaatit ja äärelliset mallit. Myös tutkielmassa käytetyt merkintätavat vastaavat pääosin kirjassa käytettyjä merkintöjä. Logiikoista esittelemme ensimmäisen ja toisen kertaluvun logiikat, monadinen toisen kertaluvun logiikan sekä transitiivisen sulkeuman ja deterministisen transitiivisen sulkeuman logiikat. Luomme myös yleissilmäyksen vaativuusteoriaan ja edellä mainittujen logiikkojen vaativuusluokkiin.

Büchin lauseen todistusta varten tutustumme ensimmäisen kertaluvun ja monadisen toisen kertaluvun logiikkojen Ehrenfeucht-Fraïsse peleihin. Näiden pelien avulla tarkastelemme logiikan kaavojen toteutumista äärellisissä malleissa ja edelleen äärellisten mallien keskinäistä samankaltaisuutta. Tutkielman viimeisessä luvussa esitämme Büchin lauseen laajennoksen, joka siis kokoaa säännölliset kielet, äärelliset automaatit, monadisen toisen kertaluvun logiikan sekä transitiivisen sulkeuman logiikat samaan lauseeseen.

Oletamme entuudestaan tunnetuiksi tavallisimmat joukko-opin ja logiikan merkinnät, rekursiivisen määrittelyn ja induktioperiaatteen. Tampereen Yliopiston kurssi Johdatus äärellisten mallien teoriaan tarjoaa hyvät pohjatiedot aihealueen ymmärtämiseen.