380 utilize vacuous interval theorem - #381
Draft
wdcraft01 wants to merge 13 commits into
Draft
Conversation
Add the singleton_interval theorem to number_sets/integers theorems, for potential reduction of a single-element integer Interval, such as Interval(3, 3) = {3..3}, to a singleton enumerated set Set(3) = {3}. This will then be utilized in the Interval().shallow_simplification() method to simplify such Interval expressions (if _simpification_directives_ set appropriately).
Establish the number_sets/integers/Interval.shallow_simplification() method, dealing initially with just two special cases: reducing an empty or "vacuous" Interval to the empty set EmptySet, and reducing a singleton Interval(a,b) where a = b, to a singleton enumerated Set(a) = {a}.
Update number_sets/integers demonstrations notebook to include some testing and demonstration of recent establishment of number_sets/integers/Interval.shallow_simplification() method.
Add empty_set_membership_is_bool and empty_set_nonmembership_is_bool theorems to logic/sets/ theorems notebook.
Establish several EmptySet-related theorems at the logic/sets level, including: empty_set_contradiction, non_empty_def, non_empty_unfolding, and non_empty_folding.
Establish EmptySetMembership and EmptySetNonmembership classes at the level of logic/sets. Still under development/construction. Commit also inlcudes EmptySetMembership.derive_contradiction() and EmptySetMembership.deny_via_contradiction() methods, but it's not clear that either method logically belongs specifically here as EmptySetMembership methods.
Add module-level affirm_via_empty_set_contradiction() and deny_via_empty_set_contradiction() function to empty_set_membership.py. Also add _readily_provable() and _readily_disprovable() methods to both the EmptySetMembership and EmptySetNonmembership classes, a conclude() method to the EmptySetNonmembership class, and perform some general cleanup. Also update the logic/sets demonstrations notebook to demo and test recent changes.
wwitzel
approved these changes
Jun 20, 2026
wwitzel
left a comment
wwitzel
left a comment
Collaborator
There was a problem hiding this comment.
This looks good. I'll merge it in and test it all out.
Collaborator
|
This actually breaks summation where it expects an Interval domain and this feature can reduce a singular or vacuous Interval. Hmm... I'll figure out a fix. It goes to show how even simple improvements can break things, which is why they must be tested. |
Collaborator
|
No worries. I fixed the summation issue by changing the 'sum_single' axiom to work with a singleton Set instead of a singleton Interval. |
…tribute check Update NotEquals.side_effects() to include a check for a NotEquals operand with a 'not_equals_side_effects' attribute, and yielding such side effects. In the near-term this is intended to catch inequalities involving the empty set (see next commit).
Add EmptySetLiteral. not_equals_side_effects() method, intended to be called from the NotEquals.side_effects() method and provide the incidental/side-effect result that Exists_{x}[x in A] when we have 'A ≠ EmptySet'.
…et.not_equals_side_effects()
Update the logic/sets demonstrations notebook to test and demonstrate recently-established EmptySet.not_equals_side_effects(), allowing the automatic conclusion that Exists_{x}[x in A] whenever we have [A ≠ EmptySet].
Add an InSet.existential_side_effects() method, intended to be called from Exists.side_effects() method for cases where the Exists has an InSet for its instance_expr. The existential_side_effects() essentially then deduces that the set involved is not the empty set.
…fects() Augment the Exists.side_effects() method with call to instance_expr.existential_side_effects() method, currently intended to target the InSet.existential_side_effects() and automatically deduce that the set involved is not the empty set.
Update sets/membership demonstrations notebook to test and demonstrate the recently-established InSet.existential_side_effects() method and the recently augmented Exists.side_effects() method.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This branch focuses on two related but independent "upgrades," focusing on (1) Interval.shallow_simplification, and (2) an EmptySetMembership class.
(1) The branch provides a simple implementation of Interval.shallow_simplification(), focusing on the simplification of (a) empty intervals of the form Interval(a, b) with b < a, simplifying such intervals to the EmptySet, and (b) singleton intervals of the form Interval(a,a), simplifying such intervals to a singleton set Set(a) = {a}.
(2) The branch also provides simple implementations of EmptySetMembership and EmptySetNonmembership classes and some related methods, as well as two module-level functions in the empty_set_membership.py code:
affirm_via_empty_set_contradiction()anddeny_via_empty_set_contradiction().One major goal of these modifications is to then allow related updates to the SetOfAll class so that a set comprehension on an empty domain can be easily reduced to an empty set. Modifications to the SetOfAll class and related methods might themselves probably be implemented, though, in a separate branch. I need to check on earlier work done on the SetOfAll class and related methods.