On the finitization of Priorean linear time

A labelled sequent calculus for Priorean linear time is defined through the method of internalization of the possible-worlds semantics into the syntax. The calculus enjoys desirable structural properties, such as syntactic cut elimination, but requires an infinitary mathematical rule stating that between any two points there are only finitely many points. By replacing the infinitary rule with two weaker finitary rules a system for non-standard discrete frames is obtained. A conservativity result for an appropriate fragment of the original calculus is proved syntactically.