A Possible and Necessary Consistency Proof

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.

Grantor dc:publisher

Helsingin yliopisto

Year dc:date.issued

2011

Author dc:creator

• Kanckos, Annika

• filosofia

Statement dc:rights

• Julkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.
• This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
• 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.

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/10138/26114

OAI identifier oai:identifier

oai:helda.helsinki.fi:10138/26114