Display calculi for nominal tense logics

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation of MNTL into the minimal tense logic of inequality (ℒ_≠) 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 δℒ_≠ for ℒ_≠. We show that every MNTL-valid formula admits a cut-free derivation in δMNTL. We also show that a restricted display calculus δ^-MNTL, is not only complete for MNTL, but that it enjoys cut-elimination for arbitrary sequents. Finally, we give a weak Sahlqvist-type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ^-MNTL respectively. The display calculi based upon δMNTL enjoy cut-elimination for valid formulae only, but those based upon δ^-MNTL enjoy cut-elimination for arbitrary sequents.