search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

Add WLPO to iset.mm #4040

Closed jkingdon closed 1 month ago

jkingdon commented 1 month ago

We already have Omni and Markov (where _om e. Omni is LPO and _om e. Markov is MP). Given that precedent, the obvious notation for WLPO is _om e. WOmni (well, or some other name for WOmni but if there is an established name for what I am calling "weakly omniscient" I haven't seen it).

Includes a few theorems analogous to ones we have for Omni and Markov, and the usual theorem relating the three, A e. Omni <-> ( A e. WOmni /\ A e. Markov )

jkingdon commented 1 month ago

I'm going to merge this now rather than go to greater lengths to solicit feedback (especially about the phrase "weakly omniscient" and the notation WOmni). If we think of something better it shouldn't be too hard to change later.