Even and odd integers

[avekens]

In one of my recent PRs, I needed/provided a lot of theorems about even and odd integers. I realized (again) that even and odd integers are mentioned in set.mm at several places, but in different ways:

Even integers:

• ( N / 2 ) e. ZZ
• 2 || N
• E. i e. ZZ N = ( 2 x. i )

Odd integers:

• ( ( N + 1 ) / 2 ) e. ZZ
• ( ( N - 1 ) / 2 ) e. ZZ
• -. ( N / 2 ) e. ZZ
• 2 || ( N + 1 )
• 2 || ( N - 1 )
• -. 2 || N
• E. i e. ZZ N = ( ( 2 x. i ) + 1 )

In all cases, it must be usually assumed that N is at least a number (N e. CC) , because we cannot derive from ( N / 2 ) e. ZZ that N e. ZZ (Gérard made a corresponding remark recently...).

In Februrary, I already provided definitions (as hypothesis/$e statement) for the set of even and odd integers:

• E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
• O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }

Of cource, any of the equivalent definitions could be usedfor a definition, e.g. E = { z e. ZZ | ( z / 2 ) e. ZZ }.

Since the concepts of even and odd integers are very commen and frequently used, I want to propose to provide explicit definitions Even or Odd for them. By such definitions, theorems could be stated without choosing a special representation, e.g. ~nneo (currently ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) ) ) could be written as ( N e. NN -> ( N e. Even <-> -. N e. Odd ) ). Instead of Even or Odd, we could choose the symbols ZZ_even and ZZ_odd or, shorter, ZZ_e and ZZ_o, using the representation of ZZwith corresponding subscripts for typesetting.

What do you think about such definitions? Such definitions and related theorems could be placed in a section "Even and odd integers" after section "5.4.8 Integers (as a subset of complex numbers)".

In a more general definition, we could restrict the range of integers, for example

odd = { <. x , y >. | ( x C_ ZZ /\ y e. x /\ ( ( y - 1 ) / 2 ) e. ZZ ) },

allowing for talking about e.g. odd positive integers or odd integers greater than or equal to 7:

• NN odd 3 - meaning "3 is an odd positive integer"
• ( ZZ>= ` 7 ) odd 9 - meaning "9 is an odd integer greater than or equal to 7"

But I think this would go too far, at least for the moment ...

[david-a-wheeler]

I personally agree that even and odd are common enough that they're worth a definition, but we generally try to avoid small definitions and this is on a hairy edge. I would expect Norman or Mario to speak up. If we do not have separate definitions, at least having a convention would be good.

If we have a definition or convention, I would prefer one that works under constructive mathematics, and ideally would be short. So something like 2 || ( N + 1) for odd would be better than something that uses not.

[david-a-wheeler]

By the way, I prefer "2 ||" over anything directly using "/" for this purpose. I think that's simpler. That is a personal preference, but I wouldn't be surprised if other people also find it simpler.

So I prefer

• Even as 2 || N
• Odd as 2 || ( N + 1 )

[nmegill]

I have mixed feelings about adding the class constants Even and Odd. There are no symbol savings using 'N e. Even' in place of '2 || N'. There is a small savings for 'N e. Odd', but it isn't clear it's worth it. One could argue that 'N e. Even' is more readable than '2 || N', but that's what the comment is for. And maybe it is because I'm used to it, but I immediately interpret '2 || N' as 'N is even' in my head. Usually we don't have separate definitions for essentially the same thing, and because of the extra step of unwinding the definition it's not clear there are proof size savings in general.

In conclusion, I'm on the fence about adding Even and Odd. They aren't my preference, but if enough people feel strongly about them I will not reject them.

Regarding the inconsistent use of idioms '( N / 2 ) e. ZZ' vs. '2 || N' vs. ..., it might be worthwhile to retrofit theorems to use '2 || N' and '2 || ( N + 1 )' everywhere, so they become the standard idioms people are used to seeing. That would also make it easier to convert them to 'N e. Even', 'N e. Odd' later on if we decide to do that.

OTOH I dislike:

odd = { <. x , y >. | ( x C_ ZZ /\ y e. x /\ ( ( y - 1 ) / 2 ) e. ZZ ) },

This function is not immediately obvious, and it isn't used in the literature AFAIK, so the reader has to look it up. To me, using the somewhat awkward '( ZZ>= ` 7 ) odd N' just to eliminate the conjunct '7 <_ N' seems overly obscure with not much benefit. If I saw that, I would have to stop and unravel it in my head.

