Information Technology Reference
In-Depth Information
Proposition 2. (V1) W/Ind A ↆ{
[[ i ]] M : i
ʘ
}
.
W/Ind A ∪{∅}
(V2)
{
[[ i ]] M : i
ʘ
}ↆ
.
(V3) [[ i ]] M
[[ j ]] M =
,fori,j
ʘ,andi
= j.
Ind A
(V4) For i,j
ʘ,if ( x, y ) /
, [ x ] Ind A
=[ i ]] M and [ y ] Ind A
=[ j ]] M ,then
i
= j.
From conditions (V1)-V(4), it is evident that the element of ʘ are used as
nominals to name the equivalence classes of Ind A
such that different equivalence
classes are provided with different names. We use these nominals to give the
following deductive system. Let B
1
2
3
ↆA
,
B ∈{
B ,
B ,
B }
,and i
ʘ .
Axiom schema:
1. All axioms of classical propositional logic.
2.
B ( ʱ
ʲ )
(
B ʱ
B ʲ ).
1
3.
ʱ
ʱ .
1
1
4. ʱ
ʱ .
1
1
1
5.
ʱ
ʱ .
m
ʱ
n
ʱ ,where m, n
∈{
1 , 2 , 3
}
6.
.
7. C ʱ → B ʱ for C ↆ B .
8. ( a, v )
k
a ( a, v )for k
∈{
1 , 3
}
.
a
9.
¬
( a, v )
¬
( a, v ).
v∈V a ( a, v )
( a, v )) .
a
1
10. i
( i
v∈V b
( b,v )
( b,v ))
ʱ .
11. i
1
B∪{b}
ʱ
1 B
1
( i
2
B∪{b}
2
12. ( b,v )
ʱ
B (( b,v )
ʱ ).
v∈V b
( b,v )
ʱ .
3 B
3 B
1
13. i
ʱ
( i
( b,v ))
∪{
b
}
1
14. i
( a, v )
( i
( a, v )).
15. i
∧¬
( a, v )
1
( i
→¬
( a, v )).
16. i∈ʘ i .
17.
¬
i
∨¬
j for distinct elements i and j of ʘ .
1
A
18. i
i .
Rules of inference :
N. ʱ
MP.
ʱ
B ʱ
ʱ
ʲ
ʲ
The notion of theoremhood is defined in the usual way, and we write
ʱ to
indicate that ʱ is a theorem of the above deductive system.
Axioms 7-13 relate attribute, attribute-values of the objects with the relations
corresponding to the modal operators
B , k
. For instance, let R B be
∈{
1 , 2 , 3
}
2 B , and let us see how the
axioms 7, 10 and 12 relate attribute, attribute-values of the objects with R B .
Axiom 7 for
the relation corresponding to the modal operator
2 B corresponds to the condition R B
R C for C
B . Axiom 10
 
Search WWH ::




Custom Search