Cut-Free Display Calculi for Nominal Tense Logics
Résumé
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.
Origine : Fichiers produits par l'(les) auteur(s)