Computational complexity of quantifier-free negationless theory of field of rational numbers

• Published in: Annals of pure and applied logic 2001-12, Vol.113 (1), p.175-180
• Main Author: Kossovski, Nikolai
• Format: Article
• Language: English
• Subjects: Decidability complexity; Theory of binary rational numbers; Theory of rational numbers; Universal negationless theory
• ISSN: 0168-0072
• DOI: 10.1016/S0168-0072(01)00057-4

The following result is an approximation to the answer of the question of Kokorin (Logical Notebook, Unsolved Problems of Mathematics, Novosibirsk, 1986, 41pp; in Russian) about decidability of a quantifier-free theory of field of rational numbers. Let Q 0 be a subset of the set of all rational numbers which contains integers 1 and −1. Let Q 0 be a set containing Q 0 and closed by the functions of addition, subtraction and multiplication. For example Q 0 coincides with Q 0 if Q 0 is the set of all binary rational numbers or the set of all decimal rational numbers. It is clear that Z ⊆ Q 0 ⊆ Q , where Z is the set of all integers and Q is the set of all rational numbers. A negationless theory uses only conjunction and disjunction as logical connectives. Let T be a quantifier-free (universal or free-variable) negationless elementary theory of signature 〈 Q 0 ;| Pol,⩽〉 , where |Pol is the list of all polynomials with rational coefficients from Q 0 in which exponent of the polynomials and rational coefficients are written in binary number system. Theorem 1. Theory T is NP - hard and if Q 0 is everywhere dense then the theory T is decidable by an algorithm which belongs to EXPTIME. The set of all rational numbers or the set of all binary rational numbers may be taken instead of Q 0 . The quantifier-free negationless theory of the field of rational numbers may be regarded as a base of constructive mathematics (Section Mathematical Logic and Foundations of Mathematics, ICM, Warszawa, 1982, p. 21).