General frame
In logic, general frames (or simply frames) are Kripke frames with an additional structure, which are used to model modal and intermediate logics. The general frame semantics combines the main virtues of Kripke semantics and algebraic semantics: it shares the transparent geometrical insight of the former, and robust completeness of the latter.
Definition
A modal general frame is a triple [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math], where [math]\displaystyle{ \langle F,R\rangle }[/math] is a Kripke frame (i.e., [math]\displaystyle{ R }[/math] is a binary relation on the set [math]\displaystyle{ F }[/math]), and [math]\displaystyle{ V }[/math] is a set of subsets of [math]\displaystyle{ F }[/math] that is closed under the following:
- the Boolean operations of (binary) intersection, union, and complement,
- the operation [math]\displaystyle{ \Box }[/math], defined by [math]\displaystyle{ \Box A=\{x\in F \mid \forall y\in F\,(x\,R\,y\to y\in A)\} }[/math].
They are thus a special case of fields of sets with additional structure. The purpose of [math]\displaystyle{ V }[/math] is to restrict the allowed valuations in the frame: a model [math]\displaystyle{ \langle F,R,\Vdash\rangle }[/math] based on the Kripke frame [math]\displaystyle{ \langle F,R\rangle }[/math] is admissible in the general frame [math]\displaystyle{ \mathbf{F} }[/math], if
- [math]\displaystyle{ \{x\in F \mid x\Vdash p\}\in V }[/math] for every propositional variable [math]\displaystyle{ p }[/math].
The closure conditions on [math]\displaystyle{ V }[/math] then ensure that [math]\displaystyle{ \{x\in F \mid x\Vdash A\} }[/math] belongs to [math]\displaystyle{ V }[/math] for every formula [math]\displaystyle{ A }[/math] (not only a variable).
A formula [math]\displaystyle{ A }[/math] is valid in [math]\displaystyle{ \mathbf{F} }[/math], if [math]\displaystyle{ x\Vdash A }[/math] for all admissible valuations [math]\displaystyle{ \Vdash }[/math], and all points [math]\displaystyle{ x\in F }[/math]. A normal modal logic [math]\displaystyle{ L }[/math] is valid in the frame [math]\displaystyle{ \mathbf{F} }[/math], if all axioms (or equivalently, all theorems) of [math]\displaystyle{ L }[/math] are valid in [math]\displaystyle{ \mathbf{F} }[/math]. In this case we call [math]\displaystyle{ \mathbf{F} }[/math] an [math]\displaystyle{ L }[/math]-frame.
A Kripke frame [math]\displaystyle{ \langle F,R\rangle }[/math] may be identified with a general frame in which all valuations are admissible: i.e., [math]\displaystyle{ \langle F,R,\mathcal{P}(F)\rangle }[/math], where [math]\displaystyle{ \mathcal P(F) }[/math] denotes the power set of [math]\displaystyle{ F }[/math].
Types of frames
In full generality, general frames are hardly more than a fancy name for Kripke models; in particular, the correspondence of modal axioms to properties on the accessibility relation is lost. This can be remedied by imposing additional conditions on the set of admissible valuations.
A frame [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math] is called
- differentiated, if [math]\displaystyle{ \forall A\in V\,(x\in A\Leftrightarrow y\in A) }[/math] implies [math]\displaystyle{ x=y }[/math],
- tight, if [math]\displaystyle{ \forall A\in V\,(x\in\Box A\Rightarrow y\in A) }[/math] implies [math]\displaystyle{ x\,R\,y }[/math],
- compact, if every subset of [math]\displaystyle{ V }[/math] with the finite intersection property has a non-empty intersection,
- atomic, if [math]\displaystyle{ V }[/math] contains all singletons,
- refined, if it is differentiated and tight,
- descriptive, if it is refined and compact.
Kripke frames are refined and atomic. However, infinite Kripke frames are never compact. Every finite differentiated or atomic frame is a Kripke frame.
Descriptive frames are the most important class of frames because of the duality theory (see below). Refined frames are useful as a common generalization of descriptive and Kripke frames.
Operations and morphisms on frames
Every Kripke model [math]\displaystyle{ \langle F,R,{\Vdash}\rangle }[/math] induces the general frame [math]\displaystyle{ \langle F,R,V\rangle }[/math], where [math]\displaystyle{ V }[/math] is defined as
- [math]\displaystyle{ V=\big\{\{x\in F \mid x\Vdash A\} \mid A\hbox{ is a formula}\big\}. }[/math]
The fundamental truth-preserving operations of generated subframes, p-morphic images, and disjoint unions of Kripke frames have analogues on general frames. A frame [math]\displaystyle{ \mathbf G=\langle G,S,W\rangle }[/math] is a generated subframe of a frame [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math], if the Kripke frame [math]\displaystyle{ \langle G,S\rangle }[/math] is a generated subframe of the Kripke frame [math]\displaystyle{ \langle F,R\rangle }[/math] (i.e., [math]\displaystyle{ G }[/math] is a subset of [math]\displaystyle{ F }[/math] closed upwards under [math]\displaystyle{ R }[/math], and [math]\displaystyle{ S=R\cap G\times G }[/math]), and
- [math]\displaystyle{ W=\{A\cap G \mid A\in V\}. }[/math]
A p-morphism (or bounded morphism) [math]\displaystyle{ f\colon\mathbf F\to\mathbf G }[/math] is a function from [math]\displaystyle{ F }[/math] to [math]\displaystyle{ G }[/math] that is a p-morphism of the Kripke frames [math]\displaystyle{ \langle F,R\rangle }[/math] and [math]\displaystyle{ \langle G,S\rangle }[/math], and satisfies the additional constraint
- [math]\displaystyle{ f^{-1}[A]\in V }[/math] for every [math]\displaystyle{ A\in W }[/math].
The disjoint union of an indexed set of frames [math]\displaystyle{ \mathbf F_i=\langle F_i,R_i,V_i\rangle }[/math], [math]\displaystyle{ i\in I }[/math], is the frame [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math], where [math]\displaystyle{ F }[/math] is the disjoint union of [math]\displaystyle{ \{F_i \mid i\in I\} }[/math], [math]\displaystyle{ R }[/math] is the union of [math]\displaystyle{ \{R_i \mid i\in I\} }[/math], and
- [math]\displaystyle{ V=\{A\subseteq F \mid \forall i\in I\,(A\cap F_i\in V_i)\}. }[/math]
The refinement of a frame [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math] is a refined frame [math]\displaystyle{ \mathbf G=\langle G,S,W\rangle }[/math] defined as follows. We consider the equivalence relation
- [math]\displaystyle{ x\sim y\iff\forall A\in V\,(x\in A\Leftrightarrow y\in A), }[/math]
and let [math]\displaystyle{ G=F/{\sim} }[/math] be the set of equivalence classes of [math]\displaystyle{ \sim }[/math]. Then we put
- [math]\displaystyle{ \langle x/{\sim},y/{\sim}\rangle\in S\iff\forall A\in V\,(x\in\Box A\Rightarrow y\in A), }[/math]
- [math]\displaystyle{ A/{\sim}\in W\iff A\in V. }[/math]
Completeness
Unlike Kripke frames, every normal modal logic [math]\displaystyle{ L }[/math] is complete with respect to a class of general frames. This is a consequence of the fact that [math]\displaystyle{ L }[/math] is complete with respect to a class of Kripke models [math]\displaystyle{ \langle F,R,{\Vdash}\rangle }[/math]: as [math]\displaystyle{ L }[/math] is closed under substitution, the general frame induced by [math]\displaystyle{ \langle F,R,{\Vdash}\rangle }[/math] is an [math]\displaystyle{ L }[/math]-frame. Moreover, every logic [math]\displaystyle{ L }[/math] is complete with respect to a single descriptive frame. Indeed, [math]\displaystyle{ L }[/math] is complete with respect to its canonical model, and the general frame induced by the canonical model (called the canonical frame of [math]\displaystyle{ L }[/math]) is descriptive.
Jónsson–Tarski duality
General frames bear close connection to modal algebras. Let [math]\displaystyle{ \mathbf F=\langle F,R,V\rangle }[/math] be a general frame. The set [math]\displaystyle{ V }[/math] is closed under Boolean operations, therefore it is a subalgebra of the power set Boolean algebra [math]\displaystyle{ \langle\mathcal P(F),\cap,\cup,-\rangle }[/math]. It also carries an additional unary operation, [math]\displaystyle{ \Box }[/math]. The combined structure [math]\displaystyle{ \langle V,\cap,\cup,-,\Box\rangle }[/math] is a modal algebra, which is called the dual algebra of [math]\displaystyle{ \mathbf F }[/math], and denoted by [math]\displaystyle{ \mathbf F^+ }[/math].
In the opposite direction, it is possible to construct the dual frame [math]\displaystyle{ \mathbf A_+=\langle F,R,V\rangle }[/math] to any modal algebra [math]\displaystyle{ \mathbf A=\langle A,\wedge,\vee,-,\Box\rangle }[/math]. The Boolean algebra [math]\displaystyle{ \langle A,\wedge,\vee,-\rangle }[/math] has a Stone space, whose underlying set [math]\displaystyle{ F }[/math] is the set of all ultrafilters of [math]\displaystyle{ \mathbf A }[/math]. The set [math]\displaystyle{ V }[/math] of admissible valuations in [math]\displaystyle{ \mathbf A_+ }[/math] consists of the clopen subsets of [math]\displaystyle{ F }[/math], and the accessibility relation [math]\displaystyle{ R }[/math] is defined by
- [math]\displaystyle{ x\,R\,y\iff\forall a\in A\,(\Box a\in x\Rightarrow a\in y) }[/math]
for all ultrafilters [math]\displaystyle{ x }[/math] and [math]\displaystyle{ y }[/math].
A frame and its dual validate the same formulas; hence the general frame semantics and algebraic semantics are in a sense equivalent. The double dual [math]\displaystyle{ (\mathbf A_+)^+ }[/math] of any modal algebra is isomorphic to [math]\displaystyle{ \mathbf A }[/math] itself. This is not true in general for double duals of frames, as the dual of every algebra is descriptive. In fact, a frame [math]\displaystyle{ \mathbf F }[/math] is descriptive if and only if it is isomorphic to its double dual [math]\displaystyle{ (\mathbf F^+)_+ }[/math].
It is also possible to define duals of p-morphisms on one hand, and modal algebra homomorphisms on the other hand. In this way the operators [math]\displaystyle{ (\cdot)^+ }[/math] and [math]\displaystyle{ (\cdot)_+ }[/math] become a pair of contravariant functors between the category of general frames, and the category of modal algebras. These functors provide a duality (called Jónsson–Tarski duality after Bjarni Jónsson and Alfred Tarski) between the categories of descriptive frames, and modal algebras. This is a special case of a more general duality between complex algebras and fields of sets on relational structures.
Intuitionistic frames
The frame semantics for intuitionistic and intermediate logics can be developed in parallel to the semantics for modal logics. An intuitionistic general frame is a triple [math]\displaystyle{ \langle F,\le,V\rangle }[/math], where [math]\displaystyle{ \le }[/math] is a partial order on [math]\displaystyle{ F }[/math], and [math]\displaystyle{ V }[/math] is a set of upper subsets (cones) of [math]\displaystyle{ F }[/math] that contains the empty set, and is closed under
- intersection and union,
- the operation [math]\displaystyle{ A\to B=\Box(-A\cup B) }[/math].
Validity and other concepts are then introduced similarly to modal frames, with a few changes necessary to accommodate for the weaker closure properties of the set of admissible valuations. In particular, an intuitionistic frame [math]\displaystyle{ \mathbf F=\langle F,\le,V\rangle }[/math] is called
- tight, if [math]\displaystyle{ \forall A\in V\,(x\in A\Leftrightarrow y\in A) }[/math] implies [math]\displaystyle{ x\le y }[/math],
- compact, if every subset of [math]\displaystyle{ V\cup\{F-A \mid A\in V\} }[/math] with the finite intersection property has a non-empty intersection.
Tight intuitionistic frames are automatically differentiated, hence refined.
The dual of an intuitionistic frame [math]\displaystyle{ \mathbf F=\langle F,\le,V\rangle }[/math] is the Heyting algebra [math]\displaystyle{ \mathbf F^+=\langle V,\cap,\cup,\to,\emptyset\rangle }[/math]. The dual of a Heyting algebra [math]\displaystyle{ \mathbf A=\langle A,\wedge,\vee,\to,0\rangle }[/math] is the intuitionistic frame [math]\displaystyle{ \mathbf A_+=\langle F,\le,V\rangle }[/math], where [math]\displaystyle{ F }[/math] is the set of all prime filters of [math]\displaystyle{ \mathbf A }[/math], the ordering [math]\displaystyle{ \le }[/math] is inclusion, and [math]\displaystyle{ V }[/math] consists of all subsets of [math]\displaystyle{ F }[/math] of the form
- [math]\displaystyle{ \{x\in F \mid a\in x\}, }[/math]
where [math]\displaystyle{ a\in A }[/math]. As in the modal case, [math]\displaystyle{ (\cdot)^+ }[/math] and [math]\displaystyle{ (\cdot)_+ }[/math] are a pair of contravariant functors, which make the category of Heyting algebras dually equivalent to the category of descriptive intuitionistic frames.
It is possible to construct intuitionistic general frames from transitive reflexive modal frames and vice versa, see modal companion.
References
- Alexander Chagrov and Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.
- Patrick Blackburn, Maarten de Rijke, and Yde Venema, Modal Logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001.
 |  |
