Admissible Rule - Semantics For Admissible Rules

Semantics For Admissible Rules

A rule Γ/B is valid in a modal or intuitionistic Kripke frame, if the following is true for every valuation in F:

if for all, then .

(The definition readily generalizes to general frames, if needed.)

Let X be a subset of W, and t a point in W. We say that t is

• a reflexive tight predecessor of X, if for every y in W: t R y if and only if t = y or x = y or x R y for some x in X,
• an irreflexive tight predecessor of X, if for every y in W: t R y if and only if x = y or x R y for some x in X.

We say that a frame F has reflexive (irreflexive) tight predecessors, if for every finite subset X of W, there exists a reflexive (irreflexive) tight predecessor of X in W.

We have:

• a rule is admissible in IPC if and only if it is valid in all intuitionistic frames which have reflexive tight predecessors,
• a rule is admissible in K4 if and only if it is valid in all transitive frames which have reflexive and irreflexive tight predecessors,
• a rule is admissible in S4 if and only if it is valid in all transitive reflexive frames which have reflexive tight predecessors,
• a rule is admissible in GL if and only if it is valid in all transitive converse well-founded frames which have irreflexive tight predecessors.

Note that apart from a few trivial cases, frames with tight predecessors must be infinite, hence admissible rules in basic transitive logics do not enjoy the finite model property.