Dear Vaughan, I don't think one can give a straight answer to this question: it all depends on what you mean by `the logic of a topos'. I presume you're thinking of the fact that, in Set, any function 2^n --> 2 is a polynomial in the Boolean operations (i.e., is the interpretation of some n-ary term in the theory of Boolean algebras). One could ask the same question about a general topos, with `Heyting' replacing `Boolean'; but the answer would mostly be `no', even for Boolean toposes. On the other hand, one might well *define* `the internal logic of a topos' as meaning the collection of all natural operations on subobjects -- that is, the collection of all morphisms \Omega^n --> \Omega. Incidentally, there is nothing unnatural or counterintuitive about `the notion of internal Heyting algebra: it is a very natural consequence of the definition of a subobject classifier, see A1.6.3 in the Elephant. Peter On Sun, 16 Mar 2008, Vaughan Pratt wrote:
As I understand the internal logic of a topos it consists of certain morphisms from finite powers of Omega to Omega. In the case of Set it consists of all such morphisms. For which toposes is this not the case, and for those how are the morphisms that do belong to the internal logic best characterized?
I do hope it's not necessary to start from the notion of an internal Heyting algebra, that sounds so counter to mathematical practice and intuition.
If the internal logic consists of precisely those morphisms preserved by geometric morphisms this will give me the necessary motivation to go to the mats with geometry.
Vaughan