REPORTS ON MATHEMATICAL LOGIC 46 (2011), 29–57

A b s t r a c t. The notion of “sequences ” is fundamental to prac-tical reasoning in computer science, because it can appropriately represent “data (information) sequences”, “program (execution) sequences”, “action sequences”, “time sequences”, “trees”, “or-ders ” etc. The aim of this paper is thus to provide a basic logic for reasoning with sequences. A propositional modal logic LS of sequences is introduced as a Gentzen-type sequent calculus by ex-tending Gentzen’s LK for classical propositional logic. The com-pleteness theorem with respect to a sequence-indexed semantics for LS is proved, and the cut-elimination theorem for LS is shown. Moreover, a first-order modal logic FLS of sequences, which is a first-order extension of LS, is introduced. The completeness the-orem with respect to a first-order sequence-indexed semantics for FLS is proved, and the cut-elimination theorem for FLS is shown. LS and the monadic fragment of FLS are shown to be decidable