A Possible and Necessary Consistency Proof

Visa fullständig post



Permalänk

http://urn.fi/URN:ISBN:978-952-10-6946-8
Titel: A Possible and Necessary Consistency Proof
Författare: Kanckos, Annika
Medarbetare: Helsingfors universitet, humanistiska fakulteten, institutionen för filosofi, historia, kultur- och konstforskning
Utgivare: Helsingin yliopisto
Datum: 2011-05-21
Språk: en
Permanenta länken (URI): http://urn.fi/URN:ISBN:978-952-10-6946-8
http://hdl.handle.net/10138/26114
Nivå: Doktorsavhandling (monografi)
Abstrakt: After Gödel's incompleteness theorems and the collapse of Hilbert's programme Gerhard Gentzen continued the quest for consistency proofs of Peano arithmetic. He considered a finitistic or constructive proof still possible and necessary for the foundations of mathematics. For a proof to be meaningful, the principles relied on should be considered more reliable than the doubtful elements of the theory concerned. He worked out a total of four proofs between 1934 and 1939. This thesis examines the consistency proofs for arithmetic by Gentzen from different angles. The consistency of Heyting arithmetic is shown both in a sequent calculus notation and in natural deduction. The former proof includes a cut elimination theorem for the calculus and a syntactical study of the purely arithmetical part of the system. The latter consistency proof in standard natural deduction has been an open problem since the publication of Gentzen's proofs. The solution to this problem for an intuitionistic calculus is based on a normalization proof by Howard. The proof is performed in the manner of Gentzen, by giving a reduction procedure for derivations of falsity. In contrast to Gentzen's proof, the procedure contains a vector assignment. The reduction reduces the first component of the vector and this component can be interpreted as an ordinal less than epsilon_0, thus ordering the derivations by complexity and proving termination of the process.De begränsningar av formella system som uppdagades av Gödels ofullständighetsteorem år 1931 innebär att Peanoaritmetikens konsistens endast kan bevisas med hjälp av fundamentala principer som inte kan formaliseras inom systemet. Trots att Hilberts finitistiska metoder inte kunde producera ett konsistensbevis, så fortsatte sökandet efter ett bevis med konstruktiva metoder. För att ett bevis skall vara meningsfullt borde principerna som används vara mera pålitliga än de element som betvivlas inom teorin. Avhandlingens titel hänvisar till ett citat av Gentzen då han motiverar behovet av konsistensbevis för första ordningens aritmetik. Gentzen själv producerade fyra konsistensbevis och analyserade hur väl dessa stämde överens med Hilberts program. Gentzen använde konstruktiva metoder i sina bevis, men det debatteras huruvida dessa metoder kan anses vara finitistiska. Det tredje och mest kända beviset presenterar en reduktion av härledningar av kontradiktioner. Med hjälp av transfinit induktion visas att reduktionsprocessen terminerar i en enkel härledning som konstateras vara omöjlig. Därför kan det inte finnas någon härledning av en kontradiktion. Avhandlingen undersöker och jämför Gentzens bevis från olika aspekter. Konsistensen av intuitionistisk Heytingaritmetik bevisas både i sekvenskalkyl och i naturlig deduktion. Det tidigare beviset är i Gentzens anda och innehåller ett snittelimineringsbevis för kalkylen och en syntaktisk studie av den aritmetiska delen av systemet. Det senare beviset påminner om ett normaliseringsbevis och visar terminering med hjälp av en vektortilldelning.Gödelin vuonna 1931 jullkaisemista epätäydellisyyslauseista seurausi rajoituksia formaalisille järjestelmille: Niiden mukaan Peano-aritmetiikan ristiriidattomuus voidaan todistaa ainoastaan periaatteilla, jotka eivät ole formalisoitavissa järjestelmän itsensä sisällä. Vaikka Hilbertin finitistisillä menetelmillä ei siksi pystytty tuottamaan konsistenssitodistusta, todistuksen etsiminen jatkui konstruktiivisillä menetelmillä. Jotta todistus olisi mielekäs, siinä käytettyjen periaatteiden oli oltava luotettavampia kuin teorian itsensä sisältämät periaatteet. Väitöskirjan otsikko viittaa Gentzenin kirjoitukseen, jossa hän perustelee ensimmäisen kertaluvun aritmetiikan konsistenssitodistuksen tarvetta. Gentzen itse laati neljä sellaista konsistenssitodistusta ja analysoi, missä määrin ne olivat yhdenmukaisia Hilbertin ohjelman kanssa. Gentzen käytti konstruktiivisia menetelmiä todistuksissaan ja on paljon väitelty kysymys, voidaanko näitä menetelmiä pitää finitistisinä. Kolmannessa ja tunnetuimassa Gentzenin todistuksessa esitetään ristiriitaisuuksien päättelyn reduktiomenetelmä. Transfiniittistä induktiota käyttämällä osoitetaan, että reduktioprosessi päättyy yksinkertaiseen päättelyyn, jollainen on erikseen todettu mahdottomaksi. Tämän vuoksi ristiriitaa ei voida päätellä. Väitöskirjassa selvitetään ja vertaillaan Gentzenin todistuksia eri näkökulmista. Intuitionistisen Heyting-aritmetiikan ristiriidattomuus osoitetaan sekä sekvenssikalkyylissä että luonnollisessa päättelyssä. Ensimmäinen todistus seuraa Gentzenin henkeä ja siinä sovelletaan ns. leikkaussäänön eliminointitodistusta sekä syntaktista analyysia järjestelmän aritmeettisesta osasta. Jälkimmäinen todistus muistuttaa luonnollisen päättelyn normalisointitodistusta ja näyttää reduktion päättymisen vektorimäärityksen avulla.
Subject: filosofia
Licens: Publikationen är skyddad av upphovsrätten. Den får läsas och skrivas ut för personligt bruk. Användning i kommersiellt syfte är förbjuden.


Filer under denna titel

Totalt antal nerladdningar: Laddar...

Filer Storlek Format Granska
apossibl.pdf 759.3Kb PDF Granska/Öppna

Detta dokument registreras i samling:

Visa fullständig post