General frame
Encyclopedia
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.
, where 
is a Kripke frame (i.e., R is a binary relation
on the set F), and V is a set of subsets of F which is closed under
The purpose of V is to restrict the allowed valuations in the frame: a model
based on the Kripke frame 
is admissible in the general frame F, if
for every propositional variable
p.
The closure conditions on V then ensure that
belongs to V for every formula A (not only a variable).
A formula A is valid in F, if
for all admissible valuations 
, and all points 
. 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
may be identified with a general frame in which all valuations are admissible: i.e., 
, where 
denotes the power set of F.
A frame
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.
induces the general frame 
, 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
is a generated subframe of a frame 
, if the Kripke frame 
is a generated subframe of the Kripke frame 
(i.e., G is a subset of F closed upwards under R, and S is the restriction of R to G), and
A p-morphism (or bounded morphism)
is a function from F to G which is a p-morphism of the Kripke frames 
and 
, and satisfies the additional constraint
for every 
.
The disjoint union of an indexed set of frames
, 
, is the frame 
, where F is the disjoint union of 
, R is the union of 
, and
The refinement of a frame
is a refined frame 
defined as follows. We consider the equivalence relation
and let
be the set of equivalence classes of 
. Then we put
: as L is closed under substitution, the general frame induced by 
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.
General frames bear close connection to modal algebra
s. Let
be a general frame. The set V is closed under Boolean operations, therefore it is a subalgebra
of the power set Boolean algebra
. It also carries an additional unary operation, 
. The combined structure 
is a modal algebra, which is called the dual algebra of F, and denoted by 
.
In the opposite direction, it is possible to construct the dual frame
to any modal algebra 
. The Boolean algebra 
has a Stone space, whose underlying set F is the set of all ultrafilter
s of A. The set V of admissible valuations in
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
of any modal algebra is isomorphic to 
itself. This is not true in general for double duals of frames, as the dual of every algebra is descriptive. In fact, a frame 
is descriptive if and only if it is isomorphic to its double dual 
.
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
and 
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.
, where 
is a partial order on F, and V is a set of upper subset
s (cones) of F which 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
is called
Tight intuitionistic frames are automatically differentiated, hence refined.
The dual of an intuitionistic frame
is the Heyting algebra
. The dual of a Heyting algebra 
is the intuitionistic frame 
, where F is the set of all prime filters of A, the ordering 
is inclusion, and V consists of all subsets of F of the form
where
. As in the modal case, 
and 
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
.
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, general frames (or simply frames) are Kripke frames with an additional structure, which are used to model modal
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
and intermediate
Intermediate logic
In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic, thus consistent superintuitionistic logics are called intermediate logics .-Definition:A superintuitionistic logic is a...
logics. The general frame semantics combines the main virtues of Kripke semantics
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
and algebraic semantics
Algebraic semantics
An programming language theory, the algebraic semantics of a programming language is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner....
: it shares the transparent geometrical insight of the former, and robust completeness of the latter.
Definition
A modal general frame is a triple, where is a Kripke frame (i.e., R is a binary relationBinary relation
In mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
on the set F), and V is a set of subsets of F which is closed under
- the Boolean operations of (binary) intersectionIntersection (set theory)In mathematics, the intersection of two sets A and B is the set that contains all elements of A that also belong to B , but no other elements....
, unionUnion (set theory)In set theory, the union of a collection of sets is the set of all distinct elements in the collection. The union of a collection of sets S_1, S_2, S_3, \dots , S_n\,\! gives a set S_1 \cup S_2 \cup S_3 \cup \dots \cup S_n.- Definition :...
, and complementComplement (set theory)In set theory, a complement of a set A refers to things not in , A. The relative complement of A with respect to a set B, is the set of elements in B but not in A...
, - the operation
, defined by 
.
The purpose of V is to restrict the allowed valuations in the frame: a model
based on the Kripke frame is admissible in the general frame F, if for every propositional variablePropositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
p.
The closure conditions on V then ensure that
belongs to V for every formula A (not only a variable).A formula A is valid in F, if
for all admissible valuations , and all points . A normal modal logicNormal modal logic
In logic, a normal modal logic is a set L of modal formulas such that L contains:* All propositional tautologies;* All instances of the Kripke schema: \Box\toand it is closed under:...
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
may be identified with a general frame in which all valuations are admissible: i.e., , where 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
is called
- differentiated, if
implies 
, - tight, if
implies 
, - compact, if every subset of V with the finite intersection propertyFinite intersection propertyIn general topology, a branch of mathematics, the finite intersection property is a property of a collection of subsets of a set X. A collection has this property if the intersection over any finite subcollection of the collection is nonempty....
has a non-empty intersection, - atomic, if V 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 induces the general frame , where V is defined asThe fundamental truth-preserving operations of generated subframes, p-morphic images, and disjoint unions of Kripke frames have analogues on general frames. A frame
is a generated subframe of a frame , if the Kripke frame is a generated subframe of the Kripke frame (i.e., G is a subset of F closed upwards under R, and S is the restriction of R to G), andA p-morphism (or bounded morphism)
is a function from F to G which is a p-morphism of the Kripke frames and , and satisfies the additional constraint for every .The disjoint union of an indexed set of frames
, , is the frame , where F is the disjoint union of , R is the union of , andThe refinement of a frame
is a refined frame defined as follows. We consider the equivalence relationEquivalence relation
In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
and let
be the set of equivalence classes of . Then we putCompleteness
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: as L is closed under substitution, the general frame induced by 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
Modal algebra
In algebra and logic, a modal algebra is a structure \langle A,\land,\lor,-,0,1,\Box\rangle such that*\langle A,\land,\lor,-,0,1\rangle is a Boolean algebra,...
s. Let
be a general frame. The set V is closed under Boolean operations, therefore it is a subalgebraSubalgebra
In mathematics, the word "algebra", when referring to a structure, often means a vector space or module equipped with an additional bilinear operation. Algebras in universal algebra are far more general: they are a common generalisation of all algebraic structures...
of the power set Boolean algebra
. It also carries an additional unary operation, . The combined structure is a modal algebra, which is called the dual algebra of F, and denoted by .In the opposite direction, it is possible to construct the dual frame
to any modal algebra . The Boolean algebra has a Stone space, whose underlying set F is the set of all ultrafilterUltrafilter
In the mathematical field of set theory, an ultrafilter on a set X is a collection of subsets of X that is a filter, that cannot be enlarged . An ultrafilter may be considered as a finitely additive measure. Then every subset of X is either considered "almost everything" or "almost nothing"...
s of A. The set V of admissible valuations in
consists of the clopenClopen set
In topology, a clopen set in a topological space is a set which is both open and closed. That this is possible for a set is not as counter-intuitive as it might seem if the terms open and closed were thought of as antonyms; in fact they are not...
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
of any modal algebra is isomorphic to itself. This is not true in general for double duals of frames, as the dual of every algebra is descriptive. In fact, a frame is descriptive if and only if it is isomorphic to its double dual .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
and become a pair of contravariant functors between the categoryCategory (mathematics)
In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
of general frames, and the category of modal algebras. These functors provide a duality
Equivalence of categories
In category theory, an abstract branch of mathematics, an equivalence of categories is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics...
(called Jónsson–Tarski duality after Bjarni Jónsson
Bjarni Jónsson
Bjarni Jónsson is an Icelandic mathematician and logician working in universal algebra and lattice theory. He is emeritus Distinguished Professor of Mathematics at Vanderbilt University and the honorary editor in chief of Algebra Universalis...
and Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
) between the categories of descriptive frames, and modal algebras.
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, where is a partial order on F, and V is a set of upper subsetUpper set
In mathematics, an upper set of a partially ordered set is a subset U with the property that x is in U and x≤y imply y is in U....
s (cones) of F which contains the empty set, and is closed under
- intersection and union,
- the operation
.
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
is called
- tight, if
implies 
, - compact, if every subset of
with the finite intersection property has a non-empty intersection.
Tight intuitionistic frames are automatically differentiated, hence refined.
The dual of an intuitionistic frame
is the Heyting algebraHeyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
. The dual of a Heyting algebra is the intuitionistic frame , where F is the set of all prime filters of A, the ordering is inclusion, and V consists of all subsets of F of the formwhere
. As in the modal case, and 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
Modal companion
In logic, a modal companion of a superintuitionistic logic L is a normal modal logic which interprets L by a certain canonical translation, described below...
.