Norm

[avekens]

@david-a-wheeler The problem with using || to define even and odd integers is that integers are defined in section "5.4.8 Integers (as a subset of complex numbers)" (already containing theorems about even and odd integers) and || is defined in section "6.1.3 The divides relation". I think the following defining properties (which I would prefer)

• even as ( N / 2 ) e. ZZ
• odd as ( ( N + 1 ) / 2 ) e. ZZ are not more complicated and not much longer than the expressions using ||. Having the definitions using /, many theorems about even and odd numbers can be provided already in "PART 5 REAL AND COMPLEX NUMBERS" and do not need additional material from "PART 6 ELEMENTARY NUMBER THEORY".

[nmegill]

• even as ( N / 2 ) e. ZZ
• odd as ( ( N + 1 ) / 2 ) e. ZZ are not more complicated and not much longer than the expressions using ||.

I see your point and don't disagree.

[avekens]

@nmegill unfortunately, it seems that we wrote/write our comments at the same time...

Compared with using || to define even and odd integers, the term "N e. Even" would have the advantage that N e. ZZ can be derived from it. This is not possible for "2 || N". Look, for example, at ~ oddm1even: ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) ) Having definitions for Even and Odd, this could be written as ( N e. Odd <-> ( N - 1 ) e. Even ), which is shorter and more explicit.

Furthermore, I also do not like such a complicated definition as "odd = { <. x , y >. | ( x C_ ZZ /\ y e. x /\ ( ( y - 1 ) / 2 ) e. ZZ ) }", but I wanted to mention the possibility to have a more specific definition. I think we do not need to discuss this further, unless somebody has good additional arguments for such a definition.

Finally, I do not strongly insist on adding definitions for even and odd integers - I think there are advantages and good reasons for having them. We can wait until others share this point of view (collecting pro's and con's in this issue) , and can decide later if and how such definitions are included in main set.mm. Meanwhile, I'll try to provide a consolidated proposal in my mathbox.

[nmegill]

Compared with using || to define even and odd integers, the term "N e. Even" would have the advantage that N e. ZZ can be derived from it. This is not possible for "2 || N".

Actually, N e. ZZ can be derived from 2 || N (~ dvdszrcl). It can't be derived from 2 || ( N + 1 ), however.

Look, for example, at ~ oddm1even: ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) ) Having definitions for Even and Odd, this could be written as ( N e. Odd <-> ( N - 1 ) e. Even ), which is shorter and more explicit.

N e. ZZ can't be derived from ( N - 1 ) e. Even, so you still need N e. ZZ for the reverse implication.

[david-a-wheeler]

The problem with using || to define even and odd integers is that integers are defined in section "5.4.8 Integers (as a subset of complex numbers)" (already containing theorems about even and odd integers) and || is defined in section "6.1.3 The divides relation"

Good point.

[david-a-wheeler]

I suggest creating a proposal. I think even & odd are common enough that a definition would be sensible, though in the end that's up to Norm. I think the argument for defining "odd" is stronger, but once you define odd it'd be absurd to not define even. At least a single convention would be good, though it's easier to encourage the using definitions than using conventions (they're a little easier to spot). I think it's important that the definition or convention will work unchanged in iset.mm; I expect that would be true for most definitions or conventions.

What is your proposed definition for odd?

(deleted nonsense after I realized it was nonsense.)

[digama0]

