Timeline for What can be expressed in and proved with the internal logic of a topos?
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 22, 2020 at 23:13 | comment | added | Vlad Patryshev | Peter, this definition sounds new to me; I liked it a lot; thank you! | |
| Jan 21, 2020 at 19:56 | comment | added | Peter LeFanu Lumsdaine | sorry, yes, I usually work with toposes with an NNO, and forget not everyone assumes that. In the absence of an NNO, you can still define an equivalent sense of finiteness, but the definition is slightly more complex: $X$ is finite precisely if it satisfies “$X$ is Kuratowski-finite [i.e. any subobject of $PX$ containing singletons and closed under binary joins must contain the maximal subobject], and any two elements of $X$ are either equal or not equal” in the internal logic. | |
| Jan 21, 2020 at 19:33 | comment | added | Vlad Patryshev |
@PeterLeFanuLumsdaine Nat is not necessarily present in a topos. Of course the idea about an isomorphism between a [0..n] and an X does define finiteness. But I don't see how logic is involved here. We don't even need a subobject classifier for that.
|
|
| Jan 20, 2020 at 12:30 | comment | added | Peter LeFanu Lumsdaine | Many of the usual definitions of finite can be written in the internal logic of a topos. For instance, the formula “there is some n in Nat such that there is some bijection between X and {1,…,n}” will hold (in the internal language of Set) exactly if X is finite in the usual sense. | |
| Jan 19, 2020 at 4:15 | comment | added | Vlad Patryshev | @PeterLeFanuLumsdaine can you give more details on how logic can help distinguish a finite set from an infinite set? I don't see how. | |
| Mar 21, 2013 at 6:29 | comment | added | Peter LeFanu Lumsdaine | I’m not sure I follow your second paragraph. The logic of Set certainly can tell the difference between a finite and an infinite set. Of course, it doesn’t do so in a novel way, since the logic of Set is just (a large fragment of) the logic we reason in all the time. But that novelty is exactly what can get more interesting when one moves to a different topos! | |
| Mar 21, 2013 at 5:43 | history | answered | Vlad Patryshev | CC BY-SA 3.0 |