Re: Kripke semantics and Alexandrov topology

Re: Kripke semantics and Alexandrov topology

[Vaughan Pratt]

YES, because it doesn't matter.

Bill's question is not well framed (besides the potential for ambiguity in
the answer arising from "Am I wrong to say that").  Is the question is about
intuitionistic logic/Heyting algebra itself, or its domain of discourse,
ostensibly posetal Kripke structures?  If the former, then the canonical
models obtained by dualizing Heyting algebras are Stone(-Priestley(-Heyting))
spaces, whose topology is compact, the logic being finitary.  If the latter,
and if Stone topology is more bother than discrete topology (surely the case
from a pedagogical standpoint), then the Alexandrov topology is preferable;
this in general is not compact.

But variations between topologies having the same specialization order
describe only what points are approached in the (infinite) limit.  Since
intuitionistic logic is entirely finitary and does not concern itself with
limiting processes, it doesn't matter what topology Kripke semantics is
based on.  Hence YES, Bill is wrong to imply that it does matter (other
than for the secondary reasons discussed above).

Best, Vaughan

>YES, because, given a poset X, the category of sheaves over X equipped 
>with the Alexandrov topology is equivalent to the category of 
>*covariant* functors  X --> Set.  A very important, basic fact, which 
>is at the foundation of a lot of things in topos theory and computer 
science.
>
>Cheers,
>François
>>
>>    I have been re-reading the chapter on intuitionism
>> in Goldblatt's book, specifically the section on
>> Kripke semantics. Am I wrong to say that Kripke
>> semantics is based on the Alexandrov topology
>> generated by the underlying poset?
>>
>> Regards, Bill

Re: Kripke semantics and Alexandrov topology

[Francois Lamarche]

YES, because, given a poset X, the category of sheaves over X equipped 
with the Alexandrov topology is equivalent to the category of 
*covariant* functors  X --> Set.  A very important, basic fact, which 
is at the foundation of a lot of things in topos theory and computer 
science.

Cheers,

François

> Hello,
>
>    I have been re-reading the chapter on intuitionism
> in Goldblatt's book, specifically the section on
> Kripke semantics. Am I wrong to say that Kripke
> semantics is based on the Alexandrov topology
> generated by the underlying poset?
>
> Regards, Bill
>

Kripke semantics and Alexandrov topology

[Galchin Vasili]

Hello,

   I have been re-reading the chapter on intuitionism
in Goldblatt's book, specifically the section on
Kripke semantics. Am I wrong to say that Kripke
semantics is based on the Alexandrov topology
generated by the underlying poset?

Regards, Bill