Database Reference
In-Depth Information
That the Gödel translation can be extended to an embedding of at least a few
particular intuitionistic modal systems into some classical multi-modal logics was
observed by several authors [
22
,
23
,
27
].
The propositional intuitionistic logic with connectives
∧
,
∨
,
⇒
,
0
(
¬
φ
is defined
0
where
0
is contradiction) and the modal operators
i
,
i
as
φ
1
,...,n
,is
an IM-logic (Intuitionistic Modal logic [
26
]) if it is a set of formulae containing
intuitionistic logic IL (with only first four connectives above) and closed under sub-
stitution, Modus Ponens and the congruence rules
⇒
=
φ
⇔
ψ
=
1
,...,n
.
The way how, for a given negation logical operator of intuitionistic logic, we
can find its algebraic counterpart in the Birkhoff polarity was shown previously in
Example
42
. Now, in this section, we will represent the algebraic operators in the
quotient algebra
L
alg
by the corresponding logical operations. Notice that in
L
alg
all operators are preceded by the closure operator
Γ
(equal to power-view closure
operator
T
for databases), so that the first step is to obtain the logical operator cor-
responding to this algebraic closure operator.
i
φ
⇔
i
ψ
, for all
i
Remark
First of all, we have to verify if the monotonic closure operator
Γ
can
be interpreted by a unique modal operator (in this case it has to be an existential
modal operator from the fact that it is monotonic and satisfies the first additive modal
property for the bottom element
). The answer is negative
because the second additive property does not hold, and from Lemma
20
, instead of
equality we have for any two
S,S
∈
F
{
0
}∈
F
(W)
,
Γ(
{
0
}
)
={
0
}
S
)
Γ(S
))
.
(W)
only that
Γ(S
∪
⊇
(Γ (S)
∪
ρλ
is a monotonic operator, obtained by com-
position of two negation operators, multiplicative operator
ρ
and additive operator
λ
,
both of which are modal negation operators (as we have seen in Example
42
,thein-
tuitionistic negation
However, the closure operator
Γ
=
¬
is a modal,
¬=
R
−
1
≤
¬
c
, where
¬
c
is classic (standard) nega-
universal modal operator for accessibility relation
R
−
1
tion and
R
−
1
≤
, we obtained
≤
the algebraic additive operator
λ
R
−
1
≤
). Consequently,
Γ
in a logical representation
has to be a
composed modal
logical operator, as follows:
Lemma 24
ρλ
,
obtained from Dedekind-McNeile Ga-
lois connection
,
corresponds to the composition of two modal operators
The closure operator Γ
=
R
≤
R
−
1
≤
,
where
R
≤
is a universal modal operator for the accessibility relation R
≤
,
and
is an existential modal operator for the accessibility relation R
−
1
≤
R
−
1
≤
.
Both these two operators are normal modal operators
,
and we denote by IL
Γ
the
IM-logic with
1
=
R
≤
and
2
=
R
−
1
≤
.
Proof
For a given formula
φ
of the DB weak topos logic with the algebra
L
alg
,
let
S
K
be a set of worlds where
φ
is true. Then, for the incompatibility
binary relation
R
≤
(equal to the poset
=
φ
≤
), we have the Dedekind-McNeile Galois
