Ehrenfeuchtin ja Fraïssén peli

TAMPEREEN YLIOPISTO Pro gradu -tutkielma

Piia Nieminen

Ehrenfeuchtin ja Fraïssén peli

Matematiikan ja tilastotieteen laitos Matematiikka

Marraskuu 2008

Tampereen yliopisto

Matematiikan ja tilastotieteen laitos

NIEMINEN, PIIA: Ehrenfeuchtin ja Fraïssén peli Pro gradu -tutkielma, 30 s.

Matematiikka Marraskuu 2008

Tiivistelmä

Ehrenfeuchtin ja Fraïssén peli sai alkunsa ranskalaisen Roland Fraïssén tut- kimuksista elementaarisen ekvivalenssin parissa. Myöhemmin puolalais-ame- rikkalainen Andrzej Ehrenfeucht antoi Fraïssén saavuttamille tuloksille peli- teoreettisen muotoilun. Ehrenfeuchtin ja Fraïssén peli on malliteorian mene- telmä, joka perustuu struktuurien samanlaisuuden tarkasteluun. Menetelmä on osoittautunut erityisen hyödylliseksi logiikoiden ilmaisuvoiman tutkimuk- sissa. Tässä tutkielmassa Ehrenfeuchtin ja Fraïssén peliä käsitellään äärellis- ten mallien teorian kannalta. Osoitetaan, että kyseinen menetelmä riittää ka- rakterisoimaan ensimmäisen kertaluvun logiikan ilmaisuvoiman. Lisäksi kä- sitellään Ehrenfeuchtin ja Fraïssén pelin hyödyllisyyttä toisen kertaluvun lo- giikassa. Osoitetaan, että eräs Ehrenfeuchtin ja Fraïssén pelin laajennus riit- tää karakterisoimaan eksistentiaalisen monadisen toisen kertaluvun logiikan ilmaisuvoiman.

Sisältö

1 Johdanto 3

2 Valmistelevia tarkasteluita 4

2.1 Käsitteitä . . . 4

2.2 Ensimmäisen kertaluvun logiikka . . . 6

2.2.1 Syntaksi . . . 6

2.2.2 Semantiikka . . . 8

3 Samanlaisuus 10 3.1 Isomorsmi . . . 11

3.2 Elementaarinen ekvivalenssi . . . 12

4 Ehrenfeuchtin ja Fraïssén peli 15 5 Ensimmäisen kertaluvun logiikan ilmaisuvoima 19 5.1 Ehrenfeuchtin ja Fraïssén lause . . . 21

5.2 EF-peli FO-logiikan ilmaisuvoiman kuvaajana . . . 23

6 Toisen kertaluvun logiikan ilmaisuvoima 24 6.1 Toisen kertaluvun logiikka . . . 24

6.2 EF-pelin sovellukset SO-logiikan ilmaisuvoiman kuvaajana . . 26

Viitteet 30

1 Johdanto

Klassinen malliteoria on matemaattiseen logiikkaan pohjautuva osa-alue, jo- ka tutkii matemaattisten struktuurien ominaisuuksia ja luokittelua. Tutki- mukset ovat keskittyneet pääosin äärettömiin struktuureihin tai sellaisiin struktuuriluokkiin, jotka sisältävät sekä äärellisiä että äärettömiä struktuu- reita. Klassisen malliteorian tulokset ovat antaneet tärkää tietoa ensimmäi- sen kertaluvun logiikan ominaisuuksista ja ilmaisuvoimasta, mutta toisaalta äärellisiin struktuureihin rajoituttaessa tärkeimmät tulokset ovat osoittau- tuneet hyödyttömiksi. Äärellisiin struktuureihin rajoittuminen tuli aiheelli- seksi, kun tietotekniikan ja tietojenkäsittelytieteen kehitys toi tullessaan mo- nia malliteorialle läheisiä ongelmia. Muun muassa tietokantateorian, lasket- tavuuden ja tietojenkäsittelytieteen formaalien kielten ongelmat olivat hel- posti kuvattavissa logiikan ja malliteorian menetelmin. Klassinen malliteoria pitäytyi kuitenkin omissa tutkimuskohteissaan ja tuloksissaan. Tietojenkä- sittelytieteen ongelmia syntyi ratkomaan uusi suuntaus - äärellisten mallien teoria - johon on myöhemmin viitattu myös tietojenkäsittelytieteen logiikka- na [7, s. 1].

Olennaisimpien tulosten hyödyttömyydesta huolimatta klassisen malli- teorian menetelmien joukosta löytyy tapauksia, joita myös äärellisten mal- lien teoria on soveltanut hyvinkin menestyksekkäästi. Yksi näistä harvoista menetelmistä on Ehrenfeuchtin ja Fraïssén peli, lyhyemmin EF-peli, joka pe- rustuu kahden struktuurin samanlaisuuden tarkasteluun. EF-peli sai alkunsa ranskalaisen Roland Fraïssén menetelmästä kuvata struktuurien elementaa- rista ekvivalenssia. Puolalais-amerikkalainen Andrzej Ehrenfeucht muotoili Fraïssén algebrallista hahmotelmaa niin, että se soveltui myös peliteoreet- tisiin tarkasteluihin. Pelin kulku perustuu edestakaisin-menetelmään (back- and-forth method), jossa kaksi pelaajaa valitsee kahden struktuurin alkioi- ta tiettyjen sääntöjen mukaisesti. Toinen pelaajista pyrkii osoittamaan, että tarkasteltavat struktuurit ovat erilaiset, kun toinen pelaaja puolustaa struk- tuurien samanlaisuutta. EF-pelillä ja sen kehitelmillä on saavutettu tärkeitä tuloksia muun muassa ensimmäisen ja toisen kertaluvun logiikan ilmaisuvoi- maan liittyen.

Tämän tutkielman tavoite on esitellä havainnollisesti mutta täsmällisesti Ehrenfeuchtin ja Fraïssén peliä ja sen hyödyllisyyttä ensimmäisen kertaluvun logiikan sekä toisen kertaluvun logiikan ilmaisuvoiman kuvaamisessa. Lukijal- ta odotetaan yliopistotasoisen matematiikan perusteiden hallintaa ja erityi- sesti logiikan perusteiden ymmärtämistä. Koska kirjallisuudessa merkinnät ja määritelmät eroavat monin tavoin toisistaan, eikä yhdenkään yksittäisen teoksen tyyli tuntunut sellaisenaan tutkielmaan sopivalta, tekijä on katso- nut parhaaksi käyttää toisen luvun tarvittavien käsitteiden ja merkintöjen huolelliseen esittelyyn. Tutkielman kolmannessa luvussa käsittellään kahta olennaista samanlaisuuden käsitettä ja esitellään osa Fraïssén elementaari-

sen ekvivalenssin hahmotelmasta. Toisen ja kolmannen luvun tärkeimmäksi lähdeteokseksi voidaan lukea Ebbinghausin, Flumin ja Thomasin kirja Mat- hematical Logic [2], joka käsittelee matemaattista logiikkaa laajasti mutta täsmällisesti. Myös Libkinin teos Elements of Finite Model Theory [4] sekä Ebbinghausin ja Flumin teos Finite Model Theory [1] ovat olleet mainitta- vassa osassa. Neljännessä luvussa keskitytään EF-pelin ja sen ominaisuuksien esittelyyn. Edellä mainittujen teosten lisäksi neljännessä luvussa oli suurena apuna Hodgesin kirja A Shorter Model Theory [3], joka toi hieman erilaisen näkökulman EF-peliin. Tutkielman viides luku käsittelee määriteltävyyttä ja ensimmäisen kertaluvun logiikan ilmaisuvoimaa. Luvussa todistetaan Ehren- feuchtin ja Fraïssén lause ja osoitetaan EF-pelin merkittävyys ensimmäisen kertaluvun logiikan määriteltävyystuloksien kannalta. Viidennessä luvussa tärkeimmäksi lähteeksi osoittautui Libkinin teos [4]. Kyseinen teos on olen- naisessa osassa myös viimeisessä luvussa, jossa EF-pelin hyödyllisyyttä käsi- tellään toisen kertaluvun logiikan ilmaisuvoiman kuvaamisessa. Toisen kerta- luvun logiikan tarkasteluissa uusia näkökulmia toi myös Kolaitis'n ja Libkinin toimittama kokoomateos Finite Model Theory and it's Applications [5].

2 Valmistelevia tarkasteluita

2.1 Käsitteitä

Aakkosto σ on epätyhjä äärellinen joukko vakiosymboleita c₁, . . . , c_n, relaa- tiosymboleitaR₁, . . . , R_n⁰ja funktiosymboleitaf₁, . . . , f_n⁰⁰. Jokaisella relaatio- ja funktiosymbolilla on paikkalukuk ∈N⁺, joka kertoo relaation tai funktion attribuuttien määrän. Käytetäänk paikkaiselle relaatiosymbolille ja k⁰ paik- kaiselle funktiosymbolille yleisiä merkintätapojaR(c₁, . . . , c_k)jaf(c₁, . . . , c_k⁰). Paikkaluku 0 on varattu vakiosymboleille, sillä vakiot voidaan kuvata nolla- paikkaisiksi funktioiksi. Jos aakkosto ei sisällä funktiosymboleita, kutsutaan sitä relationaaliseksi aakkostoksi. Aakkostoa kutsutaan puhtaasti relationaa- liseksi, jos se sisältää ainoastaan relaatiosymboleita. Useimmiten on yksinker- taisempaa keskittyä relationaalisten tai puhtaasti relationaalisten aakkosto- jen käsittelyyn, eikä tämä tuota suurempia ongelmia määritelmien tai todis- tusten kannalta. Palataan relationaalisen aakkoston muodostamiseen myö- hemmin.

