Pikatietä logiikan rajalle
Antti Valmari
Jyväskylän yliopisto
antti.valmari@jyu.fi
Johdanto
Tämän kirjoituksen tavoitteena on esitellä joitakin logiikan keskeisiä käsitteitä kuten looginen seuraus, ja sen jälkeen osoittaa eräs varsin voimakas ja yleispätevä mutta poikkeuksellisen helppotajuinen rajoitus koskien mahdollisuuksia ilmaista ja todistaa väitteitä.
Vuoden 1900 tienoilla logiikan tutkimus edistyi valtavaa vauhtia. Silloin toivottiin, että logiikan avulla löytyisi yleispätevä menetelmä tarkastaa matemaattisten väitteiden pätevyyksiä. Monien matemaatikkojen suureksi pettymykseksi 1930-luvulla paljastui, että sellaista menetelmää ei voi olla olemassa. Itse asiassa jo lukujen 0, 1, 2, 3, … yhteenlasku ja kertolasku käyttäytyvät niin monimutkaisesti, että vaikka rajoittauduttaisiin niihin, ei täydellistä totuustarkastinta voi olla olemassa.
Tämä tulos tunnetaan Gödelin ensimmäisenä epätäydellisyyslauseena. (Jos ollaan aivan tarkkoja, ne eivät ole sama asia, vaan ovat vain hyvin läheistä sukua toisilleen.) Sillä oli valtava merkitys. Sitä on kansantajuistettu moneen kertaan. Ikävä kyllä tuloksen todistus sisältää suuren määrän teknisiä yksityiskohtia, joita ei voida kansantajuistuksissa käydä läpi. Siksi kansantajuistukset jättävät tuloksen jossain määrin mysteeriksi.
Logiikan periaatteellisiin rajoituksiin on kuitenkin olemassa muitakin reittejä. Tässä kirjoituksessa esitellään ja todistetaan rajoitus, joka liittyy saavutettavuuden käsitteeseen. Saavutettavuus on arkikokemukselle tuttu esimerkiksi maantiekartoista: paikkakunta on saavutettavissa toisesta, jos ja vain jos ensin mainitusta pääsee jälkimmäiseen maanteitä pitkin. Esimerkiksi Lappeenranta on saavutettavissa Turusta, mutta Maarianhamina ei ole, koska Maarianhamina sijaitsee meren takana niin että välissä ei ole siltaa eikä tunnelia.
On olemassa vahvuudeltaan erilaisia logiikoita. Joissakin niistä on rajoitteita siinä mitä kaavojen avulla voidaan ilmaista, mutta todistamisen osalta tilanne on ihanteellinen: jokainen pätevä kaava voidaan todistaa, ja mitään epäpätevää kaavaa ei voi todistaa. (Luvussa “Looginen seuraus” selviää, mitä “pätevä” tarkoittaa tässä yhteydessä, ja miksi se, toisin kuin “tosi”, on tähän oikea käsite.) Joissakin muissa ilmaisuvoima on suurempi, mutta vastaavasti todistamiskyky jää rajallisemmaksi: on olemassa päteviä kaavoja, joita ei voi todistaa päteviksi.
Tässä kirjoituksessa käsiteltävä tulos sanoo, että jokaisessa logiikassa, jossa saavutettavuus voidaan ilmaista kaavana, jää todistamiskyky vajaaksi. Ei ole olemassa, ei voi olla olemassa, sellaista logiikkaa, että siinä pystytään puhumaan saavutettavuudesta ongelmitta, ja todistamaan kaikki ne väitteet joiden pitäisi olla todistettavissa!
Tämä tulos voidaan johtaa lyhyellä päättelyllä suoraan peruskäsitteistä, ilman pitkiä monimutkaisia konstruktioita ja ilman juuri minkäänlaisia taustatietoja matematiikasta tai logiikasta. Toki täytyy tietää mitä saavutettavuus, todistaminen, looginen seuraus ja muutama muu peruskäsite tarkoittavat, mutta ne kerrotaan tässä kirjoituksessa. Itse asiassa suurin osa tästä kirjoituksesta esittelee ja havainnollistaa peruskäsitteitä, ja “suuren” tuloksemme todistusta on selvästi alle puolet.
Sille ei voi mitään, että tämän kirjoituksen lukeminen vaatii halua ja kykyä huolelliseen abstraktiin ajatteluun. Mutta se lienee hyväksyttävää, ottaen huomioon, että tämä lehti on Matematiikkalehti Solmu.
Suunnatut graafit ja niiden kaavat
Suunnattu graafi on matemaattinen rakenne, joka voi edustaa vaikkapa maantiekarttaa. Siinä on kahdenlaisia osia: solmuja ja kaaria. Solmut piirretään tavallisesti ympyröinä ja kaaret nuolina. Kukin kaari alkaa jostakin solmusta ja päättyy johonkin solmuun. Alla olevassa kuvassa on suunnattu graafi, jossa on kahdeksan solmua ja yksitoista kaarta.
Jos samasta solmusta alkaa monta kaarta, niin kunkin niistä täytyy päättyä eri solmuun kuin muut. Siis ei saa olla esimerkiksi kahta eri kaarta, joista molemmat alkavat solmusta A ja molemmat päättyvät solmuun B.
Maantiekarttasovelluksessa solmut edustavat risteyksiä ja kaaret risteysten välisiä yksisuuntaisia tienpätkiä. Kaksisuuntainen tienpätkä esitetään piirtämällä solmujen välille kaari kumpaankin suuntaan. Kuvassa solmujen B ja C välillä on kaari kumpaankin suuntaan.
Jotta voisimme puhua suunnatun graafin ominaisuuksista logiikan kaavoilla, otamme käyttöön merkinnän \(u \to v\) tarkoittamaan, että solmusta \(u\) on kaari solmuun \(v\). Kuvan esimerkissä \(\textsf{A} \to\textsf{B}\) on tosi, mutta \(\textsf{A} \to\textsf{E}\) ei ole tosi. Sen, että jokin kaava ei ole tosi, voi väittää lisäämällä kaavan eteen “\(\neg\)”. Alkuperäisen kaavan ympärille voidaan laittaa sulkeet “\((\)” ja “\()\)” varmistamaan, että täydennetyn kaavan rakenne tulee ymmärretyksi oikein. Kuvan tapauksessa \(\neg (\textsf{A} \to\textsf{E})\) on tosi.
Kahden kaavan yhdistelmä \(\textit{kaava}_1 \wedge \textit{kaava}_2\) väittää, että sekä \(\textit{kaava}_1\) että \(\textit{kaava}_2\) on tosi. Nytkin kaavan osien ympärille voi laittaa sulkeet helpottamaan kaavan lukemista. Esimerkiksi \((\textsf{A} \to\textsf{F}) \wedge (\textsf{E} \to\textsf{F})\) on kuvassa tosi. Vastaavasti \(\textit{kaava}_1 \vee \textit{kaava}_2\) väittää, että \(\textit{kaava}_1\) tai \(\textit{kaava}_2\) tai molemmat on tosi. Kuvassa \((\textsf{G} \to\textsf{H}) \vee (\textsf{H} \to\textsf{G})\) on tosi ja \((\textsf{B} \to\textsf{C}) \vee (\textsf{C} \to\textsf{B})\) on tosi, mutta \((\textsf{B} \to \textsf{D}) \vee (\textsf{D} \to\textsf{B})\) ei ole tosi.
Kaava \(u = v\) väittää, että \(u\) ja \(v\) ovat sama solmu, ja \(u \neq v\) väittää, että ne eivät ole sama solmu. Niinpä \(u \neq v\) tarkoittaa täsmälleen samaa kuin \(\neg (u = v)\).
Ilmaus \(\exists u: \textit{kaava}\) väittää, että on olemassa ainakin yksi solmu, jolle \(\textit{kaava}\) on tosi. Esimerkiksi \(\exists u: (\textsf{F} \to u)\) väittää, että \(\textsf{F}\):stä lähtee ainakin yksi kaari. Se ei ole tosi kuvan esimerkissä. Kaava \(\exists v_1: \exists v_2: {(u \to v_1)} \wedge {(u \to v_2)} \wedge v_1 \neq v_2\) väittää, että solmusta \(u\) lähtee ainakin kaksi kaarta. Se on tosi jos \(u\):ksi valitaan kuvan solmu A, mutta ei ole tosi jos \(u\):ksi valitaan B. Ilmaus \(\forall u: \textit{kaava}\) väittää, että \(\textit{kaava}\) on tosi jokaisella solmulla. Esimerkiksi \(\forall u: \exists v: (u \to v)\) väittää, että jokaisesta solmusta lähtee ainakin yksi kaari. Se ei ole kuvassa tosi, koska F:stä ei lähde yhtään kaarta.
Alla oleva kaava sanoo, että mistään solmusta ei lähde enempää kuin yksi kaari. Tulemme tarvitsemaan sitä myöhemmin, joten annamme sille (tylsän) nimen (1).
\[\neg \exists u: \exists v_1: \exists v_2: (u \to v_1) \wedge (u \to v_2) \wedge v_1 \neq v_2 \tag{1}\]
Looginen seuraus
Suunnattuja graafeja voi käyttää sekä siten, että solmuilla on nimet, että siten, että nimiä ei ole. Maantiekartan tapauksessa nimet ovat tärkeitä — on eri asia ajaa Tampereelta Jyväskylän kautta Kuopioon kuin Rovaniemeltä Kajaanin kautta Joensuuhun. Mutta kun tutkitaan, millaisia rakenteeltaan erilaisia suunnattuja graafeja on olemassa, eivät nimet ole tärkeitä. Alla on näytetty jokainen suunnattu graafi, jossa on kaksi solmua, ja kustakin solmusta lähtee enintään yksi kaari.
Kuvan graafeista ensimmäinen on ainoa, jossa ei ole yhtään kaarta, eli jolle \(\neg \exists u: \exists v: (u \to v)\) on tosi. Kaava \(\exists u: (u \to u)\) on tosi toiselle, neljännelle ja viidennelle graafille, mutta ei muille. Sen, että solmuja on täsmälleen kaksi, voi sanoa kaavalla \(\exists u: \exists v: u \neq v \wedge \forall w: {w = u} \vee w = v\). Mille tahansa kuvan graafeista voi jonkin aikaa miettimällä keksiä sellaisen joukon kaavoja, että valittu graafi toteuttaa niistä jokaisen, mutta jokainen muu suunnattu graafi jättää toteuttamatta ainakin yhden.
Kun on valittu joukko kaavoja, niin on kolme mahdollisuutta. Voi olla, että on olemassa monta suunnattua graafia, joille jokainen joukon kaavoista on tosi. Voi olla, että sellaisia suunnattuja graafeja on täsmälleen yksi. Ja voi olla, että niitä ei ole yhtään. Esimerkiksi jos joukon kaavat sanovat, että solmuja on enintään kaksi, kustakin solmusta lähtee enintään yksi kaari, ja johonkin solmuun päättyy kolme kaarta, niin mikään suunnattu graafi ei toteuta niitä kaikkia. Nimittäin jos solmuja on enintään kaksi ja kustakin lähtee enintään yksi kaari, niin kaaria on kaikkiaan enintään kaksi, joten mihinkään solmuun ei voi päättyä kolmea.
Kaava on looginen seuraus joukolle kaavoja, jos ja vain jos jokainen suunnattu graafi, joka toteuttaa joukon jokaisen kaavan, toteuttaa myös ensin mainitun kaavan.
Hyvin yksinkertainen esimerkki on, että \(\neg \exists u: (u \to u)\) on looginen seuraus kaavasta \(\neg \exists u: \exists v: (u \to v)\). Ensimmäinen sanoo, että ei ole kaarta, joka päättyy samaan solmuun kuin mistä se alkaa, ja jälkimmäinen sanoo, että kaaria ei ole lainkaan. Nimittäin jos kaaria ei ole lainkaan, niin ei ole sellaista kaarta, joka päättyy samaan solmuun kuin mistä se alkaa.
Monimutkaisempi esimerkki on, että \(\exists u: (u \to u)\) on looginen seuraus kaavoista, jotka sanovat, että solmuja on enintään kaksi ja kaaria on ainakin kolme. Nimittäin edellä sanottiin, että jos samasta solmusta alkaa monta kaarta, niin kunkin niistä täytyy päättyä eri solmuun kuin muut. Niinpä jos kahden solmun tapauksessa halutaan piirtää mahdollisimman monta kaarta ilman että mikään päättyy siihen solmuun josta se alkaa, niin mahdollisuudet loppuvat, kun on piirretty kaari solmusta toiseen ja kaari takaisinpäin.
Loogisen seurauksen määritelmällä on sellainen ehkä kummalliselta tuntuva ominaisuus, että jos mikään suunnattu graafi ei toteuta joukon jokaista kaavaa, niin mikä tahansa kaava on joukon looginen seuraus. Tällöin myös kaikki aina epätodet kaavat, kuten \(\exists u: {u \neq u}\), ovat loogisia seurauksia.
Sen ei kannata antaa häiritä. Aina epätosien kaavojen ilmaantuminen seurauksiin ei tarkoita, että logiikassa olisi vikaa, vaan se on vain merkki siitä, että asetetut lähtökohdat ovat mahdottomat. Saadut omituiset seuraukset eivät voi oikeasti toteutua, koska ne ovat seurauksia lähtökohdista, jotka eivät voi oikeasti toteutua.
Päättelemiselle on tavallista, että jos lähtökohdat ovat ristiriitaiset, niin pätevät päättelysäännöt voivat tuottaa mitä tahansa. On esimerkiksi oikein päätellä, että jos \(x = 0\), niin kertomalla molemmat puolet viitosella saadaan \(5x = 0\). Samaan tapaan saadaan \(3x = 0\). Niistä yhdessä voi päätellä \(5x = 3x\). Mutta jos lähtökohtiin kuuluu myös \(x = 1\), niin se ja \(5x = 3x\) tuottavat yhdessä \(5 = 3\)!
Hullu lopputulos \(5 = 3\) ei ole merkki siitä, että olisi tehty päättelyvirhe, vaan siitä, että lähtökohdat \(x = 0\) ja \(x = 1\) ovat ristiriitaiset. Tästä syystä (ja muista syistä) on etu eikä haitta, että loogisen seurauksen käsite on määritelty siten, että jos lähtökohdat ovat ristiriitaiset, niin mikä tahansa kaava on looginen seuraus.
On mahdollista, että kaava ei ole looginen seuraus, mutta myöskään sen vastakohdan ilmaiseva kaava ei ole looginen seuraus. Esimerkiksi \(\exists u: (u \to u)\) ei ole looginen seuraus mutta myöskään \(\neg \exists u: (u \to u)\) ei ole looginen seuraus kaavoista, jotka sanovat että solmuja on kaksi ja kustakin lähtee enintään yksi kaari. Tämän tietää siitä, että edellä olleessa kuvassa on sekä suunnattu graafi, jossa on solmu, josta on kaari itseensä, että suunnattu graafi, jossa ei ole sellaista solmua.
Siis kaava on lähtökohtien looginen seuraus, jos ja vain jos kaava on tosi joka ikisessä rakennelmassa, joka toteuttaa kaikki lähtökohdat. Voi olla, että lähtökohdissa ei ole riittävästi informaatiota määräämään jostakin kaavasta, onko se tosi vai eikö ole. Siinä tapauksessa kaava ei ole lähtökohtien looginen seuraus, mutta myöskään vastakkainen kaava, joka saadaan lisäämällä eteen “ei”, ei ole lähtökohtien looginen seuraus.
Lähtökohdaksi annettu joukko kaavoja voi olla joko äärellinen tai ääretön. Esimerkiksi alakoulussa opitut yhteenlaskujen tulokset muodostavat äärettömän joukon kaavoja: \(1+1 = 2\), \(1+2 = 3\), \(25 + 17 = 42\), \(123 + 456 = 579\), ….
Äärellinen lähtökohtien joukko voidaan ilmoittaa kirjoittamalla jokainen kaava erikseen. Mutta äärettömän joukon tapauksessa se ei ole mahdollista. Siksi äärettömän joukon tapauksessa vaaditaan, että on olemassa jokin menetelmä, jolla mistä tahansa kaavasta voi testata, onko se mukana lähtökohdissa vai eikö ole. Kokonaislukujen yhteenlaskun tapauksessa sellainen menetelmä on olemassa. Esimerkiksi kaavan \(23975896 + 6532746 = 30408642\) voi testata laskemalla yhteenlaskun \(23975896 + 6532746\) kynällä ja paperilla, ja tarkastamalla, tuliko tulokseksi \(30408642\).
Saavutettavuus
Suunnatun graafin solmu \(v\) on saavutettavissa solmusta \(u\), jos ja vain jos \(u\):sta pääsee \(v\):hen nollaa tai useampaa kaarta pitkin. Tässä määritelmässä kaaria saa kulkea vain niiden suuntaisesti (siis esimerkiksi A:sta B:hen mutta ei toisinpäin), ensimmäisenä kuljetun kaaren pitää alkaa \(u\):sta, seuraavan kaaren pitää alkaa siitä mihin edellinen päättyy, ja viimeisen kaaren pitää päättyä \(v\):hen. Esimerkkikuvassamme D on saavutettavissa A:sta, mutta ei toisinpäin. Toisaalta D on saavutettavissa B:stä ja B on saavutettavissa D:stä.
Koska saavutettavuuden määritelmä sallii myös nolla kaarta, on jokainen solmu saavutettavissa itsestään. (Mistä tahansa pääsee itseensä pysymällä paikallaan.) Jos \(v\) on saavutettavissa \(u\):sta ja \(v \to w\), niin myös \(w\) on saavutettavissa \(u\):sta — jollei muuta kautta, niin ainakin siten, että mennään ensin \(u\):sta \(v\):hen ja jatketaan siitä kulkemalla kaari \(v\):stä \(w\):hen.
Sen, että \(u\):sta on kaari \(w\):hen ja sieltä edelleen \(v\):hen voi väittää kaavalla \((u \to w) \wedge (w \to v)\). Tällaisen kaavan saa kirjoittaa lyhyemmässä muodossa \(u \to w \to v\).
Tähänastisilla keinoillamme voidaan väittää esimerkiksi, että \(v\) on saavutettavissa \(u\):sta enintään neljällä kaarella. Se onnistuu vaikka seuraavalla kaavalla: \[\begin{array}{ll} & u = v\\ \vee & (u \to v)\\ \vee & (\exists w_1: (u \to w_1 \to v))\\ \vee & (\exists w_1: \exists w_2: (u \to w_1 \to w_2 \to v))\\ \vee & (\exists w_1: \exists w_2: \exists w_3: (u \to w_1 \to w_2 \to w_3 \to v)) \end{array}\] Samalla tavalla voi ilmaista saavutettavuuden millä tahansa ennalta asetetulla kaarten määrän ylärajalla, jos jaksaa kirjoittaa tarpeeksi pitkän kaavan. Mutta tällä tavalla ei voi ilmaista edellä määriteltyä saavutettavuutta. Ne eivät ole sama asia, koska edellä määritellyssä ei ole ylärajaa kaarten määrälle.
On olemassa niin sanotut ensimmäisen kertaluvun logiikka ja toisen kertaluvun logiikka. Toisen kertaluvun logiikka on ensimmäisen kertaluvun logiikan laajennos, eli siinä on käytettävissä kaikki samat ilmaisukeinot kuin ensimmäisessäkin kertaluvussa, ja lisäksi muuta. Tähän asti olemme käyttäneet ensimmäisen kertaluvun logiikkaa. Näytämme seuraavaksi, että ottamalla käyttöön toisen kertaluvun tarjoaman keinon, voi saavutettavuuden ilmaista asettamatta kaarten määrälle ylärajaa.
Toisen kertaluvun logiikassa \(\exists\):lla ja \(\forall\):lla voi luoda paitsi muuttujan kuten edellä, myös symbolin, joka ottaa solmun ja tuottaa totuusarvon. Sellainen edustaa jotakin joukkoa solmuja. Esimerkiksi \(\exists P: P(u) \wedge \neg P(v)\) sanoo, että on olemassa sellainen joukko solmuja, että \(u\) kuuluu siihen mutta \(v\) ei kuulu. Jos \(u\) on eri solmu kuin \(v\), niin se on totta, sillä esimerkiksi \(u\) yksinään muodostaa sellaisen joukon. Toisaalta jos \(u\) on sama solmu kuin \(v\), niin \(\exists P: P(u) \wedge \neg P(v)\) ei ole totta, koska se väittää, että on olemassa sellainen joukko solmuja, johon \(u\) samanaikaisesti kuuluu ja ei kuulu.
Kaava \(\exists x: \exists y: P(x) \wedge (x \to y) \wedge \neg P(y)\) sanoo, että jokin kaari vie \(P\):n edustaman joukon sisältä ulos. Perustelemme kohta, että seuraava kaava on tosi jos ja vain jos \(v\) on saavutettavissa \(u\):sta:
\[\begin{split} &\forall P: \neg P(u) \vee P(v) \vee {}\\ &\quad\quad \exists x: \exists y: P(x) \wedge (x \to y) \wedge \neg P(y) \end{split} \tag{2} \]
Oletamme ensin, että \(v\) ei ole saavutettavissa \(u\):sta. Osoitamme, että (2) ei toteudu antamalla esimerkin sellaisesta \(P\), että se ei toteuta \(\neg P(u)\) eikä \(P(v)\) eikä \(\exists x: \exists y: P(x) \wedge (x \to y) \wedge \neg P(y)\).
Valitsemme \(P\):ksi täsmälleen ne solmut, jotka ovat saavutettavissa \(u\):sta. Oletuksemme vuoksi \(v\) ei kuulu niihin, eli \(P(v)\) ei ole tosi. Koska \(u\) on saavutettavissa itsestään kulkemalla nolla kaarta, on \(P(u)\) tosi, joten \(\neg P(u)\) ei ole tosi. Jos \(x\) on saavutettavissa \(u\):sta ja \(x\):stä on kaari \(y\):hyn, niin \(y\) on saavutettavissa \(u\):sta kulkemalla ensin \(x\):ään ja sitten mainittua kaarta pitkin \(y\):hyn. Ei siis ole olemassa sellaisia solmuja \(x\) ja \(y\), että \(P(x) \wedge (x \to y) \wedge \neg P(y)\) on tosi. Toisin sanoen, \(\exists x: \exists y: P(x) \wedge (x \to y) \wedge \neg P(y)\) ei ole tosi.
Vielä tarvitsee osoittaa, että jos \(v\) on saavutettavissa \(u\):sta, niin (2) toteutuu. On tarkasteltava jokainen joukko solmuja. Jos tarkasteltava joukko sisältää \(v\):n, niin \(P(v)\) on sille tosi. Jos se ei sisällä \(u\):ta, niin \(\neg P(u)\) on sille tosi. Muussa tapauksessa se sisältää \(u\):n muttei \(v\):tä. Koska \(v\) on saavutettavissa \(u\):sta, niin on olemassa reitti \(u\):sta \(v\):hen. Koska joukko sisältää \(u\):n mutta ei \(v\):tä, on tällä reitillä kohta, jossa solmu kuuluu joukkoon mutta reitin seuraava solmu ei kuulu. Sille \(P(x) \wedge (x \to y) \wedge \neg P(y)\) on tosi. Niinpä \(\exists x: \exists y: P(x) \wedge (x \to y) \wedge \neg P(y)\) on tosi.
Päätteleminen
Jotta voitaisiin päätellä, lähtökohtina käytettävien kaavojen lisäksi tarvitaan päättelysääntöjä. Päättelysääntöjen kokoelma riippuu käytössä olevasta logiikasta (kuten edellä todettiin, ei ole olemassa vain yhtä logiikkaa, vaan monta erilaista). Samallekin logiikalle se voidaan muodostaa monilla eri tavoilla.
Kunnolliset päättelysääntöjen kokoelmat ovat liian monimutkaisia tässä esitettäviksi. Toisaalta tämä kirjoitus ei tarvitse päättelysääntöjen yksityiskohtia, vaan hyvin karkea yleiskäsitys riittää. Siksi tyydymme pariin pieneen esimerkkiin päättelysääntöjen käyttämisestä. Ne eivät liity suunnattuihin graafeihin.
Jos on päätelty että aurinko paistaa ja on päätelty että linnut laulavat, niin saa päätellä \((\)aurinko paistaa\() \wedge (\)linnut laulavat\()\).
Jos on päätelty, että jokainen ihminen on laulun arvoinen, niin saa päätellä, että sinä olet laulun arvoinen.
Kaavan todistaminen tarkoittaa askel askeleelta etenevää päättelyä, joka nojautuu vain lähtökohdiksi annettuihin kaavoihin sekä valittuun kokoelmaan kuuluviin päättelysääntöihin, ja tuottaa todistettavan kaavan lopputuloksekseen.
Päättely voi koostua vain äärellisestä määrästä päättelyaskelia, koska muutoin se kestäisi äärettömän kauan eli ei loppuisi koskaan. Kukin päättelyaskel voi käyttää vain äärellistä määrää lähtökohdiksi asetettuja kaavoja, koska on mahdotonta käsitellä yhtäaikaa ääretöntä määrää informaatiota.
Näistä seuraa, että vaikka lähtökohdiksi annettuja kaavoja voi olla äärettömän monta, kukin yksittäinen päättely käyttää niistä vain äärellistä määrää. Päättely voi esimerkiksi käyttää mitä tahansa kokonaislukujen yhteenlaskujen tuloksia ja toinen päättely joitakin muita, mutta mikään yksi päättely ei voi käyttää niitä kaikkia.
Logiikan rajoista kertova tulos
Nyt meillä on kaikki tarvittavat käsitteet, jotta voimme lausua logiikan rajoista kertovan tuloksemme. Sen, että tulos pitää paikkansa, perustelemme seuraavassa luvussa.
Tulos koskee jokaista logiikkaa, joka pystyy ilmaisemaan kaavana käsitteen “saavutettavuus”. Jokainen päättelyjärjestelmä sille logiikalle joko todistaa jonkin epäpätevän kaavan, tai jättää todistamatta jonkin pätevän kaavan. (Tässä yhteydessä “pätevä” tarkoittaa, että kaava on lähtökohtien looginen seuraus.)
Saavutettavuus ilmaistiin edellä toisen kertaluvun logiikan kaavana (2). Siksi tuloksesta seuraa, että toisen kertaluvun logiikalle ei ole olemassa päättelyjärjestelmää, joka pystyy todistamaan kaiken sen mitä pitääkin mutta ei todista mitään liikaa. (Toisen kertaluvun logiikkaa käytetään vähemmän kuin ensimmäisen kertaluvun. Tämä on yksi syy siihen.)
Tuloksen perustelu
Perustelemme edellisen luvun tuloksen seuraavasti. Oletamme, että käytettävissä oleva logiikka pystyy ilmaisemaan käsitteen “saavutettavuus” kaavana, ja että päättelyjärjestelmä todistaa kaikki lähtökohtien loogiset seuraukset. Osoitamme, että se todistaa myös ainakin yhden kaavan, joka ei ole lähtökohtien looginen seuraus.
Oletamme siis, että käytettävissä on kaava, joka sanoo, että solmu \(v\) on saavutettavissa solmusta \(u\). Se voi olla (2) tai se voi olla jokin muu. Emme ota kantaa miltä se oikeasti näyttää, mutta jotta voisimme puhua siitä, meidän täytyy merkitä sitä jotenkin. Merkitsemme sitä \(u \to^* v\).
Otamme tässä vaiheessa lähtökohdiksi seuraavat kaavat (myöhemmin jätämme osan pois):
\(\forall u: \forall v: u \to^* v\) (jokainen solmu on saavutettavissa jokaisesta solmusta)
kaava (1) (kustakin solmusta lähtee enintään yksi kaari)
\(\exists v_1: \exists v_2: v_1 \neq v_2\) (solmuja on ainakin kaksi)
\(\exists v_1: \exists v_2: \exists v_3: v_1 \neq v_2 \wedge v_1 \neq v_3 \wedge v_2 \neq v_3\) (solmuja on ainakin kolme)
\(\exists v_1: \exists v_2: \exists v_3: \exists v_4: v_1 \neq v_2 \wedge v_1 \neq v_3 \wedge {v_1 \neq v_4} \wedge v_2 \neq v_3 \wedge v_2 \neq v_4 \wedge v_3 \neq v_4\) (solmuja on ainakin neljä)
…(solmuja on ainakin viisi, solmuja on ainakin kuusi, …)
Viimeisen pompulan kohdalla olevat kolme pistettä edustavat äärettömän montaa kaavaa. On helppo keksiä, miten kukin niistä kirjoitetaan. Siksi mistä tahansa kaavasta voi testata, kuuluuko se lähtökohdiksi asettamiimme kaavoihin. Niinpä luvun “Looginen seuraus” lopussa asetettu vaatimus toteutuu.
Kolme ensimmäistä kaavaa sulkee pois suuren joukon suunnattuja graafeja. Alla olevassa kuvassa on pois suljetuista kolme esimerkkiä. Niissä ensimmäinen kaava ei toteudu, mutta toinen ja kolmas toteutuvat. Kolmannessa esimerkissä on äärettömän monta solmua ja kaarta.
Kolme ensimmäistä kaavaa jättää jäljelle vain alla olevassa kuvassa näytetyt suunnatut graafit, eli silmukat, jotka koostuvat 2, 3, 4, … solmusta ja kaaresta. On helppo tarkastaa, että jokainen sellainen suunnattu graafi toteuttaa kolme ensimmäistä kaavaa. Perustelemme kuvan jälkeen, että mikään muu suunnattu graafi ei toteuta.
Jos suunnatussa graafissa on alle kaksi solmua, niin se ei toteuta kolmatta kaavaa. Jos siinä on ainakin kaksi solmua ja jos jostakin solmusta ei lähde yhtään kaarta, niin siitä solmusta ei pääse muihin solmuihin, joten ensimmäinen kaava ei toteudu. Jos jostakin solmusta lähtee monta kaarta, niin toinen kaava ei ole tosi.
Tarkastamatta on enää suunnatut graafit, joissa on ainakin kaksi solmua ja jokaisesta solmusta lähtee täsmälleen yksi kaari. Valitaan jokin solmu ja kuljetaan siitä alkaen kaaria. Jos lopulta tullaan takaisin siihen solmuun, josta aloitettiin, ja jos matkan varrella käytiin jokaisessa solmussa, niin graafi on kuvan mukainen. Jos matkan varrella ei käyty jokaisessa solmussa, niin käymättä jääneet eivät ole saavutettavissa aloitussolmusta. Jos ei tulla takaisin siihen solmuun, josta aloitettiin, niin aloitussolmu ei ole saavutettavissa reitin muista solmuista. Kummassakaan tapauksessa ensimmäinen kaava ei ole tosi. (Tällaisista oli esimerkkejä aikaisemmassa kuvassa.)
Loput lähtökohtakaavat sanovat, että solmuja täytyy olla ainakin kolme, solmuja täytyy olla ainakin neljä, solmuja täyty olla ainakin viisi, …. Jos ne kaikki toteutuvat, niin solmuja on äärettömän monta. Se ei itsessään ole mahdotonta. Alla on esimerkki suunnatusta graafista, jossa on äärettömän monta solmua ja jossa jokainen solmu on saavutettavissa jokaisesta.
Mutta on mahdotonta, että solmuja on äärettömän monta, kustakin lähtee enintään yksi kaari, ja jokainen on saavutettavissa jokaisesta. Kun jostakin solmusta lähdetään kulkemaan kaaria pitkin, niin jos ei koskaan tulla takaisin siihen solmuun josta aloitettiin, niin aloitussolmu ei ole saavutettavissa reitin muista solmuista. Jos tullaan takaisin siihen solmuun josta aloitettiin, niin kuljettiin vain äärellinen määrä solmuja. Siinä tapauksessa reitin ulkopuolelle jäi äärettömän monta solmua. Ne eivät ole saavutettavissa aloitussolmusta.
Ei siis ole olemassa suunnattua graafia, joka toteuttaa jokaisen lähtökohdaksi asettamamme kaavan. Luvussa “Looginen seuraus” todettiin, että aina epätosi kaava \(\exists u: u \neq u\) on tällöin lähtökohtien looginen seuraus. Päättelyjärjestelmä pystyy todistamaan sen, koska tämän luvun alussa rajoituimme sellaisiin päättelyjärjestelmiin, jotka pystyvät todistamaan kaikki loogiset seuraukset.
Luvussa “Päätteleminen” kerrottiin, että kukin päättely käyttää vain äärellistä määrää lähtökohdiksi annettuja kaavoja. Siksi on olemassa jokin sellainen luku \(n\), että se päättely, joka todistaa \(\exists u: u \neq u\), ei käytä mitään kaavoista “solmuja on ainakin \(n+1\)”, “solmuja on ainakin \(n+2\)”, …. (Luvuksi \(n\) kelpaa suurin, joka löytyy niistä kaavoista “solmuja on ainakin \(n\)”, joita päättely käyttää. Jollei päättely käytä mitään niistä, voidaan valita \(n = 1\).)
Seuraavaksi tarkastelemme, mitä tapahtuu, jos poistamme käyttämättä jääneet kaavat lähtökohdistamme. Mainittu päättely menee edelleen läpi, koska se ei käytä poistettuja kaavoja. Toisaalta silmukka, jossa on \(n\) solmua ja \(n\) kaarta, toteuttaa kaikki jäljelle jääneet lähtökohtakaavat. Mutta \(\exists u: u \neq u\) ei päde sille. Niinpä päättelyjärjestelmä todistaa jäljelle jääneistä lähtökohdista kaavan \(\exists u: u \neq u\), joka ei ole jäljelle jääneiden lähtökohtien looginen seuraus.
Loppuhuomautuksia
Totesimme luvussa “Logiikan rajoista kertova tulos”, että tuloksestamme seuraa, että toisen kertaluvun logiikalle ei ole olemassa päättelyjärjestelmää, joka pystyy todistamaan kaiken sen mitä pitääkin mutta ei todista mitään liikaa. Suurella vaivalla voidaan todistaa, että ensimmäisen kertaluvun logiikalle on olemassa sellainen päättelyjärjestelmä. Se ja tuloksemme yhdessä kertovat, että ensimmäisen kertaluvun logiikalla ei voi ilmaista kaavana käsitettä “saavutettavuus”. Niinpä logiikassakin pätee sananlasku “suo siellä, vetelä täällä”.
Tässä kirjoituksessa esitelty tulos ei ole ensimmäinen logiikan rajoja koskeva tulos. Ensimmäinen oli 1930-luvulla suurella vaivalla todistettu tulos, joka on liian monimutkainen tässä kerrottavaksi. Mutta sillä on seuraus, joka voidaan kertoa tässä: ei voi olla olemassa menetelmää, joka pystyy selvittämään mistä tahansa kaavasta, joka noudattaa kohta kerrottavia rajoitteita, onko se tosi. Kaava puhuu luonnollisista luvuista (eli luvuista 0, 1, 2, …). Siinä ei saa esiintyä muuta kuin lukuvakioita kuten \(0\) ja \(1\), yhteenlaskuja “\(+\)”, kertolaskuja “\(\cdot\)”, yhtäsuuruuden vertailuja “\(=\)” sekä ensimmäisen kertaluvun logiikan symboleita.
Koska luonnolliset luvut ovat monen muun matemaattisen järjestelmän taustalla, seuraa tästä tuloksesta, että monella muullakaan matematiikan alalla ei voi olla olemassa menetelmää selvittää mistä tahansa sen alan kaavasta, onko se tosi.
Koska ensimmäisen kertaluvun logiikalle on olemassa edellä kerrotunlainen päättelyjärjestelmä, seuraa tuloksesta myös, että luonnollisten lukujen ominaisuuksia ei voi esittää kattavasti asettamalla lähtökohdaksi joukko ensimmäisen kertaluvun kaavoja, joka täyttää luvun “Looginen seuraus” lopussa mainitun menetelmäehdon.
Luonnollisten lukujen ominaisuudet voi esittää kattavasti toisen kertaluvun kaavoilla. Samaan tapaan kuin edellä saavutettavuuden käsitteen avulla, myös tätä kautta pääsee siihen johtopäätökseen, että toisen kertaluvun logiikalle ei ole olemassa päättelyjärjestelmää, joka todistaa kaiken sen mitä pitääkin eikä yhtään enempää.
Vuoden 1900 tienoilla matematiikka oli kriisissä. Matematiikka oli laajentunut uusille alueille ja vanhoilla alueilla saavutettiin entistä mahtavampia tuloksia, mutta samalla törmättiin ristiriitoihin, jotka kertoivat, että jotakin on pielessä. Kriisi ratkesi vähän kerrassaan vuoteen 1950 mennessä. Logiikalla oli suuri merkitys pielessä olleiden asioiden tunnistamisessa ja korjaamisessa, ja toisaalta kriisi vauhditti logiikan tutkimusta.
Näistä asioista kertoo vuonna 2009 ilmestynyt sarjakuvaromaani “Logicomix: Nerouden ja hulluuden rajalla” (Apostolos Doxiadis, Christos Papadimitriou, Alecos Papadatos ja Annie Di Donna). Siinä on pikkuisen otettu taiteilijan vapauksia historiallisten tosiseikkojen suhteen, ja myös matematiikan osalta on jouduttu jonkin verran vetämään mutkia suoriksi. Siitä huolimatta se on erittäin suositeltavaa lukemista. Se on ylivoimaisesti kiehtovin johdatus tähän aihepiiriin mitä löytää voi!