Timeline for What can be expressed in and proved with the internal logic of a topos?
Current License: CC BY-SA 3.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Jul 1, 2017 at 19:43 | history | suggested | Matthieu FG |
Added cat log tag
|
|
| Jul 1, 2017 at 19:29 | review | Suggested edits | |||
| S Jul 1, 2017 at 19:43 | |||||
| Apr 10, 2013 at 11:19 | comment | added | Michal R. Przybylek | And if I understand correctly your answer, it was: "Because it is difficult to incorporate external properties of an object with internal reasoning in a topos in a smooth way.". | |
| Apr 10, 2013 at 11:19 | comment | added | Michal R. Przybylek | But now you are not reasoning in the internal logic of Grph, but in the internal logic of all (or any) elementary toposes satisfying your axiom (of course, such logic is pretty useless until you can show any non-trivial interesting facts about objects satisfying your definitions). If I understand correctly the idea underlying the first Francois's question “Why is it important for $V$ to be parameter-free definable?”, it was exactly about “Why it is important for $V$ to be characterisable in the internal logic of a topos?” (cont) | |
| Apr 10, 2013 at 11:18 | comment | added | Michal R. Przybylek | However, both you and Francois felt that such a logic is not really convenient (i.e. showing anything in such a logic is essentially the same as showing that things externally), so you tried to characterise $V$ in the internal logic of any topos and arrived at the axiom “there is a truth value $v \in \Omega$ such that $(v \rightarrow p)=\neg\neg p$ for all $p \in \Omega$”. (cont) | |
| Apr 10, 2013 at 11:17 | comment | added | Michal R. Przybylek | @Andrej, I really like your answer --- and not only :-) because it (together with your conversation with Francois) supports what I have said in the above comments. First, you have externally characterised an object $V$ and added its „external” properties as a kind of axioms to the internal logic of a topos. This roughly corresponds to using the internal logic of category Grph. (cont) | |
| Apr 5, 2013 at 17:23 | vote | accept | David Spivak | ||
| Apr 4, 2013 at 8:57 | comment | added | Andrej Bauer | @Michal: one idea is to use the internal language of a class of categories to prove their general properties. Another idea is to use the internal language of a particular category to prove its properties. @Zhen Lin: you suspect wrong, the game here is precisely to figure out what extras should be added to the general internal language of toposes. The question never said anything about using just "pure" internal language of toposes. | |
| Apr 4, 2013 at 8:47 | answer | added | Andrej Bauer | timeline score: 33 | |
| Mar 21, 2013 at 6:34 | comment | added | Peter LeFanu Lumsdaine | @Zhen Lin: true, the internal logic talks about all objects as though they were just unstructured sets. But one can still often re-express external local notions in these terms — see e.g. the internal construction of a sheafification. Talking about local operators, for instance, isn’t tacking on anything extra: they can be described entirely using the internal logic itself, as constructions based on certain elements of $\mathcal{P}(\Omega)$. (From the internal point of view, they’re just Grothendieck topologies on the terminal category.) | |
| Mar 21, 2013 at 5:43 | answer | added | Vlad Patryshev | timeline score: -5 | |
| Mar 20, 2013 at 0:01 | comment | added | Zhen Lin | Actually, Kuratowski-finiteness can be formulated within geometric logic, and a Kuratowski-finite object in $\textbf{Grph}$ is precisely a graph $G$ with finitely many edges and finitely many vertices, such that the two maps $G(A) \to G(V)$ are surjective. In fact, the finite graphs are precisely the Kuratowski-subfinite objects. | |
| Mar 19, 2013 at 22:05 | comment | added | Michal R. Przybylek | The idea of using an internal logic is not to reason in a particular category, but to perform a uniform reasoning for all categories satisfying some properties --- in exactly the same way as there is no sense to use the logic of a particular Heyting algebra to reason about that Heyting algebra. | |
| Mar 19, 2013 at 21:59 | comment | added | Michal R. Przybylek | On the other hand, for a given graph G, a formula "X is a finite graph" (i.e. X is a subgraph of G and is finite) may be easily constructed by taking the large disjunction over all finite (in any sense) subgraphs of G (in cocomplete toposes, algebras of subobjects have arbitrary disjunctions). | |
| Mar 19, 2013 at 21:58 | comment | added | Michal R. Przybylek | David, it is really hard for me to make your question precise. The reason is that in an internal logic of any category we talk about internal things. For example, there is no internal formula "X is a finite graph" true for all finite (in any sense) graphs, because "X" have to be bounded to the internal structure of an object in the category. (cont) | |
| Mar 19, 2013 at 19:10 | comment | added | Zhen Lin | I suspect the answer to all your questions, other than the one about finiteness, is no. In the internal logic of a topos, objects are "sets" and have no further internal structure. That is not to say we can't tack on extra gadgets to make that internal structure visible – for example, we could introduce some local operators to extract the edge set and the vertex set – but then you may as well work from the external point of view. | |
| Mar 19, 2013 at 17:50 | history | edited | David Spivak | CC BY-SA 3.0 |
added a minor question.
|
| Mar 19, 2013 at 17:34 | history | asked | David Spivak | CC BY-SA 3.0 |