Ehrenfeucht-Fraïssé-pelistä

TAMPEREEN YLIOPISTO Pro gradu -tutkielma

Hanna Sulonen

Ehrenfeucht-Fraïssé-pelistä

Informaatiotieteiden yksikkö Matematiikka

2012

Tampereen yliopisto

Informaatiotieteiden yksikkö

SULONEN, HANNA: Ehrenfeucht-Fraïssé-pelistä Pro gradu -tutkielma, 30 s., 0 liites.

Matematiikka 2012

Tiivistelmä

Tässä työssä käsitellään Andrzej Ehrenfeuchtin 1960-luvulla kehittämää Eh- renfeucht-Fraïssé-peliä, jonka pääsovellus on ensimmäisen kertaluvun logii- kan 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ä tehok- kaampia työkaluja, mutta äärellisten mallien tapauksessa EF-pelit ovat sovel- lettavuudeltaan 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 pre- dikaattilogiikan peruskäsitteistöä. Ensimmäisen kertaluvun logiikasta käyte- tään tässä työssä merkintää FO. Työn alussa määritellään muun muassa aak- kosto 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äk- si tutustutaan termien ja kaavojen totuusarvoihin mallissaAsekä 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 isomor- fismin, EF-pelin voittotilanteen ja EF-pelin voittostrategian sekä kaavojen kvanttoriasteen määritelmät. Seuraavaksi esitetään EF-lause seurauslausei- neen, 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 tyyppe- jä, 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.

Sisältö

1 Johdanto 7

2 Valmistelevia tarkasteluja 8

2.1 Mallit . . . 8

2.2 Ensimmäisen kertaluvun logiikan käsitteitä . . . 11

2.3 Kyselyt . . . 13

3 Ehrenfeucht-Fraïssé-pelit 15 3.1 EF-pelin kulku . . . 15

3.2 EF-peliin liittyviä määritelmiä ja lauseita . . . 20

3.3 Tyypit . . . 22

3.4 EF-lauseen todistus . . . 25

Viitteet 30

1 Johdanto

Tässä työssä käsitellään Ehrenfeucht-Fraïssé-peliä, joka on yksi tärkeimmis- tä menetelmistä määrittelemättömyystulosten todistamiseen. Ehrenfeucht- Fraïssé-pelin kehitti Puolassa syntynyt ja Amerikassa asunut matemaatikko Andrzej Ehrenfeucht 1960-luvulla. Ehrenfeucht käytti Ehrenfeucht-Fraïssé- pelissä ranskalaisen matemaatikon Roland Fraïssén 1950-luvulla kehittämää back-and-forth-metodia, mistä nimi Ehrenfeucht-Fraïssé-peli johtuu.

Ehrenfeucht-Fraïssé-pelien pääsovellus on ensimmäisen kertaluvun logii- kan määrittelemättömyystulosten todistaminen. Äärettömien mallien tapauk- sessa löytyy määrittelemättömyystulosten todistamiseen monia Ehrenfeucht- Fraïssé-pelejä tehokkaampia työkaluja, joten joissakin malliteoriaa käsittele- vissä teoksissa Ehrenfeucht-Fraïssé-pelit mainitaan vain lyhyesti. Äärellis- ten mallien tapauksessa Ehrenfeucht-Fraïssé-pelit ovat kuitenkin sovellet- tavuudeltaan erittäin hyviä. Malliteoriassa ei ole monia muita äärellisten mallien tapauksessa päteviä menetelmiä kuin Ehrenfeucht-Fraïssé-pelit, jo- ten Ehrenfeucht-Fraïssé-pelejä käytetään paljon äärellisten mallien teoriassa ja sen sovelluksissa tietojenkäsittelytieteessä. Ehrenfeucht-Fraïssé-pelejä voi käyttää esimerkiksi tietokantakielien ilmaisuvoiman mittaamiseen.

Ehrenfeucht-Fraïssé-pelejä käyttäen saadaan parhaimmillaan todistettua määrittelemättömyystuloksia melko yksinkertaisesti. Useimmat pelejä käyt- täen tehdyt todistukset ovat kuitenkin melko monimutkaisia ja niiden vaikeus nousee yleensä nopeasti kun todistettavat asiat muuttuvat monimutkaisem- miksi.

Tämän työn aluksi tarkastellaan ensimmäisen kertaluvun logiikan eli pre- dikaattilogiikan peruskäsitteistöä. Ensimmäisen kertaluvun logiikasta käyte- tään tässä työssä merkintää FO. Luvussa 2 esitetään sellaisia logiikan FO perusmääritelmiä, joita tarvitaan myöhemmin Ehrenfeucht-Fraïssé-peliä kä- sittelevässä luvussa 3. Ehrenfeucht-Fraïssé-pelistä käytetään tässä työssä ly- hennystä EF-peli. Malleja tarkastelevassa alaluvussa 2.1 määritellään muun muassa aakkosto ja malli sekä käsitellään homomorfisuutta mallien välillä.

Näiden lisäksi alaluvussa 2.1 määritellään mallin alimalli sekä suuntaamaton verkko, joka on eräs esimerkki mallista. Seuraavassa alaluvussa 2.2 tarkas- tellaan logiikan FO syntaksia ja semantiikkaa. Logiikan FO termit ja kaa- vat sekä näiden vapaat muuttujat määritellään, minkä lisäksi tutustutaan termien ja kaavojen totuusarvoihin mallissa A sekä käsitellään aakkostojen laajentamista. Luvun 2 viimeisessä kyselyjä käsittelevässä alaluvussa 2.3 määritellään k-paikkainen kysely ja Boolen kysely sekä tarkastellaan kyse- lyjen määriteltävyyttä ja logiikan FO ilmaisuvoimaa äärellisten mallien ta- pauksessa. Kyselyihin palataan tämän työn luvussa 3.

Luvussa 3 keskitytään EF-pelin tarkasteluun. Luku aloitetaan tarkaste- lemalla EF-pelin lähtökohtaa ja kulkua. Tämä tehdään alaluvussa 3.1 esittä- mällä EF-pelin säännöt ja määrittelemällä muun muassa osittainen isomorfis-

mi, EF-pelin voittotilanne ja EF-pelin voittostrategia. EF-pelien voittostra- tegioita havainnoillistetaan alaluvussa 3.1 viidellä esimerkillä sekä lauseilla 3.1 ja 3.2. Näiden EF-peliä koskevien määritelmien ja lauseiden jatkoksi esitetään seuraavassa alaluvussa 3.2 muita EF-peliin liittyviä määritelmiä ja lauseita kuten kaavojen kvanttoriasteen määritelmä sekä EF-lause (lause 3.3). EF-lauseelle esitetään myös kolme seurauslausetta, jotka käsittelevät mallien ominaisuuksien ja kyselyjen määriteltävyyttä logiikassa FO. Tyyppe- jä käsitellään seuraavassa alaluvussa 3.3 esittämällä r-tyyppien määritelmä sekä niihin liittyvä lause 3.7. Alaluvussa 3.3 esitetään myös yksi apulause sekä kolme seurauslausetta. Luvun 3 päättävässä alaluvussa 3.4 esitetään todistus EF-lauseelle 3.3 sekä määritellään Hintikka-kaavat, joita käyttäen esitetään vaihtoehtoinen todistus EF-lauseelle. Alaluvussa 3.4 määritellään myös back-and-forth-relaatio.

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.

2 Valmistelevia tarkasteluja

Tässä luvussa esitellään logiikan FO peruskäsitteitä. Alaluvussa 2.1 käsitel- lään malleja sekä homomorfisuutta mallien välillä. Alaluvussa 2.2 esitellään lisää logiikan FO peruskäsitteitä. Tämän luvun viimeisessä alaluvussa 2.3 tarkastellaan kyselyjä.

2.1 Mallit