I have always had a preference for using 2 || N and -. 2 || N for even and odd. Yes, you also need some kind of closure assumption but you want that in any proof anyway and N e. Odd just means one more thing to rewrite away. I'm not convinced that this definition leads to any proof savings.

[nmegill]

I looked through some even/odd uses again, and I don't think there are enough cases to justify introducing Even and Odd classes at this point. I agree with Mario that 2 || N and -. 2 || N are nice little idioms for even and odd to use as our convention. I don't see people having trouble understanding these, especially if even or odd is mentioned in the comment.

To eliminate the proliferation of different idioms that @avekens mentioned, we would want to have || available wherever we talk about even and odd. One possibility is to move ~ df-dvds up to the "5.4 Integer sets" area with ~ zneo and friends; however, "show usage zneo /recursive" shows only 6 theorems before the number theory section "6.1 Elementary properties of divisibility". So it might make more sense to move those 6 down there instead (assuming I haven't missed any).

A single convention would also make it easier to retrofit Even and Odd if someday we choose to add them.

(As an aside, I noticed is that the mod operation occurs before ~ df-dvds. Since mod is somewhat related to ||, I wonder if moving the mod theorems to the number theory section would be advantageous. I haven't looked at it carefully, though.)

[avekens]

With PR #1690, I provide a proposal for the definitions of even and odd numbers in my mathbox. Here the header comment of section "Even and odd numbers":

Even and odd numbers can be characterized in many different ways. In the following, the definition of even and odd numbers is based on the fact that dividing an even number (resp. an odd number increased by 1) by 2 is an integer, see ~ df-even and ~ df-odd . Alternate definitions resp. charaterizations are provided in ~ dfeven2 , ~ dfeven3 , ~ dfeven4 and in ~ dfodd2 , ~ dfodd3 , ~ dfodd4 , ~ dfodd5 , ~ dfodd6 . Each characterization can be useful (and used) in an appropriate context, e.g. ~ dfodd6 in ~ opoeALT and ~ dfodd3 in ~ oddprmALT . Having a fixed definition for even and odd numbers, and alternate characterizations as theorems, advanced theorems about even and/or odd numbers can be expressd more explicitly, and the appropriate characterization can be chosen for their proof, which may become clearer and sometimes also shorter (see, for example, ~ divgcdoddALT and ~ divgcdodd ).

Revising the existing theorems, I often found simpler or even shorter proofs, because a consistent and systematic "framework" for even and odd numbers was available. This is, in my opinion, an additional argument for having such a definition.

If it is accepted that the definition and related theorems are moved to main set.mm, subsubsection "Definitions and basic properties" can become a subsection named "Even and odd numbers" of section ​"5.4 Integer sets" (because these are special subsets of the integers, like the nonnegative or positive integers). The rest can be placed in later sections, after the required definitions are available.

Concerning the discussion "convention instead of definition": I do not like the informal approach of conventions for mathematical concepts (othe conventions, e.g. naming conventions, are OK!) in such a formal system like Metamath - it must always be checked manually, and is not supported by the tools (e.g. minimize). In addition, it would be a lot of work to revise existing theorems to follow these conventions, requiring to transform the chosen representation into the appropriate one. Therefore, I am still in favour of the "definition way".

[avekens]

Working on Fermat numbers, I stumbled again over theorems for even/odd numbers, using different notations/idioms for even/odd numbers. Therefore, I want to propose to implement Norm's proposal (see comment on 22-Jun-2020), based on the idioms 2 || N and -. 2 || N for even resp. odd numbers (I think these idioms are already used often). I would create a new section "Even and odd numbers" which will contain all available theorems for even and numbers, and maybe transscribe theorems which are currently only available using other idioms for even and odd numbers.

By this, we avoid new definitions, but we will have a single place for the basic theorems on even and odd numbers.

Would this be OK?

[david-a-wheeler]

I'm good with 2 || N as the normal convention for even numbers. We should make sure the convention is documented in several places to make it clear.

I'm less excited about -. 2 || N for odd numbers. It's easily misunderstood, as it requires careful noting of the closure. The "not" is misleading & I'd like things to work relatively easily with intuitionistic logic when that's not too hard (I've learned that "not" is more complicated there!!).

Norman Megill:

Actually, N e. ZZ can be derived from 2 || N (~ dvdszrcl). It can't be derived from 2 || ( N + 1 ), however.

I think 2 || ( N + 1 ) is a clearer way to express "N is an odd number". That doesn't involve carefully checking the class. I haven't tried to create the proof, but it seems to me it should be possible to prove that ( 2 || ( N + 1) ) -> N e. ZZ ) . Why would that be hard?

[digama0]

I prefer -. 2 || N (and my contributions to set.mm have generally treated that version as the preferred way to say "odd"). Intuitionistically, it is the same as 2 || ( N + 1 ) or other notions of oddness, because divisibility on the natural numbers is decidable.

[benjub]

@david-a-wheeler:

it seems to me it should be possible to prove that ( 2 || ( N + 1) ) -> N e. ZZ ) . Why would that be hard?

I think it is a set.mm-convention that the reverse closure for addition and multiplication of complex numbers should not be used since set.mm uses their axiomatic definition, and not their construction from ZF (it is a bit strange to do this only for the complex numbers and not for other things, but @nmegill had reasons to do this, I think mainly due to the commonality of the complex number axioms in textbooks).

[digama0]

it seems to me it should be possible to prove that ( 2 || ( N + 1 ) -> N e. ZZ ) . Why would that be hard?

@benjub is correct, but just to spell out the argument: Because || has domain ZZ X. ZZ, we know ( N + 1 ) e. ZZ. Because + has the domain CC X. CC, either N e. CC or (/) e. ZZ. In the first case, ( ( N + 1 ) - 1 ) = N so N e. ZZ as well. The second case can't be disproven unless we assume ~0ncn which is a forbidden lemma.

[benjub]

+ has the domain CC X. CC

Actually, I think that even this should not be used in set.mm.

[david-a-wheeler]

I hesitate about -. 2 || N because, for example, this is true for 1 / 2 . Yes, it's fine when N is a natural or integer, but I fear that may misleading to humans in context. But if there's no obviously better solution it would of course work. I just want to ensure that humans fully understand the result, not just machines.

[avekens]

There are several advantages to use -. 2 || N as convention for odd numbers compared with 2 || ( N + 1):

• -. 2 || N is already used about 90 times in set.mm, whereas 2 || ( N + 1) occurs only 3 times ( 2 || ( N - 1) occurs 4 times) - a lot of effort would be necessary to convert these 90 theorems...
• -. 2 || N is the natural counterpart of 2 || N, showing the dichonomy of an integer: it is either even or odd. With 2 || ( N + 1 ) one could ask: Is there an M so that 2 || ( N + M ) but neither 2 || N nor 2 || ( N + 1)? (of course there is no such M, but it is not obvious at a first glance)
• to split a proof into two cases (one for even and one for odd numbers), the law of excluded middle (~exmid or ~exmidd) can be used immediately with 2 || N and -. 2 || N. Otherwise, a theorem N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) is required (not difficult to prove, but not existing yet!)

