Consistency, Decidability, Completeness for the Arithmetic of Order with Successor

I shall employ the calculi ccqt, presented in Chapter 2.9, but as I consider sets C of sentences, I may as well use the calculi ccqs. (cf. Lemma 2.9.2) or a classical sequent calculus and the derivabiliy of C = > v (cf. Theorem 2 .1 0 .1 ) . Working with ccqt,, together with v also the sentence (V )v is pro­ vable ; together with t v also (3 )~iv is provable (already in ccqs), hence also ->(V )v. Consequently, consistency of C will be secured if for no sentence v both v and are provable.