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?
Best Answer
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.