General Frame - Intuitionistic Frames

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 subsets (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 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.