Introduction

We are going to investigate axiomatic theories formulated in the language L0 of arithmetic. Such a theory T is sound if the standard model N is a model of T, i.e. all axioms of T are true in N. If T is sound then, trivially, each formula provable in T is true in N. We confine our attention to theories containing a rather weak finitely axiomatized theory Q (which will be defined in a moment) and shall study an infinite hierarchy of sound theories whose union is called Peano arithmetic; the theories from the hierarchy are called fragments of Peano arithmetic. In this chapter and the next, we shall elaborate positive results on these theories, i.e. we shall show that the expressive and deductive power of these fragments is rather big: our aim will be to show how some amount of arithmetization of metamathematics yields the possibility of speaking inside a fragment of arithmetic not only of numbers but also of finite sets and sequences and of definable infinite sets of numbers. This is the main result of Sect. 1. In Sect. 2 we shall study the structure of the hierarchy of fragments, i.e. show various equivalent axiomatizations and several inclusions among fragments. Section 3 is devoted to the development of some recursion theory in fragments, notably to a proof of the Low basis theorem, which can be viewed as a strong form of König's lemma. (The Low basis theorem will be crucial in proofs of combinatorial principles in fragments; this will be done in Chap. II.) Finally Sect. 4 further develops metamathematics in fragments; among other things, the Low arithmetized completeness theorem, i.e. a strong form of the completeness theorem, will be proved.

Let us close this introduction with two remarks: first, the reader will find here (in Part A) actual proofs of various theorems in fragments, not only proofs of provability of these theorems. (Model-theoretic methods of proving provability of a sentence in a fragment can be found in Chap. IV.) It is hoped that the reader will feel comfortable in these fragments and will gain good practice in proving theorems in them.