pylogic.proposition.quantified package¶

Submodules¶

pylogic.proposition.quantified.exists module¶

class pylogic.proposition.quantified.exists.Exists(variable: Variable, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: _Quantified[TProposition]

by_single_substitution(term: Any, proven_proposition: Proposition | None = None) → Self[source]¶: Logical inference rule. If self is exists x: P(x) and term is y and P(y) is proven, return a proven exists x: P(x).

by_substitution(*terms: Any, proven: Proposition) → Self[source]¶

Logical inference rule. Continually substitute until the innermost exists proposition is unwrapped.

If self is exists x: exists y: P(x, y) and terms is (a, b) and P(a, b) is proven, return a proven exists x: exists y: P(x, y).

de_morgan() → Proposition[source]¶

Apply De Morgan’s law to an existentially quantified sentence.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

exists_modus_ponens(other: Forall[Implies[TProposition, B]]) → Exists[B][source]¶: Logical inference rule. If self is exists x: P(x) and given forall x: P(x) -> Q(x) and each is proven, conclude exists x: Q(x).

extract(name: str | None = None, latex_name: str | None = None) → tuple[Symbol, TProposition][source]¶: Logical inference rule. If self is proven, return a constant and a proven inner proposition.

classmethod from_proposition(existential_var_name: str, expression_to_replace: Any | None, inner_proposition: TProposition, latex_name: str | None = None, positions: list[list[int]] | None = None, is_assumption: bool = False, description: str = '', **kwargs) → Exists[TProposition][source]¶

latex_name: str | None: The latex representation of the existential variable.
positions: list[list[int]]: This is a list containing the positions of the expression_to_replace in self. If None, we will search for all occurences of the expression_to_replace in self. This is a nested list representing the path we need to go down in the proposition tree, For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) existential_var = q and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q)

Other keyword arguments are passed to the variable.

to_exists_in_set(**kwargs) → ExistsInSet[Proposition][source]¶

If self matches the structure,

exists x: (x in set /P (x))

convert self to an ExistsInSet statement.

to_exists_unique(**kwargs) → ExistsUnique[Proposition][source]¶

If self matches the structure,

exists x: (P (x) /forall y: [P (y) -> y = x])

convert self to an ExistsUnique statement.

to_exists_unique_in_set(**kwargs) → ExistsUniqueInSet[Proposition][source]¶

If self matches the structure,

exists x: x in set /P (x) /[forall y: (y in set /P (y)) -> y = x])

convert self to an ExistsUniqueInSet statement.

class pylogic.proposition.quantified.exists.ExistsInSet(variable: Variable, set_: Set | Variable, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Exists[And[IsContainedIn, TProposition]]

copy() → Self[source]¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self[source]¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

classmethod from_proposition(existential_var_name: str, expression_to_replace: Term | None, set_: Set | Variable, inner_proposition: TProposition, latex_name: str | None = None, positions: list[list[int]] | None = None, is_assumption: bool = False, description: str = '', **kwargs) → ExistsInSet[TProposition][source]¶

latex_name: str | None: The latex representation of the existential variable.
positions: list[list[int]]: This is a list containing the positions of the expression_to_replace in self. If None, we will search for all occurences of the expression_to_replace in self. This is a nested list representing the path we need to go down in the proposition tree, For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) existential_var = q and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q)

Other keyword arguments are passed to the variable.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_exists(**kwargs) → Exists[And[IsContainedIn, TProposition]][source]¶: Convert self to a regular exists statement.

to_exists_in_set(**kwargs) → Self[source]¶

If self matches the structure,

exists x: (x in set /P (x))

convert self to an ExistsInSet statement.

