Dear Peter, Your answers come as something of a relief, in that on the one hand it seemed unlikely that every morphism \Omega^n --> \Omega would arise as a Heyting polynomial, yet I didn't see why that should be taken as grounds for calling such counterexamples nonlogical. This was the nature of my concern about Heyting algebras, that they might feature somehow in the antecedent of someone's definition of logicality. I'm more than happy to have Heyting algebras arise as a natural consequence of something even more natural such the notion of topos. I've known and loved Heyting algebras much longer than I have toposes, yet I now see toposes as being prior to Heyting algebras in the causal chain of things, and would be most uncomfortable with a definition of logicality in a topos that arbitrarily took the notion of Heyting algebra as a criterion in any essential way. So I find the thought that there could be logical morphisms in a topos that aren't Heyting polynomials quite comforting, as it tends to put Heyting algebras in their place as themselves a natural *part* of the internal logic of a topos thus understood without however being the whole of it. In a private reply Andrej Bauer made the nice point, obvious in retrospect, that the logical morphisms as the morphisms \Omega^n --> \Omega shouldn't assume n is finite or even discrete, to allow quantification over any type. He also brought up the matter of higher order logic which hadn't been on my agenda but probably should be at some point. Vaughan Prof. Peter Johnstone wrote:
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