Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Exercise 11.6 seems to need WLPO not LPO #1162

Open
jkingdon opened this issue Aug 4, 2024 · 3 comments
Open

Exercise 11.6 seems to need WLPO not LPO #1162

jkingdon opened this issue Aug 4, 2024 · 3 comments

Comments

@jkingdon
Copy link
Contributor

jkingdon commented Aug 4, 2024

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

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
@jkingdon jkingdon mentioned this issue Aug 4, 2024
Open
@mikeshulman
Copy link
Contributor

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
Copy link
Contributor Author

jkingdon commented Aug 5, 2024

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
Copy link
Contributor

I think my suggested change would keep the intended punch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jkingdon @mikeshulman