Proof Analysis in Temporal Logic

The logic of time is one of the most interesting modal logics, and its importance is widely acknowledged both for philosophical and formal reasons. In this thesis, we apply the method of internalisation of Kripke-style semantics into the syntax of sequent calculus to the proof-theoretical analysis of temporal logics. Sequent systems for different flows of time are obtained as modular extensions of a basic temporal calculus, through the addition of appropriate mathematical rules that correspond to the properties of temporal frames: a general and uniform treatment is thus achieved for a wide range of temporal logics. All the calculi enjoy remarkable structural properties, in particular are contraction and cut free. Linear discrete time is analysed by means of two infinitary calculi. The first is obtained by means of a rule with infinitely many premises, and the second through a new definition of provability which admits, under certain conditions, derivation trees with infinite branches. The first calculus enjoys the desired structural properties, but the presence of an infinitary rule is harmful for proof analysis. Two finitary systems are identified by replacing the infinitary rule with a weaker finitary rule, and by bounding the number of its premises, respectively. Corresponding, somehow complementary, conservativity results are proved with respect to adequate fragments of the original calculus. The second calculus stems from a closure algorithm which exploits the fixed-point equations for temporal operators and gives saturated sets of closure formulas from a given formula. Finitisation is obtained in the form of an upper bound to the proof-search procedure, and decidability follows as a major consequence.