27
$\begingroup$

There are several books and articles on topos theory which mention the internal language, but I can't manage to see the big picture from any of them. I would like a soft explanation of how the entities in the definition of an elementary topos come to together and give rise to this internal logic.

Does everything rely on the internal Heyting algebra structure of the subobject classifier?

How does one go from this to reasoning naturally like with sets?

$\endgroup$
4
  • 4
    $\begingroup$ Have you looked in Maclane and Moerdijk's book? As you say, you get the Heyting operations on subobjects from those on the subobject classifier...for quantifiers, you need adjoints to pullback along morphisms, and given all these operations, you can construct subobjects using the exact same formulas as in the category of sets. Perhaps you could clarify where you're stuck? $\endgroup$
    – Kevin Arlin
    Dec 15, 2015 at 18:22
  • $\begingroup$ @KevinCarlson It was hard for me to extract what you just wrote from Maclane and Moerdijk. An expanded version of your comment is exactly what I'm looking for - a clear overview. If you could post a more detailed answer describing briefly how exactly these things work that would be perfect! $\endgroup$
    – Arrow
    Dec 15, 2015 at 23:24
  • $\begingroup$ I don't have the time to write a detailed answer right now, but might later. Just a quick reply: "How does one go from this to reasoning naturally like with sets?" The answer is the soundness theorem: If $\varphi$ is a formula which constructively (more precisely, intuitionistically) implies a further formula $\psi$, then $\mathcal{E} \models \varphi$ ("$\varphi$ holds in the topos $\mathcal{E}$") implies $\mathcal{E} \models \psi$. This is why you can import "all of constructive mathematics" into the internal universe of a topos. $\endgroup$
    – Ingo Blechschmidt
    Dec 16, 2015 at 12:50
  • 1
    $\begingroup$ Dear @IngoBlechschmidt, do you by any chance have some time to write a detailed answer? $\endgroup$
    – Arrow
    Jun 4, 2017 at 18:17

0

Reset to default

You must log in to answer this question.