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 sijoitperus-tuu 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äsvälttämät-tä syysvälttämät-tä 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₁ ∈C pe-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älavul-laisen 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 struktuuriläärellisel-le 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ä et-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].

In document Ehrenfeuchtin ja Fraïssén peli (sivua 13-24)