Prove qnnen in iset.mm

[jkingdon]

This is stated in http://us.metamath.org/mpeuni/qnnen.html but the iset.mm proof likely will need to be different in several ways:

• We will presumably prove http://us.metamath.org/mpeuni/xpnnen.html (well, or more exactly we'll show a one to one and onto mapping between NN0 X. NN0 and NN0, which is close enough) by means of the Cantor diagonal function, and explicitly inverting it as shown in https://en.wikipedia.org/wiki/Pairing_function#Inverting_the_Cantor_pairing_function .

  • To do it this way will presumably require a number of http://us.metamath.org/ileuni/df-fl.html related theorems beyond the rationals. I think it is likely true that the floor function from inverting the pairing function is always either irrational (and thus apart from any integer, and thus we can show it has a floor), or rational (in which case all the existing floor related theorems in iset.mm work), although I might have to spend a bit more time with https://en.wikipedia.org/wiki/Quadratic_irrational_number before I understand all the issues here.

  • There are a number of steps involved in showing that this closed form involving floor inverts the pairing function, but hopefully these are straightforward :crossed_fingers:

• Once we have ZZ X. NN ~~ NN there is still another step, which is that there are multiple elements of ZZ X. NN which correspond to a given rational number. Is is true that _om ~<_ A /\ A ~<_ _om -> A ~~ _om ? We know that the full http://us.metamath.org/mpeuni/sbth.html implies excluded middle but some special cases - so far http://us.metamath.org/ileuni/fisbth.html - are provable.

  • Presumably there is some other way to prove this part if we don't get _om ~<_ A /\ A ~<_ _om -> A ~~ _om

[tirix]

Worst case, an obvious way would be to construct a bijection between NN and QQ, which I believe is purely computational and should be feasible in iset.mm. Math Stack Exchange / Math Overflow have examples with e.g. continued fraction expansions.

Otherwise, about inverting the Cantor diagonal function, you could avoid it by using ~ oddpwdc which you already proved in iset.mm, and is very near to a bijection between ( NN X. NN ) and NN. The missing required bijection/equinumerosity between J (odd integers) and NN, resp. NN0 and NN are trivial and probably otherwise useful.

[jkingdon]

using ~ oddpwdc which you already proved in iset.mm, and is very near to a bijection between ( NN X. NN ) and NN.

Oooh, nice idea. This is now submitted as #2597

As for what will be needed to show QQ ~~ NN X. NN, will come back to that. Still not sure what the easiest approach will be. Some of the "purely computational and should be feasible" approaches seemed like they might be a lot of work even if there is no big conceptual hurdle. But we'll see, I'm not sure whether we'll findi something which bypasses that sort of approach.

[tirix]

Nice to see it done! It looks like it was quite trivial.

Yes, unfortunately, "purely computational" does not mean "simple"!

Another way to get a bijection between NN and QQ might be the Calkin-Wilf sequence, where as the corresponding formula also includes an "integral part". That "integral part" could simply be written ( p - ( p mod q ) ) / q for a rational number p / q, but this does not seem to be a "simple" solution either.

[jkingdon]

Nice to see it done! It looks like it was quite trivial.

"Trivial" might be a slight overstatement, because we were missing xpen (that one sort of worried me but the hard part was already in set.mm as xpf1o, and the xpf1o proof copied over with no significant change), and proving the equinumerosity of odd positive integers and positive integers, while not especially difficult, was a new proof of 59 steps many of which involved digging around to see which existing theorems to apply.

On the plus side we already had http://us.metamath.org/ileuni/nn0ennn.html so I didn't need to prove that part.

[tirix]

The artist's work always looks easier for the onlooker ;-)

[digama0]

Regarding special cases of sbth, https://arxiv.org/pdf/1904.09193.pdf is a good reference for the (generally negative) statements about schroeder-bernstein provability in intuitionistic logic. I think it might be useful to formalize some of the things about omniscient sets, e.g. with the definition

A e. Omni <-> A. f : A --> 2o ( E. x e. A ( f ` x ) = (/) \/ A. x e. A ( f ` x ) = 1o )

With that definition, _om e. Omni will be a nice way to write LPO, and the existence of infinite omniscient sets like N_infty will also be useful for these kind of proofs.

[digama0]

Based on that proof, I am fairly sure that _om ~<_ A /\ A ~<_ _om -> A ~~ _om is not provable, because it implies LPO -> EM, which is not as strong as I would like but should not be intuitionistically provable in any case. The argument goes as follows:

