An axiom system for the weak monadic second order theory of two successors

A compelte axiom system for the weak monadic second order theory of two successor functions, W2S, is presented. The axiom system consists, roughly, of the generalized Peano axioms and of an inductive definition of the finite sets. For the proof, methods of J. R. Buchi and J. Doner are used to obtain a new decision procedure for W2S, whose proofs are easily formalized. Different finiteness axioms are discussed. This paper was written while the author was visiting at Purdue University, and appeared first as Report CSD TR-56, Purdue University, 1971.