pylogic.structures package

Subpackages

Submodules

pylogic.structures.class_ module

pylogic.structures.class_.Class(n: int, *args, **kwargs) → Collection[Class[int]][source]
pylogic.structures.class_.class_(n: Literal[0]) → type[Set][source]
pylogic.structures.class_.class_(n: Literal[1]) → Collection[Class[Literal[1]]]
pylogic.structures.class_.class_(n: Literal[2]) → Collection[Class[Literal[2]]]
pylogic.structures.class_.class_(n: Literal[3]) → Collection[Class[Literal[3]]]
pylogic.structures.class_.class_(n: Literal[4]) → Collection[Class[Literal[4]]]
pylogic.structures.class_.class_(n: Literal[5]) → Collection[Class[Literal[5]]]
pylogic.structures.class_.class_(n: Literal[6]) → Collection[Class[Literal[6]]]
pylogic.structures.class_.class_(n: Literal[7]) → Collection[Class[Literal[7]]]
pylogic.structures.class_.class_(n: Literal[8]) → Collection[Class[Literal[8]]]
pylogic.structures.class_.class_(n: Literal[9]) → Collection[Class[Literal[9]]]
pylogic.structures.class_.class_(n: Literal[10]) → Collection[Class[Literal[10]]]
pylogic.structures.class_.class_(n: int) → Collection[Class[int]]

Create the python class Collection{n} whose instances are collections that can contain only all collections of type Collection{n-1}. Collection0 is the same as Set. So, Collection1() can use restricted comprehension over all Set instances, Collection2() can use restricted comprehension over Collection1 instances, etc.

Note that a Collection{n} instance cannot contain a Collection{n-2} or lower instance.

pylogic.structures.class_.class_n_hash(self) → int[source]
pylogic.structures.class_.class_n_init(self, name: str, elements: Iterable[Any] | None = None, containment_function: Callable[[Any], bool] | None = None, predicate: Callable[[Any], Proposition] | None = None)[source]
pylogic.structures.class_.class_n_repr(self) → str[source]
pylogic.structures.class_.containment_function(self, x: Any) → bool[source]
pylogic.structures.class_.contains(self, other: Any, is_assumption: bool = False, **kwargs) → IsContainedIn[source]
pylogic.structures.class_.copy(self)[source]
pylogic.structures.class_.deepcopy(self)[source]
pylogic.structures.class_.equals(self, other: Any, **kwargs) → Equals[source]
pylogic.structures.class_.illegal_occur_check(self, containment_function: Callable[[Any], bool] | None = None, predicate: Callable[[Any], Proposition] | None = None) → Literal[False][source]

Perform the illegal occurrence check on the containment function and predicate. Returns False if no illegal occurrences are found. Raises a ValueError if an illegal occurrence is found.

https://en.wikipedia.org/wiki/Axiom_schema_of_specification#In_Quine%27s_New_Foundations We follow this New Foundations specification where we can have a set of all sets, but the argument of the containment function or predicate cannot appear on both sides of an IsContainedIn statement, avoiding Russell’s paradox.

Note that we can still have sets that contain themselves, and (obviously) sets that do not contain themselves.

We check for this in a Set or Collection{n} instance S by checking if S.containment_function(S) recurses forever or if a proposition of the form Expr(…S…) in Expr(…S…) appears in S.predicate(S) If an (AttributeError, TypeError, ValueError) occurs during these checks, we assume the functions are valid, since it means S does not match an implicit pattern.

pylogic.structures.class_.illegal_occur_check_pred(self, predicate_of_self: Proposition) → bool[source]
pylogic.structures.class_.predicate(self, x: Any) → Proposition[source]
pylogic.structures.class_.to_sympy(self)[source]

pylogic.structures.collection module

class pylogic.structures.collection.Collection(name, bases, dct)[source]

Bases: type, Generic[N]

Python metaclass for all collections/classes Set, Class{n}.

pylogic.structures.ordered_set module

class pylogic.structures.ordered_set.OrderedSet[source]
class pylogic.structures.ordered_set.OrderedSet(*args, **kwargs)

Bases: Set

A set with a total order (such as <=) and a corresponding strict total order (such as <).

