A G"odel Calculus for Linear Temporal Logic

We consider G"odel temporal logic (sf GTL), a variant of linear temporal logic based on G"odel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be sc pspace-complete. In this paper we provide a deductive calculus for sf GTL, and show this calculus to be sound and complete for the above-mentioned semantics.