COMPLEXITY OF RATIONAL LEVEL SUBLOGICS  DECIDABILITY 

N.K.Kossovski
Faculty of Mathematics and Mechanics
St.Petersburg University,
St.Petersburg, 198904, Russia

   Rational level logic was introduced in [1]. Sometimes it is sufficient
to use only a subset of the set of all rational numbers. So we have the 
following. 
      Let  M  be the standard model of the universal theory of all rational
numbers in the following signature: all rational numbers as constants,
unary function -, binary functions +, max, min ,
ternary function of branching  if A >= 0 then B else C fi ,
binary predicates   >=, =  , (n+1)-ary predicate of belonging of  X0 to
{X1, ... , Xn}.
   LEMMA 1. The system of inequalities is decidable in rational 
numbers by an algorithm of the class   EXP-LIN-TIME.
   THEOREM 1. The set of true formulae of  M  is
decidable by an algorithm  of the class   EXP-LIN-TIME.
   The proof is based on the lemma 1 and the use of an inference
in the sequent calculus with the reversible rules .
   Such a model M is similar to the rational level logic described in [1].
It also may be interpreted as a generalization of the fuzzy logic [2,3] 
to all rational numbers.
   Let  I  be the standard model of the universal theory of all integer
numbers in the following signature: all integer numbers as constants,
unary function -, binary functions +, max, min ,
ternary function of branching  if A >= 0 then B else C fi ,
binary predicates   >=, =  , (n+1)-ary predicate of belonging of  X0 to
{X1, ... , Xn}.
    LEMMA 2. The system of inequalities is decidable in integer 
numbers by an algorithm of the class  EXPTIME.
   THEOREM 2. The set of true formulae of  I  is
decidable by an algorithm  of the class   EXPTIME.
      The proof of the theorem 2 is based on the lemma 2 and the 
use of an inference in the sequent calculus with the reversible rules.
  Let  C  be a subset of  I   in which every variable has values
only from a finite set of rational numbers.
   THEOREM 3. The set of true formulae of  C  is decidable by an
algorithm of the class  EXP-LIN-TIME.
   The proof is based on the use of an inference in the sequent calculus
with the reversible rules and on the  search of a solution of a system of
inequalities by Turing machine on linear space.
  Now  the class  EXP-LIN-TIME cannot be changed by  P  because 
it will imply  P=NP.

                        References
1. N.Kossovski. Sequent Calculus for Generalization of Getmanova's
   Logic to the Predicates. Logic Colloquium'94. Abstracts of Contributed
   papers. Universite d'Auvergne (Clermont 1), (1994), p.73.
2. L.A.Zadeh. Fuzzy Sets. Inf. Control 8 (1965), pp. 338-353.
3. L.A.Zadeh. Fuzzy Logic. Neural Network and Soft Computing. 
   Comm. of the ACM 37 (1994), pp. 77-89.