Subsystems of open induction

Abstract

In [ Sho58 ] und [ She63 ] wurde gezeigt, dass es einfache, manchmal endliche, alternative Axiomatisierungen von offener Induktion in verschiedenen Kontexten der Arithmetik gibt. Dies eröffnet zwei Fragen: Benötigt man die gesamte offene Induktion, um diese alternativen Axiomatisierungen zu beweisen oder genügt eine echte Teilmenge? Gibt es solche alternativen Axiomatisierungen von offener Induktion nur im arithmetischen Kontext oder auch für andere induktive Datentypen? Wir zeigen in dieser Arbeit, dass unterschiedliche Teilsysteme der offenen Induktion oftmals gleich stark sind, in dem Sinne, dass sie die gleichen Formeln beweisen. Als Spezialfall sehen wir, dass die gesamte offene Induktion in verschiedene interessanten Fällen gleich viel beweist, wie Induktion über eine echte Teilmenge der Menge aller offenen Formeln (z.B. Literale). Darüber hinaus gibt es in Analogie zu den Resultaten von Shoenfield und Shepherdson in vielen der von uns betrachteten Fälle eine alternative einfache Axiomatisierung von offener Induktion.

In [ Sho58 ] and [She63 ] it was shown that there are simple, sometimes finite, alternative axiomatizations of open induction in the context of various arithmetical theories. This begs two questions: Does one need all open instances of the induction axiom to prove these alternative axiomatizations or do certain subsets suffice? Does this only work in the context of arithmetics or for other inductive data types as well? In this thesis, we show that various subsystems of open induction are equally strong in the sense that they prove the same theorems. In particular, in multiple interesting cases, open induction collapses to induction over a proper subset of the set of all open formulas (e.g. literals). Moreover, in many of the cases, we considered, there are simple axiomatizations of open induction in analogy to the results of Shoenfield and Shepherdson.