Tässä alaluvussa tarkastellaan malleja ja niiden ominaisuuksia esittämällä määritelmiä sekä kolme esimerkkiä, joilla havainnoillistetaan malleja ja ho- momorfisuutta mallien välillä.

Määritelmä 2.1. Aakkostoσon kokoelma vakiosymboleja, relaatiosymbole- ja ja funktiosymboleja. Relaatiosymboleista käytetään myös nimitystä predi- kaattisymbolit, ja niitä merkitäänP₁, . . . , P_n, . . .. Vakiosymboleja merkitään c₁, . . . , c_n, . . . ja funktiosymboleja merkitään f₁, . . . , f_n, . . .. Jokaisella aak- koston σ relaatiosymbolilla P ja funktiosymbolilla f on paikkaluku n∈Z⁺. RelaatiosymbolinP paikkalukua merkitään #(P) ja funktiosymbolinf paik- kalukua merkitään #(f).

Lisäksi sovitaan, että vakiosymbolin c paikkaluku #(c) on 0. Aakkoston σ vakiosymbolien joukosta käytetään merkintää Con(σ), relaatiosymbolien joukosta käytetään merkintääRel(σ) ja funktiosymbolien joukosta käytetään merkintää F un(σ).

Määritelmä 2.2. σ-malli A = hA,(c^A)c∈Con(σ),(P^A)P∈Rel(σ),(f^A)f∈F un(σ)i koostuu mallinAuniversumistaA =Dom(A) sekä aakkostonσ vakiosymbo- lien, relaatiosymbolien ja funktiosymbolien tulkinnoista, jotka määritellään seuraavasti:

• jokainen aakkoston σ vakiosymboli c_i tulkitaan alkioksi c^A_i ∈A;

• jokainen aakkostonσ k-paikkainen relaatiosymboliP_i tulkitaan univer- sumin A k-paikkaiseksi relaatioksi P_i^A⊆A^k; ja

• jokainen aakkostonσ k-paikkainen funktiosymbolif_i tulkitaan univer- sumin A k-paikkaiseksi funktioksi f_i^A:A^k →A.

Mallin A sanotaan olevan äärellinen, jos sen universumi A on äärellinen joukko.

Esimerkki 2.1. Jos aakkosto σ sisältää kaksipaikkaiset funktiosymbolit + ja ·, vakiosymbolit 0 ja 1 sekä kaksipaikkaisen relaatiosymbolin ≤, ovat R = hR,+^R,·^R,0,1,≤^Ri ja Q = hQ,+^Q,·^Q,0,1,≤^Qi esimerkkejä aakkos- ton σ malleista. Mallin R universumi on reaalilukujen joukkoR ja mallinQ universumi on rationaalilukujen joukko Q. Symbolit +^R ja +^Q tarkoittavat malleissa tavallisia reaalilukujen ja rationaalilukujen yhteenlaskuja, ·^R ja ·^Q tarkoittavat tavallisia reaalilukujen ja rationaalilukujen kertolaskuja ja ≤^R ja ≤^Q tarkoittavat tavallisia reaalilukujen ja rationaalilukujen järjestyksiä.

Tässä työssä jatkossa tarkasteltava aakkosto σ on aina relationaalinen.

Aakkosto σ sisältää siis relaatiosymboleja ja vakiosymboleja, mutta se ei si- sällä lainkaan funktiosymboleja. Aakkostoa sanotaan puhtaasti relationaali- seksi, jos se sisältää ainoastaan relaatiosymboleja.

Jos σ on aakkosto, niin merkitsemme jatkossa kaikkien äärellisten σ- mallien luokkaa Str[σ].

Määritelmä 2.3. Olkoon aakkosto σ = {E}, missä E on kaksipaikkainen relaatiosymboli. Suuntaamattomalla verkolla (lyhyemmin verkolla) tarkoi- tetaan aakkoston σ mallia G, jossa E^G on irrefleksiivinen ja symmetrinen relaatio. Verkko on suunnattu, jos sille vaaditaan vain relaation E^G irreflek- siivisyyden voimassaolo.

Verkon solmuiksi sanotaan mallin G universumin Dom(G) alkioita, ja verkon särmiksi sanotaan pareja {a, b}, missä (a, b)∈E^G.

Jos suunnatulle verkolle G pätevät ehdot n ≥ 1 ja ((a₁, a₂),(a₂, a₃), . . . , (a_n, a_n+1)) ∈ E^G, niin a₁, . . . , a_n+1 on pituudeltaan n oleva polku verkon alkiosta a₁ alkioon a_n+1.

Tarkastellaan seuraavaksi homomorfisuutta mallien välillä.

Määritelmä 2.4. Olkoot A ja B σ-malleja, ja olkoon h : Dom(A) → Dom(B) kuvaus. Kuvaus h onhomomorfismi mallistaA malliinB, jos seu- raavat ehdot toteutuvat:

1. Jokaisella c∈Con(σ) pätee h(c^A) =c^B.

2. Jos ehdot P ∈ Rel(σ), #(P) = n ja (a₁, . . . , a_n) ∈ P^A pätevät, niin (h(a₁), . . . , h(a_n))∈P^B.

3. Jos ehdot f ∈ F un(σ), #(f) = n ja (a₁, . . . , a_n) ∈ Dom(A)ⁿ pätevät, niin h(f^A(a₁, . . . , a_n)) =f^B(h(a₁), . . . , h(a_n)).

Kuvauksenhsanotaan olevanvahva homomorfismimallistaAmalliinB, jos ehto 2 pätee myös seuraavassa vahvemmassa muodossa:

2´. Jos P ∈ Rel(σ), #(P) = n ja (a₁, . . . , a_n) ∈ Dom(A)ⁿ pätevät, niin (a₁, . . . , a_n)∈P^A⇔(h(a₁), . . . , h(a_n))∈P^B.

Kuvaus h on mallien A ja B välinen isomorfismi, jos h : Dom(A) → Dom(B) on vahva homomorfismi ja bijektio. MallienAjaBsanotaan olevan isomorfiset, jos niiden välillä on isomorfismi. Mallien A ja B isomorfisuutta merkitäänA∼=B.

Kaksi mallia A ja B ovat isomorfiset, jos malli B voidaan muodostaa mallista A korvaamalla jokainen alkio a ∈ A alkiolla h(a) ∈ B muuten muuttamatta mallin rakennetta.

Esimerkki 2.2. Tarkastellaan verkkoja A=hV, E^AijaB=hW, E^Bi, missä V ={1,2,3}, E^A = {{1,3},{2,3}}, W ={1,2,3,4} ja E^B ={{1,2},{1,3}, {2,3},{3,4}}.

Kuvaus h :{1,2,3} → {1,2,3,4}, h(x) = x on homomorfismi, sillä mal- lien A ja B aakkostojen ainoat symbolit ovat relaatiosymbolit E^A ja E^B ja toinen homomorfiaehto on voimassa:

Kun (a, b) ∈ E^A, niin {a, b} = {1,3} tai {a, b} = {2,3} ja koska {h(a), h(b)}={a, b}on myös verkonBsärmä, pätee (h(a), h(b))∈E^B. Kuvaus h ei ole vahva homomorfismi, sillä esimerkiksi (1,2)∈/ E^A mutta (h(1), h(2)) = (1,2)∈E^B. Siis kuvaushei ole isomorfismi. Nähdään helposti, ettei mallien välisen isomorfisuuden toinen ehto päde: koska verkkoAsisältää kolme solmua ja verkko B sisältää neljä solmua, ei ole olemassa bijektiota f :Dom(A)→Dom(B).

Esimerkki 2.3. Osoitetaan, että on olemassa epäisomorfiset verkot, joissa on yhtä monta solmua ja yhtä monta särmää.

Tarkastellaan verkkoja A = hV, E^Ai ja B = hW, E^Bi, missä V = {1,2, 3,4}, E^A = {{1,3},{1,4},{2,4},{3,4}}, W = {1,2,3,4} ja E^B = {{1,2}, {1,4},{2,3},{3,4}}.

