Database Reference
In-Depth Information
In fact, for the binary accessibility relation
R
on
X
equal to the binary partial order-
ing '
' which is reflexive and transitive, we obtain the S4 modal framework with
the universal modal quantifier
≥
, defined by
6.
M
|=
b
φ)
,
so that from 4. and 5. we obtain for the inuitionistic implication and negation that
⇒
M
|=
a
φ
iff
∀
b(a
≥
b
implies
¬
c
are the classical
(standard) propositional implication and negation, respectively. Thus, we extend
V
to any given formula
φ
by
V(φ)
is equal to
⇒
c
and
¬
is equal to
¬
c
, where
⇒
c
and
={
a
|
M
|=
a
φ
}∈
H(W)
and say that
φ
is true in
M
if
V(φ)
=
W
. Consequently, the complex algebra of the truth values is a Heyting
algebra:
7.
H
(W)
=
(H(W),
⊆
,
∩
,
∪
,
⇒
h
,
¬
h
,
∅
,W)
,
where
⇒
h
is a relative pseudo-complement in
H(W)
and
¬
h
is a pseudo-
∈
¬
h
(S)
=
⇒
h
∅
complement such that for any hereditary subset
S
H(W)
,
S
(the
empty set
∅
is the bottom element in the truth-value lattice
(H(W),
⊆
,
∩
,
∪
)
, corre-
sponding to falsity; thus, a formula
φ
is false in
M
if
V(φ)
=∅
).
Let
φ
be a propositional formula, F be a Kripke frame,
M
be a model on F, and
K be a class of Kripke frames, then:
(a) We say that
φ
is
true
in
M
, and write
M
|=
φ
,if
M
|=
a
φ
for every
a
∈
W
(i.e.,
if
V(φ)
=
W
);
(b) We say that
φ
is
valid
in the frame F, and write F
|=
=
φ
,if
V(φ)
W
for every
valuation
V
on F. We denote by
Log(
F
)
={
φ
|
F
|=
φ
}
the set of all formulae
that are valid in F;
(c) We say that
φ
is
valid
in K, and write K
|=
φ
,ifF
|=
φ
for every F
∈
K.
Analogously, let
H
=
(W,
≤
,
∧
,
∨
,,
¬
,
0
,
1
)
be a Heyting algebra. A function
v
:
→
W
is called a valuation into this Heyting algebra. We extend the valuation
from PR to all propositional formulae via the recursive definition:
PR
v(φ
∧
ψ)
=
v(φ)
∧
v(ψ),
v(φ
∨
ψ)
=
v(φ)
∨
v(ψ),
v(φ
⇒
ψ)
=
v(φ) v(ψ).
=
Aformula
φ
is
true
in
H
under
v
if
v(φ)
1;
φ
is
valid
into
H
if
φ
is true for every
valuation in
H
, denoted by
H
φ
. Algebraic completeness means that a formula
φ
is
HA
-valid iff it is valid in
every
Heyting algebra:
8.
φ
is
HA
-valid iff
|=
IL
φ
.
The “soundness” part of 8. consists in showing that the axioms 1-11 are
HA
-valid
and that Modus Ponens inference preserves this property (in fact, if for a given
valuation
v
,
v(φ)
1).
The completeness of IL w.r.t.
HA
-validity can be shown by the Lindenbaum-
Tarski algebra method by establishing the equivalence relation
=
v(φ
⇒
ψ)
=
1 then
v(φ)
≤
v(ψ)
so
v(ψ)
=
∼
IL
for the IL-
formulae (
IPC
), as follows:
9.
φ
ψ
).
The Lindenbaum algebra for IL is then the quotient Heyting algebra
∼
IL
ψ
iff
IL
φ
⇒
ψ
and
IL
ψ
⇒
φ
(i.e., iff
IL
φ
⇔
H
IL
=
(
IPC
∼
IL
,
,
,
,,
¬
)
