Blending margins: the modal logic K has nullary unification type

DOI10.1093/LOGCOM/EXT055MaRDI QIDQ3450207zbMATH OpenOpenAlexFDO

Authors Emil Jeřábek

Publication date 3 November 2015

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1108.6240

zbMATH Keywords

admissible rulesdescription logicmodal logicrule of marginsunification type

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27)

Abstract: We investigate properties of the formula $poBoxp$ in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins $phioBoxphi/phi,egphi$, and as a consequence, we obtain various negative results about admissibility and unification in K. We describe a complete set of unifiers (i.e., substitutions making the formula provable) of $poBoxp$, and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analyzed in terms of projective formulas, introduced by Ghilardi; in particular, projective formulas coincide for these logics with formulas that are admissibly saturated (i.e., derive all their multiple-conclusion admissible consequences) or exact (i.e., axiomatize a theory of a substitution). In contrast, we show that in K, the formula $poBoxp$ is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic ALC.

Recommendations

• About the unification type of modal logics between \(\mathbf{KB}\) and \(\mathbf{KTB} \)
• Unification in first-order transitive modal logic
• Remarks about the unification types of some locally tabular normal modal logics
• scientific article; zbMATH DE number 7599937
• Projective unification in transitive modal logics

Cited in

(16)

• About the unification type of \(\mathbf{K}+\square \square \bot\)
• Unification in pretabular extensions of S4
• Finitary unification in locally tabular modal logics characterized
• Admissible rules for six intuitionistic modal logics
• Contact logic is finitary for unification with constants
• Tutorial on admissible rules in Gudauri
• Unification in epistemic logics
• KD is nullary
• Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality
• About the unification types of modal logics
• Unification in subsystems of polymodal provability logic GLP
• Computing most general unifiers in Euclidean modal logics
• Projective relative unification through duality
• On the unification problem for \(\operatorname{GLP} \)
• About the unification type of modal logics between \(\mathbf{KB}\) and \(\mathbf{KTB} \)
• Restricted unification in the DL \(\mathcal{FL}_0\)

This page was built for publication: Blending margins: the modal logic K has nullary unification type

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3450207)