LOGICAL THEORY OF POST's LOGICS WITH LINEAR ORDER

The communication is devoted to the introduction of a logical theory of Post's Logics with linear order and a sequent calculus for this theory. This calculus may be applied to computer representation of knowledge. In the communication the use of rational numbers is proposed as logical values for graded knowledge representation. It is useful to grade knowledge which represent in informational systems, for example, by priority of their using. We use possibilities of Post's logics and extend them by comparisons of logical values of predicate formulas. The paper is a further development of level logics proposed by Kosovski . The introduced logic is able to replace fuzzy and continuous logics in practice, since only finite sets of rational numbers from a finite diapason are used.
There may be another approach consisting in the use of even-valued Post's logics for natural sciences and odd-valued Post's logics (which include a paradoxical value) for humanitarian and applied sciences.
Every logical value is a rational number. The abbreviation [a..b]/q, where a, b, q -- non negative integers, $a\; \le \; b$ and q ≥ 1 is used for a finite diapason of nonnegative rational numbers. A rational number r is in [a..b]/q if for some integer m r=m/q and $a\; \le \; m\; \le \; b$. We use a propositional variable with a list of upper indices to fix a diapason in which rational numbers or their negations are used.

So values of $p^\{a,b,q\}$ belong to the set of rational numbers from diapason [a..b]/q or [-b..-a]/q, values of p^{a,b} belong to the set of integers from diapason [a..b] or [-b..-a]. Analogous abbreviations will be used for predicate symbols. So formulas with the only 0,~b or 0,~b,~q as the list of upper indices correspond to 2b+1-valued Post's logic. Formulas with the only a,~b or a,~b,~q as the list of upper indices correspond to 2(b-a)-valued Post's logic.
Predicate formulas of S are defined as usually on the base of atomic formulas with the use of negation, conjunction, disjunction, four-place connective if B < A then C else D fi, and quantifiers, beginning with atomic formulas of S. Conditional expression is interpretated as in programming languages.

Let the comparison sign has one of the following types: ≤, <. A comparison sign is placed between predicate formulas. Such a formula is called a logical comparison, or, more briefly comparison.

Logical values of comparisons are defined in usual way (in the classical two-valued logic).

Lemma : The system of inequalities is decidable in rational numbers by an algorithm of the class

N.K.Kossovski, A.V.Tishkov

St.-Petersburg State University

kosov@nkk.usr.pu.ru