Title: Cut elimination in inductive proofs of weakly quantified theorems
Language: English
Authors: Libal, Tomer 
Qualification level: Diploma
Advisor: Leitsch, Alexander
Issue Date: 2008
Number of Pages: 89
Qualification level: Diploma
Abstract: 
In dieser Arbeit wird erst der Gentzensche Beweis der Konsistenz der Peano- arithmetik vorgestellt, dann wird die Methode auf eine Klasse induktiver Be- weise erweitert. Da die Schnittregel in der Peanoarithmetik nicht redundant ist, ist Schnittelimination nur für Teilklassen möglich; hier wird die Teilklasse aller induktiven Beweise von Sätzen ohne starke Quantoren untersucht. Es wird gezeigt, dass bei dieser Klasse alle essentiellen Schnitte eliminiert werden können.

After presenting Gentzen's cut elimination theorem and the proof of the consistency of Peano arithmetic, we extend the cut elimination procedure to a certain class of inductive proofs. Cut elimination is possible only on subclasses of all inductive proofs. We will investigate the subclass of inductive proofs of theorems without strong quantifiers.
We will show that all inductions can be removed following Gentzen's proof of the consistency of Peano arithmetic and therefore, that essential cuts are redundant.
Keywords: Schnittelimination; Gentzen; Beweistheorie; Induktion; Schnittregel; Peanoarithmetik; Gentzensche Beweis der Konsistenz der Peano-
Cut elimination; Gentzen; Proof Theory; Induction; Cut Rule; Peano Arithmetic; Gentzen's proof of the consistency of Peano Arithmetic
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-26492
http://hdl.handle.net/20.500.12708/11174
Library ID: AC05038838
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

7
checked on May 6, 2021

Download(s)

48
checked on May 6, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.