Titelaufnahme

Titel
Cut elimination in inductive proofs of weakly quantified theorems / by Tomer Libal
VerfasserLibal, Tomer
Begutachter / BegutachterinLeitsch, Alexander
Erschienen2008
UmfangXII, 89 Bl.
HochschulschriftWien, Techn. Univ., Dipl.-Arb., 2008
Anmerkung
Zsfassung in dt. Sprache
SpracheEnglisch
DokumenttypDiplomarbeit
Schlagwörter (DE)Schnittelimination / Gentzen / Beweistheorie / Induktion / Schnittregel / Peanoarithmetik / Gentzensche Beweis der Konsistenz der Peano-
Schlagwörter (EN)Cut elimination / Gentzen / Proof Theory / Induction / Cut Rule / Peano Arithmetic / Gentzen's proof of the consistency of Peano Arithmetic
URNurn:nbn:at:at-ubtuw:1-26492 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Cut elimination in inductive proofs of weakly quantified theorems [0.47 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

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.

Zusammenfassung (Englisch)

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.