Might I recommend Sheaves in Geometry and Logic by MacLane and Moerdijk. To quote bits from the blurb:

Sheaves also appear in logic as carriers for models of set theory as as for the semantics of other types of logic.

The applications to axiomatic set theory and the use in forcing ...are then described.

...the construction of topoi related to geometric languages and logic.

(Edit: Ed Dean beat me to it, but only just)