add_to_both_sides_of_inequality: ForallInSet[ForallInSet[ForallInSet[Implies[TotalOrder, TotalOrder]]]]
order_definition: ForallInSet[ForallInSet[Iff[TotalOrder, Or[StrictTotalOrder, Equals]]]]
order_is_antisymmetric: ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], Equals]]]
order_is_reflexive: ForallInSet[TotalOrder]
order_is_strongly_connected: ForallInSet[ForallInSet[Or[TotalOrder, TotalOrder]]]
order_is_transitive: ForallInSet[ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], TotalOrder]]]]
product_of_nonnegatives_is_nonnegative: ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], TotalOrder]]]
classmethod property_add_to_both_sides_of_inequality(set_: Set, total_order: TotalOrderOp, plus_operation: SpecialInfix[Term, Term, Expr, Expr]) → ForallInSet[ForallInSet[ForallInSet[Implies[TotalOrder, TotalOrder]]]][source]
classmethod property_order_definition(set_: Set, total_order: Any, strict_total_order: Any) → ForallInSet[ForallInSet[Iff[TotalOrder, Or[StrictTotalOrder, Equals]]]][source]
classmethod property_order_is_antisymmetric(set_: Set, total_order: Any) → ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], Equals]]][source]
classmethod property_order_is_reflexive(set_: Set, total_order: Any) → ForallInSet[TotalOrder][source]
classmethod property_order_is_strongly_connected(set_: Set, total_order: Any) → ForallInSet[ForallInSet[Or[TotalOrder, TotalOrder]]][source]
classmethod property_order_is_transitive(set_: Set, total_order: Any) → ForallInSet[ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], TotalOrder]]]][source]
classmethod property_product_of_nonnegatives_is_nonnegative(set_: Set, total_order: TotalOrderOp, times_operation: SpecialInfix[Term, Term, Expr, Expr]) → ForallInSet[ForallInSet[Implies[And[TotalOrder, TotalOrder], TotalOrder]]][source]

Assuming the total order is a <= b, return 0 <= a and 0 <= b implies 0 <= a*b

classmethod property_strict_order_definition(set_: Set, total_order: Any, strict_total_order: Any) → ForallInSet[ForallInSet[Iff[StrictTotalOrder, And[TotalOrder, Not[Equals]]]]][source]
classmethod property_strict_order_is_asymmetric(set_: Set, strict_total_order: Any) → ForallInSet[ForallInSet[Implies[StrictTotalOrder, Not[StrictTotalOrder]]]][source]
classmethod property_strict_order_is_connected(set_: Set, strict_total_order: Any) → ForallInSet[ForallInSet[Implies[Not[Equals], Or[StrictTotalOrder, StrictTotalOrder]]]][source]
classmethod property_strict_order_is_irreflexive(set_: Set, strict_total_order: Any) → ForallInSet[Not[StrictTotalOrder]][source]
classmethod property_strict_order_is_transitive(set_: Set, strict_total_order: Any) → ForallInSet[ForallInSet[ForallInSet[Implies[And[StrictTotalOrder, StrictTotalOrder], StrictTotalOrder]]]][source]
strict_order_definition: ForallInSet[ForallInSet[Iff[StrictTotalOrder, And[TotalOrder, Not[Equals]]]]]
strict_order_is_asymmetric: ForallInSet[ForallInSet[Implies[StrictTotalOrder, Not[StrictTotalOrder]]]]
strict_order_is_connected: ForallInSet[ForallInSet[Implies[Not[Equals], Or[StrictTotalOrder, StrictTotalOrder]]]]
strict_order_is_irreflexive: ForallInSet[Not[StrictTotalOrder]]
strict_order_is_transitive: ForallInSet[ForallInSet[ForallInSet[Implies[And[StrictTotalOrder, StrictTotalOrder], StrictTotalOrder]]]]
strict_total_order: Any
total_order: Any

pylogic.structures.sequence module

class pylogic.structures.sequence.FiniteSequence(name: str, length: Any, initial_terms: Sequence[T] | None = None, **kwargs)[source]

Bases: Sequence[T]

A finite sequence is a sequence with a finite number of terms.

to_sympy() → SeqBase | SeqPer[source]
class pylogic.structures.sequence.Pair(name: str, first: T, second: T)[source]

Bases: FiniteSequence[T]

A pair is a finite sequence with two terms.

class pylogic.structures.sequence.PeriodicSequence(name: str, initial_terms: TSequence[T] | None = None, period: int | Constant[int] | T | None = None, **kwargs)[source]

Bases: Sequence[T]

A periodic sequence is an infinite sequence that repeats after a certain number of terms.

to_sympy() → SeqBase | SeqPer[source]
class pylogic.structures.sequence.Sequence(name: str, initial_terms: TSequence[T] | None = None, nth_term: Callable[[int], T] | None = None, predicate: Callable[[Term], Proposition] | None = None, real: bool | None = None, **kwargs)[source]

Bases: Generic[T]

A sequence is a countably infinite or finite ordered list of elements.