Nyt kummassakin verkossa on neljä solmua ja neljä särmää. Olkoon f : {1,2,3,4} → {1,2,3,4} mielivaltainen bijektio ja olkoon a= f(4). Nyt sol- musta 4 lähtee verkossa A kolme särmää. Solmusta a lähtee kuitenkin ver- kossaBaina kaksi särmää riippumatta siitä, mikä verkonBsolmu aon. Siis

on olemassa sellainen x ∈ {1,2,3}, että (4, x) ∈ E^A mutta (f(4), f(x)) = (a, f(x))∈/ E^B, joten kuvaus f ei ole isomorfismi.

Määritellään tämän alaluvun lopuksi mallin alimalli.

Olkoon malli Arelationaalinen. Jos A∈Str[σ] ja A₀ ⊆A, sanotaan että universuminA₀ määräämämallinAalimallionσ-malliB, jonka universumi B =A₀ ∪ {c^A |c∈Con(σ)}. Tässä päteec^B=c^A jokaisella vakiosymbolilla cja P^B =P^A∩B^k jokaisella k-paikkaisella relaatiosymbolillaP.

Alimallia käytettäessä poistetaan siis käytöstä osa alkuperäisen mallin alkioista, mutta säilytetään kaikki alkuperäisen mallin sisältämät tulkinnat.

2.2 Ensimmäisen kertaluvun logiikan käsitteitä

Tässä alaluvussa tarkastellaan logiikan FO perusteita. Tarkastelu aloitetaan logiikan FO termien ja kaavojen muodostamisesta ja aiheen käsittelyä jatke- taan tarkastelemalla termien arvoa mallissa ja kaavojen totuusarvoa mallis- sa.Olkoon σ aakkosto. Logiikan FO kaavat muodostuvat seuraavista osista:

• muuttujista x₁, x₂, x₃, . . .,

• konnektiiveista ¬,∨,∧,→,↔,

• eksistentiaali- ja universaalikvanttoreista∃,∀,

• yhtäsuuruusmerkistä =,

