L – decidability of some invariant systems.
Robert Sochacki
University of Opole
Outline
Definition of the invariant system
System W
Sobocinski’s system
Remarks
Invariant systems
System (X, R) is an invariant system if:
, and
,
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( )
L-decidable systems
The system based on a set of rejection rules and a set of rejected axioms is called L-decidable if and only if the following conditions hold:
where T is the set of all theses,
T* is the set of all rejected formulas, and
S is the set of all formulas
S T
T II
T T
I
) (
) (
System W
The system W is defined by the following matrix:
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.
Consider the following functors:
q CCpqCApqKp q
p
F0 ( , )
,
qCpq ACCNpApqAp
q p
F ( , )
2
, 1
).
, ( )
,
( 0
1 p q F q p
F
System W – cont.
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
2 1 1
, 1
2 1 1
, 0 )
, (
2 1
y or x
if
y and x
if y
x f
0 1
, 1
0 1
, ) 0
,
1(
y or x
if
y and x
y if x f
Rejected axioms
The formulas:
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.
The main theorem:
Let be an arbitrary formula of the system W. If , then . T
T
Sobocinski’s system
The implicational-negational system of Sobocinski is given by the following
matrix:
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
Sobocinski’s system –cont.
Consider the following functors:
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
Sobocinski’s system – cont.
The following functions correspond to functors in the matrix MSc,n:
………
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
Sobocinski’s system – cont.
The negations of the functions defined on the previous slides:
………
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
Sobocinski’s system – cont.
Now we can define the following functors:
) , ( )
, ( )
, ( ...
)...
, ( )
, ( )
, (
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
) , ( )
, ( )...
, ( )
, ( )
,
( 1 2 1 2
0 p q CF p q CF p q CF p q NG p q
F k k k
), , ( )
, ( ) , ( ....
)...
, ( ) , ( )
, (
2 0
2
2 1
1
q p NG p q CNG q p CF
q p CF q p CF q p F
k k k
Sobocinski’s system – cont.
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 ,
(
Sobocinski’s system – cont.
Now consider the following functor:
The following function corresponds to the functor in the matrix MSc,n:
).
, ( )
,
( p q CN 2CppCCqpNG0 p q AS
} 1 ,
0 { y
for x,
} , max{
) ,
(x y x y k
as
Rejected axioms
The formulas:
or
) , ( p q Fi
)) ,
( )),...),
, ( ),
, ( (
(A F r p F q s F u v
AS S i j t
Sobocinski’s System – cont.
The main theorem:
Let be an arbitrary formula of the Sobocinski system.
If , then . T T
