4
$\begingroup$

I'm learning about topos theory and its many uses in (intuitionistic) logic. The definition of an elementary topos $\mathbf{C}$ requires the category to have exponentiation, that is, given $\mathbf{C}$-objects $A$ and $B$, there exists another $\mathbf{C}$-object $B^A$ which is "the object of all $A\to B$ morphisms".

Now, when developing the propositional logic, the valuations, the meet/join/negation/implication operations in the algebra of subobjects I haven't seen the exponential construction at all.

I'm wondering why is it crucial that a categroy has exponential objects (or power objects) in order to "do" strong enough internal logic, or similar enough to the $\mathbf{Set}$ topos internal logic.

What construction, rule of inference, quantification, formula or whatever, needs exponentiation/power objects?

$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

The exponential $B^A$ corresponds to the implication (or function space) $A \Rightarrow B$. The reason you have not seen exponentiation explicitly appear in the treatment of propositional logic is that in that setting you can define implication in terms of negation and disjunction, i.e. as $\neg A \lor B$. However, in other settings (such as constructive logic), this is not possible, and implication must be given separately.

There is a distinction to be drawn, though, between the logic of the lattice of subobjects (giving the propositional logic definable within the topos) and the internal language of the topos itself (which is a higher-order logic). We may have exponentials of the subobjects and not general exponentials in the category itself, or vice versa. The exponential is important in toposes for giving constructions of function spaces (like in the category of sets), which is exactly what makes the internal language "higher-order" logic.

If you want to learn more about exponentiation and implication (or, more generally, function types in a type theory), the place to start is the correspondence between the simply-typed $\lambda$-calculus and cartesian-closed categories. The internal language of toposes subsumes the simply-typed $\lambda$-calculus, so this is a simpler starting point.

This other answer about the distinction between $\vdash$ and $\Rightarrow$ in categorical logic might also be helpful.

$\endgroup$
2
  • 1
    $\begingroup$ I don't think this really gets at the issue. In a topos, you're not talking about $A\implies B$ where $A,B$ are objects, but where they are subobjects of some fixed $C$. And then $A^B$, the exponential object in the topos, is not related to $A\implies B$ in the subobject lattice. $\endgroup$ Commented Dec 7, 2020 at 17:42
  • 1
    $\begingroup$ @KevinArlin: thanks for raising this point. I think there are two aspects: one is the relationship between exponentials of subobjects and exponentials in the topos, and one is the role of exponentials in a general logic or type theory. I think we focused on different aspects of the question, though I have now tried to expand upon the other aspect in my answer. $\endgroup$ Commented Dec 7, 2020 at 17:56
4
$\begingroup$

Your observation that Cartesian closedness of $\mathbf C$ is not relevant to getting a Heyting algebra structure on the subobject lattices, and even the adjoints $\forall$ and $\exists$ to the substitution morphisms between subobject lattices, is entirely correct. Indeed, many non-Cartesian closed $\mathbf C$ have a perfectly good internal first-order logic (namely, Heyting categories.)

Instead, the core reason for the cartesian closedness of a topos is to allow the internalization of higher-order logic. In a mere Heyting category, you can't define, for instance, a topological space. In a topos, you can formalize things like "a family of subsets of $X$ closed under intersection and finite union" as a nice subobject of $\mathcal P(X)$, where the "powerobject" of $X$ is defined as $\Omega^X$, $\Omega$ being the subobject classifier required in the definition of a topos.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.