On a Decision Method in Restricted Second Order Arithmetic

Abstract

In this chapter, SC is a fraction of the restricted second order theory of natural numbers or of the first order theory of real numbers. This chapter discusses the definability in SC and outlines an effective method for deciding the truth of sentences in SC. A congruence of finite rank on words is in congruence with the finite partition of concatenation; a multi-periodic set of words is a union of congruence classes of a congruence of finite rank. These concepts are related to that of a finite automaton and turn out to be the key to an investigation of SC. The results concerning SC may be viewed as an application of the theory of finite automata to logic. In turn, SC arises quite naturally as a condition-language on finite automata or sequential circuits and “sequential calculus” is an appropriate name for SC. The significance of the decision method for SC is that it provides a method for deciding whether or not the input (i)-to-output (u) transformation of a proposed circuit A (i, r, u) satisfies a condition C (i, u) stated in SC.