• suluista ),( sekä

• aakkostonσ symboleista.

Määritellään seuraavaksi logiikan FO σ-termit, termien arvo mallissa A, σ-kaavat sekä termien ja kaavojen vapaat muuttujat.

Määritelmä 2.5. Olkoon σ aakkosto. Logiikan FO σ-termit määritellään seuraavasti:

• Jokainen muuttujax on termi.

• Jokainen vakiosymboli con termi.

• Jos t₁, . . . , t_k ovat termejä ja f on k-paikkainen funktiosymboli, niin f(t₁, . . . , t_k) on termi.

σ-mallin A tulkintafunktio on funktio α : {xi | i ∈ N} → A. Termin t arvo mallissa Atulkinnalla α määritellään seuraavasti:

• x^A,α_i =α(x_i) jokaisella i∈N.

• c^A,α=c^A jokaisella c∈Con(σ).

• Jos t=f(t₁, . . . , t_k) jaf ∈F un(σ), niint^A,α =f^A(t^A,α₁ , . . . , t^A,α_k ).

Määritelmä 2.6. Olkoon σ aakkosto. Logiikan FO σ-atomikaavat ja σ- kaavat määritellään seuraavasti:

• Jos t₁ ja t₂ ovat termejä, niin t₁ =t₂ on atomikaava.

• Jos t₁, . . . , t_k ovat termejä, ja P on k-paikkainen relaatiosymboli, niin P(t₁, . . . , t_k) on atomikaava.

• Jokainen atomikaava on kaava.

• Jos ϕ₁ ja ϕ₂ ovat kaavoja, niin ¬ϕ₁ ja ϕ₁∧ϕ₂ ovat kaavoja.

• Jos ϕon kaava, niin ∃xϕ on kaava.

Tiettyjen kaavojen sijasta käytetään tavallisesti lyhennysmerkintöjä:

• ϕ₁ ∨ϕ₂ ⇔ ¬(¬ϕ₁∧ ¬ϕ₂),

• ϕ₁ →ϕ₂ ⇔ ¬ϕ₁∨ϕ₂,

• ϕ₁ ↔ϕ₂ ⇔(ϕ₁ →ϕ₂)∧(ϕ₂ →ϕ₁),

• ∀xϕ⇔ ¬∃x¬ϕ.

Kaavan, joka ei sisällä eksistentiaali- tai universaalikvanttoreita ∃ ja ∀, sanotaan olevan kvanttoriton.

Määritelmä 2.7. Termintvapaat muuttujat Fr(t) määritellään seuraavasti:

• Fr(x) ={x}.

• Fr(c) = ∅, kunc∈Con(σ).

• Jos t=f(t₁, . . . , t_k) jaf ∈F un(σ), niin Fr(t) = Fr(t₁)∪ · · · ∪Fr(t_k).

Kaavanϕ vapaat muuttujat Fr(ϕ) määritellään seuraavasti:

• Fr(t=t⁰) = Fr(t)∪Fr(t⁰).

• Fr(P(t₁, . . . , t_k)) = Fr(t₁)∪ · · · ∪Fr(t_k), kun P ∈Rel(σ).

• Negaatio ¬ei sido muuttujia, joten Fr(ϕ) = Fr(¬ϕ).

• Fr(ϕ₁∧ϕ₂) = Fr(ϕ₁)∪Fr(ϕ₂). (Sama pätee kaavalle ϕ₁∨ϕ₂).

• Fr(∃xϕ) = Fr(ϕ)\{x}. (Sama pätee kaavalle ∀xϕ).

Ne termien ja kaavojen muuttujat jotka eivät ole vapaita, ovat sidottuja.

Kaavaa sanotaan lauseeksi, jos siinä ei ole lainkaan vapaita muuttujia. Mer- kintää ϕ(~x) käytetään, jos ~x sisältää kaikki kaavan ϕvapaat muuttujat.

Tarkastellaan seuraavaksi kaavojen totuutta mallissa A.

Määritelmä 2.8. Olkoon A σ-malli, olkoon α mallin A tulkintafunktio ja olkoon ϕ σ-kaava. Määritellään kaavan ϕ totuus mallissa A tulkinnalla α (merkitään tätä A, α|=ϕ) seuraavasti:

• A, α|=t₁ =t₂ ⇔t^A,α₁ =t^A,α₂ .

• A, α|=P(t₁, . . . , t_k)⇔(t^A,α₁ , . . . , t^A,α_k )∈P^A.

• A, α |= ¬ϕ ⇔ A, α 6|= ϕ. Tässä A, α 6|= ϕ tarkoittaa, että kaava ϕ ei päde mallissaA tulkinnalla α.

• A, α|=ϕ₁∧ϕ₂ ⇔A, α |=ϕ₁ ja A, α|=ϕ₂

• A, α |= ∃x_iϕ ⇔ A, α(a/x_i) |= ϕ jollakin a ∈ A. Tässä α(a/x_i) on tulkintafunktio, joka saadaan vaihtamalla muuttujan x_i tulkinnaksi a. Siis α(a/x_i)(x_j) =α(x_j) kun j 6=i ja α(a/x_i)(x_j) = a kunj =i. Tulkintafunktiosta α riittää informaatio a₁ = α(x₁), . . . , an =α(xn), jo- ten voidaan merkitäA,(a₁, . . . , a_n)|=ϕ(x₁, . . . , x_n) tai lyhyestiA, ~a|=ϕ(~x).

Tätä lyhyttä merkintätapaa käytetään myöhemmin tässä työssä.

Tämän alaluvun lopuksi tarkastellaan mallien aakkostojen laajentamista.

Olkoon aakkostoσ⁰ eri kuin aakkostoσ. OlkoonAσ-malli ja olkoonA⁰ σ⁰- malli siten, että malleillaAjaA⁰ on sama universumiA. Tällöin merkinnällä (A,A⁰) tarkoitetaan sellaista universumin A σ ∪σ⁰-mallia jolle pätee, että kaikki aakkoston σ vakio- ja relaatiosymbolit tulkitaan kuten mallissa A, ja kaikki aakkoston σ⁰ vakio- ja relaatiosymbolit tulkitaan kuten mallissa A⁰.

Tyypillisessä tapauksessa aakkosto σ⁰ sisältää ainoastaan vakiosymbole- ja. Tällainen mallin aakkoston laajentaminen mahdollistaa siirtymisen edes- takaisin kaavojen ja lauseiden välillä, mikä on erityisen hyödyllistä monis- sa pelejä koskevissa tarkasteluissa. Merkinnällä σn tarkoitetaan aakkostonσ laajentamista n:llä uudella vakiosymbolilla c₁, . . . , c_n.

2.3 Kyselyt

Tässä alaluvussa määritellään k-paikkainen kysely ja Boolen kysely. Lisäksi tässä alaluvussa tarkastellaan kyselyjen määriteltävyyttä jossakin logiikassa Lsekä esitetään lause 2.1, joka kuvaa logiikan FO ilmaisuvoimaa äärellisten mallien tapauksessa.

Määritelmä 2.9. Olkoon aakkosto σ relationaalinen. Määritellään aakkos- ton σ k-paikkainen kysely ja Boolen kysely seuraavasti.

(a) k-paikkainen σ-kysely (missä k≥0) on kuvaus q siten, että

• Jokaisella mallilla A ∈ Str(σ), q(A) on universumin A k-paikkainen relaatio, ja

• Kuvausq säilyy kaikissa isomorfismeissa. Siis jos kuvaus h on mallien AjaBvälinen isomorfismi, niinq(B) =h(q(A)). Tämä on yhtäpitävää sen kanssa, että kuvaus h on isomorfismi (A, q(A))→(B, q(B)).

(b) Boolen σ-kysely (tai 0-paikkainen kysely), on kuvaus q : Str(σ) → {0,1} joka säilyy isomorfismeissa. Siis jos A∼=B, niin q(A) = q(B).

Esitetään seuraavaksi kyselyjä havainnoillistava esimerkki.

Esimerkki 2.4. Olkoon Averkko. Nyt

• Verkon transitiivinen sulkeuma on esimerkki kyselystä, jossak = 2. Siis q(A) = TC(A) = {(a, b)| solmusta a kulkee polku solmuunb }.

• Verkon eristettyjen solmujen joukko on esimerkki kyselystä, jossak = 1.

Siis q(A) = {a|a∈Dom(A)∧ ¬∃b ∈Dom(A) : (a, b)∈E^A}.

Huomautus. Boolen kysely määrää malliluokanK_q ={A∈ Str(σ)| q(A) = 1}. Kääntäen, josK ⊆Str(σ) on isomorfismin suhteen suljettu malliluokka, niin siihen liittyy Boolen kysely q_K, missä q_K(A) = 1⇔A∈K.

Määritelmä 2.10. Olkoon kuvausq n-paikkainenσ-kysely. Kyselynqsano- taan olevan määriteltävissä logiikassaLmikäli on olemassa sellainen logiikan L σ-kaava ϕ(x₁, . . . , x_n), että kaikilla malleilla A pätee

q(A) ={(a₁, . . . , a_n)∈Aⁿ |A, ~a|=ϕ(~x)}.

Jos kyselyqon määriteltävissä kaavallaϕ, voidaan merkinnänq(A) sijasta käyttää merkintää ϕ(A).

Esitetään tämän alaluvun lopuksi lause, joka kuvaa logiikan FO ilmaisu- voimaa äärellisten mallien tapauksessa.

Lause 2.1. Jokaisella äärellisellä mallillaAon olemassa sellainen FO-lause ϕA, että kaikilla malleilla B pätee B|=ϕA jos ja vain jos A∼=B.

Todistus. Vrt. [1, s. 13]. OlkoonA={a₁, . . . , a_n}. Merkitään~a= (a₁, . . . , a_n).

Olkoon kaava

Θn ={Ψ| kaava Ψ on muotoa R(x_ij, . . . , x_ik), missä i_j ∈ {1, . . . , n} ja x_i =c tai x_i =x_j, ja kaavan sisältämät muuttujat löytyvät joukostax₁, . . . x_n.}

ja olkoon kaava

ϕA=∃x1, . . . , xn(^{^}{Ψ|Ψ∈Θn,A, ~a|= ΨA(~x)} ∧^{^}{¬Ψ|Ψ∈Θn, A, ~a |=¬Ψ(~x)} ∧ ∀x_n+1(x_n+1 =x₁∨ · · · ∨x_n+1 =x_n)).

Nyt kaavasta ϕ_A seuraa, että B|=ϕ_A jos ja vain jos mallit Aja B ovat isomorfisia.

3 Ehrenfeucht-Fraïssé-pelit

Malliteoriassa on hyviä työkaluja määriteltävyyskysymysten tutkimiseen, ku- ten esimerkiksi lähteessä [2, s. 16] esitetyt kompaktisuuslause ja Löwenheim- Skolem-lause. Nämä työkalut eivät kuitenkaan usein toimi äärellisten mallien tapauksessa. Tässä luvussa tarkasteltavat EF-pelit tarjoavat ratkaisun tähän ongelmaan. EF-pelejä voidaan hyödyntää sekä äärellisten että äärettömien mallien tapauksessa (ainakin logiikkaa FO tarkasteltaessa), mutta äärettö- mien mallien tarkasteluun on olemassa selvästi EF-pelejä tehokkaampiakin välineitä. Äärellisten mallien tapauksessa EF-pelit ovat kuitenkin sovelletta- vuudeltaan erinomaisia.

Alaluvussa 3.1 esitetään EF-pelin säännöt sekä muutamia EF-peliin liit- tyviä määritelmiä ja esimerkkejä. Näiden määritelmien ja esimerkkien lisäksi esitetään voittostrategiaa koskeva lause 3.1 ja lause 3.2, jonka mukaan pe- laajalla D on voittostrategia r kierroksen EF-pelissä, jossa mallit A ja B ovat tietyn ehdon toteuttavia järjestettyjä joukkoja. Alaluvussa 3.2 esite- tään lisää EF-peliin liittyviä määritelmiä ja lauseita. Kyseisessä alaluvussa esitetään muun muassa EF-lause (lause 3.3), joka todistetaan myöhemmin alaluvussa 3.4. Alaluvussa 3.3 käsitellään tyyppejä. Tämän luvun päättä- vässä alaluvussa 3.4 esitetään todistus EF-lauseelle 3.3 sekä vaihtoehtoinen EF-lauseen todistus, jossa käytetään Hintikka-kaavoja. Alaluvussa 3.4 tar- kastellaan myös tilannetta, jossa pelaaja D voittaa EF-pelin ilman yhtään tehtyä siirtoa, sekä tarkastellaan back-and-forth-relaatiota.

3.1 EF-pelin kulku

Tämän alaluvun aluksi esitellään EF-pelin säännöt. EF-pelin pelilaudan muo- dostavat mallitAjaB. Pelissä on kaksi pelaajaa, joita nimitetään duplikaat- toriksi (merkitään tässä työssä jatkossa kirjaimella D) ja spoileriksi (merki- tään kirjaimella S). Pelaajat D ja S pelaavat r kierrosta kestävän EF-pelin, jota merkitään EF^r(A,B). Pelaajan D tavoite pelissä on osoittaa, että mallit A ja B ovat samankaltaisia, eikä niitä siis voi erottaa toisistaan. Pelaaja S taas pyrkii osoittamaan, että mallit Aja B eroavat toisistaan.

EF-pelin kullakin kierroksella 1 ≤ i ≤ r pelaajat suorittavat seuraavat siirrot:

• Pelaaja S valitsee toisen malleista A tai B sekä jonkin tämän mal- lin alkion. Pelaaja S valitsee siis alkion a_i ∈ Dom(A) tai alkion b_i ∈ Dom(B).

• Pelaaja D vastaa valitsemalla alkion toisesta mallista siten, että jos pelaaja S valitsi alkion a_i ∈ Dom(A), pelaaja D valitsee alkion b_i ∈ Dom(B). Vastaavasti jos pelaaja S valitsi alkionb_i ∈Dom(B), valitsee pelaaja D alkiona_i ∈Dom(A).

Seuraavaksi määritelläänosittainen isomorfismi, minkä jälkeen tarkastel- laan EF-pelin voittotilannetta.

Määritelmä 3.1. Olkoot A ja B σ-malleja. Olkoon aakkosto σ relationaa- linen ja olkoot ~a = (a₁, . . . , a_n) ∈ Aⁿ ja~b = (b₁, . . . , b_n) ∈ Bⁿ. Pari (~a,~b) määrittää mallien A ja B välisen osittaisen isomorfismin, jos seuraavat eh- dot pätevät:

• Jokaisella i, j ≤n pätee

a_i =a_j jos ja vain josb_i =b_j.

• Jokaisella aakkostonσ vakiosymbolillac ja jokaisella i≤n pätee a_i =c^A jos ja vain josb_i =c^B.

• Jokaisella aakkostonσ k-paikkaisella relaatiosymbolilla P ja jokaisella jonolla indeksejä (i₁, . . . , i_k)∈[1, n] pätee

(a_i1, . . . , a_ik)∈P^A jos ja vain jos (b_i1, . . . , b_ik)∈P^B.

Merkitään kaikkien osittaisisomorfismien joukkoa P art(A,B). Jos pari (~a,~b) määrittää mallien A ja B välisen osittaisen isomorfismin, merkitään

~a7→~b∈P art(A,B).

Kun EF-peliä on pelattunkierrosta, pelaajat ovat tehneet siirrot (a₁, . . . , a_n) ja (b₁, . . . , b_n). Olkoot c₁, . . . , c_l aakkostonσ vakiosymbolit. Tällöin mer- kitään ~c ^A = (c^A₁, . . . , c^A_l) ja vastaavasti ~c ^B = (c^B₁, . . . , c^B_l ). Pelaaja D voit- taa EF-pelin, jos pelin tuloksena syntyvä (~a,~b) on voittotilanne pelaajalle D.

Tämä pätee jos ((~a, ~c ^A),(~b,~c ^B)) on osittainen isomorfismi mallien A ja B välillä.

Pelaajan EF-pelissä käyttämä pelistrategia on joukko sääntöjä, jotka sa- novat pelaajalle täsmälleen miten tämän tulee pelata riippuen pelissä aiem- min tehdyistä siirroista. Sanotaan, että pelaaja käyttää EF-pelissä tiettyä strategiaa, jos pelaajan jokainen pelissä tekemä siirto noudattaa tämän stra- tegian sääntöjä.

Määritellään seuraavaksi EF-pelin voittostrategia sekä esitetään sitä kos- keva lause 3.1. Tämän jälkeen esitetään viisi esimerkkiä voittostrategiois- ta. Näistä esimerkeistä kahdessa kuvaillaan voittostrategioita tapauksessa, jossa tutkittavat mallit ovat yksinkertaisia joukkoja. Kahdessa esimerkissä kuvaillaan voittostrategioita yksinkertaisten verkkojen tapauksessa. Viimei- sessä viidennessä esimerkissä kuvaillaan voittostrategiaa lineaarijärjestysten tapauksessa.

Määritelmä 3.2. Sanotaan, että pelaajalla D on voittostrategia pelissä EF^r(A,B), jos pelaaja D pystyy aina pelissä valitsemaan alkionsa siten, että pelaaja D voittaa pelin r kierroksen jälkeen riippumatta siitä, mitä alkioita pelaaja S pelissä valitsee. Merkitään A'_r B, jos pelaajalla D on voittostra- tegia pelissä EF^r(A,B).

Merkinnällä (A, ~a) '_r (B,~b) tarkoitetaan, että pelaajalla D on voitto- strategia, kun EF-peliä jatketaan tilanteesta, jossa pelissä on pelattu tietyt alkiot.

Huomautus. Jos A '_n B pätee, niin silloin pätee myös A '_r B kaikilla r≤n.

Huomautus. Pelaajalla S on voittostrategia pelissä EF^r(A,B), jos pelaajalla D ei ole voittostrategiaa kyseisessä pelissä. Esitetään tämä asia seuraavaksi lauseena.

Lause 3.1. Täsmälleen toisella pelaajista D ja S on voittostrategia pelissä EF^r(A,B).

Tämän lauseen todistusta hahmotellaan esimerkiksi lähteessä [3, s. 53].

Esimerkki 3.1. Sisältäköön aakkostoσkaksipaikkaiset funktiosymbolit +, : ja<. Olkoot Q=hQ,+^Q,:^Q, <^Qija Z=hZ,+^Z,:^Z, <^Ziaakkostonσ malleja.

Symbolit +^Q ja +^Z tarkoittavat malleissa tavallisia rationaalilukujen ja ko- konaislukujen yhteenlaskuja, :^Q ja :^Z tarkoittavat tavallisia rationaalilukujen ja kokonaislukujen jakolaskuja ja <^Q ja <^Z tarkoittavat tavallisia rationaali- lukujen ja kokonaislukujen järjestyksiä. Tarkastellaan peliä EF³(Q,Z).

Pelaaja S voi voittaa pelin EF³(Q,Z) esimerkiksi pelaamalla seuraavasti:

Pelaaja S valitsee pelin ensimmäisellä kierroksella alkion a₁ = 5 ∈ Z.

Pelaaja D vastaa tähän valitsemalla alkion b1 ∈Q.

Pelin toisella kierroksella pelaaja S valitsee alkion a2 = 6∈ Z. Siis a1 <

a₂. Nyt pelaajan D on vastattava tähän valitsemalla sellainen alkio b₂ ∈ Q, jolle päteeb₁ < b₂.

Pelin kolmannella kierroksella pelaaja S valitsee alkion b₃ = ^b1+b₂ ² ∈ Q.

Nyt koska b1 < b2, pätee b1 < ^b1+b₂ ² < b2. Pelaaja D ei nyt pysty valitsemaan sellaista alkiotaa₃ ∈Z, jolle pätisi 5< a₃ <6, jolloin pelaaja S voittaa pelin EF³(Q,Z).

Esimerkki 3.2. Tarkastellaan verkkoja G = hV, E^Gi ja H = hW, E^Hi, missä V = {a, b, c}, E^G = {{a, b},{b, c},{a, c}}, W = {1,2,3,4,5,6} ja E^H={{1,2},{2,3},{3,4},{4,5},{5,6},{1,5}}.

Osoitetaan, että pelaajalla S on voittostrategia pelissä EF³(G,H).

Tarkastellaan peliä EF³(G,H). Pelaaja S voi valita pelin kierroksilla esi- merkiksi verkon G solmut a, b ja c. Tällöin valitut solmut ja niiden välillä olevat särmät muodostavat piirin. Pelaaja D ei voi valita solmuja verkosta H siten, että niiden väliset särmät muodostaisivat piirin. Siis pelaajalla S on voittostrategia pelissä EF³(G,H).

Esimerkki 3.3. Tarkastellaan verkkojaG=hV, E^Gi jaH=hW, E^Hi, missä V = {a, b, c, d}, E^G = {{a, b},{b, c},{a, c},{c, d}}, W = {1,2,3} ja E^H = {{1,2},{2,3}}.

Osoitetaan, että pelaajalla D on voittostrategia pelissä EF²(G,H).

Kuvaillaan pelaajan D voittostrategia pelissä EF²(G,H). Pelin ensimmäisen kierroksen mahdolliset siirrot ovat:

• Jos pelaaja S valitsee alkionc, vastaa pelaaja D alkiolla 2.

• Jos pelaaja S valitsee alkion 2, vastaa pelaaja D alkiollac.

• Jos pelaaja S valitsee jonkin alkioistaa,btaid, vastaa pelaaja D alkiolla 1.

• Jos pelaaja S valitsee toisen alkioista 1 tai 3, vastaa pelaaja D alkiolla a.

Pelin toisella kierroksella pelaaja D voi aina vastata pelaajan S siirtoon siten, että jos valitut verkonGalkiot muodostavat särmän, niin myös valitut verkonHalkiot muodostavat särmän. Vastaavasti, jos valitut verkonGalkiot eivät muodosta särmää, voi pelaaja D tehdä toisen kierroksen valintansa siten, että valitut verkon H alkiot eivät muodosta särmää. Siis pelaajalla D on voittostrategia pelissä EF²(G,H).

Esimerkki 3.4. Tarkastellaan tyhjän aakkoston σ malleja A ja B. Olkoot

|A|,|B| ≥n. Osoitetaan, ettäA'_nB.

Kuvaillaan pelaajan D voittostrategiaa. Oletetaan, että EF-peliä on pe- lattu i kierrosta ja näillä kierroksilla on pelattu alkiot (a₁, . . . , a_i) ∈ A ja (b₁, . . . , b_i) ∈ B. Oletetaan, että pelaaja S valitsee pelin kierroksella i+ 1 alkion a_i+1 ∈ A. Jos a_i+1 = a_j pätee ehdolla i ≥ j, vastaa pelaaja D valit- semalla alkion b_i+1 = b_j ∈B. Muutoin pelaaja D vastaa pelaajan S siirtoon valitsemalla jonkin alkionb_j+1 ∈B−{b₁, . . . , b_i}(tällainen alkio on olemassa, koska oletuksen mukaan|B| ≥n).

Näin pelaamalla pelaaja D voittaa pelin, koska riippumatta siitä, minkä alkion pelaaja S valitsee pelin kullakin kierroksella, pystyy pelaaja D aina

vastaamaan valitsemalla pelattavan alkion vastaavasti kuin pelaaja S valit- si. Koska |A|,|B| ≥ n, alkioita riittää valittaviksi kummassakin mallissa n kierroksen ajaksi.

Esimerkki 3.5. Olkoon aakkosto σ = {<}. Oletetaan, että L₁ ja L₂ ovat järjestettyjä joukkoja siten, että |L₁|,|L₂| ≥ n. Oletetaan myös, että L₁ ja L2 ovat eri pituiset. Tutkitaan päteekö L1 'nL2.

Nähdään helposti, että L₁ '_n L₂ ei päde yleisesti edes tilanteessan= 2.

Oletetaan, ettäL₁ sisältää kolme alkiota {1,2,3}ja L₂ sisältää kaksi alkiota {1,2}. Järjestys on lukujen tavallinen järjestys tarkasteltavissa järjestetyissä joukoissa L₁ ja L₂. Pelaaja S valitsee ensimmäiseksi alkion 2∈L₁. Pelaajan D on vastattava valitsemalla toinen alkioista 1 tai 2 ∈ L₂. Oletetaan, että pelaaja D vastaa valitsemalla alkion 1 ∈ L2. Tällöin pelaaja S pelaa seu- raavaksi alkion 1 ∈L₁, mikä johtaa pelaajan D häviöön. Pelaajan D pitäisi nimittäin valita lineaarijärjestyksen L₂ alkio, joka on pienempi kuin 1, mikä ei kuitenkaan ole mahdollista. Jos pelaaja D valitsee ensimmäisellä kierrok- sella alkion 2 ∈ L₂, valitsee pelaaja S alkion 3∈ L₁ ja näin ollen pelaaja D häviää taas. Siis L₁ '₂ L₂ ei päde.

Väite L1 'n L2 ei päde, jos järjestettyjen joukkojen L1 ja L2 pituudet eivät ole riittävän suuria. Pelaajalla D on voittostrategia silloin, kun järjetetyt joukotL₁ jaL₂sisältävät paljon enemmän alkioita kuin pelissä on kierroksia.

Tämän osoittaa seuraava lause. Tässä työssä esitetään lauseelle yksi todistus, toinen todistus löytyy esimerkiksi lähteestä [2, s. 30-31].

Lause 3.2. Olkoon r >0 ja olkoot A ja B järjestettyjä joukkoja siten, että

|A|,|B| ≥2^r. Tällöin A'_r B.

Todistus. Vrt. [2, s. 29-31]. Laajennetaan aakkostoa kahdella uudella vakio- symbolilla, minja max, jotka tarkoittavat järjestettyjen joukkojen pienintä ja suurinta alkiota. Osoitetaan, että A '_r B pätee tässä laajennetussa aak- kostossa.

Olkoon mallin A universumi joukko {1, . . . , n} ja olkoon mallin B uni- versumi joukko {1, . . . , m}. Järjestys on malleissa A ja Blukujen tavallinen järjestys. Oletetaan, ettän, m≥2^r+ 1. Universumin alkioidenxjay välinen etäisyys määritellään kaavalla d(x, y) = |x−y|. Osoitetaan, että pelaaja D voi pelata siten, että ipelatun kierroksen jälkeen pätee seuraava tilanne.

(∗) Olkoot~a= (a−1, a₀, a₁, . . . , a_i) ja~b= (b−1, b₀, b₁, . . . , b_i), missäa₁, . . . , a_i jab1, . . . , biovat pelin kierroksilla 1, . . . , ipelatut alkiot jaa−1 =min^A, b−1 = min^B, a₀ = max^A, b₀ = max^B. Tällöin voidaan olettaa olevan voimassa seuraava tilanne kaikilla −1≤j, l ≤i:

1. Jos d(a_j, a_l)<2^r−i, niin d(b_j, b_l) =d(a_j, a_l).

2. Jos d(a_j, a_l)≥2^r−i, niin d(b_j, b_l)≥2^r−i. 3. a_j ≤a_l ⇔b_j ≤b_l.

Todistetaan induktiolla i:n suhteen, että pelaaja D voi pelata pelin jokai- sella kierroksellaisiten, että (∗) pätee. Tapausi= 0 on selvä, sillä oletuksesta

|A|,|B| ≥2^r seuraad(a−1, a₀)≥2^r ja d(b−1, b₀)≥2^r.

Tehdään sitten induktio-oletus, että pelaaja D on pelannut pelissä siten, että (∗) päteei:llä. Osoitetaan, että pelaaja D voi vastata pelaajan S seuraa- vaan siirtoon niin, että (∗) päteei+ 1:llä. Oletetaan, että pelaaja S valitsee kierroksella i+ 1 alkion mallista A (tapaus alkion valinta mallista B vas- taavasti). Jos pelaaja S valitsee sellaisen alkion a_j ∈ A, jolle j ≤ i, vastaa pelaaja D valitsemalla alkion b_j ja (∗) pätee triviaalisti. Muutoin pelaajan S valitsema alkio sijaitsee jollakin välillä, joka olkoon sellainen, ettei siltä ole valittu pelissä aiemmin yhtään alkiota. Olkoon tälle pelaajan S valitsemalle alkiolle a_j < a_i+1 < a_l. Nyt on kaksi mahdollista tapausta:

• d(a_j, a_l)<2^r−i. Tällöind(b_j, b_l) =d(a_j, a_l) ja välit [a_j, a_l] ja [b_j, b_l] ovat yhtä pitkät. Siksi on olemassa sellainen alkio b_i+1, että d(a_j, a_i+1) = d(b_j, b_i+1) jad(a_i+1, a_l) = d(b_i+1, b_l). Väite pätee siisi+ 1:llä.

• d(a_j, a_l) ≥ 2^r−i. Tässä tapauksessa on d(b_j, b_l) ≥ 2^r−i. Nyt on kolme mahdollista tapausta:

1. d(a_j, a_i+1) < 2^r−(i+1). Tällöin d(a_i+1, a_l) ≥ 2^r−(i+1) ja alkio b_i+1 voidaan valita siten, että d(b_j, b_i+1) = d(a_j, a_i+1) ja d(b_i+1, b_l) ≥ 2^r−(i+1).

2. d(a_i+1, a_l) < 2^r−(i+1). Tämä tapaus on samankaltainen edellisen kanssa.

3. d(aj, ai+1) ≥ 2^r−(i+1) ja d(ai+1, al) ≥ 2^r−(i+1). Koska d(bj, bl) ≥ 2^r−i, voidaan alkio b_i+1 valita välin [b_j, b_l] keskeltä ja siten varmis- taa, että d(b_j, b_i+1)≥2^r−(i+1) ja d(b_i+1, b_l)≥2^r−(i+1).

Siis kaikissa näissä tapauksissa (∗) päteei+ 1:llä.

Näin todistettiin, että pelaaja D voi voittaarkierroksen EF-pelin mallien A ja Bvälillä ja siten A'_rB.

3.2 EF-peliin liittyviä määritelmiä ja lauseita

Tässä alaluvussa esitetään EF-peliin liittyviä määritelmiä ja lauseita. Ensim- mäiseksi esitetään EF-pelin tarkastelujen kannalta tärkeä kaavojen kvantto- riasteen määritelmä. Tämän jälkeen esitetään EF-lause sekä sille kolme seu- rauslausetta.

Määritelmä 3.3. Logiikan FO kaavan ϕ kvanttoriaste qr(ϕ) määritellään seuraavasti:

• Jos ϕon atomikaava, niinqr(ϕ) = 0.

• qr(¬ϕ) = qr(ϕ).

• qr(ϕ₁∧ϕ₂) =qr(ϕ₁∨ϕ₂) =max{qr(ϕ₁), qr(ϕ₂)}.

• qr(∃xϕ) =qr(∀xϕ) =qr(ϕ) + 1.

Merkintä FO[k] tarkoittaa kaikkien niiden FO-kaavojen ϕjoukkoa, joille pätee qr(ϕ)≤k.

Kaavan kvanttoriaste ei yleisesti ottaen ole sama kuin siinä käytetty- jen kvanttorien lukumäärä. Voidaan esimerkiksi määritellä joukko kaavoja induktiolla seuraavasti: d₀(x, y) ≡ E(x, y), ja d_k(x, y) ≡ ∃z(dk−1(x, z) ∧ dk−1(z, y)). Tällöin qr(d_k) = k, mutta kaavassa d_k käytettyjen kvanttorien kokonaismäärä on 2^k−1. Kaavoille, joissa kaikki kvanttorit ovat kaavan edes- sä, kvanttoriaste on kuitenkin sama kuin kaavassa käytettyjen kvanttorien lukumäärä.

Olkoon S joukko aakkoston σ FO-lauseita. Kaksi σ-mallia A ja B to- teuttavat samat joukon S lauseet, jos kaikille joukon S lauseille Φ pätee A|= Φ⇔B|= Φ.

Lause 3.3 (EF-lause). Olkoot A ja B relationaalisen aakkoston malleja.

Tällöin seuraavat ehdot ovat yhtäpitäviä.

1. Mallit A ja B toteuttavat samat FO[r]-kaavat.

2. A'_r B.

EF-lause on hyödyllinen määrittelemättömyystuloksia todistettaessa. EF- lause todistetaan seuraavassa alaluvussa 3.4.

Seuraavaksi esitettävää seurauslausetta käytetään määrittelemättömyys- tulosten todistamisessa.

Seurauslause 3.4. Oletetaan, että aakkosto σ on äärellinen. Äärellisten σ- mallien ominaisuus P ei ole määriteltävissä logiikassa FO, jos ja vain jos jokaisella r ∈ N on olemassa kaksi äärellistä äärellisen aakkoston omaavaa σ-mallia Ar ja Br siten, että pätee:

jos A_r '_r B_r ja mallilla A_r on ominaisuus P, niin mallilla B_r ei ole ominaisuutta P.

Todistetaan tämä seurauslause seuraavaksi toiseen suuntaan. Toisen suun- nan todistus esitetään myöhemmin.

Todistus. Vrt. [2, s. 33]. Tehdään vastaoletus, että ominaisuus P voidaan määritellä lauseella Φ. Olkoon r =qr(Φ) ja olkoot A_r ja B_r kaksi äärellistä σ-mallia, joille pätee A_r '_r B_r. Siis jos mallilla A_r on ominaisuus P, niin myös mallilla B_r on ominaisuus P, mikä on ristiriidassa oletusten kanssa.

Siis vastaoletus on väärin ja ominaisuus P ei ole määriteltävissä logiikassa FO.

Huomautus. Jos aakkostoσ on ääretön, pätee implikaatio yllä olevassa seu- rauslauseessa.

Huomautus. Yllä olevan seurauslauseen ominaisuuksia voidaan ajatella Boo- len kyselyinä q. Boolen kysely q(A) = 1, jos ominaisuus pätee mallille A, ja vastaavasti q(A) = 0 jos mallillaA ei ole kyseistä ominaisuutta.

EF-pelit ovat täydellisiä kuvaamaan FO-määriteltävyyttä, kun aakkosto on äärellinen. Pelien käyttö helpottaa usein määriteltävyyskysymysten tut- kimista. Ilman pelejäkin voidaan esimerkiksi todistaa, että tyhjän aakkoston σ tapauksessaparillisuusei ole FO-määriteltävä (ks. [2, s. 25]). Käyttämällä kyseistä menetelmää ei kuitenkaan voida osoittaa, että parillisuusei ole FO- määriteltävä äärellisten lineaarijärjestysten tapauksessa. Muita menetelmiä käyttäen tämän osoittaminen on paljon vaikeampaa kuin EF-pelejä käyttä- mällä. Seuraavassa seurauslauseessa nähdään, kuinka helposti kyseinen väite voidaan todistaa EF-pelien avulla.

Seurauslause 3.5. Parillisuus ei ole FO-määriteltävä äärellisten lineaari- järjestysten tapauksessa.

Todistus. Vrt. [2, s. 33]. Olkoon A_r lineaarijärjestys, jossa on 2^r alkiota ja olkoon B_r lineaarijärjestys, jossa on 2^r+ 1 alkiota. Nyt lauseen 3.2 mukaan A_r '_rB_r ja väite seuraa suoraan seurauslauseesta 3.4.

3.3 Tyypit

Tässä alaluvussa käsitellään tarkemmin logiikkaa FO[r], ja tutustutaan tyyp- pien käsitteeseen.

Ensimmäiseksi tässä alaluvussa tarkastellaan logiikkaa FO[0]. Se koostuu atomikaavojen Boolen kombinaatioista. FO[0]:n lauseet ovat kvanttorittomia.

Relaationaalisen aakkoston σ tapauksessa tällaiset lauseet ovat Boolen kom- binaatioita muotoa c = c⁰ ja muotoa R(c₁, . . . , c_r) olevista kaavoista, joissa c, c⁰, c₁, . . . , c_r ovat aakkoston σ vakiosymboleja.

Seuraavaksi oletetaan, että ϕ on FO[r+ 1]-kaava. Jos ϕ = ϕ₁ ∨ϕ₂ tai ϕ = ϕ₁ ∧ϕ₂, niin sekä ϕ₁ että ϕ₂ ovat FO[r+ 1]-kaavoja. Jos ϕ = ¬ϕ₁, niin ϕ₁ ∈ FO[r+ 1]. Kuitenkin jos ϕ=∃xψ tai ϕ =∀xψ, niin ψ on FO[r]- kaava. Siten jokainen FO[r+ 1]:n kaava on ekvivalentti muotoa ∃xψ (missä ψ ∈ FO[r]) olevien kaavojen Boolen kombinaation kanssa. Tätä käyttäen voidaan todistaa seuraava apulause.

Apulause 3.6. Olkoon aakkostoσ on äärellinen. Tällöin FO[r]sisältää loo- gista ekvivalenssia vaille vain äärellisen määrän aakkoston σ kaavoja, joissa on m vapaata muuttujaa x₁, . . . , x_m.

Todistus. Vrt. [2, s. 34]. Todistetaan väite induktiolla r:n suhteen. Perusta- paus FO[0] sisältää vain äärellisen määrän sellaisia atomikaavoja, joiden va- paat muuttujat ovat joukossa x₁, . . . , x_m. FO[0] sisältää siten vain äärellisen

määrän näiden kaavojen boolen kombinaatioita, joista jokainen on ekviva- lentti sellaisen disjunktiivisen normaalimuodon kanssa, joka ei sisällä toistoa.

Tehdään induktio-oletus, että väite pätee FO[r]:n tapauksessa. Osoite- taan, että väite pätee FO[r+ 1]:n tapauksessa.

Muistetaan, että jokainen FO[r + 1]:n kaava ϕ(x₁, . . . , x_m) on boolen kombinaatio kaavoista∃x_m+1ψ(x₁, . . . , x_m, x_m+1), joissaψ ∈F O[r]. Nyt ole- tuksen mukaan m+ 1 vapaata muuttujaa (x₁, . . . , x_m+1) sisältävien FO[r]- kaavojen määrä on loogista ekvivalenssia vaille äärellinen ja siten väitteen voidaan päätellä pätevän myös m vapaata muuttujaa sisältävien FO[r+ 1]- kaavojen tapauksessa.

Määritellään seuraavaksi tyypit.

Määritelmä 3.4. Olkoon aakkosto σ relationaalinen. Olkoon A σ-malli ja olkoon~a ∈A^m. Tällöin mallinAja jonon~a r-tyyppi määritellään seuraavasti:

tp_r(A, ~a) ={ϕ∈F O[r]|A, ~a|=ϕ(~x)}.

Mikä tahansa joukko muotoa tp_r(A, ~a) olevia kaavoja on r-tyyppi.

Erityistapauksessa m = 0 tp_r(A) määritellään joukoksi FO[r]-lauseita, jotka pätevät mallissa A. Jokaisella kaavalla ϕ(x₁, . . . , x_m) ∈ FO[r] pätee ϕ∈S tai ¬ϕ∈S, josS onr-tyyppi.

Nyt näyttäisi siltä, että r-tyypit ovat luonnostaan äärettömiä. Sitä ne ovatkin, mutta r-tyyppejä tarkasteltaessa riittää, että mukaan otetaan ää- rellinen määrä kaavoja. Tiedetään, että FO[r] sisältää ekvivalenssia vaille ää- rellisen määrän kaavoja, joissa on m vapaata muuttujaa. Olkoot ϕ₁(~x), . . . , ϕ_M(~x) kaikki sellaiset FO[r]:n epäekvivalentit kaavat, joissa esiintyy vapaat muuttujat ~x = (x₁, . . . , x_m). Jokaisen r-tyypin määritellään vastaavan tiet- tyä joukon {1, . . . , M} sellaista osajoukkoa K, johon indeksit i kuuluvat.

Yksinkertaisella kaavalla

α_K(~x)≡ ^{^}

i∈K

ϕ_i

voidaan testata, että jono ~x toteuttaa kaikki sellaiset kaavat ϕ_i, joille pätee i∈K ja että jono~xei toteuta sellaisia kaavoja ϕ_j, joille pätee j /∈K.

Huomataan, että kaavaα_K(~x) on myös FO[r]-kaava, koska siinä ei esiinny yhtään uutta kvanttoria.

Kaikki kaavatα_K ovat toisensa poissulkevia. Siis indeksijoukoilleK 6=K⁰ pätee: jos A |= α_K(~a) niin A |= ¬α_K⁰ (~a). Jokainen FO[r]-kaava saadaan joidenkin kaavojenαK disjunktiona. Seuraava lause toimii yhteenvetona yllä esitetyistä asioista.

Lause 3.7. Vrt. [2, s. 35]. a) Olkoon relationaalinen aakkosto σ äärellinen.

