First-order Logic and Formulas#

First-order logic recursively builds terms from variables and a specified set of function symbols with specified arities, which includes constant symbols with arity zero. Next, atomic formulas are built from terms and a specified set of relation symbols with specified arities. Finally, first-order formulas formulas are recursively built from atomic formulas and a fixed set of logical operators.

Logic1 focuses on interpreted first-order logic, where the above-mentioned function and relation symbols have an implicit semantics, which is not explicitly expressed via axioms within the logical framework.

Terms#

Logic1 supports SymPy expressions as terms with SymPy symbols as variables. Find more details in the SymPy documentation. Get started with the Introductory Tutorial.

SymPy supports several ways to define Symbols and Symbolic Expressions. The most basic and flexible one is the use of the function sympy.core.symbol.symbols(). We give an example:

>>> import sympy
>>> x, y = sympy.symbols('x, y')
>>> isinstance(x, sympy.core.symbol.Symbol)
True
>>> x
x
>>> term = x**2 - 2*x*y + y**2
>>> isinstance(term, sympy.core.expr.Expr)
True
>>> term
x**2 - 2*x*y + y**2

Latin and Greek one-letter symbols can be conveniently imported from sympy.abc:

>>> from sympy.abc import x, epsilon
>>> (x + epsilon) ** 2
(epsilon + x)**2

Another approach uses sympy.core.sympify.sympify(). This function parses strings into SymPy expressions. Symbols newly introduced this way are not implicitly available as Python variables. However, one can generally use sympy.core.sympify.sympify(), since symbols with the same name are identical:

>>> import sympy
>>> s = sympy.sympify
>>> term = s('y + delta')
>>> term
delta + y
>>> y
Traceback (most recent call last):
...
NameError: name 'y' is not defined
>>> s('y')
y
>>> s('y') is term.args[1]
True

Atomic Formulas#

Logic1 does not use any relations from SymPy but implements its own relations. We distinguish between relation symbols, like \(\leq\), and atomic formulas built from relation symbols with a suitable number of argument terms, like \(x \leq x+1\).

Logic1 primarily aims at interpreted first-order logic. For many algorithms in this setting the choice of admissible relation symbols, and also of admissible function symbols, plays a crucial rule in the sense that slight variations of those choices lead to entirely different algorithmic approaches for the same problems. Examples for such algorithms are simplification, quantifier elimination, and decision procedures. The choice of admissible function and relation symbols takes place with the implementation of theories, which we discuss later on. It is also theories that fix a domain of computation and give function and relation symbol a semantics in that domain.

The module logic1.atomlib.sympy provides a library of classes for atomic formulas with SymPy terms. Theories can select a set classes from this collection, possibly modify via subclassing, and implement additional atomic formulas on their own. In particular, subclassing allows to restrict the set of admissible function symbols via argument checking in the constructors and initializers of the derived classes.

Equations and Inequalities#

Equations and inequalities are a popular kind of atomic formulas. They appear in many interesting theories including Ordered Sets, Presburger Arithmetic, and Real Closed Fields. The classes in the following table allow to realize equations and inequalities as their instances.

relation

arity

in words

class

\(=\)

2

equal

Eq

\(\neq\)

2

not equal

Ne

\(\geq\)

2

greater-equal

Ge

\(\leq\)

2

less-equal

Le

\(>\)

2

greater than

Gt

\(<\)

2

less than

Lt

We have a closer look at the class Lt. The other classes are similar. The following snippet is not complete and it contains attributes that are actually inherited from super classes. Compare the documentation of Lt in the API Reference.

class logic1.atomlib.sympy.Lt

Bases: logic1.atomlib.sympy.BinaryAtomicFormula

A class for atomic formulas with relation \(<\).

# Class data attributes:

func = Lt

The relation symbol of the atomic formula.

complement_func = Ge

The complement relation symbol of func.

converse_func = Gt

The converse relation symbol of func.

dual_func = Le

The dual relation symbol of func.

# Instance data attributes:

args: tuple

The tuple of arguments of func, which equals (lhs, rhs).

property lhs: sympy.core.expr.Expr

The left hand side term of the atomic formula, which is args[0].

property rhs: sympy.core.expr.Expr

The right hand side term of the atomic formula, which is args[1].

The attributes func, lhs, and rhs give access to the mathematical components of an atomic formula:

>>> from logic1.atomlib.sympy import *
>>> atom = Lt(0, 1)
>>> atom
Lt(0, 1)
>>> atom.func, atom.lhs, atom.rhs
(<class 'logic1.atomlib.sympy.Lt'>, 1, 0)

Since func is the class Lt itself, it is callable as a constructor, and we have everything together to decompose and construct atomic formulas:

>>> new_atom = atom.func(atom.lhs, atom.rhs)
>>> new_atom
Lt(0, 1)
>>> new_atom == atom
True
>>> new_atom is atom
False
>> Gt(2, new_atom.rhs)
Gt(2, 1)

More generally, one can use the argument tuple args instead of lhs and rhs:

Important

If f is any of our atomic formulas, then f == f.func(*f.args).

The same holds for SymPy expressions, which is discussed in the section Recursing through an Expression Tree of the SymPy documentation. This explains our generic attribute name func when actually referring to relations. The attributes func and args will be available throughout Logic1 also for non-atomic formulas.

The constructors and initializers of our classes here check the validity of their arguments and raise ValueError with additional information when problems are detected:

