Admissible Rule - Projectivity and Unification

Projectivity and Unification

Admissibility in propositional logics is closely related to unification in the equational theory of modal or Heyting algebras. The connection was developed by Ghilardi (1999, 2000). In the logical setup, a unifier of a formula A in a logic L (an L-unifier for short) is a substitution σ such that σA is a theorem of L. (Using this notion, we can rephrase admissibility of a rule A/B in L as "every L-unifier of A is an L-unifier of B".) An L-unifier σ is less general than an L-unifier τ, written as σ ≤ τ, if there exists a substitution υ such that

for every variable p. A complete set of unifiers of a formula A is a set S of L-unifiers of A such that every L-unifier of A is less general than some unifier from S. A most general unifier (mgu) of A is a unifier σ such that {σ} is a complete set of unifiers of A. It follows that if S is a complete set of unifiers of A, then a rule A/B is L-admissible if and only if every σ in S is an L-unifier of B. Thus we can characterize admissible rules if we can find well-behaved complete sets of unifiers.

An important class of formulas which have a most general unifier are the projective formulas: these are formulas A such that there exists a unifier σ of A such that

for every formula B. Note that σ is a mgu of A. In transitive modal and superintuitionistic logics with the finite model property (fmp), one can characterize projective formulas semantically as those whose set of finite L-models has the extension property: if M is a finite Kripke L-model with a root r whose cluster is a singleton, and the formula A holds in all points of M except for r, then we can change the valuation of variables in r so as to make A true in r as well. Moreover, the proof provides an explicit construction of a mgu for a given projective formula A.

In the basic transitive logics IPC, K4, S4, GL, Grz (and more generally in any transitive logic with the fmp whose set of finite frame satisfies another kind of extension property), we can effectively construct for any formula A its projective approximation Π(A): a finite set of projective formulas such that

1. for every
2. every unifier of A is a unifier of a formula from Π(A).

It follows that the set of mgus of elements of Π(A) is a complete set of unifiers of A. Furthermore, if P is a projective formula, then

if and only if

for any formula B. Thus we obtain the following effective characterization of admissible rules:

if and only if