350 add theorems to sets package #352
Open
Conversation
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
Commit empty _sub_theories_.txt files that keep re-appearing , hoping this will end their dogged determination to manifest in every branch. The _sub_theories_.txt files are for the _core_/expression sub-packages: composite, conditional, label, lambda_expr, and operation.
Establish the logic/booleans/exclusive_disjunction sub-theory package (no content yet).
… theorems Begin construction of XOr class and related axioms and theorems, just the __init__() and unary_reduction() methods and a few axioms and theorems to allow some functionality.
Update exclusive_disjunction xor axioms, gradually borrowing and modifying from the logical Or disjunction. Here we add xor truth table axioms, axioms about well-definedness, and axioms for defining multi-operand XOr.
Further adapt the disjunction (Or) theorems to the exclusive disjunction (XOr) theory package. Most of these translated just fine, with a few left out because the translation not yet clear (for example, the or_if_any theorem acknowledging that a disjunction is TRUE if any of the operands are TRUE, is more challenging for the XOr since the XOr is TRUE if exactly an odd number of the operands are TRUE and the rest are FALSE).
Update XOr class methods in xor_op.py and XOr demonstrations nb. Roughly 40% of the disjunction Or methods have been translated over into XOr methods and briefly tested in the XOr demonstrations.ipynb.
…kage Correct the destructive_multi_dilemma theorem in logic/booleans/disjunction package (swapping ExprRange of As with ExprRange of Bs).
Fix the XOr.conclude() method for simple cases of (T xor F) and (F xor T), where each corresponding theorem needed a .expr suffix in the if condition.
Update XOr demonstrations page for correction (see previous commit) to XOr.conclude() method.
We already have in_bool_def and unfold_is_bool, essentially forms of (or precursors for) the "law of the excluded middle", but we now add versions using the XOr (instead of the inclusive disjunction Or): the in_bool_def_xor and unfold_is_bool_xor. Now we two options for "unfolding" what it means for A to be Boolean: the strong version of (A) xor (Not(A)) or the weaker version of (A) or (Not(A)).
Add some more XOr-related theorems to the logic/booleans collection of theorems, including: unfold_is_bool_xor_explicit, xor_implies_or, and x_or_implies_or_binary.
Continue to add XOr class methods(), based on analogous methods in Or (disjunction) class, now through the Or.deny_via_contradiction() method. Also update the XOr demonstrations page to accommodate the new XOr methods.
Finish translating the Or class methods in the XOr class and update the exclusive_disjunction demonstrations.ipynb notebook with simple tests of the XOr methods. Most of the methods are quite satisfactory. A notable exception is the XOr.shallow_simplification() method, which is fairly primitive compared to the Or version. The weakness is due in part to the absence of quantification-related theorems and methods in the XOr class. Further development should consider possible theorems and methods acknowledging that an XOr evaluates to TRUE if and only if exactly an odd number of its operands evaluate to TRUE and the remaining operands evaluate to FALSE.
Add to the logic/booleans package the xor_as_or_and_not_and theorem expressing the XOr in terms of Or and And.
Update XOr().shallow_simplification() to deal more effectively with the binary XOr() cases and allow evaluative simplification comparable to what happens in the Or class. Also updates the XOr demonstrations.ipynb notebook.
Fix a bug in _core_/_theory_storage.py in which 'hash_id' is somehow being used before it is defined. This is a bug that was also fixed independently in the separate branch 331-theory-of-graphs-development back on 4/24/2025, but never absorbed into master. See email w/WW on 4/24/2025 with suggestion for how to fix.
Add to logic/booleans/exclusive_disjunction the `not_left_if_right` and `not_right_if_left` XOr-related theorems (in part because they look useful for some work in the 329-QEC branch dealing with pseudo-partitions of naturals into evens and odds.
Establish preliminary proofs of four XOr theorems in the logic/booleans/exclusive_disjunction sub-theory package: `left_if_not_right`, `right_if_not_left`, `not_left_if_right`, and `not_right_if_left`.
Establish proofs of some simple XOr theorems, namely: false_xor_false_negated, false_xor_true, true_xor_false, true_xor_true_negated, xor_if_only_left, and xor_not_if_both.
Correct the constructive_dilemma and constructive_multi_dilemma theorems in logic/booleans/exclusive_disjunction (XOr), changing conclusions to Or() instead of the original XOr().
Add the xor_as_or_but_not_and theorem to the logic/booleans/exclusive_disjunction (XOr) sub-theory package. This is a fairly standard descriptive theorem, often used in the guise of a definition of XOr.
Establish the proofs of two simple theorems in logic/booleans/exclusive_disjunction (XOr), namely xor_if_only_right and xor_not_if_neither. Also some clean-up editing of the logic/booleans/exclusive_disjunction theorems notebook.
Establish proofs for five theorems in the logic/booleans/exclusive_disjunction sub-theory package, namely: `binary_xor_both_contradiction`, `binary_xor_neither_contradiction`, `not_xor_as_both_or_neither`, `xor_as_or_but_not_and`, and `xor_as_or_of_and`.
… methods Add XOr().derive_not_right_if_left() and XOr().derive_not_left_if_right() methods, utilizing recently created theorems. Also add some testing blocks in the logic/booleans/exclusive_disjunction demonstrations notebook.
…mma thm Update the XOr.derive_via_multi_dilemma() method for the recently-corrected constructive_dilemma (producing a disjunction V instead of an exclusive disjunction). Also update logic/booleans/exclusive_disjunction demonstrations notebook for the updated method.
Add the comprehension_superset_reduction theorem to the logic/sets/comprehension sub-theory package, in anticipation of its utility in one or more proofs being pursued in branch 329-QEC-development. Basically: if (forall y, ~Q(y)), then the set {y | Q(y)}_{y in S} reduces to {y | Q(y)}_{y in (S - A)}.
Add 3 thms to logic/sets sub-theory pkg, namely: `element_implies_non_zero_card`, `card_finite_subset_lesseq_card_superset`, and `finite_subset_with_card_of_superset_is_superset`. These are being added in anticipation of them being useful in proofs of one or more theorems in the separate 329-QEC-dev branch.
Add the SetOfAll.reduce_superset() method and update demonstrations notebook for the comprehension sub-theory package to test and demonstration the new method.
This reverts commit 691fa61.
…theory pkg" This reverts commit bc7a5b1.
Add 2 partition-related theorems to the logic/sets sub-theory package, namely: `bipartition_eq_set_differences` and `bipartition_membership_eq_set_differences`, both relating the bipartition of a set S into A and B to the differences S - A = B and S - B = A.
Add maximal_size_subset_is_superset theorem to the logic/sets sub-theory package, a modified version of a similar theorem added in a recent previous commit, basically saying that if a set B has cardinality <= n, but we have a subset A of B with cardinality n, then A = B and |B| = n.
Clean up logic/sets theorems notebook a bit, collecting imports at top of notebook.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 adds three useful set-theory theorems to the logic/sets sub-theory package, namely:
element_implies_non_zero_card, (any set with an element has cardinality greater than 0)card_finite_subset_lesseq_card_superset, (relates cardinality of subset to superset)finite_subset_with_card_of_superset_is_superset(relates cardinalities to set equalities)These are being added in anticipation of them being useful in proofs of one or more theorems in the separate 329-QEC-dev branch.
In the commits one will also find dev and commits, then commit reversions, for a comprehension_superset_reduction theorem and related SetOfAll().superset_reduction() method; that theorem and its related method were instead added directly to branch 329-QEC because of difficult-to-manage merge issues (arising because considerable SetOfAll() class development occurred earlier this year directly in branch 329-QEC).