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 | |
---|---|---|---|---|---|
Apr 5, 2013 at 17:23 | vote | accept | David Spivak | ||
Apr 5, 2013 at 17:21 | history | edited | David Spivak | CC BY-SA 3.0 |
typo
|
Apr 5, 2013 at 6:15 | comment | added | Andrej Bauer | Oh, I am actually grateful to you for drilling into this. I thought it was obvious we wanted to do things internally, so we needed some internal axioms to start from. It's sometimes very hard to guess what the audience is really thinking :-) | |
Apr 4, 2013 at 22:51 | comment | added | François G. Dorais | OK. I see, and you want to prove these in the internal logic. There are many ways to look at this and I now see I was blindsided. Thanks for your patience, Andrej. | |
Apr 4, 2013 at 21:27 | comment | added | Andrej Bauer | If I just have some type $V$ and know nothing about it, that is not very useful. I need to know some properties, so I can start proving things. | |
Apr 4, 2013 at 19:41 | comment | added | François G. Dorais | Ah, I see. You're distinguishing the fact that $G$ is not a variable in the internal logic. I think I'm on the same page now. Still, that doesn't explain why you want $V$ to be definable. | |
Apr 4, 2013 at 19:32 | comment | added | François G. Dorais | But $V$ is a specific graph here. Why is it important that $V$ is definable in the internal logic? Isn't it sufficient that $V$ exists? | |
Apr 4, 2013 at 19:29 | comment | added | François G. Dorais | So, the discrete graphs (as identified by peeking into the objects) are precisely the graphs such that $G \times V \to G$ is epi. There is a simple formula in the internal logic, which evaluates to $\top \in \Omega$ precisely for such $G$. | |
Apr 4, 2013 at 19:11 | comment | added | François G. Dorais | OK. I'm lost now. Are we talking about the same thing? At what point do you need quantification over all types? Let's back up... What is "the projection $G\times V \to G$ is onto"? (I interpret it as the usual way of saying that the projection $G \times V \to G$ is epi in the internal logic.) | |
Apr 4, 2013 at 18:18 | comment | added | Andrej Bauer | I do not understand this parameter business. The internal language of the topos of graphs is a type theory. Every object of the topos is a type, i.e., the internal language is a real mix of semantics and syntax. Also, there is no such thing as a "parameter type". We might do some things schematically by using metavariables in place of types. So perhaps this is different from set theory, where sets are individuals that can be parametrized over in the language. In the topos language, anything of the form "for all types, ..." is not part of the language. | |
Apr 4, 2013 at 17:23 | comment | added | François G. Dorais | OK, I understand. Since it's conservative to add such a constant there is no harm done, but why is it advantageous to add $V$ as a constant rather than use it as a parameter? (Sorry for bugging you with all these questions, I'm just very curious to understand your point of view.) | |
Apr 4, 2013 at 17:04 | comment | added | Andrej Bauer | I do not think of $V$ as a parameter. It is a primitive type in the internal language of the topos of graphs, i.e., it is a constant. It is no more a parameter than the type $N$ of the natural numbers. It is good that we can characterise $V$ up to isomorphism wiht an internal statement, because then its interpretation is fixed. | |
Apr 4, 2013 at 16:11 | comment | added | François G. Dorais | "A graph $G$ is discrete when the projection $G\times V \to G$ is onto" defines discreteness using $V$ as a parameter. Later, you show that there is a parameter-free definition since $V$ is definable (up to isomorphism). Am I missing the point of the last few paragraphs where you argue that $V$ is definable? | |
Apr 4, 2013 at 15:54 | comment | added | Andrej Bauer | I am not sure I understand you. What would be a parameter-non-free definition of an object? | |
Apr 4, 2013 at 15:15 | comment | added | François G. Dorais | That was too brief a question... I didn't read the parameter-free requirement in the op's question. I do find it interesting when something is parameter-free definable and I'm happy you are addressing that issue, but I wonder why you find it such a sticking point. | |
Apr 4, 2013 at 12:23 | comment | added | François G. Dorais | Why is it important for $V$ to be parameter-free definable? | |
Apr 4, 2013 at 9:00 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 144 characters in body
|
Apr 4, 2013 at 8:47 | history | answered | Andrej Bauer | CC BY-SA 3.0 |