Databases Reference
In-Depth Information
3.4 Definability of Implicational Quantifiers
The next theorem shows that the necessary condition of definability of equiv-
alency rules proved in Theorem 4 is also the su cient condition of definability
of implicational quantifiers.
Theorem 5. Let
is classically
definable if and only if its table of maximal b has only finite number of steps.
Proof. Let Tb
be an implicational quantifier. Then
.
be a table of maximal b of
is classically definable then we prove that Tb has only finite num-
ber of steps in a similar way like we proved in the Theorem 4 that the partial
table Tbp ( a,c 0 ,d 0 ) of maximal b has finite number of steps.
Let us suppose that Tb
If
has K steps where K
0 is a natural number.
We prove that Tb is classically definable.
First let us suppose that K =0 . We distinguish two cases: Tb (1) = 0
and Tb (1) > 0 .
If it is Tb (1) = 0 then it is also Tb (0) = 0 (there is no step). It but
means that
( a,b,c,d )=0 for each 4ft table
a,b,c,d
because of it cannot
be b< 0 . Thus it is
( a,b,c,d )=1 if and only if
a,b,c,d
∈∅
. The empty
set
is but also the interval in
N
4 and the quantifier
is according to the
Theorem 3 classically definable.
If it is K =0 and Tb (1) > 0 then it is ⇒ ( a,b,c,d )=1 if and only if
a,b,c,d
0 ,
)
×
0 ,Tb (1))
×
0 ,
)
×
0 ,
)
( a,b,c,d ) is definable according to the Theorem 3.
Let us suppose that S> 0 is a natural number and that
and thus the quantifier
<a S
are all the steps in Tb . We will define intervals I 1 ,I 2 ,...,I S +1 in the fol-
lowing way.
If Tb ( a 1 )=0 then I 1 =
0
a 1 <a 2 <
···
otherwise
I 1 =
0 ,a 1 +1)
×
0 ,Tb ( a 1 ))
×
0 ,
)
×
0 ,
) .
For j =2 ,...,S we define
I j =
a j− 1 ,a j +1)
×
0 ,Tb ( a j ))
×
0 ,
)
×
0 ,
) .
The interval I S +1 is defined such that
I S +1 =
a S ,
)
×
0 ,Tb ( a S ))
×
0 ,
)
×
0 ,
) .
is implicational. Thus it is clear that the intervals
I 1 ,I 2 ,...,I S +1 are defined such that
Remember that
S +1
( a,b,c,d )=1 iff
a,b,c,d
I j
j =1
is definable. This finishes
and according to the Theorem 3 the quantifier
the proof.
Search WWH ::




Custom Search