Timeline for Mathematics without the principle of unique choice
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 9, 2018 at 18:15 | comment | added | Mike Shulman | Hmm... maybe I understand better now what you are getting at: PUC could fail in other ways than the one I had in mind. I'll update the question to clarify what I'm asking about. | |
| Jun 9, 2018 at 11:03 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
corrected typo
|
| Jun 9, 2018 at 10:29 | comment | added | Franka Waaldijk | I also disagree that the Baire space (natural) apartness is an extra structure. It is in fact the intuitionistic (and constructive) way of handling equality. It corresponds rather precisely I would say with the linear logic inequality that you mention. And I also already mentioned that with definitions as given in my thesis, PUC can hold with a different interpretation of $\exists!$. But as you know I'm enthusiastic about your linear logic paper, so I'll try to sum all this up in a fair second update. | |
| Jun 8, 2018 at 20:52 | comment | added | Franka Waaldijk | Hm, now I don't understand! Your comment strongly suggests that you already believe so much in PUC, that you feel a relation which satisfies PUC should be called a function (I disagree). And from there, that what I call a function should be called a 'strongly extensional' function... I think it would be clearer if you could phrase your question a bit differently, because I feel I gave a perfectly correct answer which just doesn't happen to be in the direction which you were expecting... Well, I don't really mind, but it might help someone to come up with the answer you're looking for :-) | |
| Jun 8, 2018 at 20:35 | comment | added | Mike Shulman | By contrast, in the linear logic of arxiv.org/abs/1805.07518, inequality relations on every set are "built into the logic", but in this case they are also built into the notion of "unique existence", so that PUC can hold (but doesn't have to). | |
| Jun 8, 2018 at 20:34 | comment | added | Mike Shulman | Ah, I see. I don't really think the question of whether all functions should be assumed strongly extensional is much related to PUC, though. In particular, in intuitionistic logic the presence of an apartness relation is extra structure on a set, and so a notion like "strongly extensional" which depends on such structure can't sensibly appear in a foundational principle like PUC. | |
| Jun 6, 2018 at 22:32 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
expanded for clarity
|
| Jun 6, 2018 at 21:57 | comment | added | Franka Waaldijk | I was probably too brief, I will expand a bit more in an update. | |
| Jun 6, 2018 at 3:50 | comment | added | Mike Shulman | I don't understand what you are saying; the ZF-definition of function makes PUC true by definition. | |
| Jun 5, 2018 at 20:06 | history | answered | Franka Waaldijk | CC BY-SA 4.0 |