N.K.Kossovski
LEVEL LOGICS
( results were presented on June 6, 1994 )
The article is devoted to the description of level logics, study
of their general initial properties and account of their natural
applications.
The long influence of the scientific chief of my degree work and
candidate thesis N.A.Shanin, who has devoted a significant period of
his life to extending of finitary understanding of mathematical
statements, has given me a courage to introduce in this article
a qualitative level interpretation of various kinds statements.
Presently it is difficult to surprise anybody by one more logic or
a whole class of logics. Nevertheless the class of logics, described
in the present article, is rather useful both in traditional areas of
application of classical logic, and in new fields of application of fuzzy
(continuous) logics, going back to R.Mc Naughton [1] and L.Zadeh [2].
The proposed logics permit to receive the same results in mathematical
psychology concerning human consciousness as gamma-algebra of Lefebvr,
introduced for simulation of subconscious (intuitive) processes of
human thinking [3], [4].
It is possible to introduce the operation of finite union of level
logics the result of which will again be a level logic. The result
of such union will include as a substructure each logic being a member
of this union. In particular therefore in the present paper there is
put forward the assumption that each person when he honestly convinces
the other in his rightness uses one of level logics. Thus more various
people which are to be convinced more vast the set of logic values which
he uses.
Every paradox, for example, the liar paradox, has the paradoxical
logic value in the level logic.
In the level logic except the material implication the level implication,
i.e. natural linear ordering of logic values as numbers can be used.
Then the rule, that every statement follows from the falsity, is transformed
to the rule that from the falsity there follows the falsity of the same or
less (by absolute value) level, as well as paradox statements and true
statements. We mark, that the paradox value is different from the false one.
During the last century the significant quantity of the various logics
was proposed. Many of them have only theoretical or mathematical
significance. In most cases the teaching of the mathematical logic to persons
not specialized in this area is limited by classical two-value logic being
the simplest level logic without the paradox value. The Lucasiewicz logic,
multi-valued logics of Post and logic of Getmanova are slightly
changed level logics ( see, for example, [5] ).
It is convenient to apply the level logic to the analysis of axiomatic
systems, after assignment to the series of axioms or to the schemes of
axioms different levels of plausibility (truth). Then in the frameworks
of one calculus it is possible to connect some classical calculuses,
for example, geometry without the famous parallel axiom and the
Euclidean geometry. These two classical calculuses are characterized by
non-negative values of statements (Euclidean geometry) and maximal
positive values of statements (geometry without parallel axiom).
It is similarly possible to use the various values of various science
postulates after the connecting of some sciences to a united system.
According to the level implication from the statement every statement
with the greater value (or level) follows. Thus it is possible to arrange
the values of different sciences according to the degree of changeability
of their postulates. For example, it is possible to propose that the logic
values of scientific postulates increase in the following sequence:
sociology, psychology, philosophy, other humanitarian sciences, natural
sciences: from biology up to chemistry, physics, mathematics and, at last,
mathematical logic.
The level logic can use all rational numbers from a closed
symmetrical about zero set of rational numbers ( but as it seems to the author,
the level logic which uses all rational numbers is of the greatest interest).
Such a set of rational numbers will be called the set of logical values
of a level logic. For many applications of continuous logic [6]
it is quite enough.
An atomic formula is a logic constant (number) or a propositional
variable with indexes. Among these indexes there may be terms, constructed
as usual from constant symbols, individual variables and various functors
for functions over the set of all constant symbols.
The logic values of conjunction and disjunction are calculated
respectively by means of calculation of minimum and maximum of logic
values of their arguments. The operation of Lucasiewicz's negation
corresponds to unary minus. The material implication ( X=> Y ) has
the logic value of íáè(-[X],[Y]), where [X],[Y] are respectively the
logic values of X and Y. The material implication is true iff the
premise is false or conclusion is true. It is possible to define the
equivalence in the usual way.
The quantifiers are the generalizations of conjunction and disjunction.
The logic value of expression ( cÕÝ ) x A is the supremum of logic values A
for all È. The logic value of expression ( ÌÀÂ )x A is the infimum of logic
values A for all È.
All logic values which are greater than zero are true or plausible (of
greater or less degree (or level) of plausibility). All logic values which
are less than zero are false ones. The logic value, equal to zero, is named a
paradoxical one. In the Getmanova's logic the number 1/2 is the paradoxical
value. Accordingly the values over 1/2 are the true values and the values
under 1/2 are the false ones. Thus the logic value of negation is calculated
according to the less convenient formula.
Predicates which can be more or less plausible are of interest
here. As an example of such predicates a binary predicate "greater than"
( logic value of which is the difference of its arguments) can serve.
By a sequent with usual interpretation we understand a sequence
of well formed formulas, separated by an arrow (a sign of sequent).
Axioms have the following form:
ç1 ò ç2 -> ç3 ò ç4,
ç1 -> ç2 å ç3,
ç1 -å ç2 -> ç3 ,
where ç1, ç2, ç3, ç4 are finite (may be empty) sequences of formulas, ò is a
formula, å is a non-negative number ( logic constant )
The deductive rules for introduction of logic connectives and quantifiers
are defined as in the traditional predicate calculus with convertible
rules for introduction of logic connectives both into antecedent and into
succedent of a sequent (it is possible to use the convertible rules for
introduction into antecedent and into succedent for quantifiers too).
The traditional rule of contraction (see, for example, [7]) with shorter
sequent rules for quantifiers may be additionally used.
The notions of deduction, deducible sequent, deducible formula are
defined as usually.
The following theorems may be easily proved.
THEOREM 1. In any level logic axioms are not false. In any level logic
the conclusion of a rule is not false, if the premises of this rule are
not false ones.
THEOREM 2. Any propositional formula logic value of which in any
level logic is not less than zero is deducible in this calculus.
THEOREM 3. Any propositional formula without logic constants not being
false in every level logic is deducible iff it is a tautology of classical
propositional calculus.
THEOREM 4. There is no a propositional formula without logic constants
being true in even one level logic with the paradox constant.
To be limited by the following basis: (íáè, - (unary), sup) it is
sufficient to have the following axioms and inference rules for propositional
calculus.
Axioms
íáè(ç,H) >= H,
íáè(ç1,A,ç2,-á) >= 0,
where ç, ç1, ç2 are finite (may be empty) sequences of formulas,
A is a formula and H is a rational number.
Rules of reflexivity and transitivity for nonstrict inequality,
interchange and deleting of double minuses:
íáè ( ç, -è ) >= î
íáè(ç,X,Y) >= î íáè(ç,-Y) >= î
-------------------- ---------------------
íáè(ç,íáè(X,Y)) >= î íáè(ç,-íáè(X,Y)) >= H
For the predicate calculus it is sufficient to add the rule of contraction
and two rules with traditional restrictions on formula A, variables è, B
and term ô:
X X
íáè ( ç, [ A ] ) >= î íáè ( ç, - [ A ] ) >= î
T T
------------------ -------------------
íáè(ç, sup A) >= î íáè(ç, -sup A) >= î
X è
Note that the sequent rules of the predicate calculus for any level
logics different from the classic binary logic were not earlier proposed.
The used signature may be extended, for example, by the introduction of
level conditional expression which has not been considered in the propositional
level logics of following form:
(if [A] >= 0 then B else C ).
This expression, as it seems to the author, is more convenient to
write in the form
(-- A ; B -- C --).
The logic value of the expression (-- A; B -- C --) coincides with B,
if A >= 0 and coincides with C, if A < 0. At the repeated use of the
level conditional expression
(-- á1; ÷1 -- (-- á2; ÷2 --(--... (--án; Bn -- C) -- ... --)--)--)
the internal parentheses as well as two minuses near every bracket
may be omitted. As a result we shall have an expression
( - A1 ; B1 -- A2; B2 --... --An; Bn -- C --).
The sequent rules for level conditional expression will be more
complex ones. To receive the conclusion
íáè(ç, (-- á ; ÷ -- ó --)) >= å
the following premises are necessary:
[A] >= 0 or MAX(ç,ó) >= å ,
-([A] > 0) or MAX(ç,÷) >= å .
For level conditional expression with minus it is sufficient
one-premise rule
íáè ( ç, (-- A; -÷ -- ( -ó ) -- )) >= å
-------------------------------------
íáè ( ç, - (-- A; B -- C -- )) >= å
In this connection it will be necessary to duplicate all previous
propositional rules for strict inequality after adding the rule
å > î
------------
íáè (ç,å) > î
and axioms of the form ç(å>î) and ç(å>=î) for such rational constants å and î
for which the strict inequality takes place. Here ç is a finite (may be empty)
sequence of inequalities. Thus now every sequent is extended to a disjunction
of strict and nonstrict inequalities.
It is possible to extend the level logic signature
with the help of introduction of the level implication from A to B
logic value of which coincides with -[A] + [B], therefore the new symbol
will not be specially introduced for it.
The algorithm of establishment of a propositional formula deducibility
on the basis of sequent calculus with convertible rules ( see, for
example, [7] ) belongs to some class of functions from åèò-LIN-TIME, i.e.
is calculated by a deterministic Turing machine in 2^(C*k) steps for some C
where k - the length of propositional formula.
In the framework of the same class of functions it is possible to receive
the algorithm of the establishment of propositional formula deducibility
in the extended signature of level logic. More precisely, the following
theorem is established.
THEOREM 5. The universal (quantifier free) elementary theory of strict
and nonstrict linear inequalities with rational coefficients over rational
numbers is decidable by an algorithm from the class åèò-LIN-TIME.
Proof. A sequent is a sequence of strict and nonstrict
inequalities. The rules of sequent members interchange, change of type of
inequality after multiplication by number -1 are continue in use.
The usual rules of addent interchange in linear inequalities and
combining of like terms are permitted.
Since the expression íáè(ç) >= 0 may be imagined as a sequent of
formulas of the form "the member of the sequence ç is greater or equal
to zero", all rules and axioms formulated before in this paper in essence
are preserved. Axioms of the form ç(A<= å1)(A > å2 ) and the form ç(A<=å1)(A>å2),
where A is a linear expression, å1 and å2 are rational numbers such
that å2 <= å1, are added.
It is required to introduce additional axioms, other than these two,
since from geometrical reasons it is clear that the union of half-spaces
will be equal to the whole space only if the following will be fulfilled.
If the sequent contains nonstrict inequalities it is needed to
check up whether it is not an axiom of first two added types
with the precision of interchange. Otherwise if the sequent
with the precision of interchange has the form ç(AE1) then we
express one variable through others in the equation á=å1 and substitute
the received expression into all members of the sequent
instead of it. This process of substitution we repeat until the members
of the sequent of form (AE) are present. The tautology of the so received
sequent is equivalent to the tautology of the former one.
If our sequent is in neither of listed(transferred) forms
its tautology is equivalent to the tautology of the sequent received
by the replacement of all nonstrict inequalities by the strict ones.
If a sequent contains only strict inequalities it
is an additional axiom iff it may be checked by linear programming methods,
as the negation of a linear inequality disjunction is a system of linear
inequalities.
In essence, there is described a polynomial algorithm of solvability
in rational numbers checking of systems of nonstrict and strict linear
inequalities with integer coefficients. The fact is that the system of linear
inequalities with some strict inequalities may contain the less number of
solutions in comparison with the system with the same but nonstrict
inequalities. The sets of solutions can differ only on bounds. The bounds
are checked up with the help of additional axioms.
The classical conjunctions, including located under the negation, are
introduced according to traditional convertible sequent rules. Negations of
atomic formulas, being inequalities, are received with the helps of
replacement of inequality signs. The theorem is proved.
Consider the following deductive system.
Axioms are such sequents which are sequences of strict or nonstrict
linear inequalities the system of negations of which has no solution
in rational numbers.
The recognition of these axioms can be carried out by methods of linear
programming.
The deductive rules are the rules of the sequent members interchange,
rearrangement of addends and addition of zero addends in linear
expressions, combining of like terms, deleting of double minus,
change of inequality sign after multiplication by (-1) of both parts of
inequalities.
Also we introduce the rule for maximum
ç(ò+á >= 0)(ò+÷ > 0)
-------------------- ,
ç(ò+íáè(á,÷) >= 0)
the same rule for strict inequality, the rule
ç(ò-á >= 0)
ç(ò-÷ >= 0)
--------------------
ç(ò-íáè(á,÷) >= 0)
and the same rule for strict inequality.
For the level conditional expression the following rules are sufficient:
ç(á >= 0)(P+ó >= 0) ç(á >= 0)(P+ó > 0)
ç(-á > 0)(P+÷ >= 0) ç(-á > 0)(P+÷ > 0)
----------------------------- ---------------------------- ,
ç(ò+(-- á ; ÷ -- ó --)) >= 0) ç(ò+(-- á ; ÷ -- ó --)) > 0)
the rule
ç(ò+(-- á ; (-÷) -- (-ó) --) >= 0)
---------------------------------- ,
ç(ò+-(-- á ; ÷ -- ó --) >= 0)
and the same rule for strict inequality.
All these rules are convertible. (The predicate rules may be also
introduced in this calculus as it was done above.)
THEOREM 6. Algorithm of deducibility establishment
in this calculus belongs to class EXP-LIN-TIME.
The algorithm of formula deducibility establishment
in the considered calculus belongs to the required class, if it has
the structure coinciding in general with the traditional
algorithm of establishment of deducibility of propositional formulas in
the sequent propositional calculus with the convertible rules.
At last we use Theorem 5.
If we should receive a polynomial algorithm for deducibility in this
calculus then we could prove that P=NP. And hence we should solve one of
the hardest problems of contemporary algorithm complexity theory. So the
bound from the theorem is now the best.
We note, that if in the level logic we are limited by a finite number of
logic values, there will be more tautology propositional formulas than
in the proposed system. Thus, the less the number of logic values the
more new tautology propositional formulas occur in the extended level logic
with level implication in its signature.
For example, in binary logic the following formula is a tautology:
MIN(|-X1+X2|, |-X2+X3|, |-X3+X1|) <= 0
( We note that |X| = MAX(X,-X) ). At increase of number of logic
values that formula, certainly, will be refutable.
The extension of the set of values of the level logic to set of all
algebraic numbers, made in the frameworks of constructive direction in
mathematics, is possible. In this case the algebraic number is defined as a
polynomial with integer coefficients and an interval for which, according to
the Sturm theorem, the criterion of uniqueness of the real root on this
interval is fulfilled. Algebraic numbers defined in such a way can be added,
subtracted and, that is more essential, checked up for the equality of one to
another with the help of an algorithm. The proposed extension is constructive
while the further extension to continuous logic [6] is not a such one.
The application of such extension of the level logic to geometrical
problems on line, on plane, in space and ets. is possible.
It is possible the further extension of algebraic number set to such
a set of constructive real numbers ( FR-constructs) for which an algorithm
for check of nonstrict inequality between any two numbers from this set
exists in addition. Such an algorithm allows to solve linear equations
in the usual for traditional mathematics way.
The logic value of unary predicate of belonging of a point to a ray
on a straight line can be equal è-è0, where è0 is a coordinate of the top
of the ray, è is a coordinate of a point, being an argument.
The logic value of the unary predicate "a point X belongs to a
segment [X0,Y0] on a line" may have the form MIN(X-X0,Y0-X), where
è is a coordinate of a point, being an argument.
The logic value of the unary predicate " a point with coordinates (X,Y)
belongs to some geometrical figure on a plane" may be equal to minimum of
distance from the bound with the sign "+", if the point is inside of the
figure, and with the sign "-" if the point is outside of this figure.
According to the known theorem from geometry a continuous closed line without
self-crossing divides the plane on two parts: internal and external one.
It is possible to introduce the similar definition for belonging of a point
to a body in the space.
By this we can precisely formalize the division of some statements on
more and less true (plausible) ones.
The level logic is useful during derivation search [8].
It is interesting that the expressibility in the logic for reasoning
about probabilities may be based on the linear inequalities too [9].
The main ideas of the present work were reported on the section
of logic of the thousandth meeting of the seminar "Algebra and logic" in
Novosibirsk on March 3, 1994.
References
1. R. Mc Naughton. A theorem about infinite-valued sentential logic.
J. Symb. Logic, 16, # 1 (1951), 1-13.
2. L.A. Zadeh, Fuzzy Setsm Information and Control, 8, 1965, 338-353.
3. à.á. ûÒÅÊÄÅÒ, ÷ÅÒÏÑÔÎÏÓÔÎÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ "ÆÏÒÍÕÌÙ ÞÅÌÏ×ÅËÁ". -
ðÒÉËÌÁÄÎÁÑ ÜÒÇÏÎÏÍÉËÁ 1 (1994), 20-24.
4. V.A. Lefebvr. The formula of man. An outline of fundamental PSYCHOLOGY
school of Social Sciences, University of California, Irvine,1991.
5. A. Getmanova, Logic. Progress Publishers: Moscow, 1089, 358.
6. ì.é. ÷ÏÌÇÉÎ, ÷.é. ìÅ×ÉÎ, îÅÐÒÅÒÙ×ÎÁÑ ÌÏÇÉËÁ. ôÅÏÒÉÑ ÐÒÉÍÅÎÅÎÉÑ.
ôÁÌÌÉÎ: áËÁÄÅÍÉÑ ÎÁÕË üÓÔÏÎÉÉ, 1991, 210 Ó.
7. î.ë. ëÏÓÏ×ÓËÉÊ, üÌÅÍÅÎÔÙ ÍÁÔÅÍÁÔÉÞÅÓËÏÊ ÌÏÇÉËÉ É ÅÅ ÐÒÉÌÏÖÅÎÉÑ Ë ÔÅÏÒÉÉ
ÓÕÂÒÅËÕÒÓÉ×ÎÙÈ ÁÌÇÏÒÉÔÍÏ×. ì.: ìçõ, 1981, 192 Ó.
8. ÷.ñ. ëÒÅÊÎÏ×ÉÞ, óÅÍÁÎÔÉËÁ ÉÔÅÒÁÔÉ×ÎÏÇÏ ÍÅÔÏÄÁ ó.à. íÁÓÌÏ×Á. ðÒÏÂÌÅÍÙ
ÓÏËÒÁÝÅÎÉÑ ÐÅÒÅÂÏÒÁ. í., ÷ÏÐÒÓÙ ËÉÂÅÒÎÅÔÉËÉ, ÷ÙÐ. 131, 30-62.
9. R.Fagin, J.H. Halpern, N. Meqiddo, Logic for reasoning about Probabilities.
Proc. 3rd IEEE Symp. on Logic in Comp. Sci., 1988, 271-291.
Supplement of translator
The proof of theorem 5 presented here may be more short and clear
with the use of [10]. To receive the new proof it is needed to change
the 4th, 5th and 6th paragraphs of the previous proof by the following text.
"A sequent is an additional axiom iff it may be checked by linear
programming methods, as the negation of a linear inequality disjunction is
a system of linear inequalities.
At first the system of linear inequalities are transformed to the system
of nonstrict linear inequalities over positive rational numbers. The last one
is transformed to the system of the same type but over all rational numbers
with the use of some linear programming method (firstly by proposition 2 of
$ 6, chapter 1 from [10]). After that we can use the algorithm of
Khachian from [11]."
Note that for the level logic predicate calculus sometimes there are
used infinity and minus infinity as logic values.
The last upper bounds were published in [12].
10. S.N. Chernikov, Linear inequalities (in Russian). Moscow, Science, 1968,
488.
11. L.G. Khachian, A polynomial algorithm in linear programming. // Dokl.
Akad.Nauk SSSR, 244, 1093-1096 (in Russian). English translation in
Soviet Math. Dokl. 20, 191-194.
12. N.K. Kossovski, Complexity of Rational Level Sublogics Decidability,
Abstracts of papers NSL'95. Second Workshop on Non-Standard Logics and
logical Aspects of Computer Science, Irkutsk, Russia, 1995, 46-47.