Sets with Cardinality Constraints

Sets with Cardinality Constraints#

The module logic1.theories.Sets implements the theory of Sets with Cardinality Constraints, based on the logic1.firstorder framework. The name “Sets” emphasizes that the models considered are plain sets without any constants or functions. We have equality and disequality, where the former is generally not considered a formal relation in interpreted first-order logic, and the latter can be considered a shorthand for the logical negation of equality.

The only formal structure actually available is an infinite set of constant relations \(\{C_n\}_{n \in \mathbb{N} \cup \{\infty\}}\), \(\{\overline{C_n}\}_{n \in \mathbb{N} \cup \{\infty\}}\), which are defined as follows:

  1. \(C_n\) holds if and only if the cardinality of the universe is at least \(n\), for \(n \in \mathbb{N}\);

  2. \(C_\infty\) holds if and only if the universe is infinite;

  3. \(\overline{C_n}\) holds if and only if \(C_n\) does not hold, for \(n \in \mathbb{N} \cup \{\infty\}\).

Variables are elements of an infinite set Sets.VV, indexed by their name as a string. Methods VV.get and VV.imp allow to retrieve several variables at once, given their names.

>>> from logic1.theories.Sets import VV
>>> x = VV['x']
>>> type(x)
<class 'logic1.theories.Sets.atomic.Variable'>

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

>>> from logic1.interactive.Sets import *
>>> a
a
>>> type(a)
<class 'logic1.theories.Sets.atomic.Variable'>

In the absence of constants and functions, all terms in this theory are variables, and there is no explicit class for terms.

Atoms are built from Variables using equality, disequality, and cardinality constraints.

>>> from logic1.theories.Sets import *
>>> x, y, z = VV.get('x', 'y' , 'z')
>>> x == y
x == y
>>> y != z
y != z
>>> C(2)
C(2)
>>> C_(99)
C_(99)

Attention

The numbers 2 and 99 are not terms but indices that are used here for denoting two out of the infinitely many existing cardinality constraints, namely \(C_2\) and \(\overline{C_{99}}\). Both these constraints are relation symbols with arity zero.

Formulas are built from atoms using Boolean connectives and quantifiers. Sets with cardinality constraints are decidable but not complete. They admit quantifier elimination.

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> qe(Ex([x, y, z], And(x == y, y != z)))
C(2)