Sets with Cardinality Constraints

Variables and Atoms

There is an infinite set Sets.VV of all Sets variables, which is an instance of the class VariableSet. The variables obtained from VV are instances of the class Variable. There are no composite terms in this theory; in other words, every term is a variable.

There is a class AtomicFormula with subclasses Eq, Ne, C, C_. Atoms are obtained as instances of these subclasses, using the class names as constructors. For equations and diseqalities, one can alternatively use the corresponding operators == and != overloaded in the class Variable. C and C_ accept positive numbers from int and oo from float as indices.

Some examples can be found on the landing page of this section.

The Set of All Variables

class logic1.theories.Sets.atomic.VariableSet

Bases: VariableSet[Variable]

The infinite set of all variables belonging to the theory of Sets. Variables are uniquely identified by their name, which is a str. This class is a singleton, whose single instance is assigned to VV.

See also

Final methods inherited from the parent class:

• firstorder.term.VariableSet.get()

  – obtain several variables simultaneously

• firstorder.term.VariableSet.imp()

  – import variables into global namespace

property stack: list[set[str]]

The class internally keeps track of variables already used. This is relevant when creating unused variables via fresh(). The stack can hold such internal states.

See also

• push() – push information to stack and reset

• pop() – restore information from stack

__getitem__(index: str) → Variable

Return the variable with the name index. Implements abstract method firstorder.term.VariableSet.__getitem__().

>>> from logic1.theories.Sets import VV
>>> VV['x']
x

fresh(suffix: str = '') → Variable

Return a fresh variable, by default from the sequence G0001, G0002, …, G9999, G10000, … This naming convention is inspired by Lisp’s gensym(). If the optional argument suffix is specified, the sequence G0001<suffix>, G0002<suffix>, … is used instead.

abstractmethod pop() → None

abstractmethod push() → None

Implement abstract methods logic1.firstorder.term.VariableSet.pop() and logic1.firstorder.term.VariableSet.push().

logic1.theories.Sets.atomic.VV = VariableSet()

The unique instance of VariableSet. This is a singleton.

Variables

class logic1.theories.Sets.atomic.Variable

Bases: Variable[Variable, Never, str]

==, !=

__eq__(other: Variable) → Eq

__ne__(other: Variable) → Ne

Construction of instances of Eq and Ne is available via these overloaded operators.

as_latex() → str

LaTeX representation as a string. Implements the abstract method firstorder.term.Term.as_latex().

fresh() → Variable

Returns a variable that has not been used so far. Implements abstract method firstorder.term.Variable.fresh().

sort_key() → str

A sort key suitable for ordering instances of this class. Implements the abstract method firstorder.term.Term.sort_key().

subs(d: dict[Variable, Variable]) → Variable

Simultaneous substitution of variables for variables.

>>> from logic1.theories.Sets import VV
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = x
>>> f.subs({x: y, y: z})
y

vars() → Iterator[Variable]

An iterator that yields this variable. Implements the abstract method firstorder.term.Term.vars().

Atoms

class logic1.theories.Sets.atomic.AtomicFormula

Bases: AtomicFormula[AtomicFormula, Variable, Variable, Never]

__le__(other: Formula[AtomicFormula, Variable, Variable, Never]) → bool

Returns True if this atomic formula should be sorted before or is equal to other. Implements abstract method firstorder.atomic.AtomicFormula.__le__().

__str__() → str

String representation of this atomic formula. Implements the abstract method firstorder.atomic.AtomicFormula.__str__().

as_latex() → str

Latex representation as a string. Implements the abstract method firstorder.atomic.AtomicFormula.as_latex().

bvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Iterate over occurrences of variables that are elements of quantified. Implements the abstract method firstorder.atomic.AtomicFormula.bvars().

classmethod complement() → type[AtomicFormula]

Complement relation. Implements the abstract method firstorder.atomic.AtomicFormula.complement().

See also

Inherited method firstorder.atomic.AtomicFormula.to_complement()

fvars(quantified: frozenset[Variable] = frozenset({})) → Iterator[Variable]

Iterate over occurrences of variables that are not elements of quantified. Implements the abstract method firstorder.atomic.AtomicFormula.fvars().

simplify() → Formula[AtomicFormula, Variable, Variable, Never]

Fast basic simplification. The result is equivalent to self. Implements the abstract method firstorder.atomic.AtomicFormula.simplify().

subs(d: dict[Variable, Variable]) → Self

Simultaneous substitution of variables for variables. Implements the abstract method firstorder.atomic.AtomicFormula.subs().

class logic1.theories.Sets.atomic.Eq

class logic1.theories.Sets.atomic.Ne

Bases: AtomicFormula

Equations and inequalities between variables.

property lhs: Variable

property rhs: Variable

The left hand side variable and the right hand side variable of an equation or inequation, respectively.

logic1.theories.Sets.atomic.oo = inf

A symbolic name for the float('inf') as an Index.

logic1.theories.Sets.atomic.Index: TypeAlias = int | float

An index, which is either a positive integer or the float('inf'), which is represented by oo.

class logic1.theories.Sets.atomic.C

class logic1.theories.Sets.atomic.C_

Cardinality constraints. From a mathematical perspective, the instances are constant relation symbols with an index, which is either a positive integer or float('inf'), represented as oo. C(n) holds iff there are at least n different elements in the universe. This is not a statement about the index n but about a range of models where this constant relation holds.

In the following example, f states that there should be at least 2 elements but not 3 elements or more:

>>> from logic1.firstorder import *
>>> from logic1.theories.Sets import *
>>> x, y, z = VV.get('x', 'y', 'z')
>>> f = Ex([x, y], x != y) & All([x, y, z], Or(x == y, y == z, z == x))
>>> qe(f)  # quantifier elimination:
And(C(2), C_(3))

The class C_ is dual to C; more precisely, for every index n, we have that C_(n) is the dual relation of C(n), and vice versa.

The class constructors take care that instances with equal indices are identical:

>>> C(1) is C(1)
True
>>> C(1) == C(2)
False

property index: Index

The index of the constant relation symbol.