Exists

class proveit.logic.Exists(instance_param_or_params, instance_expr, *, domain=None, domains=None, condition=None, conditions=None, styles=None, _lambda_map=None)

Bases: proveit.OperationOverInstances

Attributes Summary

known_instance_maps
skolem_consts_to_existential

Methods Summary

choose(self, \*skolem_constants[, print_message])	From the existential expression self = exists_{x_1,…,x_n | Q(x_1,…,x_n)} P(x_1,…,x_n), generate Skolem constants a_1,…,a_n in correspondence with the instance params x_1,…,x_n. The process will: (1) add Q(a_1,…,a_n) and P(a_1,…,a_n) to the default assumptions; (2) register the Skolem constants a_1,…,a_n in the skolem_consts_to_existential dictionary so they can be eliminated later using the eliminate() method; (3) return the newly-generated assumptions Q(a_1,…,a_n) and P(a_1,…,a_n).
conclude(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_domain_inclusion(self, …)	Conclude this exists statement from a similar exists statement over a narrower domain.
conclude_via_example(self, example_instance, …)	Conclude and return this [exists_{x_1, .., x_n | Q(x_1, …, x_n)} P(x_1, …, x_n)] from P(y_1, …, y_n) and Q(y_1, …, y_n) where y_1, …, y_n is the given example_instance.
deduce_in_bool(self, \*\*defaults_config)	Deduce, then return, that this exists expression is in the set of BOOLEANS as all exists expressions are (they are taken to be false when not true).
deduce_not_exists(self, \*\*defaults_config)	Deduce notexists_{x | Q(x) P(x) assuming not(exists_{x | Q(x) P(x)), where self is exists_{x | Q(x) P(x).
definition(self, \*\*defaults_config)	Return definition of this existential quantifier as an equation with this existential quantifier on the left and a negated universal quantification on the right.
derive_negated_forall(self, \*\*defaults_config)	From [exists_{x | Q(x)} Not(P(x))], derive and return Not(forall_{x | Q(x)} P(x)).
eliminate(skolem_constants, judgment, …)	For the provided judgment of the form S |– alpha and the tuple of Skolem constants skolem_constants that had been specified earlier using the Exists.choose(), derive and return a new judgment S’ |– alpha where all assumptions in S involving only the given skolem_constants are now eliminated. This process will only work if the provided skolem_constants exactly match a set of Skolem constants used earlier in an Exists.choose() method to produce the Skolem constant-based subset of assumptions you wish to eliminate from S.
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically for a negated exists operation.
side_effects(self, judgment)	Side-effect derivations to attempt automatically for an exists operations.
substitute_domain(self, superset, …)	Substitute the domain with a superset.
substitute_instances(self, universality, …)	Derive from this Exists operation, Exists_{..x.. in S | ..Q(..x..)..} P(..x..), one that substitutes instance expressions given some universality = forall_{..x.. in S | P(..x..), ..Q(..x..)..} R(..x..). or forall_{..x.. in S | ..Q(..x..)..} P(..x..) = R(..x..). Either is allowed in the theory of the existential quantifier. Derive and return the following type of existential operation assuming universality: Exists_{..x.. in S | ..Q(..x..)..} R(..x..) Works also when there is no domain S and/or no conditions ..Q.
unfold(self, \*\*defaults_config)	From this existential quantifier, derive the “unfolded” version according to its definition (the negation of a universal quantification).

Attributes Documentation

known_instance_maps = {}

skolem_consts_to_existential = {}

Methods Documentation

choose(self, \*skolem_constants, print_message=True)

From the existential expression self = exists_{x_1,…,x_n | Q(x_1,…,x_n)} P(x_1,…,x_n), generate Skolem constants a_1,…,a_n in correspondence with the instance params x_1,…,x_n. The process will: (1) add Q(a_1,…,a_n) and P(a_1,…,a_n) to the default

assumptions;

2. register the Skolem constants a_1,…,a_n in the skolem_consts_to_existential dictionary so they can be eliminated later using the eliminate() method;

3. return the newly-generated assumptions Q(a_1,…,a_n) and P(a_1,…,a_n)

conclude(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_domain_inclusion(self, subset_domain, \*\*defaults_config)

Conclude this exists statement from a similar exists statement over a narrower domain. For example, conclude exists_{x in B} P(x) from exists_{x in A} P(x) given A subset_eq B.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_example(self, example_instance, \*\*defaults_config)

Conclude and return this [exists_{x_1, .., x_n | Q(x_1, …, x_n)} P(x_1, …, x_n)] from P(y_1, …, y_n) and Q(y_1, …, y_n) where y_1, …, y_n is the given example_instance.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_bool(self, \*\*defaults_config)

Deduce, then return, that this exists expression is in the set of BOOLEANS as all exists expressions are (they are taken to be false when not true).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_not_exists(self, \*\*defaults_config)

Deduce notexists_{x | Q(x) P(x) assuming not(exists_{x | Q(x) P(x)), where self is exists_{x | Q(x) P(x).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

definition(self, \*\*defaults_config)

Return definition of this existential quantifier as an equation with this existential quantifier on the left and a negated universal quantification on the right.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_negated_forall(self, \*\*defaults_config)

From [exists_{x | Q(x)} Not(P(x))], derive and return Not(forall_{x | Q(x)} P(x)). From [exists_{x | Q(x)} P(x)], derive and return Not(forall_{x | Q(x)} (P(x) != TRUE)).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

static eliminate(skolem_constants, judgment, \*\*defaults_config)

For the provided judgment of the form S |– alpha and the tuple of Skolem constants skolem_constants that had been specified earlier using the Exists.choose(), derive and return a new judgment S’ |– alpha where all assumptions in S involving only the given skolem_constants are now eliminated. This process will only work if the provided skolem_constants exactly match a set of Skolem constants used earlier in an Exists.choose() method to produce the Skolem constant-based subset of assumptions you wish to eliminate from S.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for a negated exists operation.

side_effects(self, judgment)

Side-effect derivations to attempt automatically for an exists operations.

substitute_domain(self, superset, \*\*defaults_config)

Substitute the domain with a superset. From [exists_{x in A| Q(x)} P(x)], derive and return [exists_{x in B| Q(x)} P(x)] given A subseteq B.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

substitute_instances(self, universality, \*\*defaults_config)

Derive from this Exists operation, Exists_{..x.. in S | ..Q(..x..)..} P(..x..), one that substitutes instance expressions given some universality = forall_{..x.. in S | P(..x..), ..Q(..x..)..} R(..x..).

or forall_{..x.. in S | ..Q(..x..)..} P(..x..) = R(..x..).

Either is allowed in the theory of the existential quantifier. Derive and return the following type of existential operation assuming universality: Exists_{..x.. in S | ..Q(..x..)..} R(..x..) Works also when there is no domain S and/or no conditions ..Q…

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

unfold(self, \*\*defaults_config)

From this existential quantifier, derive the “unfolded” version according to its definition (the negation of a universal quantification).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.