Technical Report TR-SRS-3-95

Automated Reasoning Project

Research School of Information Sciences and Engineering

and Centre for Information Science Research

Australian National University

January, 19, 1995

ON THE COMPLETENESS OF CLASSICAL

TENSE DISPLAY LOGIC

Rajeev Gor?e

Abstract We give a purely syntactic proof of the completeness of classical

tense display logic ffi Kt: the sequent X ` Y is provable in ffi Kt iff the formula

o(X ` Y ) is a theorem of minimal tense logic Kt. Along the way we show

how to relate Kracht's structural rule for seriality to Wansing's one. Finally

we observe a trivial way to obtain the same system using different primitives.