Kripke semantics for intuitionistic propositional logic
A Kripe model for intuitionistic propositional logic PL is a triple , where
- 1.
is a set, whose elements are called possible worlds,
- 2.
is a preorder
on ,
- 3.
is a function that takes each wff (well-formed formula) in PL to a subset of , such that
- –
if is a propositional variable, is upper closed,
- –
,
- –
,
- –
,
- –
,
where , the complement
of the lower closure of any .
- –
Remarks.
- •
If were used as a primitive symbol instead of , then we require that . Then introducing by , we get .
- •
Some simple properties of : for any subset of , is upper closed. This means that for any wff , is upper closed. Also, and are disjoint, which means that for any .
One can also define a satisfaction relation between and the set of wff’s so that
for any and . It’s easy to see that
- •
for any propositional variable , if and , then ,
- •
iff and ,
- •
iff or ,
- •
iff for all such that , we have
- •
iff for all such that , we have implies .
When , we say that is true at world .
Remark. Since is upper closed, implies for any such that . Now suppose and , then iff . This shows that, as far as validity of formulas is concerned, we can take to be a partial order
in the definition above.
Some examples of Kripke models:
- 1.
Let be the model consisting of , , with and . Then , and we have the following:
- –
.
- –
, and , so
- –
, so
- –
.
- –
In fact, for any wff’s , either or , since is linearly ordered
, so that
assuming .
- –
- 2.
Let be the model consisting of , , with and . Then
- –
,
- –
,
- –
so .
- –
,
- –
,
- –
so .
- –
- 3.
Let be an arbitrary model. Then
- –
,
- –
,
- –
. The last equation comes from the fact that for any upper set , .
- –
Suppose . Then . Since is upper, is lower, so , or . This shows that modus ponens
preserves validity.
- –
- 4.
Let be any set and . Then for any wff , either or . Therefore, , and .
The pair in a Kripke model is also called a (Kripke) frame, and is said to be a model based on the frame . The validity of a wff at various levels can be found in the parent entry. Furthermore, is valid (with respect to Krikpe semantics) for PL if it is valid in the class of all frames.
Based on the examples above, we see that
- 1.
is valid in , while is not.
- 2.
is valid in the class of linearly ordered frames, while it is not valid in , and neither is .
- 3.
It is not hard to see that is valid in any weakly connected
frame, that is, for any , the set is linear.
- 4.
Any wff in any of the schemas , , or is valid in PL. See remark below for more detail.
- 5.
Any theorem
in the classical propositional logic is valid in any universal
frame, that is, a frame with a universal relation.
Remark. It can be shown that every theorem of PL is valid. This is the soundness theorem of PL. Conversely, every valid wff is a theorem. This is known as the completeness theorem of PL. Furthermore, a wff valid in the class of finite frames is a theorem. This is the finite model property of PL.