Not

class proveit.logic.Not(A, *, styles=None)

Bases: proveit.Operation

Methods Summary

affirm_via_contradiction(self, conclusion, …)	From not(A), derive the conclusion provided that the negated conclusion implies both not(A) as well as A, and the conclusion is a Boolean.
conclude(self, \*\*defaults_config)	Try to automatically conclude this negation via evaluation reductions or double negation.
conclude_negation(self, \*\*defaults_config)	Try to conclude the negation of this negation via double negation.
conclude_via_double_negation(self, …)	Prove and return self of the form not(not(A)) assuming A.
conclude_via_falsified_negation(self, …)	Prove and return self of the form not(A) assuming A=FALSE.
deduce_double_negation_equiv(self, …)	For some not(not(A)), derive and return A = not(not(A)) assuming A in Boolean.
deduce_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that this ‘not’ expression is in the set of BOOLEANS.
deduce_operand_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that the negated operand is in the set of BOOLEANS.
deny_via_contradiction(self, conclusion, …)	From not(A), derive the negated conclusion provided that the conclusion implies both not(A) as well as A, and the conclusion is a Boolean.
derive_contradiction(self, \*\*defaults_config)	From not(A), and assuming A, derive and return FALSE.
derive_in_bool(self, \*\*defaults_config)	From Not(A) derive [Not(A) in Boolean].
derive_untrue(self, \*\*defaults_config)	From not(A), derive and return A != TRUE.
derive_via_double_negation(self, …)	From not(not(A)), derive and return A.
double_negation_equivalence(self, …)	Given not(not(A)), deduce and return not(not(A)) = A.
equate_negated_to_false(self, …)	From not(A), derive and return A = FALSE.
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
in_bool_side_effects(self, judgment)	From not(A) in Boolean deduce A in Boolean, where self is not(A).
latex(self[, fence])	Return a latex-formatted representation of the Expression.
side_effects(self, judgment)	Side-effect derivations to attempt automatically.
substitute_falsehood(self, lambda_map, …)	Given not(A), derive P(A) from P(FALSE).
substitute_in_false(self, lambda_map, …)	Given not(A), derive P(FALSE) from P(A).

Methods Documentation

affirm_via_contradiction(self, conclusion, \*\*defaults_config)

From not(A), derive the conclusion provided that the negated conclusion implies both not(A) as well as A, and the conclusion is a Boolean.

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

conclude(self, \*\*defaults_config)

Try to automatically conclude this negation via evaluation reductions or double negation.

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

conclude_negation(self, \*\*defaults_config)

Try to conclude the negation of this negation via double negation. That is, conclude not(not(A)), where self=not(A), via proving A. If that fails (e.g., an unusable theorem), call conclude on not(not(A)) directly.

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

conclude_via_double_negation(self, \*\*defaults_config)

Prove and return self of the form not(not(A)) assuming A. Also see version in NotEquals for A != FALSE.

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

conclude_via_falsified_negation(self, \*\*defaults_config)

Prove and return self of the form not(A) assuming A=FALSE.

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

deduce_double_negation_equiv(self, \*\*defaults_config)

For some not(not(A)), derive and return A = not(not(A)) assuming A in Boolean.

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

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this ‘not’ expression is in the set of BOOLEANS.

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

deduce_operand_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that the negated operand is in the set of BOOLEANS.

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

deny_via_contradiction(self, conclusion, \*\*defaults_config)

From not(A), derive the negated conclusion provided that the conclusion implies both not(A) as well as A, and the conclusion is a Boolean.

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

derive_contradiction(self, \*\*defaults_config)

From not(A), and assuming A, derive and return FALSE.

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

derive_in_bool(self, \*\*defaults_config)

From Not(A) derive [Not(A) in Boolean].

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

derive_untrue(self, \*\*defaults_config)

From not(A), derive and return A != TRUE.

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

derive_via_double_negation(self, \*\*defaults_config)

From not(not(A)), derive and return A. Note, see Equals.derive_via_boolean_equality for the reverse process.

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

double_negation_equivalence(self, \*\*defaults_config)

Given not(not(A)), deduce and return not(not(A)) = A.

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

equate_negated_to_false(self, \*\*defaults_config)

From not(A), derive and return A = FALSE. Note, see Equals.derive_via_boolean_equality for the reverse process.

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

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value. This Operation.evaluation version simplifies the operands and then calls shallow_simplification with must_evaluat=True.

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

‘evaluated’ returns the right-hand side of ‘evaluation’. ‘evaluate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘evaluation’ for the inner expression.

in_bool_side_effects(self, judgment)

From not(A) in Boolean deduce A in Boolean, where self is not(A).

latex(self, fence=False, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

side_effects(self, judgment)

Side-effect derivations to attempt automatically.

substitute_falsehood(self, lambda_map, \*\*defaults_config)

Given not(A), derive P(A) from P(FALSE).

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

substitute_in_false(self, lambda_map, \*\*defaults_config)

Given not(A), derive P(FALSE) from P(A).

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