Matemaattisessa logiikassa ja äärellisten mallien teoriassa keskeisimpien käsitteiden joukkoon kuuluvat struktuurin ja mallin käsitteet. Vaikka mallilla ja struktuurilla saatetaan suomenkielisessä kirjallisuudessa tarkoittaa samaa- kin asiaa, tässä tutkielmassa kyseiset käsitteet erotetaan toisistaan. Mallin ja struktuurin ero selviää lukijalle ensimmäisen kertaluvun logiikan seman- tiikassa.

Libkinin [4, s. 13] käyttämän esitystavan mukaan aakkoston σ struktuuri A=hA,{c^A_i },{R_i^A},{f_i^A}ikoostuu universumistaA, aakkoston σ vakioiden

tulkinnoista universumin Aalkioiksic^A_i , aakkostonσ k-paikkaisten relaatioi- den tulkinnoista struktuurin A relaatioiksi R^A_i ⊆ A^k sekä aakkoston σ k- paikkaisten funktioiden tulkinnoista struktuurin A funktioiksif_i^A:A^k →A. Vaikka Libkinin käyttämä määritelmä kuvaa struktuurin kokonaisuudessaan riittävällä tavalla, merkintä A =hA,{c^A_i },{R^A_i },{f_i^A}i ei sellaisenaan kerro aakkostonσ symbolien tulkinnasta mitään, vaan esittelee suoraan struktuu- rin A vakiot, relaatiot ja funktiot. Määritellään struktuuri toisella yleisesti käytössä olevalla tavalla, jossa tulkinta käsitetään erillisenä funktiona.

Määritelmä 2.1. Olkoon σ aakkosto, jolloinσ-struktuuri A=hA, αikoos- tuu

• epätyhjästä joukosta A, jota kutsutaan struktuurin A universumiksi tai perusjoukoksi dom(A), ja

• funktiostaα, joka kuvaa aakkostonσ jokaiselle symbolille X tulkinnan α(X) =X^A struktuurissa A.

Nyt aakkoston σ jokaisen vakiosymbolin c tulkinta α(c) = c^A on struktuu- rin A alkio, eli c^A ∈ A. Aakkoston σ k-paikkaisen relaatiosymbolin tulkin- ta α(R) = R^A on struktuurin A k-paikkainen relaatio R^A ⊆ A^k. Edelleen aakkoston σ k-paikkaisen funtion tulkinta α(f) = f^A on struktuurin A k- paikkainen funktio f_i^A :A^k →A. Struktuuri A on äärellinen, jos sen univer- sumi A on äärellinen joukko.

Huomautus. Vakiosymbolien tulkinnat voivat olla samoja. Toisin sanoen voi ollac^A_i =c^A_j, vaikkai6=j pitäisi paikkansa. Relaatiosymbolit voidaan tulkita tyhjiksi, jolloin päteeR^A_i =∅ jollakin tai joillakin i∈ {1, . . . , n}.

Nyt, kun stuktuuri on määritelty täsmällisesti, voidaan jatkossa merkin- nän A = hA, αi sijaan käyttää merkintätapaa A = hA,{c^A_i },{R^A_i },{f_i^A}i. Näin säästytään funktion α tulkintojen erilliseltä esittelyltä.

Esimerkki 2.1. Tarkastella aakkostoa σ, jonka alkioita ovat vakiosymbolit 0 ja 1, kaksipaikkainen järjestysrelaatio ≤ sekä kaksipaikkaiset funktiot · ja +. Tällöin aakkostosta σ voidaan muodostaa muun muassa reaalilukujen ja rationaalilukujen järjestetyt kunnat hR,0^R,1^R,≤^R,+^R,·^Ri ja hQ,0^Q,1^Q,≤^Q ,+^Q,·^Qi[4, s. 13].

Kaikki jatkossa käsiteltävät aakkostot ja struktuurit ovat äärellisiä. Usein aakkostonσstruktuurin vakioita, relaatioita ja symboleita merkitään samoil- la symboleilla kuin aakkostossaσ. Esitellään lyhyesti eräs hyödyllinen struk- tuurityyppi ja sen käsitteistöä. Kyseistä struktuurityyppiä käytetään jatkossa useaan otteeseen.

Määritelmä 2.2. Olkoon σ = {E}, missä E on kaksipaikkainen relaatio- symboli. AakkostonσstruktuuriaG =hG, E^Gikutsutaan verkoksi, kun pätee E^G ⊆G², ja E^G on irreeksiivinen sekä symmetrinen.

Verkon G alkioita kutsutaan solmuiksi. Kun on voimassa (g₁, g₂) ∈ E^G, paria (g₁, g₂) sanotaan särmäksi. Olkoon n lukua 1 suurempi luonnollinen luku ja olkoot E(g₁g₂), E(g₂g₃), . . . , E(gn−1g_n) verkon G relaatioita. Tällöin jonog₁, . . . , g_nmuodostaa polun solmustag₁ solmuung_n. Kun vähintään kol- men solmun mittaisen polun alku- ja loppusolmu on sama, polkua kutsutaan sykliksi. Sanotaan, että verkkoG on yhtenäinen, jos mielivaltaisesta solmusta g ∈G on olemassa polku jokaiseen verkon G solmuung⁰ ∈G.

Esitetään nyt Ebbinghausin, Flumin ja Thomasin [2, s. 120] mukaisesti, kuinka mielivaltaisesta aakkostostaσvoidaan rajoittua puhtaasti relationaa- liseen aakkostoon σ^r. Menettely perustuu funktioiden ja vakioiden käsitte- lyyn kuvauksina, sillä kuvaus on helppo määritellä relaatioksi.

Olkoon σ mielivaltainen aakkosto. Muodostetaan jokaista k-paikkaista funktiosymbolia f₁, . . . , f_n⁰⁰ ∈ σ vastaamaan uusi (k + 1)-paikkainen relaa- tiosymboli F₁, . . . , F_n⁰⁰. Samalla tavoin vakiosymboleita c₁, . . . , c_n ∈ σ vas- tatkoon uudet yksipaikkaiset relaatiosymbolit C₁, . . . , C_n. Puhtaasti relatio- naalinen aakkosto σ^r koostetaan uusista relaatiosymboleista F₁, . . . , F_n⁰⁰ ja C₁, . . . , C_n sekä aakkoston σ relaatiosymboleista R₁, . . . , R_n⁰. Nyt jokainen σ-struktuuri A voidaan käsittää σ^r-struktuurina A^r määrittelemällä struk- tuurin A^r universumi ja tulkinnat alla lueteltujen kohtien mukaisesti.

• Olkoon A^r :=A.

• Olkoon R^Ar :=R^A kaikille relaatiosymboleille R∈σ.

• Määritetään relaatio F^Ar funktion f^A kuvaajaksi siten, että kaikille aakkostonσ k-paikkaisille funktiosymboleillef pätee

F^Ar(a₁. . . a_ka_k+1), jos ja vain jos f^A(a₁, . . . , a_k) = a_k+1.

• Määritetään relaatio C^Ar vakionc^A kuvaajaksi siten, että kaikille aak- koston σ vakiosymboleille c pätee

C^Ar(a), jos ja vain jos c^A=a.

Relationaaliseen aakkostoon rajoittuminen tapahtuu vastaavasti, mutta tällöin vakiot jätetään käsittelemättä. Puhtaasti relationaaliseen aakkostoon rajoittumiseen oikeuttavat lauseet löytyvät todistuksineen Ebbinghausin, Flu- min ja Thomasin kirjasta [2, s. 120-121, 186].

2.2 Ensimmäisen kertaluvun logiikka

2.2.1 Syntaksi

Ensimmäisen kertaluvun logiikka voidaan kuvata kielenä, jonka avulla asioita on mahdollista ilmaista matemaattisesti. Usein käytetään lyhyempää ilmaus- ta FO-logiikka, joka muodostuu englanninkielisestä termistä rst order logic.

Suomenkielisissä lähteissä ensimmäisen kertaluvun logiikan sijaan puhutaan usein predikaattilogiikasta, mutta joissain teoksissa predikaattilogiikan alle luetaan myös korkeamman kertaluvun logiikat. Täten voidaan ajatella, että FO-logiikka on vain yksi useista predikaattilogiikoista. FO-logiikan aakkoston pohjan ja koko syntaksin ytimen muodostavat seuraavat loogiset symbolit:

• muuttujat v₁, v₂, . . .;

• konnektiivit¬, ∨;

• sulkeet (, );

• eksistenssikvanttori∃ ja

• identiteettisymboli =.

Lisäksi FO-logiikan aakkostoon kuuluu olennaisena osana symboliaakkos- to, jonka sisältö vaihtelee sovelluksesta riippuen. Koska loogisten symbolien joukko pysyy muuttumattomana, symboliaakkosto määrittää ensimmäisen kertaluvun logiikan kielen. Jatkossa aakkosto σ on FO-logiikan symboliaak- kosto, ellei toisin mainita.

Aakkoston σ määrittämän FO-logiikan kaavanmuodostussääntöjä varten tarvitaan termin käsite, jolla tarkoitetaan yleisesti predikaattilogiikkojen kaa- vojen yksilöitä eli subjekteja.

Määritelmä 2.3. Termeiksi kutsutaan vain ja ainoastaan niitä symbolijo- noja, jotka voidaan muodostaa soveltamalla sääntöjä (i)-(iii) äärellisen monta kertaa.

(i) Jokainen muuttuja v_i on termi.

(i) Jokainen vakio c_i ∈σ on termi.

(iii) Jos t₁, . . . , t_k ovat termejä ja f on aakkoston σ k-paikkainen funktio, f(t1, . . . , tk) on termi.