Since N e. ZZ can be derived neither from -. 2 || N nor from 2 || ( N + 1 ), this is no criterion for the decision. But David made a good point: can 1 / 2 be called an odd number only because -. 2 || ( 1 / 2 ) is true?

Nevertheless, I would vote for -. 2 || N as idiom for odd numbers (although I still would prefer explicit definitions of classes Even and Odd, because then we would have N e. Odd -> -. 2 || N and N e. Odd -> 2 || ( N + 1 ) and N e. Odd -> N e. ZZ - but it seems that this is currently no option).

[benjub]

-. 2 || N is already used about 90 times in set.mm, whereas 2 || ( N + 1 ) occurs only 3 times ( 2 || ( N - 1 ) occurs 4 times) - a lot of effort would be necessary to convert these 90 theorems...

If you can change these 7 theorems, that would be great.

a theorem N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) is required (not difficult to prove, but not existing yet!)

Could you add it ? It is worth it, whatever the choice for Even/Odd is.

Nevertheless, I would vote for -. 2 || N as idiom for odd numbers (although I still would prefer explicit definitions of classes Even and Odd, because then we would have N e. Odd -> -. 2 || N and N e. Odd -> 2 || ( N + 1 ) and N e. Odd -> N e. ZZ - but it seems that this is currently no option).

