Is there anything standard in the literature about this?

I don't know; I think you know more about proof theory and non-topos-theoretic intuitionistic logic than I do. But it seems like a reasonable thing to mention.

]]>Should we clarify that a consistent logic is proof-theoretically two-valued if the only closed terms for propositions are true and false? Then even intuitionistic propositional logic (but not intuitionistic higher-order logic) is two-valued. And then a model is two-valued if the only propositions in it are true and false, so intuitionistic propositional logic has no complete two-valued models. (Of course, it has an incomplete two-valued model, the two-valued model of classical logic, and classical logic has many models that are not two-valued.) Then we can extend the internal/external distinction between boolean and two-valued that is clear for toposes. Is there anything standard in the literature about this?

]]>I wrote two-valued topos to help me tighten up Mike's latest edit to cocomplete well-pointed topos.

]]>