Timeline for In a constructive order/lattice theory are the arbitrary join and the weak suprema the same?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 14, 2021 at 23:27 | comment | added | ToucanIan | @PeterLeFanuLumsdaine yes the Bishop Analysis book is where I drew the terminology from. | |
| Aug 19, 2021 at 3:22 | comment | added | Peter LeFanu Lumsdaine | @MikeShulman: I’ve come across “supremum” used for the stronger notion (in the reals) in some constructive analysis literature — if I remember right, the Bishop + Bridges book uses that terminology. | |
| Aug 19, 2021 at 0:23 | comment | added | Mike Shulman | @მამუკაჯიბლაძე Yes, I agree -- what Toucanlan calls the "weak supremum" is the same as the join, and I've never heard it called anything but plain "supremum" even constructively. I would call the other something like a "strong supremum"; I'm not sure if there is an additional question being asked about it. | |
| Aug 18, 2021 at 20:35 | comment | added | მამუკა ჯიბლაძე | Unless I misunderstand something fundamental here, it is constructively valid that what you call weak-supremum coincides with the join - in the sense that the set of your weak-suprema is equal to the set of joins (and is a subsingleton). As for your supremum, it is different from these simply because its definition depends on another relation. Maybe @MikeShulman can provide an answer for it. | |
| Aug 18, 2021 at 20:03 | comment | added | Mike Shulman | Note that since your stronger notion of supremum is a formal De Morgan dual of the ordinary one, it can be obtained from the antithesis translation, which also supplies a list of axioms for $\nleq$ (Theorem 8.3). | |
| Aug 18, 2021 at 18:56 | history | edited | LSpice | CC BY-SA 4.0 |
Typo
|
| Aug 18, 2021 at 18:29 | comment | added | ToucanIan | @მამუკაჯიბლაძე The axiomatics of an excess relation should be shared. I originally thought they were unnecesary and beyond the scope of the question. Your are correct in saying the two formulas describe the same object, classically. My question pertains to the distinction that arises due to the intuitionstic interpretation. | |
| Aug 18, 2021 at 18:26 | history | edited | ToucanIan | CC BY-SA 4.0 |
added 1 character in body
|
| Aug 18, 2021 at 18:25 | comment | added | ToucanIan | @PaulTaylor I agree that I need to quantify x, but the choice of an excess relation is neccesary to keep things working in general for posets. | |
| Aug 17, 2021 at 19:09 | comment | added | Paul Taylor | Maybe what you're looking for is the notion of continuous lattice (or just dcpo). | |
| Aug 17, 2021 at 19:04 | comment | added | Paul Taylor | If the leading example is $\mathbb R$ then maybe $\nleq$ is just intended to be $>$. The second displayed formula needs a quantifier over $x$. | |
| Aug 16, 2021 at 16:33 | comment | added | მამუკა ჯიბლაძე | In any case $\forall a\in S(a\le b)$ precisely means that $b$ is an upper bound of $S$. Hence your definition of weak-supremum is the definition of the least upper bound, which is the same as join. It is also what I would call supremum. To clarify its relation with your definition of supremum one would need to know precise axiomatics for your relation $\not\le$. | |
| Aug 16, 2021 at 7:06 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 3 characters in body
|
| Aug 16, 2021 at 6:31 | history | asked | ToucanIan | CC BY-SA 4.0 |