I do not know whether defining Even and Odd is worth it. Going further, one could extend the operations + and x so as to allow the definition of Even = 2 NN (or 2 ZZ) and Odd = 2 NN + 1. If a lot of arithmetic combinatorics is to be done in set.mm, this might be worth it. For instance:

$a setwise = ( x, y, z |-> { t | E. u e. x E. v e. z t = u y v } ) $.
$a +set =  ( x, z |-> setwise `` ( x, +, z ))$. [I don't remember the syntax, maybe something like `(setwise `` + )` may suffice]
$a Even = ( { 2 } xset NN ) $.
$a Odd = ( ( { 2 } xset NN ) +set { 1 } ) $.

Or maybe something simpler using direct image? $a +set = (x , y |-> + " (x X. y) ) $. or something like that.

Edit: I fell prey to the pernicious trap that NN does not denote the natural numbers. Read NN0 in place of NN in the above.

Edit 2: probably better is: $a setwise = ( o |-> ( x, y |-> { t | E. u e. x E. v e. y t = u o v } ) ) $.

[david-a-wheeler]

I yield! :-). The fact that -. 2 || N is so common is a big point in its favor. We do have to be careful that N is an integer or there will be surprising results :-).

[avekens]

@benjub :

-. 2 || N is already used about 90 times in set.mm, whereas 2 || ( N + 1 ) occurs only 3 times ( 2 || ( N - 1 ) occurs 4 times) - a lot of effort would be necessary to convert these 90 theorems...

If you can change these 7 theorems, that would be great.

I checked these 7 theorems, and they are not worth to be changed: either they are already "conversion theorems", or they are lemmata with a special purpose, or they are contained in a (my!) Mathbox.

a theorem N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) is required (not difficult to prove, but not existing yet!)

Could you add it ? It is worth it, whatever the choice for Even/Odd is.

Yes, I will add this with the next PR.

Nevertheless, I would vote for -. 2 || N as idiom for odd numbers (although I still would prefer explicit definitions of classes Even and Odd, because then we would have N e. Odd -> -. 2 || N and N e. Odd -> 2 || ( N + 1 ) and N e. Odd -> N e. ZZ - but it seems that this is currently no option).

I do not know whether defining Even and Odd is worth it. Going further, one could extend the operations + and x so as to allow the definition of Even = 2 NN (or 2 ZZ) and Odd = 2 NN + 1. If a lot of arithmetic combinatorics is to be done in set.mm, this might be worth it. For instance:

$a setwise = ( x, y, z |-> { t | E. u e. x E. v e. z t = u y v } ) $.

In principle, I like this "setwise" approach, but to introduce and use it only for a definition of even and odd numbers seems to use a sledgehammer to crack nuts.

[david-a-wheeler]

I see lots of progress!

I presume the goal is to covert other theorems to this convention (e.g., evenm1odd and evenp1odd) and move them into the main body. Correct?

[avekens]

I think we can close this issue now. The basics are done, and additional theorems (new or converted) can and should be added if required. Especially theorems of my mathbox (or other mathboxes) should be added to the new section if they are used in theorems of other topics. I checked the theorems in my mathbox already, and took over some of these (in converted form), which I though are of enough general interest.

@david-a-wheeler : I think evenm1odd and evenp1odd (in my Mathbox) are already covered by oddm1even resp. oddp1even...