Lähdetään siitä, että malli on struktuuri (S,i,&tau), jossa S on jokin joukko, &tau on kokoelma relaatiosymboleita, ja i on kuvaus &tau &rarr P(S*), missä P on potenssijoukko, ja "*" on operaatio, joka ottaa unionin kaikista sen argumentin n-tupleista, kun n = 0,1,... i siis antaa tulkinnan jokaiselle relaatiolle.
Ensimmäisen kertaluvun predikaattilogiikan (FOL) tunnettekin jo. Jos M = (S,i,&tau) on malli ja &phi on FOL-lause, kirjoitamme M |= &phi, kun M on &phi:n malli. Tämä ilmaistaan myös niin, että &phi pätee M:ssä. Tulkinta on ilmeinen: Atomilauseke (eli yksittäinen relaatio) R(x) on tosi, jos annetulla x:n (käytän lihavointia osoittamaan, että kyse on vektorista, jätän ariteetin spesifioimatta kun sillä ei ole väliä) tulkinnalla ja i:n osoittamalla R:n tulkinnalla R(x) on voimassa. (Propositiot saadaan 0-ariteettisilla relaatioilla, jotka siis ovat vakioarvoisia tosiasioita) Jokainen lause on itsessään myös Teoria, eli se karakterisoi ne mallit, joissa teoria on tosi.
Kun olen esittänyt, että ei ole olemassa mitään "objektiivista todellisuutta", tätä ei tule ymmärtää makkaratukkien "kaikki on niinq sillee suhteellista"- läppänä, vaan ainoastaan niin, että teorioita muodostaessamme emme postuloi sitä, että on olemassa "yksi ja ainoa malli", vaan ainoastaan pyrimme karsimaan joitakin malleja pois. Sivuutan tässä operationalisoinnin problematiikan (joka liittyy tulkinnan kiinnittämiseen). En kirjoita filosofiasta tässä enempää, koska se ei ole nyt tässä aiheena.
FOL on siis logiikka, jossa on relaatioita, vakiosymboleja, muuttujasymboleita, ja kvantifiointi ainoastaan kiinteiden muuttujien kokoelmien yli, eli esimerkiksi ettemme implisiittisesti kvantifioi relaatioiden ariteettia. Matemaatikot tekevät näitä aika liberaalisti, mutta tietojenkäsittelyteoriaan ne eivät sovi, eivätkä yleensäkään silloin, kun semantiikan kanssa tulee olla erityisen tarkkana.
FOL:ia voidaan laajentaa mielenkiintoisella tavalla, ottamalla mukaan kiintopisteoperaatio. Kiintopisteoperaatio viittaa siihen, että voimme karakterisoida lauseen niin, että jos &phi(R) on lauseke, jossa R esiintyy tulkitsemattomana relaationa, jolla on kiinteä ariteetti (sanotaan vaikka n), voimme siirtyä juuri sen verran toisen kertaluokan puolelle, että sallimme kaavan lfp(&phi(R(x)). Tämän tulkinta toimii seuraavasti: R tulee tämän myötä määritellyksi sellaisen relaatiosekvenssin pienimmäksi (osajoukkomielessä) kiintopisteeksi, jossa sekvenssi määritellään niin, että R(0) on tyhjä joukko ja R(k) = R(k-1) U {x | &phi(R(k-1)(x)) on tosi}. Tämän sekvenssin pienin kiintopiste on siis se relaatio, jonka lfp(&phi(R(x)) määrittelee. Lauseissa voi laajennoksen jälkeen siis tällöin esiintyä paitsi muuttujia kvantifioituina, myös "vapaita" relaatioita karakterisoituna kiintopistemääritelmillä. Klassinen esimerkki on (graafeille) määritelty kaava:
&forall x &forall y: [lfp(&phi(R(u,v)): u = u &or &exist z: (u,z) &isin E &and R(z,v)](x,y)
Harjoitustehtäväksi jätetään selvittää, mitä tämä sanoo graafeista.
FOL + lfp on siitä mielenkiintoinen logiikka, että sen kaavoilla on erikoinen ominaisuus: Kun mallien joukoiksi rajoitetaan formaalit kielet tietyllä koodauksella, niin näiden mallien luokka on tarkalleen niiden kielten joukko, joihin liittyvät päätöstehtävät ovat ratkaistavissa polynomisessa ajassa. Kuuluisa P=NP- kysymys tulisi siis kertaheitolla ratkaistuksi, jos jollekin NP-täydelliselle kielelle löytyisi Lfp-karakterisointi. Jos esimerkiksi voisimme antaa hamiltonin polulle lfp-karakterisoinnin, se olisi siinä: P = NP pätisi. Toinen mahdollisuus olisi, että löytäisimme mallin NP:stä, josta voisimme osoittaa jollakin keinoin, ettei sille ole Lfp-karakterisointia.
Ei kommentteja:
Lähetä kommentti