Elämä ja teos – ajatuksia Oiva Ketosen tieteellisen saavutuksen johdosta


Metatiedot
Kieli: 
Aihepiirit: 
Tekijät: 
Julkaistu: 
2001
Kuvaus: 

Jan von Plato

Elämä ja teos – ajatuksia Oiva Ketosen tieteellisen saavutuksen johdosta

Ajatus 59, 2002, 45–58.

Jan von Plato

Elämä ja teos – ajatuksia Oiva Ketosen tieteellisen saavutuksen johdosta

Ajatus 59, 2002, 45–58.

 

 

Elämä ja teos –
ajatuksia Oiva Ketosen tieteellisen
saavutuksen johdosta

 

JAN VON PLATO

 

Voi olla, että useimpien yliopiston professorien tieteestä ei jää mitään pysyvää jäljelle. Tuollainen kolmenkymmenen vuoden ajanjakso on riittävä asian varmistamiseksi, paitsi yllätystapauksissa. Joillakin on onni keksiä yksi merkittävä asia, jota voi sitten toistaa eri muodoissa. Helsingin yliopiston pitkäaikaisen filosofian professorin Oiva Ketosen tieteellinen ura oli merkillinen: Hän teki uransa alussa yhden asian ja jätti sen sitten täydellisesti. Myöhempi tuotanto muodostuu kirjoitte­lusta, jossa tieteellisyyden oleellinen tunnusmerkki, uuden, alkuperäi­sen tiedon tavoittelu, ei ole määräävä.

 

Ketonen syntyi vuonna 1913 suureen pohjalaiseen talonpoikais­perheeseen. Kansakoulun jälkeen Ketosen opinhalu vei hänet kouluun kaupunkiin, jonne kertyi matkaa lähemmäs kolmeakymmentä kilo­metriä. Matka taittui pyörällä. Ketonen opiskeli matematiikkaa ja filosofiaa Helsingin yliopistossa 1930-luvulla. Matematiikkaa dominoi Rolf Nevanlinna, tunnettu funktioteorian tutkija, ja filosofiaa Eino Kaila. Kaila oli teatraalinen persoona, joka tunsi vetoa taiteelliseen ilmaisuun ja tieteelliseen ankaruuteen. Vuosisadan alkuvuosikymme­ninä suuresti edistynyt fysiikka, ajan ja avaruuden suhteellisuusteoria sekä mikrokosmoksen kvanttimekaniikka kiehtoivat häntä. Hän luultavasti ajatteli, että luonnon perimmäisten salaisuuksien tutkimi­nen fysiikan tieteessä oli jalointa mihin ihminen pystyi. Filosofina Kaila tietysti tunsi sen mannermaisen filosofisen suuntauksen joka nosti ylimmäksi arvoksi tuollaisen tieteellisen credon, nimittäin loogisen empirismin. Hän hakeutui sen perustajien läheisyyteen ja toi sillä

 

-45-

 

tavalla modernin loogisen tutkimuksen Suomeen. Kaila itse ei ollut mikään loogikko, vaan lähinnä tietoteoreetikko.

 

1930-luku olijännittävää aikaa logiikanja matematiikan perusteiden tutkimuksessa. Edeltävän vuosikymmenen lopulla oli saavutettu yksi­mielisyys siitä, millä tavalla sellaisia matemaattisia teorioita kuin luonnollisten lukujen 0,1,2,... teoria pitää esittää formaalisesti, se on, absoluuttisella täsmällisyydellä. Pian kävi kuitenkin ilmi, ettei mitään äärellisesti esitettävää formalismia voi olla olemassa. Tämä kuuluisa Gödelin epätäydellisyystulos vei pohjan aiemmilta yrityksiltä löytää matematiikalle kestävät perusteet. Sellaisia oli yritetty kehittää saksa­laisen matemaatikon David Hilbertin johtamassa ns. todistusteoreetti­sessa koulukunnassa.

 

Todistusteorian tutkimus elpyi varsin pian Gödelin tulosten vuonna 1931 aiheuttamasta shokista. Saksalainen logiikan tutkimuksen nero Gerhard Gentzen (1909–1945) näytti väitöskirjassaan vuodelta 1933 tien eteenpäin. Pari, kolme vuotta myöhemmin Gentzen onnistui antamaan vastauksen Gödelin toisen epätäydellisyysteoreeman syn­nyttämään tilanteeseen. Tuon teoreeman mukaan formalisoidun aritmetiikan ristiriidattomuutta ei voida osoittaa sellaisella "finitistisel­lä" tavalla kuin Hilbertin koulukunta oli vaatinut. Gentzenin viimeinen työ vuodelta 1943, kaksi vuotta ennen hänen traagista kuolemaansa, toi täydellisen selvyyden toisen epätäydellisyysteoreeman tilanteeseen.

 

