Should NN_infinity be defined in terms of NN0 or _om ?

[jkingdon]

There has been a little discussion of this but I wanted to raise it to a larger audience because (a) the best answer is not completely clear to me, and (b) unlike definitions where we can prove two definitions are equivalent, this one affects what the elements of ℕ_∞ are, so alternative definitions end up being isomorphic rather than equivalent and expressions like x ∈ ℕ_∞ behave differently depending on what definition we choose.

I'll start with the non-metamath literature (as best as I can summarize it). Every source I can remember assumes that 2 = { 0 , 1 } and that 2^ℕ is the set of sequences whose values are zero or one. The question is how to best express that in iset.mm.

The current definition of ℕ_∞ is:

df-nninf $a |- NN+oo = { f e. ( 2o ^m _om ) |
  A. i e. _om ( f ` suc i ) C_ ( f ` i ) } $.

This is in some sense the most literal translation of the informal 2^ℕ notation - we have https://us.metamath.org/ileuni/df2o3.html which fits the 2 = { 0 , 1 } idea.

However, in some ways including theorems which connect this with https://us.metamath.org/ileuni/df-xnn0.html this means a number of conversions between _om and NN0 , for example at https://us.metamath.org/ileuni/fxnn0nninf.html . So the question is whether we'd prefer this definition:

df-nninfNN $a |- NN+oo = { f e. ( { 0 , 1 } ^m NN0 ) |
  A. i e. NN0 ( f ` ( i + 1 ) ) <_ ( f ` i ) } $.

There is at least some precedent for this - for example https://us.metamath.org/mpeuni/eulerpartgbij.html .

I guess in general my assumption is we are better off working with NN0 once we get to the point of iset.mm where we can. And that the only real downside in this case is that { 0 , 1 } is more characters than 2o. But are there implications I'm not seeing?

[benjub]

Thanks for opening this issue, raised in https://github.com/metamath/set.mm/pull/2692#discussion_r925765636. I think the second option is more natural (pun intended), and makes the definition of the canonical injection I : xNN0 --> NNinfty more straightforward. I should have caught it earlier, but I think it would still be a reasonble amount of work to do the shift.

[digama0]

I think the _om definition is better because it allows reasoning that makes use of this set to be placed early and have fewer dependencies. It's more of a foundational tool than anything else, and it doesn't play well with the set ( NN0 u. { +oo } ) that you might otherwise think it is if it is placed in the xre section. No matter which definition you take you won't have the finite elements of NN+oo being the numbers in NN0, so you will have an explicit embedding function anyway.

The set 2o is also used as a canonical two-element set (aka "bool") for the purposes of definitions like df-omni as well.

[jkingdon]

I think the _om definition is better because it allows reasoning that makes use of this set to be placed early and have fewer dependencies.

If that is what we decide, I suppose we should

• move https://us.metamath.org/ileuni/df-nninf.html , https://us.metamath.org/ileuni/nnnninf.html , https://us.metamath.org/ileuni/infnninf.html to before the real number construction (perhaps in the "Omniscient sets" section with https://us.metamath.org/ileuni/df-omni.html ).
• keep https://us.metamath.org/ileuni/fnn0nninf.html through https://us.metamath.org/ileuni/inftonninf.html where they are (they are already separated from the df-nninf.html group because they depend on more integer theorems - one obvious one is https://us.metamath.org/ileuni/frechashgf1o.html ).

[jkingdon]

I should have caught it earlier, but I think it would still be a reasonble amount of work to do the shift.

No worries, there is nothing much wrong with having some theorems to look at and experience using them to help inform this sort of decision. I do agree that we shouldn't let the amount of work be the controlling factor (if we think something we didn't initially choose is really better, we can always make a plan to change things like this, whether suddenly or bit by bit).

[benjub]

Ok. (The explicit embedding is the I : xNN0 --> NNinfty I mentioned above, which is already in iset.mm.) On the other hand, it's a bit strange to have NNinfty being more basic than NN.

