Ł – decidability of some invariant systems.
Robert Sochacki
University of Opole
Outline
z Definition of the invariant system
z System W
z Sobociński’s system
z Remarks
Invariant systems
z System (X, R) is an invariant system if:
z , and
z ,
where the class of structural rules is:
] ))
( ),
( (
) , [(
: r h
h r
S At
e S
S Struct
r
e
e Π ∈
⇒
∈ Π
→
∀
∈
∀
⊆ Π
∀
⇔
∈
α α
α Struct
R ⊆
X X
Sb ( ) =
Ł-decidable systems
z The system based on a set of rejection rules and a set of rejected axioms is called Ł-decidable if and only if the following conditions hold:
z where T is the set of all theses,
z T* is the set of all rejected formulas, and
z S is the set of all formulas
S T
T II
T T
I
=
∪
∅
=
∩
∗
∗
) (
) (
System W
z The system W is defined by the following matrix:
z where:
{ } { }⎟⎟
⎠
⎜⎜ ⎞
⎝
⎛ ¬
⎭⎬
⎫
⎩⎨
= ⎧
Μ ,1 , 1 , , , ,
2 , 1
0 c k a
w
⎪⎩
⎪⎨
⎧ = = =
=
else
y or y
and x
y if x c
, 1
2) 0 1
( 1
, ) 0
, (
⎪⎪
⎩
⎪⎪⎨
⎧ ≠ ≠
=
else
y and x
if y x y
x k
2, 1
2 1 2
), 1 , min(
) , (
⎪⎪
⎩
⎪⎪⎨
⎧ ≠ ≠
=
else
y and x
if y x y
x a
2, 1
2 1 2
), 1 , max(
) , (
x x = −
¬ 1
System W – cont.
z Consider the following functors:
q CCpqCApqKp q
p
F0 ( , ) =
,
q ACCNpApqAp q
p
F ( , ) =
2 1
).
, ( )
,
( 0
1 p q F q p
F
,
=
System W – cont.
z The following functions correspond to functors in the matrix Mw:
⎩⎨
⎧
≠
≠
=
= =
1 0
, 1
1 0
, ) 0
,
0(
y or x
if
y and x
y if x f
⎩⎨
⎧
≠
≠
=
= =
0 1
, 1
0 1
, ) 0
,
1(
y or x
if
y and x
y if x f
⎪⎪
⎩
⎪⎪⎨
⎧
≠
≠
=
=
=
2 1 1
, 1
2 1 1
, 0 )
, (
2 1
y or x
if
y and x
if y
x f
Rejected axioms
z The formulas:
z or generalized disjunctions that can be build from the above formulas.
) , ( ),
, ( ),
,
( 1
2 1
0 p q F s r F t u
F
System W – cont.
z The main theorem:
Let α be an arbitrary formula of the system W. If , then .α ∉T α ∈ T ∗
Sobociński’s system
z The implicational-negational system of Sobociński is given by the following
matrix:
z where k>=3, and for
{ } { } { }
(
k k c n)
n c
S, = 0,1,2,..., −1 , 1,2,..., −1 , , Μ
⎩⎨
⎧
=
−
= ≠
y x
if k
y x
if y y
x
c 1,
) , ,
( ⎩⎨⎧
−
=
−
<
= +
1 ,
0
1 ,
) 1
( if x k
k x
if x x
n
} 1 ,...,
1 , 0 {
, y ∈ k −
x
Sobociński’s system –cont.
z Consider the following functors:
z where for l>=1:
Cqq CpN
q p G
Cqq CpN
q p G
CpNCqq q
p G
k k
1 2
2 1
0
) , (
, ...
, )
, (
, )
, (
− = −
=
=
⎪⎩
⎪⎨
⎧
=
=
+ α α
α α
l
l NN
N
N N
1 1
Sobociński’s system – cont.
z The following functions correspond to functors in the matrix MSc,n:
z z
z ………
z
⎩⎨
⎧
=
−
= ≠
0 ,
1
0 ,
) 0 ,
0(
x if k
x y if
x g
⎩⎨
⎧
=
−
= ≠
1 ,
1
1 ,
) 1 ,
1(
x if k
x y if
x g
⎩⎨
⎧
−
=
−
−
≠
= −
− 1, 2
2 ,
) 2 ,
2(
k x if k
k x if y k
x gk
Sobociński’s system – cont.
z The negations of the functions defined on the previous slides:
z
z
z ………
z
⎩⎨
⎧
=
= ≠
0 ,
0
0 ,
)) 1 , ( ( 0
x if
x y if
x g n
⎩⎨
⎧
=
= ≠
1 ,
0
1 ,
)) 2 , ( ( 1
x if
x y if
x g n
⎩⎨
⎧
−
=
−
≠
= −
− 0, 2
2 ,
)) 1 , ( ( 2
k x if
k x if y k
x g
n k
Sobociński’s system – cont.
z Now we can define the following functors:
z
z
z and in general for 0<= l < k:
z
) , ( )
, ( )
, ( ...
)...
, ( )
, ( )
, (
2 2
3
1 0
1
q p NG
p q CNG
p q CNG
p q CNG p
q CNG q
p F
k k
k k
−
−
−
− =
) , ( )
, ( ...
)...
, ( )
, ( )
, ( )
, (
2 3
1 0
1 2
q p NG
p q CNG
p q CNG p
q CNG q
p CF
q p F
k k
k k
−
−
−
− =
) , ( )
, ( ...
)...
, ( )
, ( )...
, ( )
, (
2 1
0 1
2 1
q p NG
p q CNG
p q CNG q
p CF
CF q
p CF
q p F
k l
l l
l l
−
−
−
−
= +
Sobociński’s system – cont.
z The following functions correspond to functors in the matrix MSc,n:
⎩⎨
⎧
≠
−
≠
−
=
−
= =
l y
or k
x if
k
l y
and k
x y if
x fl
2 ,
1
2 ,
) 0 ,
(
Sobociński’s system – cont.
z Now consider the following functor:
z The following function corresponds to the functor in the matrix MSc,n:
).
, ( )
,
( p q CN 2CppCCqpNG0 p q
A =
} 1 ,
0 { y
for x,
} , max{
) ,
(x y = x y ∈ k −
a
Rejected axioms
z The formulas:
z or
z
) , ( p q Fi
)) ,
( )),...),
, ( ),
, ( (
(A F r p F q s F u v
A i j t
Sobociński’s System – cont.
z The main theorem:
Let α be an arbitrary formula of the Sobociński system.
If , then .α ∉T α ∈ T ∗
