Database Reference
In-Depth Information
A general frame F =
(W,R,
H
) is called rooted if there exists a 0
W such that
a 0 b for all b W and W \{ a 0 }∈ H
. (Notice that if W is a complete lattice
0.)
For every complete Heyting algebra H ,let H denote the descriptive frame of all
prime filters of H , i.e., H
then a 0 =
= (W,R,H(W)) , where W is the set of all prime filters
. For every descriptive frame F,letF denote its complex
Heyting algebra of all admissible sets of F. Then, the following duality (isomor-
phism) for Heyting algebras (Sect. 8.4 in [ 3 ]) is valid:
(*) H
and R is the inclusion
) (and F
( F )
) (standard duality ),
and hence for every complete Heyting algebra H there exists an intuitionistic de-
scriptive frame F = (W,R , H ) such that H is isomorphic to ( H , , , , h ,
( H
,W) .
An intermediate logic L is called Kripke complete if there exists a class
K
of
Log( K ) = {
Kripke frames such that L
=
Log( F ) | F K }
, where Log( F ) ={ φ |
F |=
. It was demonstrated that if an intermediate logic L is Kripke complete, then
L is Kripke complete w.r.t. the class of its rooted frames.
An intermediate logic L has the finite model property (fmp) if for each formula
which is a non-theorem of this logic there is a finite model (thus a frame) of it in
which this formula is not true. That is, L has fmp if there exists a class
φ
}
K
of finite
Kripke frames such that L
). For example,
a method for constructing such finite counter-models which uses the loop-checker is
presented in [ 25 ], while a method not requiring loop-checker, based on contraction-
free sequent calculi is presented in [ 20 ]. Moreover, it was demonstrated that every
intermediate logic L is complete to its finitely generated rooted descriptive frames
(Theorem 8.36, [ 3 ]).
The fact that intuitionistic logic IPC is complete with respect to its finite frames
(or finite Heyting algebras) is well-known; a proof can be found in the topic [ 3 ],
in Corollary 2.33 (and also Theorem 2.57). In a personal correspondence, Michael
Zakaryaschev wrote to me that he does not remember now who was the first to prove
this result; but he guesses that it has been known since the 1940s, thus:
(**) IPC
=
Log( K ) (i.e., L is complete w.r.t.
K
=
K F ) ,
Log(
where
K F is a class of all finite rooted descriptive Kripke frames.
We defined the WMTL by the class of Heyting algebras
HA DB in Definition 64 ,
which are the complex algebras of Kripke frames in Proposition 72 , with binary
accessibility relations (W,
) equal to (also infinite) complete lattices ( Υ ,
) with
( Υ ) its bottom and top elements, respectively. Let as denote the class
of these Kripke frames by
and R Υ =
K DB (corresponding to the class of Heyting algebras
HA DB ). It is easy to verify that
K DB is a class of rooted descriptive frames, so that
for each (autoreferential) frame F K DB , its complex algebra (see Proposition 72 )
F =
L alg = Ob DB sk ,
0 , Υ
, ¬
F ( Υ )
=
,
,T
,
,
is such that for any two V 1 ,V 2
Ob DB sk = F
( Υ ) ,
V 1 V 2 = T (V 1 ,V 2 ) = W \
{ a W | a b }
;
b W \ c V 1 V 2 { b W | c b }
Search WWH ::




Custom Search