MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

They are indeed formally equivalent. See for instance Johnstone: Topos theory, p. 243 but here is a quick explanation. Given a topos $T$ one may define a geometric theory associated to it consisting of formulas describing essentially the topos. More specifically a geometric morphism from another topos $S$ to $T$ is the same thing as a model for the theory in $S$. In particular if $S$ is the category of sets this a set-theoretical model fo the theory. In general the language of the theory has arbitrary disjunctions leading to theories that in general do not have models. However, if the topos is coherent only finite disjunctions are needed and we are in the realm of the Gödel completeness theorem which then can be interpreted as saying that a coherent topos has enough points. Conversely, given a geometric theory one can associate to it a syntactic site whose objects are the formulas. An implication from a disjunction of formulas to a formula is a covering. The topos of sheaves on this site will then be a classifying topos for the theory (i.e., geometric morphisms to it are the same as models). If the theory is finitary (i.e., uses only finite disjunctions) then the topology is coherent and there are models for the theory by Deligne's theorem.
They are indeed formally equivalent. See for instance Johnstone: Topos theory, p. 243 but here is a quick explanation. Given a topos $T$ one may define a geometric theory associated to it consisting of formulas describing essentially the topos. More specifically a geometric morphism from another topos $S$ to $T$ is the same thing as a model for the theory in $S$. In particular if $S$ is the category of sets this a set-theoretical model fo the theory. In general the language of the theory has arbitrary disjunctions leading to theories that in general do not have models. However, if the topos is coherent only finite disjunctions are needed and we are in the realm of the Gödel completeness theorem which then can be interpreted as saying that a coherent topos has enough points. Conversely, given a geometric theory one can associate to it a syntactic site whose objects are the formulas. An implication from a disjunction of formulas to a formula is a covering. The topos of sheaves on this site will then be a classifying topos for the theory (i.e., geometric morphisms to it are the same as models). If the theory is finitary (i.e., uses only finite disjunctions) then the topology is coherent and there are models for the theory by Deligne's theorem.