The question has been clarified: Andreas Blass in Mathoverflow argues and come to the conclusion: "The moral of this story is that, when deducing geometric sequents from other geometric sequents, we lose no generality by assuming the internal axiom of choice (and, with it, the law of the excluded middle)." Phil Scott does the same in private mail and comes to the conclusion: "So any theorem in that language (geometric theory) true in Sets (or provable using classical logic and AC) is necessarily true in any Grothendieck topos." So, for example, if we want to prove that the validity of some equation follows from the validity of other equations in the real interval [0, 1] (equations in any geometric language interpretable in [0, 1]), then we can proceed by cases, for example, (x = 1) or (not x = 1) (which with an order relation interpretable as the usual order) amounts to (x = 1) or (x < 1). Even though that [0, 1] is not decidable. So this proof which is not valid intuitionistically will in practice be accepted as a proof in the internal language of any topos, since we accept the conclusion as true without requiring any other proof. I confess this comes as a surprise to me. Cheers, as Fred would say. e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]