Yllä kuvattuun maastoon sijoittuu Ketosen pro gradu -tutkielma "Todistusteorian perusaatteet" joka julkaistiin vuonna 1938 Suomen filosofisen yhdistyksen Ajatus-vuosikirjassa. Ketonen lähti saman vuoden syksyllä Göttingeniin jatko-opiskelijana, työskentelemään Gerhard Gentzenin ohjauksessa. Hilbertin koulukunnan kantava voima Paul Bernays oli jo joutunut lähtemään Saksasta pakoon Zürichiin nelisen vuotta aikaisemmin.

 

Emme tiedä, mitä Ketonen oppi Gentzeniltä Göttingenissä. 1940­luvun alussa hän julkaisi pari pientä artikkelia todistusteoreettisista aiheista suomeksiAjatus-vuosikirjassa. Tarkka lukeminen osoittaa, että niiden taustalla oli jo merkittäviä keksintöjä. Sitten valmistui väitös­kirja Untersuchungen zum Prädikatenkalkül vuonna 1943, noin 70-sivui­nen pieni teos. Yritän seuraavassa selostaa, mitä Ketonen sai siinä

 

-46-

 

aikaan, mutta sitä ennen tehtäköön pari huomautusta noista vaikeista ajoista.

 

Ketosen tarkoitus oli ollut mennä Zürichiin syksystä 1939, työsken­telemään Bernaysin ohjauksessa, mutta maailmansodan alkaminen esti tämän. Väitöskirja on tehty täydellisessä yksinäisyydessä sanan intellektuaalisessa mielessä. Vastaväittäjänä toimi Lars Ahlfors. Hän oli Nevanlinnan oppilas ja yksi ensimmäisten Fields-mitalien ("matema­tiikan Nobel") voittajista vuonna 1936. Sodan jälkeen Ahlfors siirtyi Harvardin yliopiston professoriksi. Ketosen väitöskirjan esipuheessa kiitetään Ahlforsia "arvokkaista neuvoista väitöskirjan esitysmuodon yhteydessä." Olen aika varma, että Ketonen on tässä puhtaan asialli­nen: Ahlforsilla ei ollut edellytyksiä ymmärtää Ketosen työn todellista arvoa. Sitä varten olisi tarvittu todistusteoreettisen tutkimuksen syvällistä ymmärtämistä. Siksi neuvot lienevät koskeneet tulosten esittämistä eikä löytämistä. Sisällön puolesta Ketonen kiittää vain Gentzeniä, joka oli häntä vuonna 1938–39 "johdattanut tämän työn aihepiiriin."

 

Äärimmäisen vaikean loogisen tutkimuksen tekeminen edellyttää poikkeuksellista keskittymiskykyä. Jos sitten ei ole edes yhtä henkilöä, jonka kanssa voisi työn edistymisestä keskustella, onnistuminen lähentelee jo ihmettä. Ketonen vei työnsä loppuun, mutta tulosten esitystä voidaan luonnehtia itselle kirjoitetuksi sanalliseksi yhteen­vedoksi. Oliko Ahlfors ehkä vaatinut lisää selityksiä? Tietyssä pisteessä loogis-matemaattinen tutkimus vaatii metodista etenemistä, tyyliin "Määritelmä. Teoreema. Todistus." Lukijan täytyy itsensä käydä asiat formaalisesti läpi. Verbaaliset selitykset eivät tätä korvaa.

 

Ketosen väitöskirja muodostuu kolmesta kappaleesta. Ensin esi­tellään Gentzenin keksimä looginen kalkyyli, ns. sekvenssikalkyyli, johon Ketonen tekee oleellisia parannuksia. Toisessa kappaleessa määritellään kalkyylissa tehdyille formaalisille päättelyille tietynlainen normaalimuoto. Sen tarkoituksena on tehdä mahdolliseksi pääteltä­vyyden vastakohtaa eli päättelyn mahdottomuutta koskevat tulokset. Tällaisia tuloksia tarvitaan esimerkiksi kun halutaan osoittaa päättelysääntöjen järjestelmä ristiriidattomaksi. Matemaattisen teorian aksioomien keskinäinen riippumattomuus voidaan myös osoittaa

 

-47-

 

päättelemättömyystodistusten kautta. Väitöskirjan kolmannessa kap­paleessa johdetaan juuri tuollaisia tuloksia alkeisgeometrian järjes­telmille. Kohokohtana on Eukleideen paralleeliaksiooman riippumat­tomuuden todistus muista aksioomista päättelemättömyystuloksen kautta.

 