Tavanomaisesti symboleilla x,y, z, . . . merkitään muuttujia, symboleilla c₁,c₂,c₃, . . . vakioita, ja symboleillat₁,t₂,t₃,. . . termejä. Myös muuttujille x, y, z,. . . voidaan tarpeen mukaan käyttää alaindeksejä.

Määritelmä 2.4. FO-kaavoiksi luetaan vain ne symbolijonot, jotka on muo- dostettu soveltamalla sääntöjä (i)-(v) äärellisen monta kertaa.

(i) Jos t₁ ja t₂ ovat termejä, niin t₁ =t₂ on kaava.

(ii) Jos t₁, . . . , t_k ovat termejä ja R on k-paikkainen relaatiosymboli, niin R(t₁, . . . , t_k) on kaava.

(iii) Jos ϕ₁ on kaava, niin ¬ϕ₁ on kaava.

(iv) Jos ϕ₁ ja ϕ₂ ovat kaavoja, niin ϕ₁∨ϕ₂ on kaava.

(v) Jos ϕ on kaava, niin ∃xϕ on kaava.

Atomikaavoiksi kutsutaan vain niitä kaavoja, jotka on muodostettu kaa- vanmuodostussäännöillä (i) ja (ii). Aakkoston σ määrittämän FO-logiikan kaavojen joukolle käytetään merkintää FO[σ]. Voidaan puhua myös σ-kaa- voista. Jatkossa käytetään standardeja lyhenteitä

ϕ∧ψ, ϕ→ψ, ϕ↔ψ ja

∀xϕ

merkintöjen¬(¬ϕ∨ψ), ¬ϕ∨ψ, (ϕ →ψ)∧(ψ →ϕ) ja ¬∃x¬ϕ sijasta tässä järjestyksessä.

Olkoon S joukko kaavoja. Jos joukon S kaavoista muodostetaan uusia kaavoja konnektiiveilla∨,∧ja¬, uusia kaavoja kutsutaanS-kaavojen Boolen kombinaatioiksi.

Kaavoissa∃xϕ ja∀xϕ kvanttorit vaikuttavat muuttujanxarvoon omalla tavallaan. Tästä syystä kvanttorin vaikutuksen alaisia muuttujia kutsutaan sidotuiksi. Vastaavasti kvanttorien vaikutuksen ulkopuolelle jääviä muuttujia sanotaan vapaiksi.

Määritelmä 2.5. Muuttujatermint =xainoa vapaa muuttuja onx. Vakio- termillä t⁰ = c ei ole vapaita muuttujia. Termin f(t₁, . . . , t_k) vapaat muut- tujat ovat termien t₁, . . . , t_k vapaat muuttujat. Atomikaavan t₁ =t₂ vapaat muuttujat ovat termient₁ jat₂ vapaat muuttujat. AtomikaavanR(t₁, . . . , t_k) vapaat muuttujat ovat termien t₁, . . . , t_k vapaat muuttujat. Käytetään kaa- vassa ϕ esiintyvien vapaiden muuttujien joukolle merkintää free(ϕ). Määri- tellään induktiivisesti:

free(¬ϕ) := free(ϕ);

free(ϕ∗ψ) := free(ϕ)∪free(ψ), kun ∗ on∧, ∨,→ tai ↔;

free(∀vϕ) := free(ϕ)− {v} ja free(∃vϕ) := free(ϕ)− {v}.

Kaavaa, jossa ei ole vapaita muuttujia, kutsutaan lauseeksi. Merkitään lauseita symboleilla Φ, Ψ, . . ..

2.2.2 Semantiikka

Syntaksin määriteltyä FO-logiikan kielen ja kaavanmuodostussäännöt, se- mantiikka antaa kielelle ja kaavoille merkityksen. Semantiikan voidaan aja- tella rakentuvan totuusrelaation ympärille. Totuusrelaatiolla ilmoitetaan

kaavojen toteutuminen tietyissä struktuureissa, toisin sanoen onko kaava to- si vai epätosi. Oletetaan, että tarkastellaan FO-kaavan ϕ totuutta struktuu- rissa A. Kaavan ϕ totuusarvo riippuu luonnollisesti vain niistä tulkinnoista, jotka annetaan kaavan vapaille muuttujille [2, s. 35-36]. Merkityksellisiä ovat tietysti myös kaavan ϕ ei-loogisten symbolien tulkinnat struktuurin A mu- kaisesti.

Määritelmässä 2.1 aakkoston σ vakio-, relaatio- ja funktiosymbolit ku- vattiin struktuurin A tulkinnoiksi funktiolla α. Kun tutkitaan FO-kaavan totuuttaσ-struktuurissaA, on muuttujien olemassaolon takia tulkittava ter- mejä pelkkien vakio- ja funktiosymbolien tulkitsemisen sijaan. Termien tul- kitsemiseksi struktuurissaA käytetään tulkintajonoa β, joka tulkitsee muut- tujat universuminAalkioiksi mutta jättää vakio- ja funktiosymbolien tulkin- nat funktiolle α. Struktuurin A tulkintajono on mikä tahansa funktio, jolla pätee β(v_i)∈A kaikilla positiivisilla kokonaisluvuillai. Tässä tulkintajonon määritelmä perustuu osittain Ebbinghausin, Flumin ja Thomasin [2, s. 27]

määritelmään.

Määritelmä 2.6. Olkoon A = hA, αi aakkoston σ struktuuri ja olkoon β struktuurin A tulkintajono. Termint arvo struktuurissaA tulkintajonollaβ on

• t^A,β =β(x), kun termi t on muuttujax;

• t^A,β =c^A funktion α mukaan, kun termit on vakio c;

• t^A,β =f^A(t^A,β₁ , . . . , t^A,β_k )funktionαmukaan, kun termitonf(t₁, . . . , t_k). Määritellään FO-kaavojen totuus Tarskin totuusmääritelmän mukaan.

Kaavoissa mahdollisesti esiintyvien kvanttorien ja sidottujen muuttujien ta- kia tulkintajonolle β määritellään funktio

β(x_i/a)(x_j) =

