The type ℕ∞ has decidable equality iff WLPO holds

[jkingdon]

This is mentioned as background knowledge at https://mathstodon.xyz/@MartinEscardo/113001536506411322 but I don't see it proved in iset.mm, or an issue for it.

In iset.mm notation this would be

A. x e. NN+oo A. y e. NN+oo DECID x = y <-> _om e. WOmni

[benjub]

/!\ Spoiler alert below the dots /!\

...

...

...

Forward implication:
Given a proposition $f \colon \omega \to 2$, define $g \in \mathbb{N}_\infty$ by $g(n) \coloneqq \min ( f(i) \mid i \leq n)$.
Then, $g$ is the point at infinity iff $\forall n \in \omega f(n)=1$.

Backward implication:
Decidability of equality with the point at infinity follows from the fact that $\mathbb{N}_\infty \subseteq \Omega$, and decidability of equality in $\mathbb{N}$ has been proved.

[jkingdon]

Backward implication:
Decidability of equality with the point at infinity follows from the fact that N ∞ ⊆ Ω

Not sure it is the same proof you have in mind, but there's a proof of this at #4469

, and decidability of equality in N has been proved.

OK.....

But how does this help us prove _om e. WOmni -> A. x e. NN+oo A. y e. NN+oo DECID x = y?

The statement that an element of NN+oo is either finite or infinite would be equivalent to .... uh LPO I guess it would be. Or perhaps you had something else in mind?

[digama0]

Given two elements of NN+oo (that is, increasing functions om -> 2o), we can compare them pointwise and return 1 if they are equal and 0 if not. Then the resulting function will be identically 1 iff the elements are equal.

[jkingdon]

Given two elements of NN+oo (that is, increasing functions om -> 2o), we can compare them pointwise and return 1 if they are equal and 0 if not. Then the resulting function will be identically 1 iff the elements are equal.

I'll try to formalize this argument. Seems like it should work.

[benjub]

I don't remember what I had in mind, but there was probably a gap anyway. Mario's proof above is in any case the way to go.

[jkingdon]

Given two elements of NN+oo (that is, increasing functions om -> 2o), we can compare them pointwise and return 1 if they are equal and 0 if not. Then the resulting function will be identically 1 iff the elements are equal.

I'll try to formalize this argument. Seems like it should work.

Formalized at #4473

[jkingdon]

I posted about this theorem at https://sfba.social/@soaproot/113659190325018274