From: Stephen Schanuel you'll learn why Boolean algebra, so familiar in sets, needs to be replaced by Heyting algebra in more general toposes.

I would expand this beyond Heyting algebras to quantales, residuated monoids, etc. See http://boole.stanford.edu/pub/seqconc.pdf for an example of a situation, namely event structures as a model catering simultaneously to concerns of branching time and "true" concurrency, that has traditionally been handled in a Boolean way. That paper extends event structures to three- and four-valued logics of behavior. This particular extension (expansion, augmentation) doesn't generalize the two-valued Boolean logic of event structures to Heyting algebras. There are exactly two three-element idempotent commutative quantales. Obviously the three-element Heyting algebra is one of them, and this HA does find application in drawing a distinction between accidental and causal temporal precedence, a topic Haim Gaifman looked into around 1988. The other, which isn't a Heyting algebra, is at the core of the notion of transition as the intermediate state between "ready" and "done," more on this in the above-cited paper. This is not to say that there is no topos-theoretic approach to this extension. In particular the above paper briefly mentions the presheaf category Set^FinBip where FinBip is the category of finite bipointed sets, as a notion of cubical set. Cubical sets certainly provide one algebraically attractive model of true concurrency that works roughly the same way as the one based on this 3-element quantale---both of them entail cubical structure---but I've been finding the latter a more elementary and natural tool for working with cubes, at least for my purposes---homologists may find limitations that I don't seem to run into. An advantage of Set^FinBip is that it accommodates cyclic structures (iterative concurrent automata), whereas the one based on 3' as I've been calling this 3-element quantale works with acyclic cubical sets, calling for iteration to be unfolded, much as formal languages "are" unfolded grammars. (Come to think of it, I don't know anything about the subobject classifier of Set^FinBip. If someone has a succinct description of it I'd be very grateful.) The main point here is that there *is* a logic of behavior that is close to but not quite intuitionistic, at least not in the strict Heyting algebra sense. Furthermore it is not a question of just finding the smallest Heyting algebra in which the above quantale embeds, since there isn't one that preserves the ordered monoid structure: a Heyting algebra must have its monoid unit at the top, which 3' as "the other three-element quantale" doesn't. So whatever relationship obtains between the subobject classifier of Set^FinBip and 3', it's not an ordered-monoid embedding of the latter in the former. See http://boole.stanford.edu/pub/seqconc.pdf for more details. Vaughan