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.<br />
de
dc.description.abstract
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.<br />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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Schnittelimination
de
dc.subject
Gentzen
de
dc.subject
Beweistheorie
de
dc.subject
Induktion
de
dc.subject
Schnittregel
de
dc.subject
Peanoarithmetik
de
dc.subject
Gentzensche Beweis der Konsistenz der Peano-
de
dc.subject
Cut elimination
en
dc.subject
Gentzen
en
dc.subject
Proof Theory
en
dc.subject
Induction
en
dc.subject
Cut Rule
en
dc.subject
Peano Arithmetic
en
dc.subject
Gentzen's proof of the consistency of Peano Arithmetic
en
dc.title
Cut elimination in inductive proofs of weakly quantified theorems