Timeline for Terminology: product on strict preorders corresponding to direct product of preorders?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 26, 2018 at 17:00 | comment | added | Mike Shulman | It's not unheard-of in constructive mathematics to refer to a construction that operates on a "strong complement" by the same name as the corresponding classical operation. For instance, one talks about the "quotient" of a group by an anti-subgroup or a ring by an anti-ideal. Sometimes one adds "strong", e.g. a "strongly extensional" function is one that reflects apartness. Using irreflexive relations rather than reflexive ones is somewhat similar, though not the same (your motivating definition "x<=y iff (x<y or x=y)" is not a complement), so you could say "product" or "strong product". | |
| Mar 27, 2018 at 22:48 | comment | added | Joel David Hamkins | I see. In that context, I would still call it the product order, but I would perhaps emphasize that it suffices to descend in only one coordinate. But since you are in a constructive logic context, I would worry that somehow I have made a fundamental mistake in how the strict orders are related to the reflexive orders, since equality can be weird constructively. And so perhaps you shouldn't listen to me. | |
| Mar 27, 2018 at 22:42 | comment | added | Peter LeFanu Lumsdaine | Sorry, when I wrote “well-orderings” I should have written “well-founded (strict) partial orderings”, where “well-founded” is defined in the constructively most useful sense: “satisfying the well-founded induction principle”. While this product doesn’t preserve totalness of the order, as you point out, it does preserve transitivity and well-foundedness (which can be seen since it embeds into the lex product). | |
| Mar 27, 2018 at 22:36 | comment | added | Joel David Hamkins | With well-orders, then the term "product order" means something else, since one wants $\alpha\cdot\beta$ to mean $\beta$ copies of $\alpha$, using the lexical order, so as to get the product itself as a well order. But of course your order is not generally a well-order, even when both factors are. | |
| Mar 27, 2018 at 22:32 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
edited body
|
| Mar 27, 2018 at 22:31 | comment | added | Peter LeFanu Lumsdaine | Like you, I usually prefer to take the reflexive orders as fundamental. However, I need this operation in a context where it’s much more natural to consider the non-strict order as fundamental (specifically: constructive well-orderings), hence asking this question. | |
| Mar 27, 2018 at 22:31 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 80 characters in body
|
| Mar 27, 2018 at 22:23 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |