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
}