Todistettavuuden raja Peanon aritmetiikassa

Abstract

Gödelin ensimmäisen epätäydellisyyslauseen nojalla Peanon aritmetiikka ei ole tarpeeksi vahva todistamaan kaikkia luonnollisille luvuille päteviä väittämiä. Osoittautuu, että laskettaville funktioille on olemassa täsmällinen funktion kasvunopeuteen perustuva ehto, jonka perusteella voidaan määrittää, onko laskettava funktio mahdollista todistaa hyvinmääritellyksi Peanon aritmetiikassa. Nopeasti kasvava hierarkia on transfiniittisellä rekursiolla määriteltävien funktioiden hierarkia, jossa jokainen funktio kasvaa nopeammin kuin sitä edeltävät funktiot. Jos laskettavan funktion voi todistaa hyvinmääritellyksi Peanon aritmetiikassa, niin sille on mahdollista esittää eksplisiittinen lauseke käyttäen ainoastaan tiettyjä aritmeettisia perusoperaatioita ja jotain kiinnitettyä nopeasti kasvavassa hierarkiassa ennen tasoa epsilon 0 esiintyvää funktiota. Tämän osoittamiseksi muodostetaan päättelysysteemi, jossa on mahdollista todistaa kaikki Peanon aritmetiikassa todistettavissa olevat tulokset, ja todistusten jokaiseen vaiheeseen liitetään sopiva ordinaali. Tämän ordinaalin ja sopivan tulkinnan avulla laskettavalle funktiolle saadaan lopulta edellä kuvailtu lauseke. Keskeinen osa todistusta on cut-säännön eliminointi, joka on yleinen todistusteoreettinen menetelmä. Cut-säännön eliminoinnin tavoitteena on muuntaa todistus muotoon, jossa jokaisesta vaiheesta on mahdollista päätellä käytetyn päättelysäännön perusteella edellinen vaihe, tai ainakin rajata mahdolliset edelliset vaiheet muutamaan vaihtoehtoon. Kenties tunnetuin konkreettinen esimerkki Gödelin epätäydellisyyslauseen mukaisesta tuloksesta Peanon aritmetiikassa on Parisin ja Harringtonin lause, joka koskee äärellisestä Ramseyn lauseesta muokattua kombinatorista periaatetta. Parisin ja Harringtonin lauseen mukaan tämä kombinatorinen periaate pätee luonnollisille luvuille, mutta ei ole todistettavissa Peanon aritmetiikassa. Kombinatorisen periaatteen perusteella voidaan muodostaa laskettava funktio, mikä tarjoaa mahdollisuuden esittää kombinatorinen todistus Parisin ja Harringtonin lauseelle. Todistuksessa osoitetaan, että kyseinen laskettava funktio kasvaa nopeammin kuin kaikki Hardyn hierarkiassa ennen tasoa epsilon 0 esiintyvät funktiot. Hardyn hierarkialla on läheinen yhteys nopeasti kasvavaan hierarkiaan, ja tuloksesta seuraa, ettei kyseiselle laskettavalle funktiolle ole mahdollista esittää aiemmin kuvailtua lauseketta, eikä sitä näin ollen voi todistaa hyvinmääritellyksi Peanon aritmetiikassa. Itse todistuksessa muodostetaan kombinatoriselle periaattelle vastaesimerkiksi kelpaava väritys, joka perustuu laskeviin jonoihin ordinaaleja.