* Kripke semantics and Alexandrov topology
@ 2003-04-22 21:48 Galchin Vasili
2003-04-24 6:45 ` Francois Lamarche
0 siblings, 1 reply; 3+ messages in thread
From: Galchin Vasili @ 2003-04-22 21:48 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Kripke semantics and Alexandrov topology
2003-04-22 21:48 Kripke semantics and Alexandrov topology Galchin Vasili
@ 2003-04-24 6:45 ` Francois Lamarche
0 siblings, 0 replies; 3+ messages in thread
From: Francois Lamarche @ 2003-04-24 6:45 UTC (permalink / raw)
To: categories
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
>
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Kripke semantics and Alexandrov topology
@ 2003-04-24 22:54 Vaughan Pratt
0 siblings, 0 replies; 3+ messages in thread
From: Vaughan Pratt @ 2003-04-24 22:54 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2003-04-24 22:54 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-04-22 21:48 Kripke semantics and Alexandrov topology Galchin Vasili
2003-04-24 6:45 ` Francois Lamarche
2003-04-24 22:54 Vaughan Pratt
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).