Ehrenfeucht-Fraïssé-pelistä
SULONEN, HANNA (2012)
2012
Matematiikka - Mathematics
Informaatiotieteiden yksikkö - School of Information Sciences
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Hyväksymispäivämäärä
2012-05-30
Julkaisun pysyvä osoite on
https://urn.fi/urn:nbn:fi:uta-1-22554
https://urn.fi/urn:nbn:fi:uta-1-22554
Tiivistelmä
Tässä työssä käsitellään Andrzej Ehrenfeuchtin 1960-luvulla kehittämää Ehrenfeucht-Fraïssé-peliä, jonka pääsovellus on ensimmäisen kertaluvun logiikan määrittelemättömyystulosten todistaminen. Ehrenfeucht-Fraïssé-pelistä käytetään tässä työssä lyhennystä EF-peli. Äärettömien mallien tapauksessa löytyy määrittelemättömyystulosten todistamiseen monia EF-pelejä tehokkaampia työkaluja, mutta äärellisten mallien tapauksessa EF-pelit ovat sovellettavuudeltaan erinomaisia. EF-pelejä käytetään paljon äärellisten mallien teoriassa ja sen sovelluksissa tietojenkäsittelytieteessä, koska malliteoriassa ei ole EF-pelien lisäksi monia muita äärellisten mallien tapauksessa päteviä menetelmiä.
Tämän työn aluksi tarkastellaan ensimmäisen kertaluvun logiikan eli predikaattilogiikan peruskäsitteistöä. Ensimmäisen kertaluvun logiikasta käytetään tässä työssä merkintää FO. Työn alussa määritellään muun muassa aakkosto ja malli sekä käsitellään homomorfisuutta mallien välillä. Seuraavaksi tässä työssä tarkastellaan logiikan FO syntaksia ja semantiikkaa. Logiikan FO termit ja kaavat sekä näiden vapaat muuttujat määritellään, minkä lisäksi tutustutaan termien ja kaavojen totuusarvoihin mallissa A sekä käsitellään aakkostojen laajentamista. Tämän jälkeen käsitellään kyselyjä ja logiikan FO ilmaisuvoimaa äärellisten mallien tapauksessa.
Tämän työn päättävässä luvussa tarkastellaan EF-pelejä. Aluksi esitetään EF-pelin säännöt ja EF-peliä koskevia määritelmiä, kuten osittaisen isomorfismin, EF-pelin voittotilanteen ja EF-pelin voittostrategian sekä kaavojen kvanttoriasteen määritelmät. Seuraavaksi esitetään EF-lause seurauslauseineen, jotka käsittelevät mallien ominaisuuksien ja kyselyjen määriteltävyyttä logiikassa FO. Lisäksi tämän työn päättävässä luvussa tarkastellaan tyyppejä, back-and-forth-relaatiota sekä Hintikka-kaavoja, joita käyttäen esitetään vaihtoehtoinen todistus EF-lauseelle.
Tässä työssä esitellään joitakin logiikan FO peruskäsitteitä, mutta työn seuraaminen edellyttää kuitenkin lukijalta logiikan perusteiden tuntemista. Lukijan tulee myös tuntea esimerkiksi relaation käsite.
Tämän työn aluksi tarkastellaan ensimmäisen kertaluvun logiikan eli predikaattilogiikan peruskäsitteistöä. Ensimmäisen kertaluvun logiikasta käytetään tässä työssä merkintää FO. Työn alussa määritellään muun muassa aakkosto ja malli sekä käsitellään homomorfisuutta mallien välillä. Seuraavaksi tässä työssä tarkastellaan logiikan FO syntaksia ja semantiikkaa. Logiikan FO termit ja kaavat sekä näiden vapaat muuttujat määritellään, minkä lisäksi tutustutaan termien ja kaavojen totuusarvoihin mallissa A sekä käsitellään aakkostojen laajentamista. Tämän jälkeen käsitellään kyselyjä ja logiikan FO ilmaisuvoimaa äärellisten mallien tapauksessa.
Tämän työn päättävässä luvussa tarkastellaan EF-pelejä. Aluksi esitetään EF-pelin säännöt ja EF-peliä koskevia määritelmiä, kuten osittaisen isomorfismin, EF-pelin voittotilanteen ja EF-pelin voittostrategian sekä kaavojen kvanttoriasteen määritelmät. Seuraavaksi esitetään EF-lause seurauslauseineen, jotka käsittelevät mallien ominaisuuksien ja kyselyjen määriteltävyyttä logiikassa FO. Lisäksi tämän työn päättävässä luvussa tarkastellaan tyyppejä, back-and-forth-relaatiota sekä Hintikka-kaavoja, joita käyttäen esitetään vaihtoehtoinen todistus EF-lauseelle.
Tässä työssä esitellään joitakin logiikan FO peruskäsitteitä, mutta työn seuraaminen edellyttää kuitenkin lukijalta logiikan perusteiden tuntemista. Lukijan tulee myös tuntea esimerkiksi relaation käsite.