Sheaves also appear in logic as carriers for models of set theory. Beginning with several examples, it explains the underlying ideas of topology and sheaf theory as well as the general theory of elementary toposes and geometric morphisms and their relation to logic.