We consider three sequent calculi for propositional linear temporal logic (PLTL) which allow us to formalize the properties of operator “always”. The main new results presented in the paper are: (1) introduction of the calculus with
looping axioms; (2) the direct proof that the presented calculi are equivalent; (3) the proof of completeness of the calculi with looping axioms and with invariant-like rule based on completeness of the calculus with the infinitary $\omega$-type rule.