Real Closed Fields

Real Closed Fields#

The module logic1.theories.RCF implements the theory of Real Closed Fields based on the logic1.firstorder framework. Real Closed Fields are the first-order theory of the real numbers with ring arithmetic, equality, and order. This can be naturally axiomatized as follows:

  1. the axioms of ordered fields,

  2. every positive element has a square root,

  3. every polynomial of odd degree has a root.

Variables are elements of an infinite set RCF.VV, indexed by their name as a string.

>>> from logic1.theories.RCF import VV
>>> x = VV['x']
>>> isinstance(x, Variable)
True
>>> isinstance(x, Term)
True

Methods VV.get and VV.imp allow to retrieve several variables at once, given their names. Terms are built from variables and rational numbers using ring arithmetic. All terms are implicitly converted to polynomials with rational coefficients. We use sparse distributive representation and deglex monomial ordering.

>>> from logic1.theories.RCF import *
>>> from gmpy2 import mpq
>>> x, y = VV.get('x', 'y')
>>> (2 * x - 3 * y) ** 3
8*x**3 - 36*x**2*y + 54*x*y**2 - 27*y**3

Admissible Number types are int, fractions.Fraction, gmpy2.mpq, and float. Fractions are entered either as build-in fractions.Fraction or as GNU multi-precision rational numbers gmpy2.mpq, while float provides a convenient interface for external input with decimal numbers.

Attention

Python division of integers yields a float, which can cause precision issues:

>>> from logic1.theories.RCF import *
>>> x, = VV.get('x')
>>> x + 0.1
x + 3602879701896397/36028797018963968

Use GNU multi-precision rational numbers for exact arithmetic:

>>> from logic1.theories.RCF import *
>>> from gmpy2 import mpq
>>> x, = VV.get('x')
>>> x + mpq(1, 10)
x + 1/10

The module logic1.interactive.RCF provides a convenient interface for interactive use, e.g., pre-defining single letter variables.

Atoms are built from polynomials using equality, disequality, and order relations. Formulas are built from atoms using Boolean connectives and quantifiers. Real closed fields are complete, decidable, and admit quantifier elimination.

>>> from logic1.interactive.RCF import *
>>> a1 = -(1 - 3*r) * (a**2 + b**2) + 2*a*r
>>> a2 = -(2 - 3*r) * (a**2 + b**2) + 4*a*r - 2*a - r
>>> collins_johnson = Ex(r, And(0 < r, r < 1, a >= 1/2, b > 0, a1 < 0, a2 > 0))
>>> qe(collins_johnson)
 And(b > 0,
     2*a - 1 >= 0,
     3*a**4 + 6*a**2*b**2 + 3*b**4 + 7*a**3 + 7*a*b**2 + 3*a**2 - b**2 - a > 0,
     3*a**4 + 6*a**2*b**2 + 3*b**4 + 10*a**3 + 10*a*b**2 + 4*a**2 - 4*b**2 - 6*a + 1 > 0,
     9*a**6 + 27*a**4*b**2 + 27*a**2*b**4 + 9*b**6 + 30*a**5 + 60*a**3*b**2 + 30*a*b**4
        + 36*a**4 + 36*a**2*b**2 + 14*a**3 - 2*a*b**2 - 5*a**2 - b**2 < 0)

Numbers obtained from terms or formulas using theories.RCF operations are generally of type gmpy2.mpq.

>>> from logic1.interactive.RCF import *
>>> t = 0.5 * x + 2
>>> t.lc()
mpq(1,2)
>>> t.constant_coefficient()
mpq(2,1)