Of course, the question would not arise if NN was genuinely equal to _om. This is sometimes (often?) done when constructing the number systems, e.g. define ZZ from NN, define the injection i : NN --> ZZ, and then say that what we defined was a temporary set ZZ' and the real ZZ is actually NN \cup ZZ' \setminus i(NN). And so on up to CC or beyond. What do you think about that approach (not as a plan for right now, obviously, but rather as a long term goal) ? A problem I can see with that is that it doesn't play well with the choice made in set.mm that the empty set is used as the default value for many things (another strange choice in my opinion).

[digama0]

Of course, the question would not arise if NN was genuinely equal to _om. This is sometimes (often?) done when constructing the number systems, e.g. define ZZ from NN, define the injection i : NN --> ZZ, and then say that what we defined was a temporary set ZZ' and the real ZZ is actually NN \cup ZZ' \setminus i(NN). And so on up to CC or beyond. What do you think about that approach (not as a plan for right now, obviously, but rather as a long term goal) ?

It's not an option in intuitionistic logic, because it needs LEM to cut out each isomorphic copy and put the old set in. For example you would need to identify the rational reals and this is not decidable.

[jkingdon]

It's not an option in intuitionistic logic, because it needs LEM to cut out each isomorphic copy and put the old set in. For example you would need to identify the rational reals and this is not decidable

Yeah, I was thinking the same thing. I guess the same problem would also happen when going from reals to complex numbers - whether the imaginary part is zero would not be decidable.

[benjub]

Right, I hadn't thought of that. And I guess since we want set.mm and iset.mm to stay as similar as possible, it's not a good idea to do it in set.mm either ? (the case of NNinfty is moot there, but I mean, in general)

If I understand correctly, the main problem is that intuitionistically, we cannot define addition on "ZZ \cup QQ \setminus i(ZZ)": if q, r are not in the image of ZZ, then we have do decide whether q +_{QQ} r is an integer, but this is not possible (whereas in the three other cases where at least q or r is in the image of integers, we can define their sum (and we can do such a definition by cases). Correct ?

[digama0]

For NN0 in ZZ or ZZ in QQ it's fine since the predicate x e. ZZ (assuming x e. QQ) is decidable, but you can't do QQ in RR or RR+ in RR or RR in CC because in each case the predicate of being in the subset is not decidable. This then causes problems showing that the new definition is isomorphic to the one you would have without the carved out subset.

To give a simple example: pi and e are both definitely irrational, but it is an open question whether their sum is irrational. To define addition on irrational numbers you would have to map the ones that turn out to be rational into the other set, but we have no way to decide this.

[benjub]

Ah, I didn't remember if the divide was from ZZ to QQ or from QQ to RR, but obviously if you know a rational, you can bound it away from zero, so all is fine. So the (first) problem you encounter is indeed defining the sum when both summands are not in the smaller set.

[jkingdon]

Here's another conundrum. How do we formalize the following (from the [PradicBrown2021] paper)?

define S : N∞ → N∞ by setting S(p)(0) = 1 and S(p)(n + 1) = p(n).

If N∞ were defined in terms of NN0 this could be (I think, my apologies if there are errors as I haven't formalized this yet):

S = ( p e. NN+oo |-> ( i e. NN0 |-> if ( i = 0 , 1 , ( p ` ( i - 1 ) ) ) ) )

but we don't have a easy way to subtract one from an element of _om (even one known to be nonzero), so I suppose we'd end up with:

G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )
S = ( p e. NN+oo |-> ( i e. _om |-> if ( i = (/) , 1o ,
   ( p ` ( `' G ` ( ( G ` i ) - 1 ) ) ) ) ) )

[digama0]

The predecessor operation on _om is U. x.

[jkingdon]

The predecessor operation on _om is U. x.

Ah, OK, as seen in, for example, https://us.metamath.org/ileuni/onsucuni2.html

[david-a-wheeler]

It's not an option in intuitionistic logic, because it needs LEM to cut out each isomorphic copy and put the old set in. ...

... And I guess since we want set.mm and iset.mm to stay as similar as possible, it's not a good idea to do it in set.mm either ?

I agree. We can't be slavish about it, but I think we should prefer to keep set.mm and iset.mm as similar as reasonably possible. If nothing else, keeping them similar is pragmatic - it simplifies moving theorems between them (where true and sensible). There are some philosophical arguments for it as well, but the pragmatic argument is enough for me :-).