Timeline for Topos Without point, from the point of view of logic
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Dec 24, 2019 at 13:34 | history | suggested | seldon | CC BY-SA 4.0 |
Spelling & grammar tidy up
|
| Dec 24, 2019 at 7:45 | review | Suggested edits | |||
| S Dec 24, 2019 at 13:34 | |||||
| Jun 8, 2012 at 12:04 | vote | accept | Simon Henry | ||
| Jun 4, 2012 at 2:00 | answer | added | François G. Dorais | timeline score: 23 | |
| Jun 4, 2012 at 0:19 | history | edited | François G. Dorais |
edited tags
|
|
| Jun 3, 2012 at 22:25 | comment | added | David Roberts♦ | "if you have boolean logic and axiom of choice then you can internalize any set theoretical proof", yes, but you need to use the stack semantics, not just the usual internal logic (aka Mitchell-Benabou languge+Kripke-Joyal semantics) - see ncatlab.org/michaelshulman/show/stack+semantics. This takes care of the unbounded replacement and separation. The only thing you are lacking to actually define ETCS (a set theory) is well-pointedness and an axiom of infinity/nno. | |
| Jun 3, 2012 at 21:34 | comment | added | Zhen Lin | Johnstone gives such a theory/topos in Part D of the Elephant, Example 3.4.14, but I must admit I don't understand it... | |
| Jun 3, 2012 at 20:39 | comment | added | Simon Henry | To Anton Festisov : not internal to X, but in Y which as axiom of choice and hence boolean logic. My idea (which of course has to be false) was that if you have boolean logic and axiome of choice then you can internalize any set theoretical proof. to Zhen Lin : Yes of course, but I haven't been able to exhibit example of such "improbable" situation... | |
| Jun 3, 2012 at 19:47 | comment | added | Zhen Lin | Well, when you have eliminated the impossible, whatever is left, however improbable, must be the truth. Therefore the proof of the inconsistency of your geometric theory $T$ cannot be internalised to $Y$, and this must be because it uses principles that are not available in a general boolean topos with choice. (For example, in ZF, we have unbounded replacement and unbounded separation...) | |
| Jun 3, 2012 at 19:42 | comment | added | Anton Fetisov | Just wondering. Why is the proof, that X has no set-theoretic models, internal to X? | |
| Jun 3, 2012 at 17:35 | history | asked | Simon Henry | CC BY-SA 3.0 |