Database Reference
In-Depth Information
Theorem 20
φ is a theorem of WMTL
.
Thus
WMTL
,
differently from
IPC
,
satisfies the De Morgan laws
.
The
weak
excluded middle
¬
φ
∨¬¬
Ob
DB
sk
,
¬
⊕¬¬
Proof
We have to show that for each
A
=
TA
∈
A
A
=
Υ
, that is,
T(
¬
∪¬¬
for each (also infinite) relation
R
A)
.
Hence J
¬
A
=
J
Υ
\
J
A
=
J
Υ
\
J
¬¬
A
, so that at least one of J
¬
A
and J
¬¬
A
=
J
A
has to be finite. Let us consider the case when J
¬¬
A
=
J
A
is finite. In what follows,
the values in J
A
will be denoted by
a
i
while the values in J
¬
A
will be denoted by
x
i
.
Thus,
R
∈
Υ
,
R
∈
A
R
2
, where
R
1
in each tuple has at least one value
a
i
, while
R
2
has only the tuples with values
x
i
in the infinite set J
¬
A
, so that
1.
R
2
∈¬
=
R
1
∪
A
can be an infinite relation.
R
1
can be an infinite relation as well because it has not only the values
a
i
of the
finite set J
A
(in every its tuple) but also the values
x
i
of the (possibly infinite) set
J
¬
A
.
Let us take any tuple
t
I
∈
1 of finite
substrings (the arity of each relation is always finite) composed of only values in
J
A
: we denote by
i
m
≥
R
1
composed of the finite number
n
≥
=
1
,...,n
, the position of the
m
th substring of a length
k
m
, composed of only elements in J
A
(so that
i
m
≤
i
l
iff
m
≤
l
), and set
i
0
=
1,
m
1,
k
0
=
1.
The remaining part of this tuple
t
I
is composed of substrings with the values
x
i
in J
¬
A
. We can have at maximum
n
l
0
=
0, and
i
n
+
1
=
ar(R)
+
+
1 such substrings, each one of the length
l
m
+
1
=
0
,
1
,...,n
.
The
I
is a complete ordered set of indexes of values
a
i
in this tuple
t
I
, thus equal
i
m
+
1
−
(i
m
+
k
m
)
,
m
=
to:
I
=
i
1
,...,i
1
+
k
1
−
1
,i
2
,...,i
2
+
k
2
−
1
,...,i
n
,...,i
n
+
k
n
−
1
.
The complete ordered set of indexes of values
x
i
in J
¬
A
in this tuple
t
I
is then
J
=
i
m
+
k
m
,...,i
m
+
1
−
1
,i
m
+
1
+
k
m
+
1
,...,i
m
+
2
−
1
,,...,i
l
+
k
l
,...,i
l
+
1
−
1
,
where
m
=
0if
i
1
>
1; 1 otherwise, and
l
=
n
if
i
n
+
k
n
<i
n
+
1
=
ar(R)
+
1;
n
−
1
otherwise.
Let us consider, for example, the tuple
t
I
=
x
1
x
2
x
3
a
1
a
2
x
4
x
5
a
3
a
4
a
5
x
6
a
6
x
7
x
8
x
9
,
so that
n
=
3;
i
1
=
4
,i
2
=
8
,i
3
=
12
,i
4
=
ar(R)
+
1
=
16;
k
1
=
2
,k
2
=
3
,k
3
=
1;
and
l
1
=
3
,l
2
=
2
,l
3
=
1
,l
4
=
3, and hence,
I
=
4
,
5
,
8
,
9
,
10
,
12
and
J
=
1
,
2
,
3
,
6
,
7
,
11
,
13
,
14
,
15
.
Let us define a function
f
:{
1
,...,n
}→
N
such that
f(
1
)
=
0 and
f(l)
=
1
≤
j
≤
l
−
1
k
j
,for2
≤
l
≤
n
. Then we define the relation:
a
f(l)
+
m
+
1
)
,
R
1
WHERE
1
R
I
=
(nome
i
l
+
m
=
≤
l
≤
n
0
≤
m
≤
k
l
−
1