Logiikan tutkimuksen johtoajatuksena 1930-luvulle asti oli ollut, että tutkimuksen kohteena ovat erityiset "loogiset totuudet." Wittgen­steinin Tractatuksen sanoin, tuollaiset totuudet ovat "tautologisia," ne eivät sulje pois mitään todellista maailmaa koskevaa asiantilaa. Siksi ne eivät myöskään sano mitään tuosta maailmasta. Tätä ajatusta yleistäen tultiin ideaan, että myös matemaattiset totuudet ovat "tyhjiä tautologi­oita." Logiikan tutkimuksen yhtenä keskeisenä ongelmana Gottlob Fregestä ja Bertrand Russellista lähtien oli ollut näyttää, miten mate­maattiset totuudet voidaan johtaa kaikkein perustavimmista loogisista totuuksista. Oikeastaan voisimme tähän liittää myös George Boolen nimen, joka 1850-luvulla kehitti algebrallista logiikan teoriaa, nykyistä lauselogiikkaa, otsikon "The Laws of Thought" alla.

 

Gentzenin väitöskirja Untersuchungen über das logische Schliessen vuodelta 1933 hylkäsi täydellisesti tuon Fregen ja Russellin käsityksen, jonka myös Hilbertin koulukunta oli muunneltuna omaksunut. Logiikka on teoria aukottoman argumentoinnin rakenteesta, matema­tiikan sisällä siis aukottoman todistamisen. Sen tulosten perusmuoto on: "Jos oletukset A,B,C,... on tehty, niin D,E,F,... seuraavat." Päättelyn muoto on hypoteettinen, oletuksista johtopäätöksiin, kun taas Fregen, Russellin, ja Hilbertin logiikassa hypoteeseilla ei ollut muodollista esitystä. Tänä päivänä saattaa tuntua merkilliseltä, että Boolesta ja Fregestä lähtevä logiikka ensimmäisinä vuosikymmeninään niin radikaalisti poikkesi vanhasta aristoteelisesta ideasta, logiikasta "demonstratiivisen argumentoinnin tieteenä." Toisaalta kaikki loogikot eivät ole vieläkään omaksuneet Gentzenin loogista vallankumousta.

 

Gentzeniä seuraten logiikan tehtävänä on huolehtia vain oletuksista johtopäätöksiin vievien askeleiden korrektisuudesta. Itse asiassa koko tavanomainen predikaattilogiikka muotoillaan niin, ettei siinä ole edes yhtä loogista aksioomaa, vaan pelkkiä päättelysääntöjä. Yksinkertai­simmat tällaiset askeleet koskevat lauselogiikkaa, eli konnektiivien

 

-48-

 

"ja", "tai", "jos..., niin ...", ja "ei" formaalisten vastineiden logiikkaa. Konnektüvilla & muodostamme kahden annetun lauseen A ja B kon­junktion A & B ("A ja B"). Konjunktiomuotoisen lauseen päättele­miseksi on riittävää, että on päätelty sen jäsenet A ja B erikseen. jälkimmäiset ovat tämän säännön "premissit," konjunktio taas sen "johtopäätös." Vastaavasti disjunktion A V B ("A tai B") päättelemisek­si on riittävää, että on päätelty vähintään yksi vaihtoehdoista A ja B. Näitä riittäviä ehtoja kutsutaan Gentzeniä seuraten vastaavien konnek­tiivien tuontisäännöiksi. Kolmas konnektiivi AÉB ilmaisee ehtolau­seen ("jos A, niin B"). Sen päättelemiseksi on riittävää olettaa A ja päätellä tästä oletuksesta B. Jos tämä ns. hypoteettinen päättely onnistuu, voidaan päätellä ehtolause AÉB. Samalla väliaikainen oletus A poistetaan päättelyn oletuksien listalta. Negaatiota "ei' voidaan käsitellä parilla eri tavalla jotka sivuutamme tässä.

 

Gentzen antoi toiseksi eri muotoja oleville lauseille käänteiset poistosäännöt. Kun tuontisäännöt antavat riittävät ehdot annettua muotoa olevan lauseen päättelemiseksi, poistosäännöt antavat välttä­mättömät ehdot noille lauseille. Ne siis lausuvat, mitä annettua muotoa olevasta lauseesta välittömästi seuraa. Konjunktion A & B välittömät seuraukset ovat A ja B erikseen. Ehtolauseesta AÉB seuraa, kun myös ehto A on päätelty, lause B. Disjunktion sääntö on monimutkaisempi ja jätämme sen tässä sivuun.

 

