Peanon aritmetiikan todistuvuuden modaalilogiikka

Abstract

Tutkielmassa tarkastellaan miten alunperin välttämättömyyden ja mahdollisuuden tutkimiseen kehitettyä modaalilogiikaa voidaan hyödyntää matemaattisen formaalin järjestelmän todistuvuuden tutkimisessa. Tätä modaalilogiikan haaraa kutsutaan todistuvuuslogiikaksi. Tutkielma on yleisesitys todistuvuuslogiikan soveltamisesta Peanon aritmetiikkaan. Tutkielmassa esitetään modaalilogiikan todistusteoria, K-semantiikka ja tunnetuimmat normaalit systeemit, joista tärkein on Peanon aritmetiikan todistuvuuden tarkasteluun soveltuva systeemi GL. Myös Peanon aritmetiikan todistusteoria ja semantiikka esitellään sekä osoitetaan, miten Peanon aritmetiikka kykenee tarkastelemaan omaa todistuvuuttaan. Näiden pohjalta muodostetaan funktio, aritmeettinen muunnos, joka muuntaa kaikki modaalilogiikan lauseet Peanon aritmetiikan lauseiksi. Tutkielman keskeiset tulokset ovat systeemin GL kiintopistelause sekä systeemin GL aritmeettinen täydellisyys ja eheys, joiden mukaan modaalilogiikan lause A on todistuva systeemissä GL jos ja vain jos sen aritmeettinen muunnos A* on todistuva Peanon aritmetiikassa. Tutkielman lopuksi osoitetaan, että matemaattisen relevanssin lisäksi todistuvuuslogiikka vastaa tyydyttävästi Quinen modaalilogiikalle asettamaan luonteeltaan filosofisempaan haasteeseen.