Those formulas which are valid in every Kripke model having constant domain whose base is the ordered set R of real numbers (or, the ordered set Q of rational numbers) are characterized syntactically.

An intermediate predicate logicS + n (n>0) is introduced and investigated. First, a sequent calculusGS n is introduced, which is shown to be equivalent toS + n and for which the cut elimination theorem holds. In § 2, it will be shown thatS + n is characterized by the class of all linear Kripke frames of the heightn.