>>> oops = Lt('1', 0)
Traceback (most recent call last):
...
ValueError: '1' is not a Term

It remains to clarify the values of complement_func, converse_func, and dual_func in general.

Mathematical definitions

Let \(\varrho \subseteq A^n\) be an \(n\)-ary relation. Then the complement relation is defined as

\[\overline{\varrho} = A^n \setminus \varrho.\]

It follows that \(\overline{\varrho}(a_1, \dots, a_n)\) is equivalent to \(\lnot \varrho(a_1, \dots, a_n)\), which is an important property for Logic1.

If \(\varrho\) is binary, then the converse relation is defined as

\[\varrho^{-1} = \{\,(y, x) \in A^2 \mid (x, y) \in \varrho\,\}.\]

In other words, the converse swaps sides. It is the inverse with respect to composition, i.e., \(\varrho \circ \varrho^{-1} = \varrho^{-1} \circ \varrho = \Delta_A\). The diagonal \(\Delta_A = \{\,(x, y) \in A^2 \mid x = y\,\}\) is equality on \(A\).

Finally, the dual relation is defined as

\[\varrho^d = \overline{\varrho^{-1}},\]

which generally equals \((\overline{\varrho})^{-1}\). For our relations here, dualization amounts to turning strict relations into weak relations, and vice versa.

Each of these transformations of relations is involutive in the sense that \(\overline{\overline{\varrho}} = (\varrho^{-1})^{-1} = (\varrho^d)^d = \varrho\).

func

complement_func

converse_func

dual_func

Eq

Ne

Eq

Ne

Ne

Eq

Ne

Eq

Ge

Lt

Le

Gt

Le

Gt

Ge

Lt

Gt

Le

Lt

Ge

Lt

Ge

Gt

Le

Of course, complement_func, converse_func, and dual_func work as constructors in the same way as func:

>>> atom
Lt(1, 0)
>>> atom.dual_func(atom.lhs, atom.rhs)
Le(1, 0)

Note

Recall that we are working at a syntactic level here, where domains and semantics of the relations are not specified yet. The concrete specifications of complement, converse, and dual relation symbols aims to have this set of relation symbols used in theories that correspond to it.

As a counterexample consider a theory of partially ordered sets, in which all of our relation symbols are meaningful. However, with a partial order, \(\geq\) is not the complement relation of \(<\). Consequently, such a theory would find another suitable set of relations somewhere, or implement it itself.

Cardinality Constraints#

Cardinality constraints are constant atomic formulas, built from relation symbols with arity 0. A cardinality constraint holds in a given theory if the cardinality of the corresponding domain satisfies the requirements imposed by the constraint. For instance, a constraint \(C_2\) can be used to state that the domain has at least two elements. It holds in the field \(\mathbb{R}\) but not in the field \(\mathbb{Z}/3\). A typical use case is the theory of Sets, which requires infinitely many constant relation symbols \(C_n\) for \(n \in \mathbb{N}\) in order to admit quantifier elimination.

The classes in the following table allow to realize cardinality constraints as their instances.

relation

m-arity

in words

class

p-arity

\(C_n\)

0

cardinality at least \(n\)

C

1

\(\overline{C}_n\)

0

cardinality less than \(n\)

C_

1
class logic1.atomlib.sympy.C

Bases: logic1.atomlib.sympy.Cardinality

A class for atomic formulas with relation \(C_n\) for \(n \in \mathbb{N} \cup \{\infty\}\).

# Class data attributes:

func = C

The relation symbol of the atomic formula.

complement_func = C_

The complement relation symbol of func.

# Instance data attributes:

args: tuple

The tuple of arguments of the constructor func, which equals (index,).

property index: int | sympy.core.numbers.Infinity

The index \(n\) of :math:C_n`, which is args [0].

Infinity \(\infty\) denotes the cardinal \(\aleph_0\). It is available as

logic1.atomlib.sympy.oo = sympy.oo

Note that we are dealing with two different notions of arity here:

m-arity:

From a mathematical viewpoint we have two families \(\{C_n\}_{n \in \mathbb{N} \cup \{\infty\}}\) and \(\{\overline{C}_n\}_{n \in \mathbb{N} \cup \{\infty\}}\) of relations, where each relation has aritiy 0.

p-arity:

From a Python viewpoint we have two classes C and C_. Each class has an instance data attribute n, which is a non-negative integer or oo. There is a corresponding constructor of arity 1.

We will encounter a similar situation with quantifiers in the next section on First-order Formulas, where both the m-arity and the p-arity will be positive.

Cardinality Constraints of the same class and with the same index are identical:

>>> from logic1.atomlib.sympy import C, oo
>>> a1 = C(0)
>>> a2 = C(0)
>>> a3 = C(oo)
>>> a1 is a2
True
>>> a1 == a3
False

First-order Formulas#

the following logical operators:

operator

m-arity

in words

class

p-arity

short

\(\bot\)

0

false

_F

0

F

\(\top\)

0

true

_T

0

T

\(\lnot\)

1

not

Not

1

~

\(\land\)

*

and

And

*

&

\(\lor\)

*

or

Or

*

|

\(\longrightarrow\)

2

implies

Implies

2

>>

\(\longleftrightarrow\)

2

equivalent

Equivalent

2

\(\exists x\)

1

exists

Ex

2

\(\forall x\)

1

for all

All

2