Ehrenfeuchtin ja Fraïssén peliä on kehitetty kuvaamaan myös toisen ker-taluvun logiikan ilmaisuvoimaa. Käsitellään tässä yhdentyyppiset EF-pelin laajennukset∃SO-logiikalle ja∃MSO-logiikalle. MSO-logiikan EF-pelistä kir-joittaa muun muassa Libkin [4, s. 116-119].
Esitellään ensimmäiseksi EF-peli ∃SO-logiikalle Kolaitista [5, s. 55] mu-kaillen. Pitäydytään relationaalisissa aakkostoissa edellisen luvun tapaan.
Määritelmä 6.6. Olkoot k1, . . . , kn, r positiivisia kokonaislukuja ja olkoot A sekä B aakkoston σ struktuureita. Eksistentiaalisen SO-logiikan EF-peli (hk1, . . . , kni, r) pelataan struktuurien A ja B välillä noudattaen seuraavia sääntöjä.
• Pelaaja I valitseek1, . . . , kn paikkaiset relaatiotR1, . . . , Rn struktuuris-taA.
• Pelaaja II valitsee k1, . . . , kn paikkaiset relaatiot R01, . . . , R0n struktuu-rista B.
• Nyt valinnatR1, . . . , Rn jaR01, . . . , R0nmäärittävät struktuurienAja B laajennukset(A, R1, . . . , Rn)ja(B, R01, . . . , R0n), joiden välillä pelaajat I ja II pelaavatrkierroksisen pelinEFr((A, R1, . . . , Rn),(B, R01, . . . , R0n)).
• Olkoot ~a = (a1, . . . , ar) ja~b = (b1, . . . , br) pelaajien I ja II suoritta-mat valinnat pelissä EFr((A, R1, . . . , Rn),(B, R10, . . . , R0n)). Pelaaja II voittaa pelin, jos pari (~a,~b) määrittelee osittaisen isomorsmin struk-tuurien(A, R1, . . . , Rn)ja(B, R01, . . . , R0n)välillä. Muutoin peli päättyy pelaajan I voittoon.
Jos pelaaja II voittaa pelin EFr((A, R1, . . . , Rn),(B, R01, . . . , R0n))pelaajan I valinnoista riippumatta, hänellä on voittostrategia myös struktuurien A ja B välisessä pelissä (hk1, . . . , kni, r). Merkitään tällöin A ∼∃SOr B.
Toisen kertaluvun semantiikasta ja lauseesta 5.3 voidaan johtaa seuraa-va tulos, jonka perusteella EF-peliä (hk1, . . . , kni, r) voidaan käyttää ∃ SO-logiikan ilmaisuvoiman arvioimisessa. Lauseen todistus sivuutetaan.
Seuraus 6.1. Olkoon Φ ESO-lause muotoa ∃X1· · · ∃Xnφ, missä relaatio-symbolien X1, . . . , Xn paikkaluvut ovat k1, . . . , kn, ja missä φ on ensimmäi-sen kertaluvun lause kvanttoriasteeltaan r. Jos A Φ pätee, ja pelaajalla II on voittostrategia struktuurien A ja B välisessä pelissä (hk1, . . . , kni, r), tällöin myös B Φ pätee.
Ominaisuuden P määrittelemättömyys ∃SO-logiikassa struktuuriluokas-sa M voidaan todistaa seuraavasti. Osoitetaan, että jokaiselle positiivisten kokonaislukujen jonollek1, . . . , kn, ron olemassa struktuuritA ∈P jaB ∈P siten, että pelaajalla II on voittostrategia näiden strukturien välisessä pelis-sä (hk1, . . . , kni, r). Menetelmä on täydellinen, sillä ominaisuuden P ollessa määrittelemätön∃SO-logiikassa struktuuriluokassaM, jokaiselle kokonaislu-kujen jonolle k1, . . . , kn, r löytyy struktuurit A ja B edellä mainittujen ehto-jen mukaisesti. Todistus sivuutetaan.
Eksistentiaalisen SO-logiikan mielenkiintoisuus perustuu lähinnä tulok-seen, jonka mukaan äärellisten struktuurien∃SO-määriteltävien ominaisuuk-sien luokka vastaa vaativuusluokkaa NP [6].
Vaikka EF-peli (hk1, . . . , kni, r)on pätevä menetelmä∃SO-logiikan ilmai-suvoiman tutkimiseen, sen käyttökelpoisuus on jokseenkin rajallinen. Pelin soveltaminen käy turhan monimutkaiseksi, jos käsitellään sellaisia kaavoja, joissa vähintään yhdellä eksistentiaalisesti kvantioidulla relaatiomuuttujal-la on lukua 1 suurempi paikkaluku [5, s. 56]. Rajoitutaan seuraavaksi yksi-paikkaisiin relaatiomuuttujiin ja ∃MSO-logiikkaan.
Eksistentiaalisen MSO-logiikan ilmaisuvoima voidaan karakterisoida Aj-tain ja Faginin pelillä, joka määritellään tässä Libkinin [4, s. 123] mukaan.
Itse asiassa peli toimii myös koko∃SO-logiikalle.
Määritelmä 6.7. Olkoot n ja r positiiviset kokonaisluvut. Käytetään mer-kintää AFn,r(P) ominaisuuden P Ajtain ja Faginin pelille (n, r) struktuuri-luokassa M. Pelissä noudatetaan seuraavia vaiheita.
• Pelaaja II valitsee struktuurin A ∈P.
• Pelaaja I valitsee n kappaletta yksipaikkaisia relaatioita R1, . . . , Rn struktuurista A.
• Pelaaja II valitsee struktuurin B ∈ P. Lisäksi pelaaja II valitsee n kappaletta yksipaikkaisia relaatioita R01, . . . , R0n struktuurista B.
• Nyt valinnatR1, . . . , Rn jaR01, . . . , R0nmäärittävät struktuurienAja B laajennukset(A, R1, . . . , Rn)ja(B, R01, . . . , R0n), joiden välillä pelaajat I ja II pelaavatrkierroksisen pelinEFr((A, R1, . . . , Rn),(B, R01, . . . , R0n)). Peli päättyy pelaajan II voittoon, josrkierroksisen pelinEFr((A, R1, . . . , Rn), (B, R10, . . . , R0n))aikana tehdyt valinnat määrittelevät osittaisen isomorsmin struktuurien (A, R1, . . . , Rn)ja (B, R01, . . . , R0n) välillä.
Osoitetaan, että Ajtain ja Faginin peli riittää karakterisoimaan ∃ MSO-logiikan ilmaisuvoiman. Olkoon ∃MSO[n, r] kaikkien muotoa ∃X1. . . ,∃Xnϕ olevien eksistentiaalisen MSO-logiikan kaavojen joukko, missä ensimmäisen kertaluvun kaavan ϕ kvanttoriaste on pienempi tai yhtäsuuri kuin r. Apu-lauseen 5.1 tavoin voidaan todistaa, että joukko∃MSO[n, r] sisältää loogista ekvivalenssia vaille vain äärellisen määrän lauseita Φ.
Lause 6.2. OminaisuusP on∃MSO-määriteltävä struktuuriluokassa M, jos ja vain jos on olemassa positiiviset kokonaisluvut n ja r siten, että pelaajalla I on voittostrategia pelissä AFn,r(P).
Todistus. Oletetaan aluksi, että ominaisuus P on määriteltävissä ∃ MSO-kaavalla ψ = ∃X1, . . . ,∃Xnϕ. Olkoot n ja r positiivisia kokonaislukuja si-ten, että kaava ψ kuuluu joukkoon∃MSO[n, r]. Osoitetaan, että pelaajalla I on voittostrategia pelissä AFn,r(P).
Oletetaan, että pelaaja II valitsee struktuurinA ∈P. Koska päteeAψ, struktuurissaAon olemassa relaatiotR1, . . . , Rnsiten, että(A, R1, . . . , Rn) ϕ pitää paikkansa. Relaatiot R1, . . . , Rn ovat pelaajan I valinta. Valitkoon pelaaja II struktuurin B ∈ P ja relaatiot R01, . . . , Rn0 struktuurista B. Kos-ka struktuuri B kuuluu ominaisuuden P komplementtijoukkoon, on oltava (B, R10, . . . , R0n) 2 ϕ. Koska qr(ψ) ≤ r pätee, niin pelaajalla I on voitto-strategia pelissäEFr((A, R1, . . . , Rn),(B, R01, . . . , R0n)). Täten pelaajalla I on voittostrategia pelissäAFn,r(P).
Oletetaan seuraavaksi, että on olemassa positiiviset kokonaisluvut n jar siten, että pelaajalla I on voittostrategia pelissä AFn,r(P). Todistetaan, että tällöin löydetään ∃MSO-kaava, joka määrittelee ominaisuudenP.
Koska pelaajalla I on voittostrategia pelissä AFn,r(P), jokaiselle struk-tuurille A ∈ P on olemassa relaatiot R1, . . . , Rn ⊆ An siten, että kai-killa struktuureilla B ∈ P ja kaikilla relaatioilla R01, . . . , R0n ⊆ Bn pelaa-ja I voittaa pelin EFr((A, R1, . . . , Rn),(B, R01, . . . , R0n)). Käyteteään parille (A, R1, . . . , Rn),(B, R01, . . . , R0n)lyhyempää merkintää(AR~,BR~0). Nyt kaikille struktuureille B ∈P ja relaatioilleR01, . . . , Rn0 on olemassa kaava ϕ(AR~,BR~0) ∈ FO[r] siten, että (A, R1, . . . , Rn) ϕ(AR~,BR~0) ja (B, R01, . . . , R0n) 2 ϕ(AR~,BR~0)
pitävät paikkansa. Olkoon
θ ≡ _
(A, ~R)
^
(B, ~R0)
ϕ(AR~,BR~0)
.
Väitetään, että kaava ∃X1, . . . ,∃Xnθ määrittelee ominaisuuden P. Nyt mie-livaltaisille sruktuureille A ∈ P ja B ∈ P pätee A ∃X1, . . . ,∃Xnθ ja B 2
∃X1, . . . ,∃Xnθ. Olkoon C ∈ P. Oletetaan, että C ∃X1, . . . ,∃Xnθ. Tällöin struktuurissaC on olemassa relaatiotR001, . . . , R00nsiten, että(C, R001, . . . , R00n) θ. Tästä johtuen myös(C, R001, . . . , R00n)ϕ(AR~,CR~00)pitää paikkansa. Tämä joh-taa kuitenkin ristiriijoh-taan, sillä struktuuri C kuuluu ominaisuudenP komple-menttijoukkoon. Koska kaavojaϕ(AR~,BR~0)on olemassa äärellisen monta, kaava θ on äärellinen. Täten kaava ∃X1, . . . ,∃Xnθ kuullu joukkoon ∃MSO[n, r] ja määrittelee ominaisuuden P.
Lisää tietoa Ajtain ja Faginin pelistä tarjoaa muun muassa Fagin [6]. Vaik-ka perinteinen ensimmäisen kertaluvun logiikVaik-ka on ilmaisuvoimaltaan∃ MSO-logiikkaa heikompi, on olemassa useita ominaisuuksia, joita edes ∃ MSO-logiikka ei pysty määrittelemään. Lauseen 6.3 todistus löytyy muun Grädelin et al. teoksesta [5, s. 57].
Lause 6.3. Olkoon M äärellisten verkkojen struktuuriluokka. Verkkojen yh-tenäisyys ei ole määriteltävissä ∃MSO-logiikassa struktuuriluokassa M.
Viitteet
[1] Ebbinghaus, Heinz-Deiter & Flum, Jörg. Finite Model Theory. Springer, Berlin Heidelberg, 2nd ed. (1999).
[2] Ebbinghaus, Heinz-Deiter; Flum, Jörg & Thomas, Wolfgang. Mathema-tical Logic. Springer, New York (1984).
[3] Hodges, Wilfrid. A Shorter Model Theory. Campridge University Press, Cambridge (1997).
[4] Libkin, Leonid. Elements of nite model theory. Springer, New York (2004).
[5] Grädel, Eric; Kolaitis, Phokion G.; Libkin, Leonid; Marx, Maarten;
Spencer, Joel; Vardi, Moshe Y.; Venema, Yde & Wenstein, Scott. Fi-nite Model Theory and its Applications. Springer, New York (2007).
[6] Fagin, Ronald. Easier ways to win logical games. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 31, 1-32, (1997).
[7] Rosen, Eric. Some aspects of model theory and nite structures. Bulletin of Symbolic Logic, Vol 8(3), 380-403, (2002).
[8] Asher, Nicholas. Partial Isomorphisms and Fraïssé's theorem (2005).
Available as http://www.utexas.edu/cola/depts/philosophy/faculty/
asher/course/PHL%20344K%202005/fraisse%20theorem.pdf. Checked 2008-10-14.