Parameters:

  • predicate (n) – Callable[[Term], Proposition] | None

  • proposition. (A function that receives a natural number and returns a)

  • proposition (sequence.predicate() actually receives a natural number n and returns a)

  • term. (about the corresponding sequence)

  • n (So `forall) –

  • predicate

  • sequence (Note that if a term x is the nth term of the)

  • `predicate (then) –

  • True (is)

  • x (but if some predicate is True for)

  • that (it doesn't necessarily mean)

  • sequence. (x is in the)

contains(other: Term, is_assumption: bool = False, **kwargs) → IsContainedIn[Term, SeqSet][source]

elementhood

define_predicate(predicate: Callable[[Term], Proposition], predicate_uses_self: bool = False) → None[source]

Define the predicate that the sequence satisfies. :param predicate: Callable[[Term], Proposition]

A function that receives a natural number and returns a proposition. sequence.predicate() actually receives a natural number n and returns a proposition about the corresponding sequence term. So for all n, predicate(n) should be True.

Parameters:

predicate_uses_self –

bool

Whether the predicate uses self (imported from pylogic.sequence) as opposed to the reference of the actual sequence. If define_predicate is being called, the sequence is already initialized and can be referenced directly in the predicate. In this case, predicate_uses_self should be False. If self is used in the predicate, predicate_uses_self should be True. This facilitates replacing self with the actual sequence instance when the predicate is called.

equals(other: Term, **kwargs) → Equals[source]
evaluate(**kwargs) → Self[source]
is_atomic = True
property is_even: bool | None
property is_finite: bool | None
is_in(set_: Set | Variable) → IsContainedIn[source]

Return the proposition self in set_.

property is_integer: bool | None
property is_list: bool | None
property is_natural: bool | None
property is_negative: bool | None
property is_nonnegative: bool | None
property is_nonpositive: bool | None
property is_nonzero: bool | None
is_not_in(set_: Set | Variable, **kwargs) → Not[IsContainedIn][source]

Return the proposition self not in set_.

property is_odd: bool | None
property is_positive: bool | None
property is_rational: bool | None
property is_real: bool | None
property is_sequence: Literal[True]
property is_set: bool | None
property is_zero: bool | None
predicate(expr: Term) → Proposition[source]

Return the proposition that the term satisfies the predicate.

expr: Term

an expression that corresponds to a natural number.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Any[source]
to_sympy() → SeqBase | SeqFormula[source]
class pylogic.structures.sequence.Triple(name: str, first: T, second: T, third: T)[source]

Bases: FiniteSequence[T]

A triple is a finite sequence with three terms.

pylogic.structures.sequence.sequences(name: str, **kwargs) → Sequence[source]
pylogic.structures.sequence.sequences(*names: str, **kwargs) → tuple[Sequence, ...]

Create one or more sequences.

pylogic.structures.set_ module

class pylogic.structures.set_.CartesPower[source]
class pylogic.structures.set_.CartesPower(*args, **kwargs)

Bases: Set

Represents the cartesian power of a set, such as R^2 = R x R.

is_atomic = False

UniversalSet * A = UniversalSet EmptySet * A = EmptySet SingletonEmpty * A = A

class pylogic.structures.set_.CartesProduct[source]
class pylogic.structures.set_.CartesProduct(*args, **kwargs)

Bases: Set

Represents the cartesian product of finitely many or countably-infinitely many sets.

is_atomic = False
class pylogic.structures.set_.Complement[source]
class pylogic.structures.set_.Complement(*args, **kwargs)

Bases: Set

Represents the complement of a set.

class pylogic.structures.set_.Difference[source]
class pylogic.structures.set_.Difference(*args, **kwargs)

Bases: Set

Represents the difference of two sets A B = A n B^c.

is_atomic = False
to_intersection() → FiniteIntersection[source]
class pylogic.structures.set_.FiniteCartesProduct[source]
class pylogic.structures.set_.FiniteCartesProduct(sets: tuple[Set | Variable, ...] | list[Set | Variable], name: str | None = None)

Bases: CartesProduct

Represents a cartesian product of a specified number of sets.

is_atomic = False
set_sequence: Sequence[Set | Variable]
class pylogic.structures.set_.FiniteIntersection[source]
class pylogic.structures.set_.FiniteIntersection(sets: Iterable[Set | Variable], name: str | None = None)

Bases: Intersection

Represents an intersection of a specified number of sets.

is_atomic = False
class pylogic.structures.set_.FiniteSet[source]
class pylogic.structures.set_.FiniteSet(*args, **kwargs)

Bases: Set

class pylogic.structures.set_.FiniteUnion[source]
class pylogic.structures.set_.FiniteUnion(sets: Iterable[Set | Variable], name: str | None = None)

Bases: Union

Represents a union of a specified number of sets.

is_atomic = False
class pylogic.structures.set_.Intersection[source]
class pylogic.structures.set_.Intersection(*args, **kwargs)

Bases: Set

Represents the intersection of finitely many or countably-infinitely many sets.

is_atomic = False
class pylogic.structures.set_.SeqSet[source]
class pylogic.structures.set_.SeqSet(*args, **kwargs)

Bases: Set

Represents a set containing all elements of a sequence.

is_atomic = False
property is_even: bool | None
property is_finite: bool | None
property is_integer: bool | None
property is_list: bool | None
property is_natural: bool | None
property is_negative: bool | None
property is_nonnegative: bool | None
property is_nonpositive: bool | None
property is_nonzero: bool | None
property is_odd: bool | None
property is_positive: bool | None
property is_rational: bool | None
property is_real: bool | None
property is_sequence: bool | None
property is_zero: bool | None
replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Any[source]
class pylogic.structures.set_.Set[source]
class pylogic.structures.set_.Set(*args, **kwargs)

Bases: object

A set S is a collection of elements. This is equivalent to Class0. In pylogic/structures/class_.py, we define Sets, the Class1 of all sets.

You can prove the proposition x in S either using the containment_function, i.e. S.containment_function(x) == True using S.contains(x).by_inspection(), or by supplying a proven proposition p of S.predicate(x) to S.contains(x).by_predicate(p).

S is the set of all x such that S.predicate(x) is a true proposition, and vice-versa. That is, S.predicate(x) <-> x in S.

Set() gives the empty set.

containment_function(x: Any) → bool[source]
contains(other: T, is_assumption: bool = False, **kwargs) → IsContainedIn[T, Self][source]
copy() → Self[source]
countable(is_assumption: bool = False, **kwargs) → Exists[source]
deepcopy() → Self[source]
dummy_eq(other: object) → bool[source]
equals(other: Term, **kwargs) → Equals[source]
eval_same(other: object) → bool[source]
evaluate(**kwargs) → Set[source]
illegal_occur_check(containment_function: Callable[[Term], bool] | None = None, predicate: Callable[[Term], Proposition] | None = None) → Literal[False][source]

Perform the illegal occurrence check on the containment function and predicate. Returns False if no illegal occurrences are found. Raises a ValueError if an illegal occurrence is found.

https://en.wikipedia.org/wiki/Axiom_schema_of_specification#In_Quine%27s_New_Foundations We follow this New Foundations specification where we can have a set of all sets, but the argument of the containment function or predicate cannot appear on both sides of an IsContainedIn statement, avoiding Russell’s paradox.

Note that we can still have sets that contain themselves, and (obviously) sets that do not contain themselves.

We check for this in a Set or Class{n} instance S by checking if S.containment_function(S) recurses forever or if a proposition of the form Expr(…S…) in Expr(…S…) appears in S.predicate(S) If an (AttributeError, TypeError, ValueError) occurs during these checks, we assume the functions are valid, since it means S does not match an implicit pattern.

illegal_occur_check_pred(predicate_of_self: Proposition) → bool[source]
is_atomic = True
property is_even: bool | None
property is_finite: bool | None
property is_integer: bool | None
property is_list: bool | None
property is_natural: bool | None
property is_negative: bool | None
property is_nonnegative: bool | None
property is_nonpositive: bool | None
property is_nonzero: bool | None
property is_odd: bool | None
property is_positive: bool | None
property is_rational: bool | None
property is_real: bool | None
property is_sequence: bool | None
property is_set: Literal[True]
is_subset_of(other: Set | Variable | SequenceTerm, **kwargs) → IsSubsetOf[source]
property is_zero: bool | None
kwargs = {'containment_function': '_containment_function', 'elements': 'elements', 'finite': '_is_finite', 'illegal_occur_check': 'dummy', 'knowledge_base': 'knowledge_base', 'latex_name': 'latex_name', 'name': 'name', 'predicate': '_predicate'}
level = 0
mutable_attrs_to_copy = ['sympy_set', 'is_union', 'is_intersection', 'is_cartes_product', 'is_cartes_power', 'is_real', '_is_set', 'is_empty', 'theorems']
predicate(x: Term) → Proposition[source]
replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Any[source]
to_sympy() → Set[source]
class pylogic.structures.set_.Union[source]
class pylogic.structures.set_.Union(*args, **kwargs)

Bases: Set

Represents the union of finitely many or countably-infinitely many sets.

is_atomic = False
pylogic.structures.set_.sets(name: str, *elements: Any, **kwargs) → Set[source]
pylogic.structures.set_.sets(*names: str, **kwargs) → tuple[Set, ...]

Module contents