Editing Admissible rule (section)

==Semantics for admissible rules==

A rule Γ/''B'' is '''valid''' in a modal or intuitionistic [[Kripke frame]] <math>F=\langle W,R\rangle</math>, if the following is true for every valuation <math>\Vdash</math> in ''F'':
:if for all <math>A\in\Gamma</math> <math>\forall x\in W\,(x\Vdash A)</math>, then <math>\forall x\in W\,(x\Vdash B)</math>.
(The definition readily generalizes to [[general frame]]s, 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 for some ''x'' in ''X'': ''x'' = ''y'' or ''x R y'' ,
*an '''irreflexive tight predecessor''' of ''X'', if for every ''y'' in ''W'': ''t R y'' if and only if for some ''x'' in ''X'': ''x'' = ''y'' or  ''x R y'' .
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:<ref>Iemhoff (2001), Jeřábek (2005)</ref>
*a rule is admissible in ''IPC'' if and only if it is valid in all intuitionistic frames that have reflexive tight predecessors,
*a rule is admissible in ''K''4 if and only if it is valid in all [[transitive relation|transitive]] frames that have reflexive and irreflexive tight predecessors,
*a rule is admissible in ''S''4 if and only if it is valid in all transitive [[reflexive relation|reflexive]] frames that have reflexive tight predecessors,
*a rule is admissible in ''GL'' if and only if it is valid in all transitive converse [[well-founded relation|well-founded]] frames that 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.