(β(x_j), kun i6=j a, kun i=j,

jossaa∈A. Toisin sanoen funktio β(x_i/a)(x_j)vastaa muutoin tulkintajonoa β mutta tulkitsee x_i esiintymät symboleiksi a∈A.

Määritelmä 2.7. Olkoon A mielivaltainen σ-struktuuri. Määritellään FO- kaavojen totuusarvo struktuurissa A tulkintajonollaβ induktiivisesti:

• A, β t0 =t1, jos ja vain jos t^A,β₀ =t^A,β₁ .

• A, β R(t₁, . . . , t_k), jos ja vain jos (t^A,β₁ , . . . , t^A,β_k )∈R^A.

• A, β ¬ϕ, jos ja vain jos A, β ϕ ei pidä paikkaansa.

• A, β ϕ∨ψ, jos ja vain jos A, β ϕ tai A, βψ.

• Olkoon ψ = ∃x_iϕ. Tällöin on voimassa A, β ψ, jos ja vain jos A, β(x_i/a)ϕ pätee jollakin a∈A.

Sanotaan, että kaava ϕ on tosi struktuurissaA tulkintajonolla β, kun pätee A, β ϕ. Koska lauseissa ei ole vapaita muuttujia, lauseen Φ totuusarvo ei riipu tulkintajonosta. Jos lauseΦon tosi struktuurissaA, käytetään merkin- tää A Φja sanotaan, että struktuuri A on lauseen Φmalli.

Kun kaavanϕvapaat muuttujat ovat muuttujienx₁, . . . , x_njoukossa, voi- daan merkitä ϕ(x₁, . . . , x_n). Merkitään ϕ(~x) silloin, kun jonon ~x pituus on selvä tai merkityksentön. Koska kaavan ϕ(x₁, . . . , x_n) totuusarvo riippuu ai- noastaan tulkinnoista β(x_i) = a_i, missä i ∈ {1, . . . , n}, voidaan merkinnän A, β ϕ sijaan käyttää merkintätapaa Aϕ(a₁, . . . , a_n)[2, s. 37].

Luvun päätteeksi esitellään erityisen hyödyllinen struktuurien laajennus Libkinin tapaan [4, s. 15-16]. Tietyssä tapauksessa struktuurien laajennus sallii kaavojen ja lauseiden edestakaisen tarkastelun, mikä on erityisen hyö- dyllistä pelien yhteydessä, sekä kaavojen ja lauseiden ilmaisuvoimaa tarkas- teltaessa.

Olkoot σ ja σ⁰ toisistaan eriävät aakkostot. Olkoon A =hA, αi σ-struk- tuuri ja olkoon A⁰ = hA, α⁰i σ⁰-struktuuri. Huomaa, että struktuureilla on sama universumi. Käytetään merkintää(A,A⁰) = hA, α, α⁰i sellaiselleσ∪σ⁰- struktuurille, jossa aakkostonσ symbolit tulkitaan struktuurinA mukaisesti tulkintafunktiolla α ja aakkoston σ⁰ symbolit struktuurin A⁰ mukaisesti tul- kintafunktiolla α⁰.

Siirrytään nyt olennaiseen laajennukseen, jossa aakkosto σ⁰ koostuu ai- noastaan vakiosymboleista c₁, . . . , c_n. Käytetään kyseisen laajennuksen aak- kostolle tästä lähtien informatiivisempaa merkintätapaa σ_n. Tässä tapauk- sessa vakiotc₁, . . . , c_ntulkitaan universuminAalkioiksia₁, . . . , a_n. Selvyyden vuoksi merkinnän (A,A⁰)sijaan käytetään merkintää (A, a₁, . . . , a_n).

Apulause 2.1. Olkoon ϕ(x₁, . . . , x_n) aakkoston σ kaava ja olkoon A σ- struktuuri. Muodostetaan σ_n-lause Φ kaavasta ϕ korvaamalla kaikki vapaat muuttujat x₁, . . . , x_n uusilla vakioillac₁, . . . , c_n. Tällöin voidaan osoittaa (in- duktiolla kaavojen suhteen):

Aϕ(a₁, . . . , a_n), jos ja vain jos (A, a₁, . . . , a_n)Φ.

3 Samanlaisuus

Täysin identtisten struktuurien tarkastelu ei ymmärrettävästi ole mielenkiin- toista. Sen sijaan on hyödyllisempää tutkia, mitä oletuksia erilaiset säännön- mukaisuudet struktuurien välillä oikeuttavat tekemään. Tässä luvussa käsi- tellään Ehrenfeuchtin ja Fraïssén pelin kannalta oleellisimpia samanlaisuu-

den käsitteitä, jotka perustuvat struktuurien alkioiden välisiin suhteisiin ja samojen lauseiden toteutumiseen eri struktuureissa.

3.1 Isomorsmi

Isomorsmi kuvaa samanlaisuutta useilla matematiikan osa-alueilla. Yleises- ti ottaen isomorsmi kuvaa rakenteellisia yhtäläisyyksiä. Jos struktuuristaA muodostetaan toinen struktuuri B korvaamalla struktuurin A alkiot toisilla alkioilla siten, että alkioiden väliset suhteet eivät muutu, struktuurit A ja B ovat isomorset. Isomorsmin täsmällinen määritelmä annetaan Ebbing- hausin, Flumin ja Thomasin [2, s. 38] mukaisesti.

Määritelmä 3.1. Olkoot A ja B aakkoston σ struktuureita. Kuvaus h : A→B on isomorsmi struktuurista A struktuuriin B, jos

(i) h on bijektio;

(ii) jokaiselle aakkoston σ vakiosymbolille cpätee h(c^A) = c^B;

(iii) jokaiselle aakkoston σ k-paikkaiselle relaatiosymbolille R ja jokaiselle jonolle a₁, . . . , a_k ∈A pätee

R^A(a₁. . . a_k), jos ja vain jos R^B(h(a₁). . . h(a_k));

(iv) jokaiselle aakkoston σ k-paikkaiselle funktiosymbolille f ja jokaiselle jonolle a₁, . . . , a_k ∈A pätee

h(f^A(a1, . . . , ak)) = f^B(h(a1), . . . , h(ak)).

Jos on olemassa isomorsmi struktuurista A struktuuriin B, käytetään mer- kitään A ∼=B ja sanotaan, että A ja B ovat isomorset.

Isomora säilyttää totuuden. Näin ollen, jos σ-struktuurit A ja B ovat isomorset, kaikille FO-lauseille Φ on voimassa AΦ, jos ja vain jos BΦ pitää paikkansa. Yleisemmin kaikille FO-kaavoilleϕ(x₁, . . . , x_n)ja tulkinnoil- leβ(x_i) = a_i, missäi∈ {1, . . . , n}, on voimassaAϕ(a₁, . . . , a_n), jos ja vain jos Bϕ(h(a₁), . . . , h(a_n))pitää paikkansa. Katso [2, s. 38-39].

Isomorsmin sijaan struktuurien samanlaisuuteen päästään helpommin käsiksi osittaisella isomorsmilla. Itse asiassa osittaisen isomorsmin todis- taminen kahden struktuurin välillä oikeuttaa tekemään hyvinkin merkittäviä oletuksia. Esitetään määritelmä lähteitä [8, s. 1] ja [4, s. 27] mukaillen.

Määritelmä 3.2. Olkoot A ja B σ-struktuureita. Kuvaus p on osittainen isomorsmi struktuurista A struktuuriin B, jos

(i) dom(p)⊆A ja rg(p)⊆B;

(ii) p on injektio;

(iii) kaikille aakkoston σ vakiosymboleille cja jokaiselle a ∈dom(p) pätee c^A =a, jos ja vain jos c^B =p(a);

(iv) kaikille aakkoston σ k-paikkaisille relaatiosymboleille R ja jokaiselle jonolle a₁, . . . , a_k ∈dom(p) pätee

R^A(a₁, . . . , a_k), jos ja vain jos R^B(p(a₁), . . . , p(a_k));

(v) kaikille aakkoston σ k-paikkaisille funktiosymboleille f ja kaikille al- kioille a₁, . . . , a_k, a∈dom(p)pätee

f^A(a₁, . . . , a_k) =a, jos ja vain jos f^B(p(a₁), . . . , p(a_k)) =p(a). Käytetään merkintääpart(A,B)struktuurien Aja B välisille osittaisille iso- morsmeille. Peliteoreettisissa tarkasteluissa on joskus luontevaa puhua parin (~a,~b) määrittelemästä osittaisesta isomorsmista, kun pätee {a₁, . . . , a_n} = dom(p) ja {b₁, . . . , b_n}= rg(p), missä~a= (a₁, . . . , a_n) ja~b= (b₁, . . . , b_n).

Puhtaasti relationaalisen aakkoston struktuureita tarkasteltaessa osittai- nen isomorsmi säilyttää atomikaavojen totuuden. Olkoon σ puhtaasti re- lationaalinen aakkosto ja olkoot A ja B aakkoston σ struktuureita. Olkoon kuvaus p osittainen isomorsmi struktuurista A struktuuriin B ja olkoon ϕ(x₁, . . . , x_n) aakkoston σ mielivaltainen atomikaava. Tällöin on voimassa A ϕ(a₁, . . . , a_n), jos ja vain jos B ϕ(p(a₁), . . . , p(a_n)) pitää paikkansa, kun a1, . . . , an ∈ dom(p). Aakkoston on oltava relationaalinen, sillä ekviva- lenssi ei päde vakioita tai funktioita sisältäville kaavoille. Toisaalta, vaikka aakkostoσolisi puhtaasti relationaalinen, osittainen isomorsmi ei säilyttäisi kvanttorillisten kaavojen totuutta. Katso [2, s. 181-182].

Siirrytään nyt käsittelemään elementaarista ekvivalenssia, joka on iso- morsmin rinnalla hyvin olennainen samanlaisuuden peruskäsite. Elemen- taarisen ekvivalenssin määritelmän lisäksi perehdytään Fraïssén tulokseen, johon Ehrenfeuct-Fraïssé peli olennaisesti perustuu.

3.2 Elementaarinen ekvivalenssi

Kun isomorsmi kertoo kahden struktuurin rakenteellisista yhtäläisyyksis- tä, elementaarinen ekvivalenssi vertaa struktuureita suhteessa käytettävään kieleen, tässä ensimmäisen kertaluvun logiikkaan.

Määritelmä 3.3. Aakkoston σ struktuurien A ja B sanotaan olevan ele- mentaarisesti ekvivalentit, jos kaikille σ-lauseille Φpätee

A Φ, jos ja vain jos BΦ.

Elementaarisesti ekvivalenteille struktuureille käytetään merkitää A ≡ B.

Fraïssén elementaarisen ekvivalenssin algebrallinen karakterisointi perus- tuu ekvivalenssirelaatioon, joka sijoittuu merkitykseltään elementaarisen ekvi- valenssin ja isomorsmin välimaastoon. Koska isomorsmi säilyttää totuu- den, mielivaltaiset isomorset struktuurit A ja B ovat elementaarisesti ekvi- valentit. Sen sijaan elementaarisesti ekvivalentit struktuurit eivät välttämät- tä ole isomorset [2, s. 39-40]. Tästä syystä kahden struktuurin elementaa- risen ekvivalenssin osoittamiseen riittää isomorsmia lievempi ehto. Fraïssé käytti elementaarisen ekvivalenssin karakterisointiin osittaisten isomorsmien joukkoja ja osittaisten isomorsmien laajennuksia. Samastetaan osittainen isomorsmipjoukkoon{(a, p(a))|a∈dom(p)}ja käytetään merkitääp⊂q, kun q on osittaisen isomorsmin p laajennus.

Määritelmä 3.4. σ-struktuurit A ja B ovat m-isomorset,A ∼=m B, jos on olemassa jono (Pj)j≤m siten, että

(i) jokainenP_j on epätyhjä joukon part(A,B)osajoukko;

(ii) kaikille j < m, p∈ P_j+1 ja a ∈A on olemassa q ∈P_j siten, että p⊆q ja a∈dom(q) ja

(iii) kaikille j < m,p ∈P_j+1 ja b ∈B on olemassa q∈ P_j siten, että p⊆q ja b∈rg(q).

Jos jonolla (P_j)_j≤m on ominaisuudet (i)-(iii), sanotaan struktuureitaA ja B m-isomorsiksi jonolla (P_j)j≤m ja merkitään(P_j)j≤m :A ∼=mB. Ominaisuu- desta (ii) käytetään käsitettä laajentumissominaisuus eteenpäin ja ominai- suuden (iii) kohdalla puhutaan laajentumisominaisuudesta taaksepäin.

Vastaavasti elementaarisen ekvivalenssin rinnalle voidaan määritellä jous- tavampi m-ekvivalenssi. Määritelmää varten tarvitaan käsite, joka antaa tie- toa kaavan rakenteesta. Kvanttoriaste selvittää, kuinka paljon kaavassa on sisäkkäistä kvantiointia enimmillään.

Määritelmä 3.5. Olkoon ϕFO-kaava. Määritellään kaavan ϕ kvanttoriaste qr(ϕ) seuraavasti:

• qr(ϕ) = 0, josϕ on atomikaava;

• qr(ϕ1∨ϕ2) = max(qr(ϕ1),qr(ϕ2));

• qr(¬ϕ) = qr(ϕ);

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

Käytetään merkintääFO[m]niiden FO-kaavojen joukolle, joiden kvanttorias- te on yhtäsuuri tai pienempi kuin m.

Esimerkki 3.1. FO[0] koostuu atomikaavojen Boolen kombinaatioista, eli kvanttorittomista kaavoista. Oletetaan, että ϕ on joukon FO[m+ 1] kaava.

Jos kaavaϕmuodostuu kaavojenϕ₀jaϕ₁ Boolen kombinaatioista, ovatϕ₀ ja ϕ₁ joukon FO[m+ 1] kaavoja. Jos on voimassaϕ =∃xψ(x) tai ϕ =∀xψ(x), kaava ψ on joukon FO[m] kaava. Tästä johtuen jokainen joukon FO[m+ 1]

kaava on ekvivalentti muotoa ∃xψ(x) olevien kaavojen Boolen kombinaation kanssa, kun ψ ∈FO[m]. Vertaa [4, s. 33].

Määritelmä 3.6. Olkoonmluonnollinen luku. Sanotaan, ettäσ-struktuurit A ja B ovat m-ekvivalentit, A ≡_m B, jos kaikille lauseille Φ ∈ FO[m] on voimassa

A Φ, jos ja vain jos BΦ.

Voidaan myös sanoa, että struktuurit A ja B ovat elementaarisesti ekviva- lentit kvanttoriasteeseen m saakka.

Esimerkki 3.2. Olkoon A ≡₀ B. Tällöin kaikille atomilauseille eli kvantto- rittomille lauseille Φ∈FO[0] pätee AΦ, jos ja vain jos BΦ pätee.

Olkoon σ puhtaasti relationaalinen aakkosto. Osoitetaan, ettäm-isomor- smi säilyttää niiden aakkoston σ kaavojen ϕ totuuden, joille on voimassa qr(ϕ)≤m [2, s. 187-188].

Apulause 3.1. Olkoon (P_j)j≤m : A ∼=m B. Tällöin jokaiselle aakkoston σ kaavalle ϕ ∈FO[m] pätee

Aϕ(a1, . . . , an), jos ja vain jos Bϕ(p(a1), . . . , p(an)), jos on voimassa p∈P_j ja a₁, . . . , a_n∈dom(p).

Todistus. Todistetaan väite induktiolla aakkoston σ kaavojen suhteen. Ol- koon ϕ(x₁, . . . , x_n) σ-kaava siten, että qr(ϕ)≤ m. Oletetaan, että p∈ P_j ja a1, . . . , an∈dom(p). Edellä mainittiin, että puhtaasti relationaalisen aakkos- ton struktuureita tarkasteltaessa osittainen isomorsmi säilyttää atomikaa- vojen totuuden [2, s. 181]. Täten väite on voimassa atomikaavoille.

• Olkoon ϕ = ¬ψ. Nyt pätee A ¬ϕ(a₁, . . . , a_n), jos ja vain jos A ψ(a1, . . . , an) ei pidä paikkaansa. Induktio-oletuksen perusteella A ψ(a₁, . . . , a_n)ei pidä paikkaansa, jos ja vain josBψ(p(a₁), . . . , p(a_n)) ei pidä paikkaansa. EdelleenBψ(p(a₁), . . . , p(a_n))ei pidä paikkaansa, jos ja vain josB ϕ(p(a1), . . . , p(an)) pätee.

• Tapaus ϕ=ψ₁∨ψ₂ todistetaan vastaavasti.

• Olkoon ϕ = ∃xψ.Koska pätee ϕ ∈ FO[m], on oltava ψ ∈ FO[m−1]. Todistetaan väite seuraavalla ekvivalenssiketjulla:

(1) Aϕ(a₁, . . . , a_n).

(2) On olemassa alkio a∈A siten, että Aψ(a₁, . . . , a_n, a).

(3) On olemassa alkio a∈A ja osittainen isomorsmiq ∈Pj−1 siten, että p⊆q, a∈dom(q) ja Aψ(a₁, . . . , a_n, a).

(4) On olemassa alkio a∈A ja osittainen isomorsmiq ∈Pj−1 siten, että p⊆q, a∈dom(q) ja Bψ(p(a₁), . . . , p(a_n), q(a)).

(5) On olemassa alkio b∈B ja osittainen isomorsmi q ∈P_j−1 siten, että q⊆p, b∈rg(q) ja Bψ(p(a₁), . . . , p(a_n), b).

(6) On olemassa alkio b∈B siten, että Bψ(p(a₁), . . . , p(a_n), b). (7) Bϕ(p(a₁), . . . , p(a_n)).

Kohtien (2) ja (3) ekvivalenssi voidaan todistaa määritelmän 3.4 kohtaan (ii) nojautuen. Kohtien (5) ja (6) ekvivalenssi voidaan todistaa vastaavasti mää- ritelmän 3.4 kohtaan (iii) nojautuen. Kohtien (3) ja (4) ekvivalenssi seuraa induktio-oletuksesta.

Apulause 3.1 on osoitettu päteväksi myös toiseen suuntaan [2, s. 190].

Näin saavutettua ekvivalenssia kutsutaan Fraïssén lauseeksi.

Seuraus 3.2 (Fraïssé). Olkoot A ja B puhtaasti relationaalisen aakkostonσ struktuureita. Tällöin kohdat (1) ja (2) ovat yhtäpitävät.

(1) A ≡_m B (2) A ∼=m B

4 Ehrenfeuchtin ja Fraïssén peli

Ehrenfeuchtin ja Fraïssén pelin kulku kuvataan kirjallisuudessa lähes poik- keuksetta samalla tavalla. Tässä mukaillaan osittain Libkinin [4, s. 26-27] ja Hodgesin [3, s. 74-75] määritelmiä.

Huomautus. Jatkossa käsitellään ainoastaan relationaalisia aakkostoja, ellei toisin mainita.

Pelikenttä koostuu kahdesta saman aakkoston struktuurista, joita merki- tään tuttuun tapaan symboleilla A ja B. Struktuurien A ja B väliselle m- kierroksiselle EF-pelille käytetään merkintää EF_m(A,B). Kierrosten määrä mon kiinnitetään ennen peliä. Peli suoritetaan kahden pelaajan välillä, joista pelaaja I pyrkii osoittamaan, että struktuurit ovat erilaiset. Pelaajan II ta- voite on osoittaa, että struktuurit ovat samanlaiset. Pelissä jokainen kierros etenee seuraavien vaiheiden mukaisesti:

• Pelaaja I valitsee joko alkion a_i stuktuurista A tai alkion b_i struktuu- rista B, missä i∈ {1, . . . , m} on kierroksen luku.

• Pelaaja II valitsee alkion jäljelle jääneestä struktuurista. Jos pelaaja I on valinnut alkion a_i struktuurista A, pelaaja II valitsee alkion b_i struktuurista B. Jos pelaaja I on valinnut alkion b_i struktuurista B, pelaaja II valitsee alkion a_i struktuurista A.

Olkoot~a = (a₁, . . . , a_i)struktuurista Asuoritetut valinnat ja~b= (b₁, . . . , b_i) struktuurista B suoritetut valinnat kun i kierrosta on pelattu. Pelaajan II on suoritettava valintansa siten, että jokaisen kierroksen i jälkeen pari (~a,~b) määrittelee osittaisen isomorsmin p struktuurien A ja B välillä. Tällöin p(a_j) = b_j pätee kaikilla j ∈ {1, . . . , i}. Ellei pelaaja II pysty suorittamaan valintaansa näillä ehdoilla, peli päättyy pelaajan I voittoon. Pelaaja II voittaa pelin vain siinä tapauksessa, että viimeisenkin kierroksen jälkeen pari (~a,~b) määrittelee osittaisen isomorsmin struktuurien A ja B välillä.

Strategia on joukko sääntöjä, joiden mukaan pelaaja suorittaa valintan- sa vastapuolen tekemästä valinnasta riippuen. Struktuurien rakenne ja teh- dyt valinnat ovat kummankin pelaajan tiedossa koko pelin ajan. Strategiaa, jota noudattamalla toinen pelaaja voittaa toisen pelaajan valinnoista riip- pumatta, sanotaan voittostrategiaksi. Jos pelaajalla II on voittostrategia m- kierroksisessa pelissä, merkitään A ∼_m B. Vain toisella pelaajista voi olla voittostrategia samassa pelissä.

Esimerkki 4.1. Jos pelaaja II tietää, että on olemassa isomorsmi h:A → B, seuraavaa strategiaa noudattamalla hän voittaa huolimatta pelin pituu- desta tai pelaajan I valinnoista.

(∗) Jos pelaaja I valitsee vuorollaan alkion a_i ∈ A, pelaaja II valitsee seuraavaksi alkion b_i = h(a_i). Jos pelaaja I valitsee alkion b_i ∈ B, pelaaja II valitsee alkion ai =h⁻¹(bi).

Apulause 4.1. Olkoot A ja B σ-struktuureita. Relaatiolla ∼_m on muun muassa alla luetellut ominaisuudet.

(1) Jos struktuurit A ja B ovat isomorset, kaikille luonnollisille luvuille m pätee A ∼_m B.

(2) Jos A ∼_m B pitää paikkansa, niin myös kaikille lukua m pienemmille luonnollisille luvuille i pätee A ∼_i B.

(3) Olkoon M σ-struktuurien luokka. Relaatio ∼_m on ekvivalenssirelaatio luokassa M.

Todistus. (1) Kun A ∼= B pitää paikkansa, pelaajalla II on voittostrategia esimerkin 4.1 mukaisesti.

(2) Oletetaan, että pelaajalla II on voittostrategia pelissä EFm(A,B). Tällöin pelaaja II pystyy suorittamaan valintansa siten, että jokaisella kier- roksella i valinnoista~a ja~b muodostuva pari (~a,~b) määrittelee struktuurien

A ja B osittaisen isomorsmin. Peli voidaan tästä johtuen keskeyttää minkä tahansa kierroksenijälkeen, ja pelaaja II voittaa pelin. Toisin sanoen pelaa- jalla II on voittostrategia myös kaikkissa niissä peleissä EF_i(A,B), missä i on lukua m pienempi luonnollinen luku.

(3) Relaatio ∼_m on selvästi reeksiivinen, sillä jokainen struktuuri on itsensä kanssa isomornen. Toisin sanoen jokaiselle struktuurille A pätee A ∼_m A ominaisuuteen (1) vedoten. Oletetaan sitten, että A ∼_m B pi- tää paikkansa. Tällöin pätee myös B ∼_m A, sillä pelin sääntöihin vedoten pelaaja II voi käyttää samaa voittostrategiaa kuin pelissäEF_m(A,B). Täten relaatio∼_m on myös symmetrinen. Todistetaan relaation ∼_m transitiivisuus peliteoriassa tyypillisellä menetelmällä [3, s. 76].

Olkoot A,B jaC aakkostonσ struktuureita. Oletetaan, että pelaajalla II on voittostrategiat peleissä EF_m(A,B) jaEF_m(B,C). Väitetään, että tällöin pelaajalla II on voittostrategia myös pelissä EF_m(A,C), eli A ∼_m C. Todis- tetaan väite käsittelemällä samaan aikaan kaikkia näitä kolmea peliä. Var- sinainen peli EF_m(A,C) pelataan pelaajien I ja II välillä siten, että pelaaja II suorittaa kyseisen pelin valinnat pelaamalla samaan aikaan kuvitteellisia apupelejäEF_m(A,B)jaEF_m(B,C). Oletetaan, että peliEF_m(A,C)alkaa pe- laajan I valinnalla a₁ ∈A, jolloin pelaaja II suorittaa valintansa seuraavalla strategialla:

(∗∗) Pelaaja II kuvittelee, että pelaaja I valitsee alkion a₁ ∈ A pelissä EFm(A,B), jolloin hän valitsee alkion b1 ∈B pelinEFm(A,B) voitto- strategian mukaisesti. Seuraavaksi pelaaja II kuvittelee valinnanb₁ ∈B olevan pelaajan I valinta pelissäEF_m(B,C)ja valitsee alkionc₁ ∈Cpe- lin EFm(B,C) voittostrategian mukaisesti. Valinta c1 ∈ C on pelaajan II vastaus pelaajan I valintaan a₁ ∈A pelissä EF_m(A,C).

Kun peliä EF_m(A,C) on pelattu m kierrosta, on muodostunut kolme jo- noa: a1, . . . , am, b1, . . . , bm ja c1, . . . , cm. Pelaajan II oletettujen voittostra- tegioiden perusteella on olemassa osittaiset isomorsmit p :{a₁, . . . , a_m} → {b₁, . . . , b_m} ja q : {b₁, . . . , b_m} → {c₁, . . . , c_m} siten, että jokaiselle alkiol- le ai pätee p(ai) = bi ja jokaiselle alkiolle bi pätee q(bi) = ci kaikilla i ∈ {1, . . . , m}. Nyt voidaan muodostaa yhdistetty kuvausq(a_i) =r(p(a_i))siten, että q : {a₁, . . . , a_m} → {c₁, . . . , c_m} on osittainen isomorsmi, joka kuvaa jokaisen alkion ai alkiolleci, kun i∈ {1, . . . , m}. Täten pelaajalla II on voit- tostrategia myös pelissä EF_m(A,C), eli A ∼_m C.

Määritelmä 4.1. Olkoon relaation < tulkinta struktuurin perusjoukon li- neaarijärjestys. Kun aakkosto σ sisältää järjestysrelaation <, aakkoston σ struktuureita kutsutaan järjestetyiksi struktuureiksi.

Esimerkki 4.2. Olkoot L ja L⁰ järjestettyjä σ-struktuureita muodoltaan h{1, . . . , n}, <i, missä luku n on yhtäsuuri tai suurempi kuin luonnollinen luku m. Onko pelaajalla II voittostrategia pelissä EF_m(L,L⁰)?

Voidaan osoittaa, että L ∼_m L⁰ ei päde edes tapauksessa m = 2. Olkoot L=h{1,2,3}, <ijaL⁰ =h{1,2}, <i. Aloittakoon pelaaja I pelin EF_m(L,L⁰) valitsemalla alkion 2 struktuurista L. Oletetaan, että pelaaja II valitsee al- kion 1 struktuurista L⁰, jolloin pelaajan I toinen valinta on alkio 1 ∈ L. Pelaaja II häviää, sillä struktuurissa L⁰ ei ole olemassa lukua 1 pienempää alkiota a. Toisaalta jos pelaaja II valitsee ensimmäiseksi alkion 2 ∈ L⁰, pe- laaja I vastaa tähän valitsemalla alkion3∈ L. Jälleen pelaaja II on mahdot- tomassa asemassa, sillä struktuurissa L⁰ ei ole lukua 2 suurempaa alkiota a. Tästä syystä pelaaja I voittaa pelin, eli L2 L⁰.

Voidaan todistaa, että pelaajalla II on voittostrategia, jos oletetaan struk- tuurienL ja L⁰ olevan riittävän paljon suurempia kuin pelin kierrosluku.

Lause 4.2. Olkoonm positiivinen kokonaisluku ja olkoot L sekä L⁰ lineaari- sia järjestyksiä siten, että |L| ≥ 2^m ja |L⁰| ≥2^m. Tällöin pätee L ∼_m L⁰. [4, s. 29].

Todistus. Lause todistetaan induktiolla pelin kierrosten lukumääränm suh- teen. Induktiotodistus ei onnistu, jos tehdään oletus ainoastaan sellaisen iso- morsmin olemassa olosta, jonka perusteella pelaajalla II on voittostrategia kierroksen i jälkeen. Tästä syystä tehdään kaksi lisäoletusta, joiden avul- la tällaisen osittaisen isomorsmin todistaminen on mahdollista ilman, että lisäoletukset itsessään koituisivat ongelmaksi.

Laajennetaan aakkostoa σ kahdella uudella vakiosymbolilla min ja max. Tulkitaan min lineaarisen järjestyksen pienimmäksi alkioksi ja max suu- rimmaksi alkioksi. Olkoon {1, . . . , n} struktuurin L universumi, ja olkoon {1, . . . , n⁰}struktuurin L⁰ universumi siten, että n, n⁰ ≥2^m. Universumin al- kioiden x ja y etäisyydelle |x−y| käytetään merkintää d(x, y). Osoitetaan, että pelaajalla II on voittostrategia pelissä EF_m(L,L⁰).

Oletetaan, että on pelattu ikierrosta peliä EF_m(L,L⁰). Jono~a = (a−1, a0, . . . , ai) koostuu alkioista a−1 = min^L, a0 = max^L ja pelin aikana teh- dyistä valinnoista a₁, . . . , a_i ∈ L. Vastaavasti jono~b = (b−1, b₀, . . . , b_i) koos- tuu alkioista b−1 = min^L0, b₀ = max^L0 ja pelin aikana tehdyistä valinnoista b₁, . . . , b_i ∈ L⁰. Nyt induktio-oletuksena kaikille−1≤j, l ≤i on voimassa:

(i) jos d(a_j, a_l)<2^m−1, niin d(b_j, b_l) =d(a_j, a_l); (ii) jos d(a_j, a_l)≥2^m−1, niin d(b_j, b_l)≥2^m−1; (iii) a_j ≤a_l, jos ja vain jos b_j ≤b_l.

Kohta (iii) riittäisi osoittamaan vaadittavan osittaisen isomorsmin olemas- saolon. Kohdat (i) ja (ii) ovat lisäoletuksia. Todistetaan, että kohdat (i)-(iii) ovat voimassa jokaisella kierroksella i. Tapaus i = 0 on selvä, sillä lauseen oletusten mukaan d(a₋₁, a₀), d(b₋₁, b₀)≥ 2^m. Todistetaan tapaus i+ 1. Ole- tetaan, että kierroksellai+ 1pelaaja I tekee valintansa struktuuristaL. (Ta- paus L⁰ on symmetrinen.) Kohdat (i)-(iii) pätevät, jos pelaaja II suorittaa valintansa seuraavien ehtojen mukaisesti.

Jos pelaaja I valitsee alkion a_i+1 = a_j, missä j ≤ i, pelaaja II valitsee vastaavasti alkionb_i+1 =b_j. Muutoin voidaan olettaa, että pelaaja I valitsee alkion a_j < a_i+1 < a_l siten, että mikään valinnoista a₁, . . . a_i ei sijoitu järjes- tyksessä alkioiden a_j ja a_l väliin. Ehdon (iii) perusteella myöskään valinnat b₁, . . . b_i eivät sijoitu järjestyksessä alkioiden b_j ja b_l väliin. Nyt pelaajan II valinta riippuu alkioiden a_j ja a_l etäisyydestä.

• Olkoond(aj, al)<2^m−i. Tällöin on voimassad(bj, bl) =d(aj, al)ja välit [a_j, a_l] sekä[b_j, b_l]ovat isomorset. Pelaaja II valitsee alkion b_i+1 siten, että alkionb_i+1 etäisyydet alkioistab_j ja b_l ovat yhtäsuuret kuin alkion ai+1 etäisyydet alkioistaaj ja al. Toisin sanoen d(aj, ai+1) =d(bj, bi+1) ja d(a_i+1, a_l) = d(b_i+1, b_l). Selvästi kohdat (i)-(iii) pitävät paikkansa.

• Olkoon sitten d(a_j, a_l) ≥ 2^m−i. Nyt on voimassa d(b_j, b_l) ≥ 2^m−i. On kolme eri mahdollisuutta.

(1) Jos pelaajan I valinta a_i+1 sijoittuu välille[a_j, a_l]siten, ettäd(a_j, a_i+1) < 2^m−(i+1), on oltava d(a_i+1, a_l) ≥ 2^m−(i+1). Tällöin pelaa- ja II voi valita alkion bi+1 siten, että d(bj, bi+2) = d(aj, ai+1) ja d(b_i+1, b_l)≥2^m−(i+1).

(2) Tapaus d(a_i+1, a_l)<2^m−(i+1) käsitellään kuten edellä.

(3) Oletetaan lopuksi, että pelaaja I valitsee alkion a_i+1 siten, että etäisyydet d(a_j, a_i+1) ≥ 2^m−(i+1) ja d(a_i+1, a_j) ≥ 2^m−(i+1) pitävät paikkansa. Koskad(b_j, b_l)≥2^m−i on voimassa, pelaaja II valitsee alkionb_i+1välin[b_j, b_l]keskeltä, jotta myös etäisyydetd(b_j, b_i+1)<

2^m−(i+1) jad(a_i+1, a_l)<2^m−(i+1) pätevät.

Täten kohdat (i)-(iii) pätevät ja on osoitettu, että pelaajalla II on voittostra- tegia m-kierroksisessa pelissä EF_m(L,L⁰).

5 Ensimmäisen kertaluvun logiikan ilmaisuvoi- ma

FO-logiikan ilmaisuvoimassa on kaksi eri puolta. Toisaalta FO-logiikka ei pys- ty määrittelemään joitakin yksinkertaisia ominaisuuksia, kuten struktuurin koon parillisuutta tai verkkojen yhtenäisyyttä. Toisaalta jokaiselle äärellisel- le struktuurille A on olemassa FO-lause Φ siten, että kaikille struktuureille B pätee

BΦ, jos ja vain jos A ∼=B.

Toisin sanoen jokainen äärellinen struktuuri voidaan kuvailla yhdellä ensim- mäisen kertaluvun lauseella [1, s. 13]. Tästä syystä yksittäiset struktuurit

eivät ole määriteltävyyden kannalta mielenkiintoisia. Sen sijaan struktuuri- luokat ja niiden ominaisuudet tuovat haasteita määriteltävyyteen. Olkoon M äärellisten struktuurien luokka, jolloin ominaisuus P määritellään iso- morsmin suhteen suljetuksi luokan M osajoukoksi. Käytetään merkintääP ominaisuuden P komplementtijoukolle M \P. Voidaan myös osoittaa, että mikä tahansa äärellisten struktuurien luokka on mahdolllista määritellä nu- meroituvalla määrällä FO-lauseita Φ_i [1, s. 14]. Tästä syystä ominaisuus P pyritään määrittelemään yhdellä FO-lauseella.

Tässä luvussa osoitetaan, että FO-logiikan ilmaisuvoima voidaan kuvata Ehrenfeuchtin ja Fraïssén pelin avulla. Tätä varten esitellään malliteorial- le tavanomainen käsite, joka jakaa FO-kaavat tyyppiluokkiin erityisen hyö- dyllisellä tavalla. Seuraava apulause voidaan todistaa myös kaavoille [2, s.

189-190]. Muista, että aakkosto σ on relationaalinen.

Apulause 5.1. Olkoon σ mielivaltainen aakkosto. Joukko FO[m] sisältää loogiseta ekvivalenssia vaille äärellisen monta lausetta Φ aakkoston σ yli.

Todistus. Todistetaan induktiolla luvun msuhteen. Vertaa [4, s. 34]. Tapaus FO[0] on selvä, sillä äärellisen relationaalisen aakkoston σ atomilauseita on olemassa vain äärellisen monta. Tästä johtuen aakkoston σ atomilauseista voidaan muodostaa äärellinen määrä Boolen kombinaatioita loogista ekviva- lenssia vaille.

Osoitetaan joukon FO[m + 1] äärellisyys. Esimerkkiin 3.1 vedoten jo- kainen lause Φ ∈ FO[m + 1] voidaan esittää Boolen kombinaationa muo- toa ∃xψ(x) olevista lauseista, missä ψ ∈FO[m]. Induktio-oletuksen mukaan joukko FO[m] sisältää äärellisen monta lausetta loogista ekvivalenssia vail- le. Täten myös joukko FO[m+ 1] sisältää äärellisen monta lausetta loogista ekvivalenssia vaille.

Määritelmä 5.1. Olkoon σ kiinteä aakkosto. Olkoon A σ-struktuuri ja ol- koon~a = (a₁, . . . , a_n) jono vakioita universuminA yli. Määritellään jonon~a asteen m n-tyyppi struktuurin A yli seuraavasti:

tp_m(A, ~a) = {ϕ∈FO[m]| Aϕ(~a)}.

Asteen m n-tyyppi voi olla mikä tahansa muotoatp_m(A, ~a)oleva kaavajouk- ko, missä~a = (a₁, . . . , a_n). Puhutaan lyhyemmin m-astetyypeistä, kun luku n on selvä.

Tapauksessa n = 0 merkitään tp_m(A). Joukko tp_m(A) koostuu niistä FO[m]lauseista, jotka pätevät struktuurissa A. Huomaa, että jokaiselle kaa- valle ϕ(x₁, . . . , x_n)∈FO[m] pätee jokoϕ ∈tp_m(A, ~a)tai ¬ϕ∈tp_m(A, ~a).

Apulauseen 5.1 perusteella voidaan todeta, että asteen m n-tyypit ovat äärellisiä loogista ekvivalenssia vaille. Koostukoon jono ϕ₁(~x), . . . , ϕ_N(~x), missä ~x = (x₁, . . . , x_n), kaikista toisistaan eriävistä joukon FO[m] kaavois- ta. Tällöin jokainen FO[m]-kaava on ekvivalentti jonkin kaavan ϕ_i kans- sa. Nyt m-astetyyppi voidaan määritellä yksikäsitteisenä osajoukkona M ⊂

{1, . . . , N}, joka määrittää m-astetyyppiin kuuluvat kaavat ϕ_i. Näin ollen m-astetyyppi voidaan esittää kaavalla

(5.1) θ_M(~x)≡ ^

i∈M

ϕ_i∧ ^

j /∈M

¬ϕ_j,

jolla on mahdollista testata, että jono ~a toteuttaa kaikki kaavat ϕ_i, mis- sä i ∈ M, eikä mitään kaavoista ϕ_j, missä j /∈ M. Huomaa, että kaa- va θ_M(~x) on myös joukon FO[m] kaava, sillä uusia kvanttoreita ei otettu mukaan. Itse asiassa kaavan θ_M(~x) ollessa joukon FO[m] kaava, on jonossa ϕ₁(~x), . . . , ϕ_N(~x)oltava kaavanθ_M(~x)kanssa ekvivalentti kaavaϕ_i. Muotoilu 5.1 on hyödyllinen havainnollistuksen kannalta.

Todetaan, että kaikille toisistaan eriäville osajoukoille M ja M⁰ pätee:

jos A ϕ_M(~a), niin A ¬ϕ_M⁰(~a). Lisäksi todetaan, että jokainen kaava ϕ ∈FO[m] voidaan ilmaista joidenkin kaavojen θ_M disjuktiona.

Lause 5.2. (1) Asteen m n-tyyppien määrä on äärellinen aakkostolle σ. (2) OlkoonT1, . . . , Tr kaikkien asteenm n-tyyppien jono. On olemassa kaa-

vat θ₁(~x), . . . , θ_r(~x) siten, että

kaikille σ-struktuureille A ja jonoille ~a ∈ Aⁿ on voimassa: A θ_i(~a), jos ja vain jos tp_m(A, ~a) =T_i

jokainenFO[m]kaavaϕ(x1, . . . , xn)on ekvivalentti joidenkin kaa- vojen θ_i disjunktion kanssa.

Jatkossa asteen m n-tyyppeihin viitataan niiden määrittelykaavoilla θ_i (5.1). On olennaista muistaa, että asteen m n-tyyppien määrittelykaavojen kvanttoriaste on m.

5.1 Ehrenfeuchtin ja Fraïssén lause

Ehrenfeuchtin ja Fraïssén pelin hyöty määriteltävyystuloksissa perustuu pe- lin seuraavaan ominaisuuteen: jos pelaajalla II on voittostrategia pelissä EFm(A,B), struktuurit A ja B ovat m-ekvivalentit. Tämän todistamises- sa käytetään tyypillisesti m-isomorsmia [1, s. 20] ja Fraïssén lausetta 3.2, mutta Libkin soveltaa kirjassaan hieman eri tavoin määriteltyä edestakaisin- relaatiota [4, s. 36]. Käytetään Libkinin edestakaisin-relaatiolle samaa sym- bolia kuin m-isomorsmille, sillä käytännössä relaatiot vastaavat toisiaan.

Huomaa, että edestakaisin-relaation määritelmän merkintätapa (A, a) viit- taa luvun 2.2 lopussa esitettyyn laajennukseen.

Määritelmä 5.2. Olkoot A ja B aakkoston σ struktuureita. Määritellään edestakaisin-relaatio A ∼=B indukiivisesti.

(i) A ∼=0 B, jos ja vain jos A ≡₀ B.

(ii) A ∼=_m+1 B, jos ja vain jos seuraavat laajenemisehdot pätevät:

eteen: kaikille a∈A on olemassa b∈B siten, että (A, a)∼=m (B, b); taakse: kaikille b ∈B on olemassa a∈A siten, että (A, a)∼=m (B, b). Lause 5.3 (Ehrenfeucht-Fraïssé). Olkoot A ja B relationaalisen aakkoston σ struktuureita. Tällöin seuraavat kohdat ovat yhtäpitävät:

(1) A ≡_m B (2) A ∼=m B (3) A ∼m B

Todistus. Todistetaan väite induktiolla FO-lauseille luvunmsuhteen. Tapaus m = 0 on selvä. Tapauksessa m+ 1 käsitellään ensimmäisenä kohtien (1) ja (2) ekvivalenssi.

Oletetaan, että struktuuritAjaBovatm+1-ekvivalentit. Osoitetaan, et- tä tällöin A ∼=m+1 B pitää paikkansa. Todistetaan laajenemisehto eteenpäin määritelmän 5.2 mukaisesti. Valitaan a ∈ A. Määritelköön kaava θ_i asteen m 1-tyypin tp_m(A, a). Nyt pätee A ∃xθ_i(x). Koska lauseen∃xθ_i(x) kvant- toriaste on m+ 1, oletuksen mukaan myös B∃xθ_i(x) pätee. Toteuttakoon b lauseen ∃xθ_i(x), jolloin on voimassa tp_m(A, a) = tp_m(B, b). Täten kaikille aakkostonσ₁ lauseilleΦ∈FO[m]pätee (A, a)Φ, jos ja vain jos(B, b)Φ pitää paikkansa. Nyt struktuurien A ja B laajennukset (A, a) ja (B, b) ovat elementaarisesti ekvivalentit lauseidenΦ∈FO[m]suhteen, ja oletuksen mu- kaan tällöin on voimassa (A, a) ∼=m (B, b). Laajenemisehton taaksepäin to- distaminen etenee vastaavalla tavalla.

Oletetaan sitten, että A ∼=m+1 Bpätee. Osoitetaan, että tällöin struktuu- rit A ja B ovat m+ 1-ekvivalentit. Huomaa yhteys apulauseeseen 3.1. Esi- merkin 3.1 mukaan jokainen FO[m+ 1]-lause on Boolen kombinaatio muo- toa ∃xψ(x) olevista lauseista, missä ψ ∈ FO[m]. Todistetaan väite muotoa

∃xψ(x) oleville lauseille. Sivuutetaan Boolen kombinaatiot. Oletetaan, että A ∃xψ(x) pitää paikkansa. On siis olemassa a ∈ A, jolle pätee A ψ(a). Määritelmän 5.2 eteen-ominaisuuden perusteella on olemassab ∈B siten, et- tä (A, a)∼=m (B, b). Induktio-oletuksen mukaan laajennukset (A, a) ja (B, b) ovat m-ekvivalentit. On siis oltava B ψ(b) ja täten myös B ∃xψ(x) pi- tää paikkansa. Toinen suunta todistuu vastaavasti määritelmän 5.2 taakse- ominaisuuteen nojautuen.

Todistetaan lopuksi kohtien (2) ja (3) ekvivalenssi. Olkoon A ∼=m+1 B. Osoitetaan, että struktuurit A ja B ovat m+ 1 ekvivalentit. Oletetaan, että pelaaja I valitsee alkion a. Laajenemisehdon perusteella pelaaja II löytää alkion bsiten, ettäA ∼=m B pitää paikkansa. Näin voidaan jatkaa edelleenm kierrosta, joiden jälkeen pelaaja II on suorittanutm+1valintaa onnistuneesti ja voittaa pelin. Toinen suunta todistetaan vastaavasti.

Kun kohtien (1) ja (2) ekvivalenssiin viitataan Fraïssén lauseena, kohtien (1) ja (3) ekvsivalenssista puhutaan Ehrenfeuchtin lauseena. Laajemmin Eh- renfeuchtin ja Fraïssén lauseista on kirjoittanut muun muassa Ebbinghaus, Flum ja Thomas [2, s. 187-192].

5.2 EF-peli FO-logiikan ilmaisuvoiman kuvaajana

Määritelmä 5.3. OminaisuusP on määriteltävissä FO-logiikassa struktuu- riluokassa M, jos on olemassa FO-lauseΦ siten, että

• jos A ∈P, niin AΦ, ja

• jos A ∈P, niin A2Φ.

Osoitetaan, että Ehrenfeuchtin ja Fraïssén peli riittää karakterisoimaan ensimmäisen kertaluvun logiikan ilmaisuvoiman. Vertaa [4, s. 35].

Lause 5.4. Ominaisuus P on määriteltävissä FO-logiikassa, jos ja vain jos on olemassa m siten, että kaikille struktuureille A ja B pätee

jos A ∈ P ja A ∼_m B, niin B ∈P.

Todistus. Oletetaan, että P on määriteltävissä FO-lauseella Φ ja asetetaan m= qr(Φ). Valitaan struktuuri A ∈ P, jolloin A on lauseenΦmalli. Olkoon Bstruktuuri, jolle päteeA ∼_m B. Tällöin lauseen 5.3 perusteella myös struk- tuurin B on oltava lauseenΦ malli ja tästä syystä B ∈P pitää paikkansa.

Oletetaan sitten, että kaikille struktuureilleAjaBpätee: jos struktuurilla Aon ominaisuusP ja pelaajalla II on voittostrategia pelissäEF_m(A,B), niin myös struktuurillaBon ominaisuusP. Nyt kahdella mielivaltaisella struktuu- rilla, joilla on sama m-astetyyppi, on ominaisuus P. Ominaisuus P voidaan siten käsittää tyyppien yhdisteenä, jolloin P on määriteltävissä joidenkin kaavojen θi disjunktiona.

Logiikoiden ilmaisuvoimaa tutkittaessa ollaan pääasiassa kiinnostuneita määrittelemättömyystuloksista. Tyypillisesti ominaisuuden määrittelemättö- myys todistetaan EF-pelillä siten, että mielivaltaiselle luonnolliselle luvulle m konstruoidaan struktuurit A ∈ P ja B ∈ P, joille pätee A ∼_m B. Edelli- seen lauseeseen vedoten tämä riittää. Muotoillaan väite täsmällisemmin.

Seuraus 5.5. Ominaisuus P ei ole määriteltävissä FO-logiikassa, jos ja vain jos kaikille luonnollisille luvuille m on olemassa struktuurit A ∈P ja B ∈P siten, että pelaajalla II on voittostrategia pelissä EF_m(A,B)

On olemassa lukuisia tunnettuja määrittelemättömyystuloksia, jotka osoit- tavat ensimmäisen kertaluvun logiikan ilmaisuvoiman heikkouden. Annetaan kaksi esimerkkiä Libkinin mukaan [4, s. 33 ja 37].

Lause 5.6. Olkoon M äärellisten lineaarijärjestysten luokka. Parillisuus ei ole määriteltävissä FO-logiikassa struktuuriluokassa M.

Todistus. Olkoon P ⊂M niiden lineaarijärjestysten luokka, joiden universu- mien mahtavuus on parillinen. Olkoot A ∈ P ja B ∈ P lineaarijärjestyksiä siten, että |A|= 2^m ja |B|= 2^m+ 1. Lauseen 4.2 perusteella pätee A ∼_m B. Nyt seurauksen 5.5 perusteella väite on tosi.

Lause 5.7. Olkoon M äärellisten verkkojen struktuuriluokka. Verkkojen yh- tenäisyys ei ole määriteltävissä FO-logiikassa struktuuriluokassa M.

Todistus. Todistetaan väite hyödyntämällä lausetta 5.6. Oletetaan, että FO- lause Φ määrittelee äärellisten verkkojen yhtenäisyyden struktuuriluokassa M, kun aakkosto σ koostuu yhdestä kaksipaikkaisesta relaatiosymbolista E. Olkoon L lineaarijärjestys siten, ettämin ja max kuvaavat järjestyksen pie- nintä ja suurinta alkiota. Lineaarijärjestyksestä L voidaan muodostaa suun- nattu verkko seuraavalla tavalla. Määritellään seuraajarelaatio:

seur(x, y) := (x < y)∧ ∀z((z ≤x)∨(z ≥y)).

Seuraajarelaatiota käyttäen määritellään FO-kaavaγ(x, y)siten, ettäγ(x, y) on tosi lineaarijärjestyksessä L, kun jokin seuraavista ehdoista on voimassa:

• ∃z(seur(x, z)∧seur(z,y)), toisin sanoen alkio y on alkion x seuraajan seuraaja;

• seur(x,max)∧y = min, toisin sanoen alkio x edeltää suurinta alkiota ja y on pienin alkio;

• x = max ja seur(min, y), toisin sanoen alkio x on suurin alkio ja y seuraa pienintä alkiota.

Nyt kaava γ(x, y) määrittelee suunnatun verkon GL lineaarijärjestyksen L alkioista. Jos lineaarijärjestyksen alkioiden määrä on parillinen, verkko GL

muodostuu kahdesta erillisestä syklistä. Jos lineaarijärjestyksen alkioiden määrä on pariton, verkko GL muodostuu yhdestä syklistä. Sijoitetaan kaa- va γ relaatiosymbolin E ilmentymien tilalle lauseessa ¬Φ, jolloin lauseella

¬Φ voidaan testata lineaarijärjestyksen parillisuutta. Lauseen 5.6 perusteel- la tämä ei ole mahdollista, joten päädytään ristiriitaan. Ei siis ole olemassa lausettaΦ, joka määrittelisi äärellisten verkkojen yhtenäisyyden.

6 Toisen kertaluvun logiikan ilmaisuvoima

6.1 Toisen kertaluvun logiikka

Vaikka FO-logiikalla on ylivertainen asema logiikoiden joukkossa, joissakin tapauksissa sen ilmaisuvoima on yksinkertaisesti liian heikko. Äärellisten