APPLICATIONS OF ALGEBRA
ZAKOPANE 2009
On a nitely axiomatizable Kripke incomplete logic
containing KT B
Zo a Kostrzycka
Brouwerian logic
KTB
Axioms CL and
K
:=
(p → q) → (
p →
q)
T
:=
p → p
B
:= p →
♦
p
Kripke frames for
KTB
De nition 1. By a Kripke frame we mean a pair
F
=
hW, Ri
where
W
-nonempty set
and
R
relation on W
.
In the case of the logic
KTB
, R is re exive and symmetric.
Elements of W are called points and the relation R is an
accessibility relation: xRy means: `y is accessible from x'.
Valuation
F
is a function V : V ar → W and can be extended
Then we de ne for each x ∈ W :
x |= p
i
x ∈ V (p)
x |= α ∧ β
i
x |= α
i x |= β
x |= α ∨ β
i
x |= α
or x |= β
x |= α → β
i
x 6|= α
or x |= β
x |= ¬α
i
x 6|= α
x |=
α
i
for any y ∈ W if xRy then y |= α
A formula α is a tautology of the logic
KTB
, if it is true
Extensions of
KTB
T
n=
KTB
⊕ (4
n)
, where
(4
n)
n
p →
n+1
p
(tran
n)
∀
x,y(
if xR
n+1y
then xR
ny)
where the relation R
nis the n-step accessibility relation
de ned below:
xR
0y
i
x = y
KTB
⊂ ... ⊂
T
n+1⊂
T
n⊂ ... ⊂
T
2⊂
T
1=
S5
.
De nition 2. A logic
L
is
Kripke complete
, if there is a
class C of Kripke frames, such that:
1. for every formula ψ ∈
L
and any frame
F
∈ C
we have
F
|= ψ
.
2. for every formula ψ 6∈
L
, there is a Kripke frame
G
∈ C
such that
G
6|= ψ
.
Problem
Miyazaki in [1] de ned one Kripke incomplete logic in
N EXT (
T
2)
and a continuum of Kripke incomplete logics
in NEXT (
T
5)
.
Kostrzycka in [2] de ned a continuum Kripke incomplete
logics in NEXT (
T
2)
.
[1] Y. Miyazaki, Kripke incomplete logics containing KTB,
Studia Logica 85, (2007), 311-326.
[2] Kostrzycka Z, On non compact logics in NEXT (
KTB
)
.
Mathematical Logic Quarterly 54, no. 6, (2008),
617-624.
Question
: Is there a
KTB
- logic which is Kripke
The aim
To de ne a logic L
∗and a formula ψ such that ψ 6∈ L
∗and
for any Kripke frame
F
the following implication holds:
Axioms for L
∗Exclusive formulas:
F
∗:= p
∗∧ ¬p
0∧ ¬p
1∧ ¬p
2∧ ¬p
3∧ ¬p
4∧ ¬p
5,
F
0:=
¬p
∗∧ p
0∧ ¬p
1∧ ¬p
2∧ ¬p
3∧ ¬p
4∧ ¬p
5,
F
1:=
¬p
∗∧ ¬p
0∧ p
1∧ ¬p
2∧ ¬p
3∧ ¬p
4∧ ¬p
5,
F
2:=
¬p
∗∧ ¬p
0∧ ¬p
1∧ p
2∧ ¬p
3∧ ¬p
4∧ ¬p
5,
F
3:=
¬p
∗∧ ¬p
0∧ ¬p
1∧ ¬p
2∧ p
3∧ ¬p
4∧ ¬p
5,
F
4:=
¬p
∗∧ ¬p
0∧ ¬p
1∧ ¬p
2∧ ¬p
3∧ p
4∧ ¬p
5,
F
5:=
¬p
∗∧ ¬p
0∧ ¬p
1∧ ¬p
2∧ ¬p
3∧ ¬p
4∧ p
5,
Q := {F
1∧
♦
F
∗∧
♦
(F
0∧ ¬
♦
F
2∧ ¬
♦
F
3∧ ¬
♦
F
4)
∧
∧
♦
(F
2∧
♦
(F
3∧
♦
(F
4∧
♦
F
5))
∧ ¬
♦
F
4∧ ¬
♦
F
5)
∧ ¬
♦
F
3}
→
♦
(F
∗∧
♦
F
0∧
♦
F
2∧
♦
F
3∧
♦
F
4∧
♦
F
5).
The role of Q:
d d d d d d
d
F
∗XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX P P P PP P P P P P P P P P P P P P P P P P P P P P P P P P P P P PP H H H H H H H H H H H H H H H H H H H H H H H @ @ @ @ @ @ @ @ @ @ @ @ d d d d d d d
F
∗F
5F
4F
3F
2F
1F
0G := {F
5∧
♦
[F
4∧
♦
(F
3∧
♦
(F
2∧
♦
(F
1∧
♦
F
0)))]
∧
♦
F
∗∧
5 ^ i=0F
i→
p
∧
2 (p ∧ F
∗)
→
5 ^ i=0♦
F
i ∧
∧
2
F
∗∨
5 _ i=0F
i ∧
2[
(F
5∨ (F
∗∧ p)) →
♦
(F
5∧
♦
F
4)]
∧
∧
4 ^ i=0 2[
(F
i∨ (F
∗∧ p)) →
♦
(F
i∧
♦
F
i+1)]} →
♦
F
0The role of G:
XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XXX X P P P P P P P P P P P P P P P P P P P P PP P P P P P P P P P P P PP H H H H H H H H H H H H H H H H H H H H H H H @ @ @ @ @ @ @ @ @ @ @ @ d d d d d d dF
∗F
5F
4F
3F
2F
1F
0XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX P P P PP P P P P P P P P P P P P P P P P P P P P P P P P P P P P PP H H H H H H H H H H H H H H H H H H H H H H H @ @ @ @ @ @ @ @ @ @ @ @ d d d d d d d
F
∗F
5F
4F
3F
2F
1F
0 ' $P
:=
{r ∧
3 ^ i=1(A
i∧ B
i∧ C
i)} →
♦
2{r ∧
(r → (q
1∨ q
2∨ q
3))},
where
A
i:=
2
(q
i→ r),
B
i:=
2
(r →
♦
q
i),
for i = 1, 2, 3
C
1:=
2
¬(q
2∧ q
3),
C
2:=
2
¬(q
1∧ q
3),
C
3:=
2
¬(q
1∧ q
2).
De nition 4.
L
∗:=
T
2⊕ G ⊕ Q ⊕ P
.
Formuªa ψ
H
∗:=
¬s
0∧ ¬s
1∧ ¬s
2∧ ¬s
3∧ ¬s
4,
H
0:=
¬s
0∧ ¬s
1∧ s
2∧ s
3∧ s
4,
H
1:=
¬s
0∧
¬s
1∧ ¬s
2∧ s
3∧ s
4,
H
2:= s
0∧ ¬s
1∧
¬s
2∧ ¬s
3∧ s
4,
H
3:= s
0∧ s
1∧ ¬s
2∧
¬s
3∧ ¬s
4,
H
4:= s
0∧ s
1∧ ¬s
2∧ ¬s
3∧
¬s
4,
H
5:=
¬s
0∧ s
1∧ ¬s
2∧ s
3∧ ¬s
4,
ψ := ¬{H
5∧
♦
[H
4∧
♦
(H
3∧
♦
(H
2∧
♦
(H
1∧
♦
H
0∧
♦
H
∗)))]}
.
Lemma 5. For every Kripke frame
F
it holds:
if
F
|= L
∗, then
F
|= ψ
.
Proof: Suppose that there is a Kripke frame
F
such that
F
|= L
∗and
F
6|= ψ
.
Then the structure
F
consists of at least seven dierent
points x
∗, x
0, x
1, x
2, x
3, x
4, x
5such that: x
1Rx
∗,
and x
iRx
jc c c c c c c
x
∗x
5x
4x
3x
2x
1x
0We de ne a valuation for the variables p
0, ..., p
5, p
∗:
V (p
i) =
{x
i}
for i = 0, ..., 5, and V (p
∗) =
{x
∗}.
That gives us:
c c c c c c c
x
∗|= F
∗x
5|= F
5x
4|= F
4x
3|= F
3x
2|= F
2x
1|= F
1x
0|= F
0The formula Q has to be true under that valuation, hence
it must hold: x
∗Rx
j, for j = 0, 2, 3, 4, 5.
@ @ @ @ @ @ @ @ @ @ @ @ c c c c cc c c
x
∗x
5x
4x
3x
2x
1x
0Let us consider a new valuation de ned on the obtained
frame:
x
∗|= p
∗,
x
i|= p
i,
for i = 0, 1, 2, 3, 4, 5
For any x such that x sees only the point x
∗we de ne:
In the other points we de ne: if xRy and y |= p
i, then
x |= p
kfor k 6= i and i = 0, 1, ..., 5 and k = 1, ..., 4. For
such valuation we obtain:
x
∗|= F
∗∧ p
i x = x
∗x |= F
0i x = x
0x |= F
5i x = x
5The antecedent of the formula G is true at x
5; the
conse-quent of G has to be true at x
5- hence x
5Rx
0. Then we
XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX P P P PP P P P P P P P P P P P P P P P P P P P P P P P P P P P P PP H H H H H H H H H H H H H H H H H H H H H H H @ @ @ @ @ @ @ @ @ @ @ @ d d d d d d d
x
∗x
5x
4x
3x
2x
1x
0 ' $P
:=
{r ∧
3 ^ i=1(A
i∧ B
i∧ C
i)} →
♦
2{r ∧
(r → (q
1∨ q
2∨ q
3))},
where
A
i:=
2
(q
i→ r),
B
i:=
2
(r →
♦
q
i),
for i = 1, 2, 3
C
1:=
2
¬(q
2∧ q
3),
C
2:=
2
¬(q
1∧ q
3),
C
3:=
2
¬(q
1∧ q
2).
Formula P is false with the following valuation:
V
∗(r) = {x
∗, x
0, ..., x
5}, V
∗(q
1) =
{x
1, x
4}, V
∗(q
2) =
{x
2, x
5}
XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XX XXX X P P P P P P P P P P P P P P P P P P P P P P P P PP P P P P P P P PP H H H H H H H H H H H H H H H H H H H H H H H @ @ @ @ @ @ @ @ @ @ @ @ d d d d d d d
x
∗|= q
3x
5|= q
2x
4|= q
1x
3x
2|= q
2x
1|= q
1x
0 ' $We take x
3. It holds: x
3|= r
and x
3|= A
i∧ B
i∧ C
ifor
i = 1, 2, 3
. However x
3n6|= q
1∨ q
2∨ q
3for n = 0, 1, and
then x
36|=
♦
2{r ∧
(r → (q
1∨ q
2∨ q
3))
}
.
Lemma 6. ψ 6∈ L
∗.
Proof. We use a general frame. General frames are
rela-tional counterparts of modal algebras. De ne:
G
=
hW, R, T i
where:
W
:=
{x
∗} ∪ {x
i, i ∈
Z
},
R := {(x
∗, x
ifor each i ∈
Z
} ∪
∪{(x
i, x
j)
i |i − j| ≤ 1; for any i, j ∈
Z
},
T
:=
{X ⊂ W : X
is nite or W \ X is nite}.
a a a a a a a a a a a a a a a a a a a a a a a a Q Q Q Q Q Q Q Q Q Q Q Q Q Q A A A A A A A A A A !! !! !! !! !! !! !! !! !! !! !! !! d d d d d d d d d
x
−2x
−1x
0x
1x
2x
3x
4x
∗G
|= P, Q, G
.
De ne a valuation:
V (s
0) =
{x
2, x
3, x
4}, V (s
1) =
{x
3, x
4, x
5}, V (s
2) =
{x
0, x
4, x
5},
V (s
3) =
{x
0, x
1, x
5}, V (s
4) =
{x
0, x
1, x
2}.
a a a a a a a a a a a a a a a a a a a a a a a a Q Q Q Q Q Q Q Q Q Q Q Q Q Q A A A A A A A A A A !! !! !! !! !! !! !! !! !! !! !! !! d d d d d d d d d
