Information Technology Reference
In-Depth Information
2.2 The Algebra-Valued Model Construction and BQ
ϕ
The following account is taken from [5] with the permission of the first author
of that paper.
We start with a model of classical set theory
V
andanalgebra
A
,
∧
,
∨
,
⃒
,
∗
,
1
,
0
. A universe of
names
is constructed by transfinite recursion:
V
(
A
)
ʱ
=
{
x
;
x
is a function and ran(
x
)
ↆ
A
V
(
A
)
ʾ
and there is
ʾ<ʱ
with dom(
x
)
ↆ
)
}
and
V
(
A
)
=
V
(
A
ʱ
)
{
x
;
∃
ʱ
(
x
∈
}
.
Let
L
∈
be the language of set theory having the propositional connectives
∧
,
∨
L
∈
extended by adding
constants corresponding to each element in
V
(
A
)
. Similar to the case in Boolean-
valued model (cf. [1]) the following (
meta-
)
induction principle
for
V
(
A
)
will be
used in this paper whenever it is needed: for every property
ʦ
of names, if for
all
x
,
→
,and
¬
.
L
A
stands for the extended language of
V
(
A
)
,wehave
∈
∀
y
∈
dom(
x
)(
ʦ
(
y
)) implies
ʦ
(
x
)
,
V
(
A
)
have the property
ʦ
.
Following the Boolean-valued model construction a map
then all names
x
∈
·
is defined from the
V
(
A
)
class of all formulas in
L
A
to the set
A
of truth values as follows. If
u,v
∈
and
˕, ˈ
are any two formulas in
L
A
then
=
x
u
∈
v
(
v
(
x
)
∧
x
=
u
)
,
∈
dom(
v
)
=
x∈
dom(
u
)
u
=
v
(
u
(
x
)
⃒
x
∈
v
)
∧
(
v
(
y
)
⃒
y
∈
u
)
,
y∈
dom(
v
)
˕
∧
ˈ
=
˕
∧
ˈ
,
˕
∨
ˈ
=
˕
∨
ˈ
,
˕
→
ˈ
=
˕
⃒
ˈ
,
∗
,
¬
˕
=
˕
=
∀
x˕
(
x
)
u∈
V
(A)
˕
(
u
)
,and
=
∃
x˕
(
x
)
u∈
V
(A)
˕
(
u
)
.
Let D
ↆ
A
be a set of
designated truth values
(in short:
designated set
). A
formula
˕
of
L
A
is said to be D-valid in
V
(
A
)
if
˕
∈
D and is denoted by
V
(
A
)
=
D
˕
. We omit D in the notation whenever it is clear from the context.
The following equations (for a formula
˕
of the language of set theory) played
a crucial role in the development of the theory in [5]:
|
=
x∈
dom(
u
)
∀
x
(
x
∈
u
→
˕
(
x
))
(
u
(
x
)
⃒
˕
(
x
)
)
.
(BQ
˕
)