Olkoon nyt annettuina oletukset A,B,...,C ja väitetty johtopäätös D. Gentzenin tuontisääntöjen avulla yritämme analysoida pääteltävän lauseen D osasiin jotka riittävät D:n päättelemiseksi. Poistosääntöjen avulla taas yritämme analysoida oletuksia A,B,...,C. Jos kaikki käy` hyvin, molemmat analyysit kohtaavat. Analyysin helpottamiseksi Gentzen kehitti täsmällisemmän loogisen kalkyylin, edellä jo mainitun sekvenssikalkyylin, ja näytti, että lauseloogiset päättelyt voidaan aina tehdä analysoimalla oletuksia ja johtopäätöstä osiin. Päättelyn onnistu­rniseksi ei tarvitse ottaa käyttöön mitään, mikä ei jo piilevästi sisälly oletuksün ja johtopäätökseen. Sanotaan nyt vaikka, että annetuista lähtökohdista maaliin pääseminen voi yleensä elämässä vaatia yllättä­viä kiertoteitä, mutta puhtaassa logiikassa sellaisia ei Gentzenin

 

-49-

 

mukaan tarvita. Tämä tulos on nimeltään Gentzenin päälause, tai "leikkausten eliminoimisteoreema."

 

Gentzen ei onnistunut ihan täydellisesti analyyttisen loogisen kalkyylin kehittämisessä. Ketosen väitöskirjan ensimmäinen kappale vie tämän perille: Ketonen keksi, että lauselogiikan päättelysäännöt voidaan muotoilla "invertiibelisti." Tämä sääntöjen ominaisuus on seuraava: Jos johtopäätöksen muoto on sellainen, että se voisi olla tietyn säännön avulla päätelty ja jos tuo johtopäätös on todella päätel­tävissä, säännöstä ilmenevät premissit ovat myös pääteltävissä. Sääntöjen luonteeseen kuuluu, että johtopäätös seuraa premisseistä. Ketonen näytti, että lauselogiikka voidaan muotoilla niin, että kääntei­nen pätee: Johtopäätös voidaan korvata sen kanssa yhtäpitävillä premisseillä. Lauselogiikan tapauksessa nämä premissit ovat, sano­kaamme, "yhtä askelta yksinkertaisempia" kuin johtopäätös. Siksi johtopäätöstä D ja oletuksia A,B,..., C analysoivat askeleet vievät lopulta yhtäpitävään tilanteeseen, jossa mitään analysoitavaa ei ole jäljellä. Jos D todella on pääteltävissä oletuksista A,B,...,C, tilanne on muotoa: E on pääteltävissä oletuksesta E, F on pääteltävissä oletuksesta F,..., missä E,F,... ovat yksinkertaisimpia, analysoimattomia oletusten A,B,...,C ja johtopäätöksen D osia. Päinvastaisessa tapauksessa törmäämme aina­kin yhteen tilanteeseen jossa olisi tehtävä päättely oletuksesta E johto­päätökseen F. Kun näillä ei ole mitään loogista muotoa, niillä ei myöskään voi olla mitään pääteltävyysyhteyttä. Siksi alkuperäinen päättelytehtävä D:hen oletuksista A,B,...,C ei voi koskaan onnistua.

 

Ketosen kalkyylin sivutuotteena saadaan kaunis todistus lauselogii­kan täydellisyydelle ja mekaaninen menetelmä päättelyiden etsimisek­si. Voimme pitää Ketosen analyyttista kalkyylia Leibnizin ja muiden unelmien täyttymyksenä lauselogiikan rajoitetussa maailmassa.

 

Lauselogiikkaa paljon monimutkaisempi on kvanttorien "kaikki" ja "on olemassa" yhdessä lauselogiikan kanssa muodostama predikaatti­logiikka. Gentzen oli näyttänyt, että lauseloogiset päättelyaskeleet voidaan erottaa kvanttorien päättelyaskeleista. Jälkimmäisissä on aina vain yksi premissi, edellisissä yksi tai kaksi. Konnektiivien ja kvantto­rien päättelyaskeleiden erottaminen voidaan visualisoida niin, että päättelyt muodostavat puun jonka runkona on, päättelyn lopusta eli

 

-50-

 

puun juuresta katsoen, ensin kvanttoriaskeleita, sitten lauseloogisten askeleiden muodostama latvaosa jossa puu voi haarautua. Välissä on tietty pääteltävyyttä ilmaiseva ns. «keskisekvenssi. Ketonen paransi Gentzenin tulosta näyttämällä, miten kvanttoripäättelyaskeleiden lukumäärä voidaan minimoida: kvanttoriosa on silloin mahdollisim­man yksinkertainen. Tällaisen päättelyn hän sanoo olevan normaali­muodossa. Ketosen analyyttinen menetelmä mekanisoi lauseloogisen päättelyn, mutta vuodesta 1936 tiedettiin, Alonzo Churchin kuuluisan tuloksen perusteella, että päättelyn löytämistä predikaattilogiikassa ei voida samalla tavalla mekanisoida. Ketosen kiinnostuksen kohde oli kuitenkin ensi sijassa päättelemättömyys. Ideaa yksinkertaisimmasta mahdollisesta päättelystä voidaan Ketosta seuraten soveltaa seuraavas­ti: Oletetaan, että väitetty päättely D:hen oletuksista A,B,...,C on mahdollinen. Silloin on olemassa yksinkertaisin mahdollinen päättely normaalimuodossa. Tutkimalla oletuksia ja väitettyä johtopäätöstä voidaan määrätä mekaanisesti periaatteessa rajoittamaton sarja mahdollisia keskisekvenssejä M1,M2,M3,... Jos väitetty päättely on mahdollinen, on olemassa joku n siten että Mn, on päättelyn keskisek­venssi. Se voidaan johtaa mekaanisesti suoritettavilla lauseloogisilla askeleilla. Kokonaismenetelmä ei kuitenkaan ole mekaaninen: Kunkin keskisekvenssin M1M2M3,... pääteltävyys voidaan tarkastaa, mutta mikään äärellinen määrä negatiivisia vastauksia ei takaa, etteikö tulevaisuudessa voisi löytyä pääteltävää keskisekvenssiä. Ketonen pyrkii löytämään tilanteita, joissa voidaan asettaa yläraja mahdollisten keskisekvenssien lukumäärälle. Yksinkertaisimmassa tapauksessa hän osoittaa, että jos jollekin n keskisekvenssi Mn, on pääteltävissä, jo M1, on pääteltävissä. M1 ei kuitenkaan ole pääteltävissä, eikä siksi mikään Mn. Niin kuin todettiin, menetelmä ei ole yleispätevä, mutta sitä voidaan soveltaa monissa yksittäistapauksissa, usein monimutkaisten valmiste­lujen jälkeen.

 

Ketosen varsinainen kohde oli soveltaa puhtaan logiikan parissa kehitettyjä analyysimenetelmiä matematiikassa. Matematiikan peruste­tutkimuksen keskeiset ongelmat ovat: teorioiden esittäminen aksio­maattisina formaalisina järjestelminä, näiden ristiriidattomuuden ja aksioomien keskinäisen rüppumattomuuden todistaminen, kysymys

 

-51-

 

järjestelmien täydellisyydestä, ja viimeisenä kysymys ratkaisumenetel­män olemassaolosta. Viimeinen voidaan vielä rajoittaa koskemaan sopivan yksinkertaista muotoa olevia lauseita. Kun keskeiset ongelmat muotoillaan todistusteorian termein, päättelyiden mahdottomuutta koskevat tulokset nousevat esille.

 

Väitöskirjan kolmannessa kappaleessa Ketonen soveltaa kehittä­miään menetelmiä alkeisgeometriaan. Suuri edeltäjä on norjalainen Thoralf Skolem (1887–1963). Eräässä unohtuneessa työssään vuodelta 1920 Skolem oli kehittänyt menetelmiä päättelyjen mahdottomuus­todistuksille. Hän oli soveltanut niitä hilateoriaan ja projektiiviseen tasogeometriaan. Edellistä voidaan yleisin termein luonnehtia Boolen aloittaman algebrallisen loogisen tradition nykyaikaisena muotona. Hila on matemaattinen rakenne, joka vastaa suunnilleen konnektiivien "ja" ja "tai" logiikkaa. Hilarakenne syntyy myös, jos tarkastellaan Dedekindin tavoin kahden luonnollisen luvun suurinta yhteistä jakajaa ja pienintä yhteistä jaettavaa. Edelleen hiloihin törmätään kun tutkitaan topologisten avaruuksien ns. avoimien joukkojen algebrallista raken­netta. Skolem oli siis kehittänyt todistusteoreettisia menetelmiä hilateoriaa varten jo kauan ennen Gentzenin aikaa. Keskeisenä tulok­sen oli, että jos väitteeseen ei kuulu eksistenssikvanttoreita, sen pääteltävyys hilateoriassa ja projektiivisessa geometriassa voidaan ratkaista mekaanisesti. Skolemin ratkaisumenetelmä hilateorialle on vielä ns. polynomiaikainen algoritmi. Eräät amerikkalaiset tutkijat olivat löytäneet yhtä tehokkaita algoritmeja 1980-luvun lopulla, vuosikymmenien kehityksen jälkeen. Oli suuri shokki kun heille vuonna 1992 paljastui, että Skolem oli pystynyt samaan täysin yksin seitsemänkymmentä vuotta aikaisemmin. Mikä on tilanne projektiivi­sessa geometriassa, sitä en osaa sanoa.

 

Ketonen muotoilee ensin Skolemin tarkasteleman geometrian aksioomajärjestelmän Gentzenin sekvenssikalkyylin termein. Hän antaa toisessa kappaleessa kehittämällään menetelmällä projektiivisen geometrian ristiriidattomuustodistuksen, sitten Skolemin ratkaisu­menetelmää vastaavan tuloksen. Seuraavaksi tarkastelu laajennetaan affiiniin tasogeometriaan jossa Eukleideen paralleeliaksiooma voidaan ilmaista. Siinä on projektiivisen geometrian yhdyssuorien ja leikkaus­-

 

-52-

 

pisteiden lisäksi myös annettujen suorien paralleelit annettujen pisteiden kautta. Ketosen työ huipentuu sen näyttämiseen, että mikään päättely ei voi johtaa paralleeliaksioomaan kun muut affiinin geomet­rian aksioomat sallitaan oletuksina.

 

Ketonen päätyy suuren vaivan jälkeen tulokseen, joka tunnettiin jo yli sata vuotta ennen, ns. epäeuklidisten geometrioiden keksimisen aikana. Mikä edistys asiaan sisältyy, siitä esitettäköön pari huomautus­ta. Kaikkien mahdollisten päättelyiden rakenteen tunteminen (normaa­limuotoisten, muista meidän ei tarvitse välittää) alkeisgeometriassa, matemaattisista tieteistä vanhimmassa, on itsessään tärkeää. Sivutuot­teina saadaan mm. ratkaisumenetelmiä yksinkertaisimpiin tapauksiin, esim. puhtaasti universaalisiin lauseisiin. Toiseksi, epäeuklidiset geometriat antavat malleja, joissa muut aksioomat paitsi paralleeli­aksiooma pätevät. Nämä mallit käyttävät reaalilukuja, mutta reaali­lukujen aritmetiikan todistusteoreettinen tutkimus ei ole toistaiseksi johtanut niiden perusteelliseen ymmärtämiseen. Ketosen riippu­mattomuustodistukset perustuvat paljon heikompiin oletuksiin kuin mitä reaalilukujen teoriassa tarvitaan. Ne korostavat "metodien puhtautta," joilla todistusteoriassa analysoidaan aksiomaattisia järjestelmiä.

 

Ketosen onni oli, että neutraalissa Sveitsissä asuva Paul Bernays kirjoitti arvioita eurooppalaisista logiikan töistä sen ajan ainoaan logiikan lehteen, USA:ssa ilmestyvään The Journal of Symbolic Logiciin. Tiedonvälitys ei ollut aukotonta: Olen esimerkiksi nähnyt kirjeen, jonka Bernays lähetti Georg Henrik von Wrightille ja jossa lukee, että jälkimmäisen kirjoittamat arviot lehteen ovat tuhoutuneet koska niitä kuljettanut postin kone joutui ilmahyökkäyksen kohteeksi.

 

Bernays kirjoitti pitkän arvion Ketosen väitöskirjasta JSL:n joulu­kuun 1945 numeroon. Siinä selvitetään ensin Ketosen tekemät muutok­set Gentzenin kalkyyliin. Uudet säännöt ovat hyvin esillä arvion ensimmäisellä sivulla. Niiden invertiibeliys käydään huolellisesti läpi, samoin kuin tämän ominaisuuden keskeiset seuraukset. Toisen kap­paleen uutuus, keskisekvenssien jonon määrittely normaalimuotoisille päättelyille tulee myös esiin, mutta ei ihan optimaalisesti. Bernays esittää, että pääteltävyydestä ylipäänsä seuraa jonkun keskisekvenssin

 

-53-

 

Mn, pääteltävyys samoin kuin kaikkien sitä seuraavien sekvenssien Mm, missä m on suurempi kuin n. Ketosen määrittelemät keskisekvenssit ovat yleisimpiä mahdollisia seuraavassa mielessä: Aina kun joku keskisekvenssi on pääteltävissä, ei välttämättä Ketosen määritelmän mukainen, myös joku Ketonen-keskisekvenssi on pääteltävissä. Nämä yleisimmät mahdolliset keskisekvenssit ovat heikoimpia mahdollisia pääteltävyyden suhteen. Mihin sitten tarvitsemme niitä? Ketosen pää­määränä olivat päättelemättömyystulokset. Jos joku keskisekvenssi on pääteltävissä, joku Ketosen määrittelemä keskisekvenssi Mn, on pää­teltävissä. Kääntäen, jos mikään Ketosen keskisekvenssi ei ole pääteltä­vissä, seuraa, ettei mikään keskisekvenssi ole pääteltävissä, eikä mitään päättelyä ylipäätänsä voi olla olemassa. Ketosen heikoimmat mahdolli­set keskisekvenssit palvelevat juuri tätä päämäärää, mutta tämä metodisesti keskeinen huomautus on vain epäsuorasti luettavissa Bernaysin arviosta.

 

Ketosen normaalimuotoisten päättelyiden keskisekvenssien avulla voidaan parantaa hiukan tunnettua Gödelin tulosta predikaattilogiikan täydellisyydestä. Ketonen on selostanut asian yleisin termein suomen­kielisessä artikkelissa joka ilmestyi Ajatus-vuosikirjassa vuonna 1941. Tuloksesta on maininta Manfred Szabon toimittaman Gentzenin koottujen töiden esipuheessa vuodelta 1969. Gödelin tuloksen mukaan jokainen predikaattilogiikan lause on joko pääteltävissä, tai sitten on mahdotonta, ettei sille ole kumoavaa vastaesimerkkiä. Ketosen pa­rannus on, että jälkimmäinen voidaan korvata suoralla kumoamisella. Keskisekvenssin systemaattinen etsiminen antaa mahdollisuuden määritellä kumoava vastamalli suoraan. Ketonen kertoi minulle, että hänen opiskelutoverinsa Max Söderman tunsi Gödelin 1930-luvun loppupuolella Wienissä ja selosti Ketosen tuloksen tälle. Jälkimmäinen myönsi, että täydellisyystulos Ketosen tavalla on hieman vahvempi. Tarinasta voimme päätellä, että Ketosella oli uusia merkittäviä tuloksia jo ennen sotien alkua.

 

Bernaysin arviossa tarkastellaan seuraavaksi päättelemättömyys­todistusten soveltamista geometriaan. Tässä vaiheessa, vuonna 1945, Bernays on lukenut tarkkaan Skolemin työn vuodelta 1920. Hän mainitsee sen keskeisiä tuloksia ja miten Ketonen laajentaa niitä

 

-54-

 

affiiniin tasogeometriaan. Kuitenkin hän sanoo, että "kaikki nämä kolmannen kappaleen todistelut, joiden tarkoituksena on osoittaa Ketosen metodien tehokkuus,... ovat varsin monimutkaisia ja vaativat työteliäitä selityksiä." Seuraavaksi väitetään, että Ketosen tarkastelut voidaan korvata yksinkertaisemmilla, sellaisilla joita arvioija itse on esittänyt kirjassa Grundlagen der Mathematik (toinen osa vuodelta 1939). Nämä arviot koskevat Ketosen päättelemättömyystuloksia. Lopussa Bernays arvelee, että Ketosen menetelmät ovat ehkä parhaat silloin kun kysymyksessä on todistuvien lauseiden päättelyjen etsiminen.

 

Ainakin kaksi amerikkalaista loögikkoa luki huolellisesti Bernaysin arvion: Haskell B. Curry otti käyttöön Ketosen kalkyylin, ensin pikku kirjassa vuodelta 1950, sitten oppikirjassa Foundations of Mathematical Logic vuodelta 1963. Hän oli myös kiinnostunut Ketosen täydellisyys­todistuksesta predikaattilogiikalle. Curryn kappaleessa Ketosen väitöskirjaa on tämän suuntaisia reunamerkintöjä. (Tieto on peräisin Jonathan Seldiniltä.) Curry piti Ketosen väitöskirjaa parhaana työnä todistusteoriasta Gentzenin töiden jälkeen.

 

Stephen Kleenen paljon luettu Introduction to Metamathematics vuodelta 1952 käyttää osaksi Ketosen loogista kalkyylia, jonka Kleene tunsi vain Bernaysin arvion kautta.

 

Toinen arvio Ketosen työstä ilmestyi lehdessä Mathematical Reviews vuonna 1948. Kirjoittaja oli hollantilainen intuitionistisen logiikan kehittäjänä tunnettu Arend Heyting. Se on lyhyt yhteenveto, jossa mainitaan Ketosen johtavan riippumattomuustuloksia alkeisgeomet­riassa Gentzenin tyyppiselle logiikan formalisoinnille määritellyn normaalimuodon kautta.

 

Varhaisin viittaus Ketosen väitöskirjaan taitaa olla Karl Popperin artikkelissa "New foundations for logic" vuodelta 1947. Siinä kehitel­lään teoriaa loogisesta päättelystä, jossa on piirteitä Gentzenin ja Ketosen kalkyyleista.

 

Tämän päivän näkökulmasta Ketosen työn merkitys on selvästi kasvanut. Tietojenkäsittelytieteen kehitys on johtanut järjestelmiin, jotka etsivät todistuksia automaattisesti. On kehitetty sekvenssikalkyy­leita, jotka soveltuvat erityisesti tähän. Troelstran ja Schwichtenbergin kirjasta Basic Proof Theory (Cambridge 1996) pystymme lukemaan

 

-55-

 

jatkuvan kehityslinjan Gentzenistä Ketosen, Kleenen, Curryn, ja Schütten kautta Dragalinin työhön vuodelta 1978, ja mainittuun Troelstraan. Kaikki nämä ovat vaikuttaneet oleellisesti ns. "kontrak­tiovapaiden" sekvenssikalkyylien kehittämisessä. Nämä kalkyylit ovat nykyisen strukturaalisen todistusanalyysin keskeisiä välineitä. Näitä käyttävät tutkijat eivät tietenkään aina tarkkaan tiedä, minkälainen historiallinen kehitys niiden takana on.

 

Ketosen kunnianhimoinen päämäärä oli soveltaa logiikan todistus­teoreettisia menetelmiä matemaattisiin järjestelmiin. Bernaysin mukaan hänen oma "yleinen konsistenssiteoreemansa" palvelee tätä tarkoitusta paremmin kuin Ketosen metodit, mutta tämä ei ole toteutunut. Ketosen ensimmäinen yritys jäi täydellisesti unohduksiin täsmälleen kuten Skolemin kaksikymmentäneljä vuotta aikaisemmin. Troelstra mainitsee kirjassaan Ketosen väitöskirjan edelläkävijänä sekvenssi­kalkyylin soveltamisessa aksiomaattisiin järjestelmiin. Kirjan Basic Proof Theory toisessa laitoksessa (2000) selostetaan uudenlaista lähestymis­tapaa tällaiseen soveltamiseen, missä aksioomat käännetään samanlai­siksi päättelysäännöiksi kuin itse sekvenssikalkyylin loogiset säännöt. Näyttäisi, että todistusanalyysin soveltaminen matematiikassa tulee selvästi yksinkertaisemmaksi, kun näin menetellään.

 

Ketosen väitöskirjassa todetaan muutaman aiheen kohdalla, että kirjoittaja suunnittelee tarkempien tutkimusten julkaisemista niistä. Siitä ei kuitenkaan tullut mitään, ja tulemme lopuksi kysymykseen, miksi Ketonen ei koskaan jatkanut loogisia tutkimuksiaan. Hänen saavutuksensa todellista merkitystä ei kukaan Suomessa voinut täysin nähdä. Bernaysin arvion kautta Ketosen looginen kalkyyli tuli tunne­tuksi, mutta muut osat jäivät myös kansainvälisesti unohduksiin. Gentzen olisi ollut Ketoselle ideaalinen lukija, mitä koskee predikaatti­loogisten päättelyiden normaalimuotoa, keskisekvenssien määrittelyä, ja niiden soveltamista matematiikassa. Gentzen oli kuitenkin kärsinyt elokuussa 1945 nälkäkuoleman, eikä ole merkkiä siitä, että hän olisi edes nähnyt Ketosen väitöskirjaa (ks. Menzler-Trott, Gentzens Problem: mathematische Logik im nationalsozialistischen Deutschland, 2001). Ketonen itse oli varmasti tietoinen saavutuksensa merkityksestä. Työstä näkyy hillitty innostus, jolla Gentzenin analyysimenetelmiä halutaan laajentaa

 

-56-

 

puhtaasta logiikasta matematiikkaan, ja vakaumus, että nämä menetel­mät tuottavat ne parhaimmat tulokset. Yhdellä Suomessa sodan aikana ilmestyneellä työllä ei saa tarvittavaa näkyvyyttä: Olisi tarvittu enemmän kärsivällisyyttä, jatkotöitä ja todistusanalyysien soveltamista uusille matematiikan alueille.

 

Matemaatikkona Ketosella oli luultavasti vain vähäiset mahdolli­suudet hankkia itselleen pysyvä paikka yliopistossa. Logiikka ja perustetutkimus matematiikan haarana olivat luksusta, joihin isoilla mailla oli varaa. Toisaalta modernin logiikan tutkimus oli Kailan vaikutuksesta vakiintunut myös osaksi filosofiaa. Logiikan tutkimuk­sen sijasta Ketonen kirjoitti teoksen Suuri maailmanjärjestys (1948), filosofoivan kirjan maailmankuvan kehityksestä. Se on hyvin kirjoitettu niin kuin suurin osa Ketosen tuotannosta, mutta sitä ei voida kuiten­kaan pitää varsinaisena tieteellisenä, uuteen tietoon tähtäävänä tutkimuksena.

 

Kun Kaila siirtyi akateemikoksi, Ketonen haki vapaaksi jäänyttä teoreettisenfilosofian professuuria. Keskusteltiin, voiko matemaatikos­ta sellaista tulla, ja mitä vaaroja tähän voisi sisältyä. Ketosesta tuli filosofian professori, mutta nerokas todistusteoreetikko katosi. Ketonen toimi opettajana ja tiedepolitiikassa aina huipulla asti, ministeriön korkeakouluosaston johtajana. Samaan aikaan suomalainen filosofia kukoisti von Wrightin, hänen oppilaansa Jaakko Hintikan ja Erik Steniuksen töiden kautta.

 

Myöhempinä vuosinaan Ketonen selitti joskus jättäneensä logiikan tutkimuksen "päänsäryn" vuoksi. Käytännöllistä syytä, nimittäin sopivaan virkaan pätevöitymistä, ei ollut: hän olisi nimityksen jälkeen voinut vapaasti jatkaa todistusteoreettisia töitään. Voimme spekuloida psykologisilla selityksillä: On poikkeuksellista tehdä täysin yksin äärimmäisen vaikeita loogisia tutkimuksia sotien keskellä. Viime mainittu pätee aivan kirjaimellisesti: Ketonen kertoi kerran kirjoit­taneensa väitöskirjaa Äänisjärven rantatöyräillä, syvällä sen ajan Neuvostoliitossa. Oliko yksityisen loogisen maailman luominen pakoa todellisuudesta? Keskittyminen tuollaisissa oloissa vaatii syvältä tulevaa motiivia. Hävisikö se rauhan ja arkielämään palaamisen myötä? Ketosen eläkevuosien yksi harrastus oli ihmismielen, sen

 

-57-

häiriöiden ja niitä parantavan psykoterapian kysymysten pohtiminen. Ehkäpä häntä olisivat huvittaneet edellä esitetyt arvelut.

 

-58-