Information Technology Reference
In-Depth Information
where the following abbreviations are used in WO ( x ):
y
x :=
t ( t
y
t
x ) ,
¬
( y =
):=
z ( z
y ) ,
( z
y =
):=
¬∃
w ( w
z
w
y ) .
Finally, we can connect the notion of ʱ -like name to the set theoretic notion
of ordinals:
Lemma 11. Let ʱ
ORD and u be an ʱ-like element in V (PS 3 ) . Then the
following hold:
i) V (PS 3 )
| =Trans( u )
ii) V (PS 3 )
|
=LO( u )
iii) V (PS 3 )
|
=WO ( u )
Proof. ( i )Wehavetoprove
y
z ( z
y
y
u
z
u )
∈{
1 , 1 / 2
}
. Since the
truth table of
in PS 3 does not contain 1 / 2 it is sucient to show
y
z ( z
y
y
u
z
u )
=1.
V (PS 3 ) . Then,
Let us take any z
=
y∈ V (PS 3 )
y ( y
u
z
y
z
u )
(
y
u
z
y
z
u
)
=
y∈ V (PS 3 )
y
u
z
y
z
u
(
(
))
=
y∈ dom( u )
( u ( y )
z
y
z
u
(
))
(since BQ ˕ hold in V (PS 3 ) for all negation-free formulas ˕ .)
For any y
dom( u )if u ( y )
=0then y is ʲ -like for some non-zero ʲ
ʱ .Let
for such an y ,
z
y
∈{
1 , 1 / 2
}
. Therefore by Theorem 10, z is ʳ -like for some
ʳ
ʲ . Clearly, ʳ
ʱ . Therefore one more application of Theorem 10 provides
z
u
∈{
1 , 1 / 2
}
. Hence combining the above results we get
( u ( y )
(
z
y
z
u
)) = 1
y∈ dom( u )
V (PS 3 ) . This leads to the fact
for any z
=1 , i.e., V (PS 3 )
y
z ( y
u
z
y
z
u )
|
=Trans( u ) .
( ii )Sinceforany ʱ, ʲ
ORD exactly one of ʱ
ʲ, ʱ = ʲ and ʲ
ʱ holds
in V , the proof can be derived easily by applying Theorems 9 and 10.
Search WWH ::




Custom Search