Computational complexity of quantifier-free negationless theory of field of rational numbers Original Research Article

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 View the MathML source be a subset of the set of all rational numbers which contains integers 1 and −1. Let View the MathML source be a set containing View the MathML source and closed by the functions of addition, subtraction and multiplication. For example View the MathML source coincides with View the MathML source if View the MathML source is the set of all binary rational numbers or the set of all decimal rational numbers. It is clear that View the MathML source, where View the MathML source is the set of all integers and View the MathML source 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 View the MathML source, where |Pol is the list of all polynomials with rational coefficients from View the MathML source in which exponent of the polynomials and rational coefficients are written in binary number system.