Tässä pro gradu-tutkielmassa tutkitaan modaalilogiikkaa todistus- ja malliteoreettisesta näkökulmasta. Työssä esitetään täydellisyystulokset modaalilogiikan systeemeille K, S4 ja S5 sekä bisimulaatiota ja äärellisiä malleja koskevia tuloksia.
Tutkielman alkupuolella esitellään modaalilogiikan perusteita, kuten syntaksi, semantiikka ja aksioomasysteemit K, S4 ja S5. Modaalilogiikan täydellisyyslauseet todistetaan tutkielman luvussa 3. Luku 4 esittelee modaalilogiikan malliteoriaa. Luvussa tutkitaan minkälaiset morfismit säilyttävät modaalisen totuuden sekä esitellään bisimulaation käsite. Lopuksi työssä tutustutaan äärellisenmallin ominaisuuteen ja miten se voidaan todistaa filtraation avulla.
Tutkielman pääasiallisina lähteinä on käytetty kirjoja Modal Logic (Blackburn, de Rijke, Venema) ja Johdatus modaalilogiikkaan (Rantala, Virtanen).
