Use of exponentiation in topos logic 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?
 A: 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.
A: 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.
