Skip to main content

Cut-free display calculi for nominal tense logics

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free