Variables and Atoms

Sets

Variables and Atoms#

class logic1.theories.Sets.atomic.VariableSet[source]#

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 parent class:

__getitem__(index: str) → Variable[source]#

Implements abstract method firstorder.atomic.VariableSet.__getitem__().

fresh(suffix: str = '') → Variable[source]#

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[source]#
abstractmethod push() → None[source]#

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

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

The unique instance of VariableSet.

class logic1.theories.Sets.atomic.Variable[source]#

Bases: Variable[Variable, Never, str]

==, !=
__eq__(other: Variable) → Eq[source]#
__ne__(other: Variable) → Ne[source]#

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

as_latex() → str[source]#

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

fresh() → Variable[source]#

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

sort_key() → str[source]#

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

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

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][source]#

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

class logic1.theories.Sets.atomic.AtomicFormula[source]#

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

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

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

__str__() → str[source]#

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

as_latex() → str[source]#

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

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

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

classmethod complement() → type[AtomicFormula][source]#

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][source]#

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][source]#

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

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

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

class logic1.theories.Sets.atomic.Eq[source]#
class logic1.theories.Sets.atomic.Ne[source]#

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[source]#
class logic1.theories.Sets.atomic.C_[source]#

Cardinality constraints. From a mathematical perspective, the instances are constant relation symbols with an index, which is either a positive integer or the 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

Contents