Tällöin sen erilaisten r-tyyppien määrä on äärellinen.

b) Olkoon T₁, . . . , T_s listaus kaikista r-tyypeistä. Tällöin on olemassa sel- laiset FO[r]-kaavat α₁(~x), . . . , α_s(~x), että seuraavat ehdot pätevät:

• jokaisella mallilla A ja jonolla~a∈A^m pätee A|=α_i(~a) jos ja vain jos tp_r(A, ~a) =T_i, ja

• jokainen sellainen FO[r]-kaava ϕ(~x), joka sisältää m vapaata muuttu- jaa, vastaa joidenkin kaavojen α_i disjunktiota.

r-tyypit yhdistetään yleensä niitä määrittäviin kaavoihin α_i. On tärkeää muistaa, että näillä kaavoilla on samat kvanttoriasteet r.

EF-lauseesta ja lauseesta 3.7 saamme seuraavan seurauslauseen.

Seurauslause 3.8. Oletetaan, että aakkosto σ on äärellinen. Ekvivalenssi- relaatiolla 'r on äärellinen määrä ekvivalenssiluokkia.

Seuraavaksi osoitetaan, että pelit ovat täydellisiä logiikan FO ilmaisuvoi- man kuvailussa.

Seurauslause 3.9. OminaisuusP on ilmaistavissa logiikassaFOjos ja vain jos on olemassa r siten, että kaikilla malleilla A ja B pätee:

