336 even and odd integers #337
Open
+3,378
−165
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
Begin to establish the IntegerEven number set (the IntegerEvenSet class and the related IntegerEvenMembership class) and begin filling in details, including the standard theorem about membership being Boolean, along with beginning testing in the integers/demonstrations.ipynb nb. The IntegerEvenSet is tucked away inside the integers package and integers.py.
Augment IntegerEvenMembership methods to include side-effect that derives membership element in superset Integer. Includes related theorem about even integers being a proper subset of the integers.
Establish axiomatic def of IntegerEven (i.e. even integers) as {2z}_{z \in Z} (in axioms for numbers/number_sets/integers).
Establish the even_int_is_double_int existential theorem for even integers (i.e. for elements of IntegerEven set). The theorem is then utilized in the IntegerEvenMembership.derive_element_as_double_int() method (see later commit). Proof of the even_int_is_double_int will likely require the SetOfAll class updates available in the QEC-development branch.
Establish IntegerEvenMembership.derive_element_as_double_int() method, which is also used in the IntegerEvenMembership.side_effects() method, returning an existential claim: if x in IntegerEven, then there exists an integer z such that x = 2z.
Update numbers/number_sets/integers/demonstrations.ipynb to include demonstration and testing of IntegerEvenMembership side-effect that x in IntegerEven means there exists z in Integer such that x = 2z.
Add even_int_within_rational theorem (unproven) to numbers/number_sets/rationals package: even integers are rational numbers. This is then utilized in the IntegerEvenMembership.derive_element_in_rational() method (separate later commit).
Add even_int_within_real theorem (unproven) to numbers/number_sets/reals package: even integers are real numbers. This is then utilized in the IntegerEvenMembership.derive_element_in_real() method (separate later commit).
…class Add the derive_element_in_rational() and derive_element_in_real() methods to IntegerEvenMembership class. These are then also utilized in the IntegerEvenMembership class side_effects() method.
Add the double_int_is_even theorem to the numbers/number_sets/integers package, which then helps with the IntegerEvenMembership.conclude() method (separate later commit).
Add IntegerEvenMembership.conclude() and IntegerEvenMembership.conclude_as_last_resort() methods, which then rely on the previously committed double_int_is_even theorem. Commit also includes some clean-up, deleting obsolete text and code.
Update number_sets/integers demonstrations.ipynb for further testing and demonstration of IntegerEvenMembership methods (mainly the conclude() method).
Establish the IntegerOddSet number set class to represent the odd integers. Also assumes the establishment of the IntegerOddMembership class, in a separate (later) commit.
Establish the axiomatic def of IntegerOdd number set (i.e. the odd integers) as {2z+1}_{z in Integer}.
Establish IntegerOdd notation for IntegerOddSet().
Establish some basic theorems for IntegerOdd number set (i.e. the odd integers): odd_int_membership_is_bool (membership in odd integers is a boolean), odd_int_within_int (an odd integer is an integer), odd_int_is_double_int_plus_one (odd int looks like 2z+1 for some integer z), double_int_plus_one_is_odd (if z is an int then 2z+1 is an odd integer). These are then actively used in the methods for the IntegerOddMembership class.
Establish the package-level imports for IntegerOdd number set.
Establish the odd_within_rational theorem (odd numbers are rational numbers) for IntegerOdd number set.
Establish the odd_int_within_real theorem (odd integers are real numbers) for the IntegerOdd number set.
Establish the IntegerOddMembership class (i.e. membership in the odd integers) and related methods. Depends on several previous commits of related theorems and package imports.
Update number_sets/integers/demonstrations.ipynb to demonstrate and test the IntegerOdd number set and the IntegerOddMembership class and related methods.
Update numbers/number_set/integers demos nb to remove a temporary `assert False` cell and allow nb to run to completion.
|
I think this is going in a good direction Let's take a closer look together on Friday. I do think that the odd numbers should be defined as O = (Z - E). I just called Bob Carr up and he agrees: the "essence" of odd numbers are that they are not even. |
Modify the axiomatic definition of IntegerOdd (the set of odd integers) to be (Z - E) (i.e., the set of integers without the set of even integers). Suggested by @wwitzel and seconded by Bob.
Add several theorems to the numbers/addition package related to the IntegerEven (even integers) and IntegerOdd (odd integers) number sets. These are then utilized in the Add.deduce_in_number_set() method: • add_int_even_closure (adding even integers gives another even integer) • add_int_even_closure_bin (sum of two even integers is an even integer) • add_int_even_from_even_odd (the sum of an even number of odd integers is an even integer) • add_int_even_from_odd_bin (the sum of two odd integers is an even integer) • add_int_odd_from_even_and_and_odd (sum of an even and an odd integer is an odd integer) • add_int_odd_from_odd_odd (the sum of an odd number of odd integers is an odd integer)
…tion theorems Update the Add.deduce_in_number_set() method to use related even/odd addition theorems in previous commit, for things like the sum of an even and an odd is an odd, and the sum of an odd number of odd integers is odd, etc.
Correct some typos in comments in integers/integer_membership.py (changing some instances of IntegerEven to IntegerOdd).
Update the numbers/number_sets/integers demonstration.ipynb notebook to include additional tests and demonstrations of the Add.deduce_in_number_set() method for more cases of even and odd integer sets.
Add some simple even/odd theorems to numbers_sets/integers: claiming that 2, 4, 6, 8 are each even (i.e. in IntegerEven), that 1, 3, 5, 7, 9 are each odd (i.e. in IntegerOdd), and that the negative of an even (or odd) is still an even (or odd). Also added the single-digit claims to the numbers.__initi__.py for automatic loading.
Add several even-integer and odd-integer theorems to numbers/multiplication package, which will then be utilized in the IntegerEven.conclude() and IntegerOdd.conclude() methods: mult_int_even_from_ints_with_any_even (product of integers is even if any operand is even) mult_int_even_from_left_even_bin, mult_int_even_from_right_even_bin (binary product of integers is even if one of the operands is even) mult_int_odd_from_all_odd (product of odd integers is odd)
Add a commuted version of a binary even/odd theorem claiming that the sum of an odd integer and an even integer is an odd integer. This will then be used to simplify some code in the Add.deduce_in_number_set() method. Also updates the add_int_even_from_even_odd theorem to allow an empty (zero operands) Add, which is axiomatically defined as 0 which is then also even.
Update IntegerEvenMembership's conclude() and side_effects() methods, removing some redundant side-effects from side_effects() and adding components in conclude() to take advantage of multiplication (Mult)-related theorems about (for example, if Mult has all integer operands with at least one operand known to be even, then the product is even). A note about including Mult cases in conclude: after discussion with @wwitzel it seemed reasonable consider such cases in conclude() in part because it was difficult to see a good/best way to inject even/odd considerations into the Mult.deduce_in_number_set() method.
Update Add.deduce_in_number_set() to use two separate binary theorems (odd + even = odd, and even + odd = odd) instead of using a single theorem for both and then commuting the result for one of them.
Update the demonstrations.ipynb notebook for number_sets/integers for recent developmental work on IntegerEvenSet and IntegerOddSet (and related membership classes), including some (indirect) testing of the IntegerEvenMembership.conclude() method which has been updated with some cases for when the element of a membership is a Mult (product) (see earlier commit).
Add missing `return` key word to a half-dozen lines in the Add.deduce_in_number_set() method.
… into 336-even-and-odd-integers
Add one more missing `return` in Add.deduce_in_number_set(), which was dropped due to a conflict when merging branch 338 into this branch 336.
Augment the IntegerEvenMembership.conclude() method with a case for the element being an instance of Add, in which case we return the element's Add.deduce_in_number_set() method using the IntegerEven number set. Not sure if this is reasonable based on the way @wwitzel likes to think about these things.
Add an observation/comment to NumberSet.conclude(), noting that an attempt to include as a step the calling of element.deduce_in_number_set() seems to lead to an infinite loop, where the actual XMembership.conclude() leads to a NumberSet.conclude(), which then leads to an XMembership.conclude, etc.
Analogous to what we did in the IntegerEvenMembership.conclude() method, augment the IntegerOddMembership.conclude() method with a case for the element being an instance of Add, in which case we return the element's Add.deduce_in_number_set() method using the IntegerOdd number set.
Analogous to what we did in the IntegerEvenMembership.conclude() method, augment the IntegerOddMembership.conclude() method with a case for the element being an instance of Neg(a) with 'a' itself being odd, in which case we the element is also odd (i.e. the negation of an odd is an odd).
Augment the IntegerOddMembership.conclude() to include the case where the membership element is a Mult() with all multiplicands odd, in which case the product should be odd. Analogous to Mult case(s) introduced into the IntegerEvenMembership.conclude() method.
Add two theorems to the number_sets/integers package for even and odd integers: odd_int_has_even_successor (an odd integer has an even integer successor) even_int_has_odd_successor (an even integer has an odd integer successor). These are then utilized in the IntegerEvenMembership.conclude() and IntegerOddMembership.conclude() methods (a separate later commit).
Update the IntegerEvenMembership.conclude() and IntegerOddMembership.conclude() methods to use recently created integer package theorems about successors of even and odd integers (see recent previous commit). Related Issue: #336.
Remove some obsolete print() statements (used for testing) from the IntegerEvenMembership.conclude() and IntegerOddMembership.conclude() methods.
Update number_sets/integers/demonstrations.ipynb notebook with demonstrations of recent modifications, especially recent modifications to the IntegerEvenMembership.conclude() and IntegerOddMembership.conclude() methods.
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 is ready for an initial review @wwitzel to see if things are generally headed in the right direction. The branch includes augmentations to integer.py and integer_membership.py that add
IntegerEvenSet(),IntegerEvenMembership(),IntegerOddSet(), andIntegerOddMembership()classes, as well as a some related common expressions, a few axioms, and several theorems. Demonstrations/testing of basic concepts can be found in the demonstrations notebook for the numbers/number_sets/integers theory package. It's possibly useful to add some further subset(s), such as a non-negative even integer setIntegerEvenNonNegSet(), which would be especially relevant when considering the degree categories of graph vertices.