Re: The internal logic of a topos

[Vaughan Pratt <pratt@cs.stanford.edu>]

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
>>
>>
>>
>
>