jos A∈P ja A'_rB, niin B∈P.

Todistus. Vrt. [2, s. 35]. Jos ominaisuus P voidaan ilmaista logiikan FO lauseella Φ, olkoon r = qr(Φ). Jos A ∈ P, niin A |= Φ. Siis mallille B, jolle päteeA'_r B, on B|= Φ ja edelleenB∈P.

Käänteisesti, jos ehdoista A ∈ P ja A '_r B seuraa B ∈ P, niin mil- le tahansa kahdelle mallille, joilla on sama tyyppi, pätee toinen seuraavista tilanteista. Joko molemmilla malleilla on ominaisuus P tai kummallakaan mallilla ei ole ominaisuutta P. Siten P on tyyppien unioni ja siis määritel- tävissä joidenkin kaavojen αi disjunktiona. Kyseiset kaavat αi määritellään tässä luvussa aiemmin esitetyllä kaavalla α_K(~x)≡^V_i∈Kϕ_i∧^V_{j /∈K}¬ϕ_j.

Ominaisuus P ei siis ole ilmaistavissa logiikassa FO, jos ja vain jos jokai- sellar:llä löytyy kaksi sellaista malliaA_r jaB_r, joille päteeA_r '_r B_r, mutta mallillaAr on ominaisuus P ja mallillaBr ei ole ominaisuutta P.

Esitetään vielä tämän alaluvun lopuksi seurauslausem-paikkaisten kyse- lyjen q määriteltävyydestä logiikassa FO.

Seurauslause 3.10. σ-mallien m-paikkainen kysely q ei ole määriteltävissä logiikassa FO, jos ja vain jos jokaisella r ∈ N on olemassa kaksi äärellistä σ-mallia A_r ja B_r ja kaksi m-jonoa~a ∈A^m ja~b∈B^m siten, että seuraavat ehdot pätevät:

• (A_r, ~a)'_r (B_r,~b), ja

• ~a∈q(A_r) ja~b /∈q(B_r).