Exercise 11.6 seems to need WLPO not LPO

[jkingdon]

My metamath contributors and I have formalized, not exactly Exercise 11.6 as stated, but something pretty close. What we have is:

• for part (ii) we were able to prove WLPO and not LPO (by itself this means little, as perhaps a different proof would yield LPO): https://us.metamath.org/ileuni/nconstwlpo.html
• for part (i) we were able to prove a stronger version of the exercise where the existence of the function follows form analytic WLPO not full excluded middle: https://us.metamath.org/ileuni/dceqnconst.html

Unless there is some subtlety here (analytic vs non-analytic omniscience principles, IZF set theory versus type theory, etc), this means that LPO, as specified in Exercise 11.6(ii), is not attainable. I'm not proposing alternate wording because I'm not sure what the best fix is. As far as I noticed, the HoTT book doesn't currently mention WLPO at all and perhaps it is too much of a digression to get into it. I suppose perhaps the exercise could be worded as decidability of real number equality (assuming that is indeed doable and easy enough for an exercise - our proof of Exercise 11.6(ii) is for WLPO not analytic WLPO)

cc @benjub

[mikeshulman]

Hmm, perhaps the intent was for part (ii) to say something like "$f(x)\neq 0$ if and only if $x \# 0$"? Then it ought to be equivalent to analytic LPO, right?

[jkingdon]

Hmm, perhaps the intent was for part (ii) to say something like "$f(x)\neq 0$ if and only if x#0"? Then it ought to be equivalent to analytic LPO, right?

Seems like it would be.[1]

The punch of the original exercise, at least for me when I first read it, is "whoa, some functions, which seem perfectly normal to the classical mathematician, can't even be shown to EXIST" (that is, it goes further than whether such functions are "well-behaved" in various senses). How best to keep that counterintuitive factor while also fixing the WLPO vs LPO issue I'm not sure I see as clearly.

[1] I formalized one direction just to check. (details might only be understandable to people who know metamath iset.mm notation but I'll post it here just in case it helps anyone, or future me).

  ${
    $d ph x $.  $d x y z $.
    nconstlpo.f $e |- ( ph -> F : RR --> ZZ ) $.
    nconstlpo.rp $e |- ( ph -> A. x e. RR ( x =//= 0 <-> ( F ` x ) =/= 0 ) ) $.
    $( A variation of ~ nconstwlpo which implies analytic LPO (real number
       trichotomy).  (Contributed by Jim Kingdon, 4-Aug-2024.) $)
    nconstlpo $p |- ( ph
        -> A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) ) $=
      ( vz cv cc0 cap wbr wdc cr wral clt wceq wcel wa cz dcbid w3o wb ad2antrr
      cfv wne simplr ffvelrnd 0zd zdceq syl2anc dcned simpr mpbird ralimdva mpd
      wf ex reap0 breq1 cbvralv bitri sylibr ) ABHZIJKZLZBMNZVCCHZOKVCVGPVGVCOK
      UACMNBMNZAVDVCDUDZIUEZUBZBMNVFFAVKVEBMAVCMQZRZVKVEVMVKRZVEVJLVNVIIVNVISQI
      SQVIIPLVNMSVCDAMSDUPVLVKEUCAVLVKUFUGVNUHVIIUIUJUKVNVDVJVMVKULTUMUQUNUOVHG
      HZIJKZLZGMNVFBCGURVQVEGBMVOVCPVPVDVOVCIJUSTUTVAVB $.
  $}

[mikeshulman]

I think my suggested change would keep the intended punch.