Let X = { x e. 1o | p } and let A := X + _om where + is disjoint union. We map _om ~<_ X + _om using the right injection, and X + _om ~<_ 1o + _om ~~ _om since X C_ 1o. So suppose we have f : _om ~~ X + _om. Now if we define g(inl(x)) = (/) and g(inr(n)) = 1o then g o. f : _om --> 2o, so by LPO there are two cases:

1. there exists n such that g(f(n)) = (/). In this case f(n) = inl(x) for some x e. 1o such that p, therefore p.
2. For all n, g(f(n)) = 1o. In this case if we assume p then inl((/)) must be in the image of f, say f(n) = inl((/)) so g(f(n)) = (/), a contradiction. Therefore -. p.

[jkingdon]

Regarding special cases of sbth, https://arxiv.org/pdf/1904.09193.pdf is a good reference for the (generally negative) statements about schroeder-bernstein provability in intuitionistic logic

This is in the iset.mm bibliography as PradicBrown2021, although we currently only cite it in two of the entries of the missing theorems list (sbth obviously but also http://us.metamath.org/mpeuni/fodomr.html which the paper uses to demonstrate how their technique works on something easier than sbth).

As far as I could tell, the proofs in the paper should be not super hard to formalize in iset.mm, but I found it somewhat tricky to read partly because of the disjoint unions. Does set.mm have any disjoint union theorems to adapt, or are we starting from scratch on this point?

[jkingdon]

Based on that proof, I am fairly sure that _om ~<_ A /\ A ~<_ _om -> A ~~ _om is not provable

OK. Part of why I was even asking is the use of the term "countably infinite" in AczelRathjen for A ~~ _om. But maybe they are just borrowing terminology from the non-intuitionistic world which is a bit misleading here.

[jkingdon]

I think it might be useful to formalize some of the things about omniscient sets

This is now an issue at https://github.com/metamath/set.mm/issues/2620

[digama0]

set.mm does not have a very developed notion of disjoint union, but it is a super useful concept that we could borrow. There is actually a definition for disjoint union in set.mm, namely df-cda, although it was not originally intended to be used as such and there are essentially no theorems that use this definition other than to talk about its cardinality.

The basic thing to know about disjoint unions is that A + B is a set with two injections inl : A --> A + B and inr : B --> A + B, and every element of A + B is either inl(a) of some a e. A or inr(b) of some b e. B. (The names inl and inr come from "left/right injection".)

[jkingdon]

set.mm does not have a very developed notion of disjoint union,

So I suspected although the reference to df-cda does indeed make things a fair bit clearer.

I've written up the topic at #2625

[jkingdon]

Here is how AczelRathjen proves QQ ~~ _om (Corollary 8.1.23). First they prove QQ is countable (QQ ~<_ _om) (Corollary 8.1.22; I think we have a lot of choices on this part because we have https://us.metamath.org/ileuni/xpnnen.html ). See subsequent comment concerning their definition of countable, which doesn't necessarily make this part difficult in iset.mm but changes what needs to be done

Then they prove

Corollary: 8.1.13 (ECST + FPA) A set A is in one-to-one correspondence with ℕ iff A is discrete and there exists a surjection f : ℕ --> A such that ∀n ∈ ℕ ∃k ∈ ℕ f (k) ∉ {f (0), . . . , f (n)}.

To be honest I haven't dug into this, or its proof, too deeply yet. But it would appear to be easier to formalize this than any of the other approaches we have identified so far.

[jkingdon]

Based on that proof, I am fairly sure that _om ~<_ A /\ A ~<_ _om -> A ~~ _om is not provable

OK. Part of why I was even asking is the use of the term "countably infinite" in AczelRathjen for A ~~ _om. But maybe they are just borrowing terminology from the non-intuitionistic world which is a bit misleading here.

Ah I think maybe I see what is going on here. Their definition of "countable" is E. f f : _om -onto-> A which I don't think is equivalent to A ~<_ _om (we have https://us.metamath.org/ileuni/exmidfodomr.html which answers part of that question, I also see there are some open - or at least not proved in iset.mm - questions listed in the missing theorems list in mmil.html ).

[jkingdon]

I am partway through formalizing the proof of the following from AczelRathjen:

Corollary: 8.1.13 (ECST + FPA) A set A is in one-to-one correspondence with ℕ iff A is discrete and there exists a surjection f : ℕ --> A such that ∀n ∈ ℕ ∃k ∈ ℕ f (k) ∉ {f (0), . . . , f (n)}.

I have gotten as far as proving the following:

    ennndcfolemg.dceq $e |- ( ph -> A. x e. A A. y e. A DECID x = y ) $.
    ennndcfolemg.f $e |- ( ph -> F : _om -onto-> A ) $.
    ennndcfolemg.P $e |- ( ph -> P e. _om ) $.
    ennndcfolemg $p |- ( ph -> E. g ( g : dom g -1-1-onto-> ( F " P )
        /\ dom g e. suc P ) ) $=

which gives you a g_P for each P e. om and the next step is to form g = `U i e. _om g_i` and prove:

• g is 1-1
• ran g = A
• dom g = _om

So what this is stuck on now is a technical question one which I thought might be obvious but I'm not quite seeing it. How do I form the union of all the g_i 's ? It reminds me of something we do in places like the union in https://us.metamath.org/ileuni/df-irdg.html . And I sort of think that the E. g in the theorem above needs to define a unique value (either by using E! and a more strict set of conditions, or explicitly constructing a mapping, or something).

I keep thinking this is going to be most easily done by building on top of seq or frec (or even https://us.metamath.org/ileuni/tfrcl.html directly with X set to suc _om so that evaluating at _om takes care of the union for us) but I haven't quite yet put together the pieces of how to do that.

My work to date is at https://github.com/jkingdon/set.mm/tree/ennncond

[benjub]

Aren't you missing an $e-hypothesis above ? At first sight, I would explicitly construct the functions (in both directions). After all, having the existence property is one of the benefits of IZF.

[jkingdon]

Aren't you missing an $e-hypothesis above ?

You mean, there is one on the branch which I don't quote here? Yes, but it is unused.

[jkingdon]

Based on that proof, I am fairly sure that _om ~<_ A /\ A ~<_ _om -> A ~~ _om is not provable, because it implies LPO -> EM

This proof is now formalized at https://github.com/metamath/set.mm/pull/3292

[jkingdon]

Status report is that #3363 has most of what we need and I have the proof of qnnen sitting on a branch waiting to put into another pull request after that one is reviewed.

[jkingdon]

Here is the summary of this effort I sent to the metamath mailing list:

I am pleased to report the successful completion of the project to formalize the equinumerosity of the rationals and the natural numbers in iset.mm.[1] This project was begun in earnest in May 2022 with the opening of a github issue[2] which quickly led to discussions and partial results followed by steady progress leading to this result.

Some of the results along the way included:

• realizing that decomposing a natural number into a power of two and an odd divisor could be an important part of the proof,[3]

• defining omniscient set notation and theorems

• defining disjoint union notation and theorems

• two impossibility proofs about the Schroeder-Bernstein theorem, the full theorem (formalizing a 2019 paper) and a special case (we have an impossibility proof of the special case but just how strong it is appears to be an open problem[4]),

• a variety of theorems about countable sets ( for example [5]), and

• an example of a novel way (novel as far as I noticed, anyway) to use the seq notation to define a family of functions both in terms of the previous member of the family and the index within the collection[6]

Many thanks to everyone who collaborated on this, especially Mario Carneiro, Thierry Arnoux, and Benoit Jubin (and probably others I'm forgetting to mention). I never could have done something like this by myself.

I'd also like to make a special acknowledgement to Peter Aczel[7] who with a coauthor wrote the textbook which contained the key lemma for this proof[8]. He died on August 1, 2023 and was a great mathematician and person according to all the tributes I read on Mastodon from people who had worked with him.

[1] https://us.metamath.org/ileuni/qnnen.html

[2] https://github.com/metamath/set.mm/issues/2595

[3] https://us.metamath.org/ileuni/oddpwdc.html

[4] https://mathoverflow.net/questions/451785/how-strong-is-the-schr%c3%b6der-bernstein-theorem-where-one-set-is-the-natural-number

[5] https://us.metamath.org/ileuni/ctm.html

[6] https://us.metamath.org/ileuni/ennnfonelemen.html and other lemmas using the hypotheses here

[7] https://en.wikipedia.org/wiki/Peter_Aczel

[8] https://us.metamath.org/ileuni/ennnfone.html , Corollary 8.1.13 in the cited textbook