First-order Framework

First-order Framework#

Implementation of first-order formulas over arbitrary signatures and theories.

Throughout this documentation we use the term theory to refer to a choice of function and relation symbols along with their arities (signature) plus a choice of a semantics of those symbols.

An abstract base class Formula implements representations of and methods on first-order formulas recursively built using first-order operators:

  1. Boolean operators:

    1. Truth values \(\top\) and \(\bot\)

    2. Negation \(\lnot\)

    3. Conjunction \(\land\) and discjunction \(\lor\)

    4. Implication \(\longrightarrow\)

    5. Bi-implication (syntactic equivalence) \(\longleftrightarrow\)

  2. Quantifiers \(\exists x\) and \(\forall x\), where \(x\) is a variable.

As an abstract base class, Formula cannot be instantiated. Nevertheless, it implements a number of properties and methods on first-order formulas. Those properties and methods are typically syntactic in the sense that they do not need to know the semantics of the underlying theories.

Boolean operators are implemented as classes derived from another abstract class BooleanFormula which is, in turn, derived from Formula. Operators are mapped to classes as follows:

\(\top\)

\(\bot\)

\(\lnot\)

\(\land\)

\(\lor\)

\(\longrightarrow\)

\(\longleftrightarrow\)

_T

_F

Not

And

Or

Implies

Equivalent

The truth values \(\top\) and \(\bot\) are operators of arity 0. As such, they are implemented as singleton classes _T and _F with unique instances T and F, respectively.

>>> T is _T()
True

For details on the arities of the other Boolean operators see the documentation of the corresponding classes. On these grounds we can construct formulas based on truth values as follows:

>>> And(Implies(F, T), Or(T, Not(T)))
And(Implies(F, T), Or(T, Not(T)))

More interesting formulas require atomic formulas as another basis of the recursive construction. This is implemented via another abstract subclass AtomicFormula of Formula, which provides an interface to various theories via further subclassing. For some of its methods, AtomicFormula already provides implementations, which delegate theory-specific parts to an abstract class Term for argument terms of atomic formulas.

We give an example using the theory RCF of Real Closed Fields, which is implemented not in logic1.firstorder but in logic1.theories.RCF. RCF is the first-order theory of the real numbers using the signature of ordered rings:

>>> from logic1.theories import RCF
>>> # Assign RCF variables to Python identifiers:
>>> a, b, x = RCF.VV.get('a', 'b', 'x')
>>> # Build formula with first-order operators + RCF variables, functions, relations:
>>> And(x >= 0, a*x + b == 0)
And(x >= 0, a*x + b == 0)

Having learned about variables, we can finally discuss first-order quantifiers and corresponding quantified formulas. Quantifiers are implemented as classes derived from another abstract class QuantifiedFormula which is, in turn, derived from Formula. Quantifiers are mapped to classes as follows:

\(\exists\)

\(\forall\)

Ex

All

For details on the arguments of quantifiers see the documentation of the corresponding classes. Here is an example:

>>> from logic1.theories import RCF
>>> a, b, x = RCF.VV.get('a', 'b', 'x')
>>> f = Ex(x, And(x >= 0, a*x + b == 0))
>>> f
Ex(x, And(x >= 0, a*x + b == 0))

Implementations of theories contribute semantic-aware methods and functions on first-order formulas. For instance, quantifier elimination (QE) computes equivalent formulas that do not contain quantifiers anymore:

>>> RCF.qe(f)
Or(And(b == 0, a == 0), And(a != 0, a*b <= 0))

The following class diagram summarizes the inheritance hierarchy.