We define cut-free display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use a translation of MNTL into the minimal tense logic of inequality (MTL ≠) which is known to be properly displayable by application of Kracht’s results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δMTL≠ for MTL≠. Since δMNTL does not satisfy Belnap’s condition (C8), we extend Wansing’s strong normalisation theorem to get a similar theorem for any extension of δMNTL by addition of structural rules satisfying Belnap’s conditions (C2)-(C7). Finally, we show a weak Sahlqvist-style theorem for extensions of MNTL, and by Kracht’s techniques, deduce that these Sahlqvist extensions of δMNTL also admit cut-free display calculi.
Demri, S., & Goré, R. (1999). Cut-free display calculi for nominal tense logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 155–170). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_16