class pylogic.proposition.quantified.exists.ExistsSubset(variable: Variable, set_: Set, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Exists[And[IsSubsetOf, TProposition]]

copy() → Self¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_exists(**kwargs) → Exists[And[IsContainedIn, TProposition]]¶: Convert self to a regular exists statement.

class pylogic.proposition.quantified.exists.ExistsUnique(variable: Variable, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Exists[And[TProposition, Forall[Implies[TProposition, Equals]]]]

copy() → Self[source]¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self[source]¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_exists_unique(**kwargs) → Self[source]¶

If self matches the structure,

exists x: (P (x) /forall y: [P (y) -> y = x])

convert self to an ExistsUnique statement.

class pylogic.proposition.quantified.exists.ExistsUniqueInSet(variable: Variable, set_: Set, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: ExistsInSet[And[TProposition, Forall[Implies[TProposition, Equals]]]]

copy() → Self[source]¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self[source]¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_exists_unique_in_set(**kwargs) → Self[source]¶

If self matches the structure,

exists x: x in set /P (x) /[forall y: (y in set /P (y)) -> y = x])

convert self to an ExistsUniqueInSet statement.

class pylogic.proposition.quantified.exists.ExistsUniqueSubset(variable: Variable, set_: Set, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: ExistsSubset[And[TProposition, Forall[Implies[TProposition, Equals]]]]

copy() → Self¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

class pylogic.proposition.quantified.exists.InferenceRule¶

Bases: dict

arguments: list[str]¶

name: str¶

pylogic.proposition.quantified.forall module¶

class pylogic.proposition.quantified.forall.Forall(variable: Variable, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: _Quantified[TProposition]

de_morgan() → Proposition[source]¶

Apply De Morgan’s law to a universally quantified sentence.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

extract_conjuncts() → list[Proposition][source]¶: Logical inference rule. Given self is proven and is of the form forall x: P(x) and Q(x), (or forall x in S: P(x) and Q(x), etc), return the propositions [forall x: P(x), forall x: Q(x)] (or [forall x in S: P(x), forall x in S: Q(x)]).

forall_modus_ponens(other: Forall[Implies[TProposition, B]] | Exists[Implies[TProposition, B]]) → Forall[B] | Exists[B][source]¶: Logical inference rule. If self is forall x: P(x) and given P(x) -> Q(x) or forall x: P(x) -> Q(x) (or exists x: P(x) -> Q(x)), and each is proven, conclude forall x: Q(x) (or exists x: Q(x)).

in_particular(expression_to_substitute: Any, **kwargs) → TProposition[source]¶: Logical inference rule. Given self is proven, replace the variable in the inner proposition and get a proven proposition.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

class pylogic.proposition.quantified.forall.ForallInSet(variable: Variable, set_: Set, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Forall[Implies[IsContainedIn, TProposition]]

copy() → Self[source]¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self[source]¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

in_particular(expression_to_substitute: Any, proof_expr_to_substitute_in_set: Proposition | None = None, **kwargs) → TProposition[source]¶: Logical inference rule. Given self is proven, replace the variable in the inner proposition and get a proven proposition.

neq_any_thus_not_in_sequence() → Not[IsContainedIn][source]¶: Logical inference rule. Given self is proven, where self is of the form forall k in Naturals: A != s[k], return a proof of ~(A in {s_n}).

neq_any_thus_not_in_set() → Not[IsContainedIn][source]¶: Logical inference rule. Given self is proven, where self is of the form forall x in S: A != x, return a proof of ~(A in S).

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_forall() → Forall[Implies[IsContainedIn, TProposition]][source]¶: Convert self to a regular forall statement.

class pylogic.proposition.quantified.forall.ForallSubsets(variable: Variable, set_: Set, inner_proposition: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Forall[Implies[IsSubsetOf, TProposition]]

copy() → Self¶

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:: A shallow copy of the proposition.
Return type:: Self

deepcopy() → Self¶

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:: A deep copy of the proposition.
Return type:: Self

in_particular(expression_to_substitute: Any, proof_expr_to_substitute_is_subset: IsSubsetOf | None = None, **kwargs) → TProposition[source]¶: Logical inference rule. Given self is proven, replace the variable in the inner proposition and get a proven proposition.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self¶

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.
positions (list[list[int]] | None) –
This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

TODO: finish replace, document replacing the quantified variables as well

For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).
equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

to_forall() → Forall[Implies[IsContainedIn, TProposition]]¶: Convert self to a regular forall statement.

class pylogic.proposition.quantified.forall.InferenceRule¶

Bases: dict

arguments: list[str]¶

name: str¶

pylogic.proposition.quantified package¶

Submodules¶

pylogic.proposition.quantified.exists module¶

pylogic.proposition.quantified.forall module¶

pylogic.proposition.quantified.quantified module¶

Module contents¶

Pylogic

Navigation

Related Topics