Unifying the model theory of first-order and second-order arithmetic via WKL0⁎

We develop machinery to make the Arithmetized Completeness Theorem more effective in the study of many models of IΔ0+BΣ1+exp, including all countable ones, by passing on to the conservative extension WKL0⁎ of IΔ0+BΣ1+exp. Our detailed study of the model theory of WKL0⁎ leads to the simplification and improvement of many results in the model theory of Peano arithmetic and its fragments pertaining to the construction of various types of end extensions and initial segments.