Stockmeyer induction
Fernando A.F. Ferreira · Birkhäuser Boston eBooks · 1990
In this work we define several first-order theories for the binary language (0,1)*, each one having induction restricted to a particular level of the Meyer-Stockmeyer (or polynomial time) hierarchy. We prove the most important (known) relationships between these theories using model-theoretic arguments. The only exception is in the proof of theorem II, where we make a simple use of a consequence of Gentzen’s Hauptsatz