Projective unification in modal logic

A projective unifier for a modal formula A, over a modal logic L, is a unifier σ for A (i.e. a substitution making A a theorem of L) such that the equivalence of σ with the identity map is the consequence of A. Each projective unifier is a most general unifier for A. Let L be a normal modal logic co...

Full description

Saved in:
Bibliographic Details
Published in:Logic journal of the IGPL 2012-02, Vol.20 (1), p.121-153
Main Authors: Dzik, Wojciech, Wojtylak, Piotr
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A projective unifier for a modal formula A, over a modal logic L, is a unifier σ for A (i.e. a substitution making A a theorem of L) such that the equivalence of σ with the identity map is the consequence of A. Each projective unifier is a most general unifier for A. Let L be a normal modal logic containing S4. We show that every unifiable formula has a projective unifier in L iff L contains S4.3. The syntactic proof is effective. As a corollary, we conclude that all normal modal logics L containing S4.3 are almost structurally complete, i.e. all (structural) admissible rules having unifiable premises are derivable in L. Moreover, L is (hereditarily) structurally complete iff L contains McKinsey axiom M.
ISSN:1367-0751
1368-9894
DOI:10.1093/jigpal/jzr028