Saturation replaces induction for a miniscoped linear temporal logic

Abstract

A new type of deductive principle (named the saturation one) is introduced for a complete class (called miniscoped) of the first order linear temporal logic with ⊗(”next”) and □(”always”). The saturation replaces induction-like postulates and intuitively corresponds to a certain type of regularity in the derivations for the logic. Non-logical axioms in ”saturated calculi” are some sequents, indicating the saturation of the derivation process in these calculi. The saturation suggests that ”nothing new” can be obtained continuing the derivation process. The non-logical axioms of the saturated calculus are constructed dependent on specific peculiarities of the given sequent. Therefore, for each given sequent (whose derivability requires the application of the induction-like postulate) a concrete saturated calculus is constructed. This property makes saturated calculi more effective than the traditional ones (based on the fixed induction-like postulate).