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äEFm(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 lauseeEdelli-seen 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ä EFm(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|= 2m ja |B|= 2m+ 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
mallien teoriassa on tästä syystä tutkittu paljon muiden logiikoiden ilmai-suvoimaa. Kun FO-logiikkaa laajennetaan lisäämällä aakkostoon uusia toi-sen kertaluvun muuttujia, saavutetaan ilmaisuvoimaltaan erityitoi-sen käyttökel-poiseksi osoittautunut toisen kertaluvun logiikka. Voidaan puhua lyhyemmin SO-logiikasta, joka tulee englanninkielisestä termistä second order logic.
Siirrytään nyt toisen kertaluvun logiikkaan laajentamalla ensimmäisen kertaluvun logiikan syntaksia. Lisätään loogisten symbolien joukkoon nume-roituvan monta k-paikkaista toisen kertaluvun logiikan muuttujaa eli relaa-tiomuuttujaa V1k, V2k, . . . jokaista lukuak≥1kohti. Kun ensimmäisen kerta-luvun muuttujia merkitään pienillä kirjaimillax, y, z,. . ., tästä lähtien isot kirjaimet X, Y, Z, . . . varataan relaatiomuuttujille.
Toisen kertaluvun logiikassa termit eivät poikkea FO-syntaksista. Sen si-jaan FO-logiikan kaavanmuodostussääntöihin on tehtävä lisäyksiä, sillä SO-kaavat voivat sisältää sekä ensimmäisen että toisen kertaluvun muuttujia.
Määritelmä 6.1. Määritellään toisen kertaluvun kaavojen joukko SO[σ]
laajentamalla määritelmää 2.4 kahdella uudella relaatiomuuttujia koskevalla säännöllä.
(i) Jost1, . . . , tk ovat termejä ja X onk-paikkainen relaatiomuuttuja, niin X(t1. . . tk)on kaava.
(ii) Jos ϕ on kaava ja X on relaatiomuuttuja, niin ∃Xϕ on kaava.
Kaavan∃Xϕkohdalla puhutaan eksistentiaalisesta toisen kertaluvun kvan-tioinnista.
SO-logiikan kaavan totuusarvoa tarkasteltaessa vapaiden muuttujien li-säksi on otettava huomioon myös relaatiomuuttujien vapaat ilmentymät. Kun kaavan ϕ∈SO[σ] vapaat muuttujat ja vapaat relaatiomuuttujat ovat muut-tujienx1, . . . , xn ja relaatiomuuttujienX1, . . . , Xm joukossa, on usein havain-nollista käyttää merkintää ϕ(x1, . . . , xn, X1, . . . , Xm).
Siirrytään SO-logiikan semantiikan määrittelyyn. Olkoon A aakkostonσ struktuuri. Toisen kertaluvun tulkintajono βII käyttäytyy muutoin samalla tavalla kuin määritelmän 2.6 tulkintajonoβ, mutta termien tulkinnan lisäksi βII kuvaa jokaisen n-paikkaisen relaatiomuuttujan Xi struktuurin A n paik-kaiseksi relaatioksi RiA.
Käsitellään vain ne tapaukset, jotka eroavat FO-logiikan semantiikasta.
Määritelmä 6.2. OlkoonA aakkostonσ struktuuri.
• A, βII X(t1, . . . , tk) pätee, jos ja vain jos tulkinnalle βII(X) = RA,βII on voimassa (tA,β1 II, . . . , tA,βk II)∈RA,βII.
• Olkoon ψ = ∃Xϕ. Tällöin on voimassa A, βII ψ, jos ja vain jos A, βII(X/R) ϕ pitää paikkansa jollakin struktuurin A relaatiolla R, missäβII(X/R)vastaa muutoin tulkintajonoaβII, mutta kuvaa sidotun relaatiomuuttujanXesiintymät relaatiolleR. Vertaa määritelmään 2.7.
Koska kaavan ϕ(x1, . . . , xn, X1, . . . , Xm) totuusarvo riippuu ainoastaan tul-kinnoista βII(xi) = ai ja tulkinnoista βII(Xj) = Rj, missä i ∈ {1, . . . , n}
ja j ∈ {1, . . . , m}, voidaan merkinnän A, βII ϕ sijaan käyttää merkintää Aϕ(a1, . . . , an, R1, . . . , Rm).
Määritelmä 6.3. Monadinen toisen kertaluvun logiikka eli MSO on SO-logiikan rajoittuma, missä kaikkien toisen kertaluvun muuttujien paikkaluku on1.
Määritelmä 6.4. Eksistentiaalinen toisen kertaluvun logiikka eli ∃SO on SO-logiikan rajoittuma, jonka kaikki kaavatϕ ovat muotoa
∃X1. . . ,∃Xmϕ,
missä ϕ on FO-kaava. Rajoittumaa kutsutaan eksistentiaaliseksi MSO-logii-kaksi, jos kaikki relaatiomuuttujat Xi ovat yksipaikkaisia. Eksistentiaaliselle MSO-logiikalle käytetään myös merkintää ∃MSO.
Määritelmä 6.5. SO-kaavan ϕ kvanttoriaste määräytyy määritelmän 3.5 sääntöjen, sekä säännön
• qr(∃Xϕ) = qr(ϕ) + 1.
mukaisesti. Käytetään merkintää SO[r] kaikille niille SO-kaavoille, joiden kvanttoriaste on yhtäsuuri tai pienempi kuin r.