Information Technology Reference
In-Depth Information
For this, we prove that LNIS has the finite model property (Proposition 11 be-
low). We will employ the standard filtration technique [3] with necessary mod-
ifications to prove this result. Let
ʣ
denote a finite sub-formula closed set of
wffs.
Consider a model
,
a∈A
V
a
,F
). We define a
M
:= (
S
,V
), where
S
:= (
U,
A
binary relation
≡
ʣ
on
U
as follows:
≡
ʣ
w
,
if and only if for all
ʲ
,w
|
w
∈
ʣ
∪D
,
M
,w
|
=
ʲ
if and only if
M
=
ʲ.
Definition 5 (Filtration model).
Given a model
M
:= (
S
,V
)
,where
S
:=
,
a∈A
V
a
,F
)
and ʣ as above, we define a model
f
=(
f
,V
f
)
,where
(
U,
A
M
S
,
a∈A
V
a
,F
f
)
f
:= (
U
f
,
-
S
A
-
U
f
:=
{
[
w
]:
w
∈
U
}
,
[
w
]
is the equivalence class of w with respect to the
≡
ʣ
;
-
F
f
([
w
]
,a
)=
F
(
w,a
)
;
-
V
f
(
p
):=
equivalence relation
U
f
:
w
{
[
w
]
∈
∈
V
(
p
)
}
f
is the filtration of
M
M
throughthesub-formulaclosedsetʣ.
First note that the definition of
F
f
is well defined as for all
w
∈
[
w
],
F
(
w,a
)=
F
(
w
,a
). Moreover,
f
is a filtration of
Proposition 8.
For any model
M
,if
M
M
through ʣ,then
the domain U
f
of
f
contains at most
2
n
elements, where
M
|
ʣ
∪D|
=
n.
Proof.
Define the map
g
:
U
f
2
ʣ∪D
where
g
([
w
]) :=
→
{
ʲ
∈
ʣ
∪D
:
M
,w
|
=
ʲ
}
.
Since
g
is injective,
U
f
contains at most 2
n
elements.
We also note the following fact.
f
B
if and only if
(
w,u
)
Ind
S
Ind
B
.
Proposition 9.
1.
([
w
]
,
[
u
])
∈
∈
f
B
if and only if
(
w,u
)
Sim
S
Sim
B
.
2.
([
w
]
,
[
u
])
∈
∈
f
B
if and only if
(
w,u
)
In
S
In
B
.
3.
([
w
]
,
[
u
])
∈
∈
Ind
S
f
B
F
f
([
w
]
,a
)=
F
f
([
u
]
,a
) for all
a
Proof.
([
w
]
,
[
u
])
∈
⃔
∈
B
⃔
F
(
w,a
)=
Ind
B
.
For the similarity and inclusion relations, it can be done in the same way.
F
(
u,a
) for all
a
∈
B
⃔
(
w,u
)
∈
Once we have Proposition 9, it is not dicult to obtain the following.
Proposition 10 (Filtration Theorem).
Let ʣ be a finite sub-formula closed
set of wffs. For all wffs ʲ
∈
ʣ
∪D
,allmodels
M
,andallobjectsw
∈
W,
f
,
[
w
]
M
,w
|
=
ʲ if and only if
M
|
=
ʲ.
Finally, from Propositions 8 and 10 we have
Proposition 11 (Finite Model Property).
Let ʱ be a wff and ʣ be the set
of all sub-wffs of ʱ.Ifʱ is satisfiable, then it is satisfiable in a finite model with
at most
2
|ʣ∪D|
elements.
