I clarify my previous question with a simple example. It is also a simpler (and more general) question whose resolution resolves the previous question on interpreting a theory in another. QUESTION: If an equation (in an algebraic theory) can be proved to hold by any means (choice, excluded middle, etc) in any Set-Model, then it holds in any model in any topos. No need to do an intuitionistic proof ? For example if we use the excluded middle in any totally ordered poset, (this includes the real interval [0, 1]) Example: The reference is the book [CDM] ``Algebraic foundations of Many-valued Reasoning?? Kluver Academic Publishers (2000) Consider the theory of MV-algebras. By a standard choice argument we have: 1) Every MV-algebra is a subalgebra of a product of MV-chains with the pointwise structure. Corollary. Given any two terms p(x, y, ... z) and q(x, y, ... z), the equation p(x, y, \ldots z) = q(x, y, \ldots z) holds in every MV-algebra if and only if it holds in every MV-chain. (denote "@" for $\oplus$, and "*" for $\odot$ 2) x @ y < 1 ==> x * y = 0 holds in any MV-chain. (very easy, [CDM] 1.6.1 page 27). 3) $x @ 0 = x$ (axiom, [CDM] page 7), $1 @ x = 1$ (very easy, [CDM] page 9). 4) The equation (a): (x @ y) @ (x * y) = (x @ y) holds in any MV-algebra. proof: By 1) it is enough to prove it for MV-chains: case (x @ y) = 1: we have 1 @ (x * y) = 1 case (x @ y) < 1: we have (x @ y) @ 0 = (x @ y) (by 2) both cases hold by 3). 5) By the completeness theorem the equation (a) follows from the axioms of the theory, (intuitionistically or classically ?) thus the equation should hold in (the internal language) for any MV-algebra object in any Grothendieck topos ? 5) Also we can argue via the presheaf classifying topos of the theory of MV-algebras and come to the same conclusion ? Is 5) valid ? Notice that, besides the use of choice in 1), if we have already a chain, we do not need 1), but we are using an exclude middle in 4) to prove the equation (invalid for example in the MV-chain [0, 1], the real interval in the object of reals of the topos). Never the less, the equation holds in [0, 1] but the proof does not ? e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]