Libal, T. (2008). Cut elimination in inductive proofs of weakly quantified theorems [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-26492
Schnittelimination; Gentzen; Beweistheorie; Induktion; Schnittregel; Peanoarithmetik; Gentzensche Beweis der Konsistenz der Peano-
de
Cut elimination; Gentzen; Proof Theory; Induction; Cut Rule; Peano Arithmetic; Gentzen's proof of the consistency of Peano Arithmetic
en
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.<br />
de
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.
