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 formula_1, where formula_2 is a Kripke frame (i.e., "R" is a binary relation on the set "F"), and "V" is a set of subsets of "F" that is closed under the following:
They are thus a special case of fields of sets with additional structure. The purpose of "V" is to restrict the allowed valuations in the frame: a model formula_5 based on the Kripke frame formula_2 is admissible in the general frame F, if
The closure conditions on "V" then ensure that formula_8 belongs to "V" for "every" formula "A" (not only a variable).
A formula "A" is valid in F, if formula_9 for all admissible valuations formula_10, and all points formula_11. A normal modal logic "L" is valid in the frame F, if all axioms (or equivalently, all theorems) of "L" are valid in F. In this case we call F an "L"-frame.
A Kripke frame formula_2 may be identified with a general frame in which all valuations are admissible: i.e., formula_13, where formula_14 denotes the power set of "F".
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 formula_1 is called
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 formula_20 induces the general frame formula_21, where "V" is defined as
The fundamental truth-preserving operations of generated subframes, p-morphic images, and disjoint unions of Kripke frames have analogues on general frames. A frame formula_23 is a generated subframe of a frame formula_1, if the Kripke frame formula_25 is a generated subframe of the Kripke frame formula_2 (i.e., formula_27 is a subset of formula_28 closed upwards under formula_29, and formula_30), and
A p-morphism (or bounded morphism) formula_32 is a function from "F" to "G" that is a p-morphism of the Kripke frames formula_2 and formula_25, and satisfies the additional constraint
The disjoint union of an indexed set of frames formula_37, formula_38, is the frame formula_1, where "F" is the disjoint union of formula_40, "R" is the union of formula_41, and
The refinement of a frame formula_1 is a refined frame formula_23 defined as follows. We consider the equivalence relation
and let formula_46 be the set of equivalence classes of formula_47. Then we put
Completeness.
Unlike Kripke frames, every normal modal logic "L" is complete with respect to a class of general frames. This is a consequence of the fact that "L" is complete with respect to a class of Kripke models formula_20: as "L" is closed under substitution, the general frame induced by formula_20 is an "L"-frame. Moreover, every logic "L" is complete with respect to a single "descriptive" frame. Indeed, "L" is complete with respect to its canonical model, and the general frame induced by the canonical model (called the canonical frame of "L") is descriptive.
Jónsson–Tarski duality.
General frames bear close connection to modal algebras. Let formula_1 be a general frame. The set "V" is closed under Boolean operations, therefore it is a subalgebra of the power set Boolean algebra formula_53. It also carries an additional unary operation, formula_3. The combined structure formula_55 is a modal algebra, which is called the dual algebra of F, and denoted by formula_56.
In the opposite direction, it is possible to construct the dual frame formula_57 to any modal algebra formula_58. The Boolean algebra formula_59 has a Stone space, whose underlying set "F" is the set of all ultrafilters of A. The set "V" of admissible valuations in formula_60 consists of the clopen subsets of "F", and the accessibility relation "R" is defined by
for all ultrafilters "x" and "y".
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 formula_62 of any modal algebra is isomorphic to formula_63 itself. This is not true in general for double duals of frames, as the dual of every algebra is descriptive. In fact, a frame formula_64 is descriptive if and only if it is isomorphic to its double dual formula_65.
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 formula_66 and formula_67 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 formula_68, where formula_69 is a partial order on "F", and "V" is a set of upper subsets ("cones") of "F" that contains the empty set, and is closed under
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 formula_71 is called
Tight intuitionistic frames are automatically differentiated, hence refined.
The dual of an intuitionistic frame formula_71 is the Heyting algebra formula_76. The dual of a Heyting algebra formula_77 is the intuitionistic frame formula_78, where "F" is the set of all prime filters of A, the ordering formula_69 is inclusion, and "V" consists of all subsets of "F" of the form
where formula_81. As in the modal case, formula_66 and formula_67 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.