Cut-Free Display Calculi for Nominal Tense Logics

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 dMNTL 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.