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

✍ Scribed by Nikolai Kossovski

• Publisher: Elsevier Science
• Year: 2001
• Tongue: English
• Weight: 70 KB
• Volume: 113
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(01)00057-4

✦ Synopsis

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 quantiÿer-free theory of ÿeld of rational numbers. Let Q0 be a subset of the set of all rational numbers which contains integers 1 and -1. Let Q0 be a set containing Q0 and closed by the functions of addition, subtraction and multiplication. For example Q0 coincides with Q0 if Q0 is the set of all binary rational numbers or the set of all decimal rational numbers. It is clear that Z ⊆ Q0 ⊆ 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 quantiÿer-free (universal or free-variable) negationless elementary theory of signature Q0; |Pol; 6 , where |Pol is the list of all polynomials with rational coe cients from Q0 in which exponent of the polynomials and rational coe cients are written in binary number system.

Theorem 1. Theory T is NP-hard and if Q0 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 Q0. The quantiÿer-free negationless theory of the ÿeld of rational numbers may be regarded as a base of constructive mathematics (Section Mathematical Logic and Foundations of Mathematics,