Subsystems of Open Induction

Abstract

We study subsystems of open induction obtained from restricting induction to atoms, literals, clauses, and dual clauses. We obtain an almost complete picture of the relationships between these systems in the language of arithmetic and its sublanguages in terms of inclusion and strict inclusion. The motivation for studying these systems is that they are strongly connected to methods of automated inductive theorem proving. As corollaries we obtain practically relevant independence results for such methods.