Dear Professor Vickers,

I'm very obliged for your e-mail, for prof. Kearnes' lucid answer (btw, is this
theorem a part of the folklore or can it be attributed to a particular author?)
to my main problem and for prof. Resende's terminological comment. Sorry I
couldn't answer ealier, I was absent.

Concerning your question about references for the proof of the theorem I
attributed to prof. Esakia: I found it in his book 'Algebry Heytinga I. Teoria
dvoistvennosti' ('Heyting algebras I. Duality Theory') published in Tbilisi,
1985 (in Russian). I am not sure if Leo Esakia himself would claim the theorem
his own. The references to the suitable chapter mention 'interesting and deep
results related to superintuitionistic logics [logical counterpart of the theory
of Heyting algebras, roughly speaking] obtained by A. Kuznetsov and his
students'; the only paper mentioned by name is Kuznetsov's work from 1971. Some
of the results from Esakia's book can be also found in his earlier paper,
published in 1974 in Soviet Mathematics Doklady.


Actually, I wouldn't be that much surprised if some of the results known now as
'part of the computer science folklore of algebraic dcpos' (btw, could you
recommend me a good handbook or monograph of the subject? this Raney's work or
something newer?) turned out to have originated in Kuznetsov's school. I have,
however, no material to support such claims, so my guess can be wrong. If you
want to investigate that, you can contact Leo Esakia by mail:
esakia@.... It is also not unlikely that such theorems could have been
proven independently in various centres. Communication between the two sides of
the Iron Curtain was far from being smooth.

Your comment on a constructive way of defining spatiality raises an interesting
point but the thing is that I'm rather interested in the theory of (varieties
of) Heyting algebra and metatheory of extensions of intuitionistic logics from a
classical point of view. It seems to me that in this field you cannot insist too
much on being constructive. Even most basic theorems like Birkhoff's 1944
theorem that every algebra is a subdirect product of subdirect irreducibilities
or Jonsson's 1967 lemma on congruence-distributive varieties use some form of
Zorn's lemma or the Axiom of Choice.

Actually, the main reason why I posted my question was my interest in an old
problem posed by Kuznetsov: for every variety of Heyting algebras, can every
equation which fails to hold be refuted in a spatial locale from the variety? If
there are any theorems e.g., of the computer science folklore of algebraic dcpos
which can be helpful in answering this question, I would be very obliged for any
information.

Best regards,
Tadeusz Litak



>X-UIDL: ^Mk!!3ZL"!cAV!!0p9!!
>Date: Mon, 01 Dec 2003 10:16:25 +0000
>From: Steve Vickers <s.j.vickers@...>
>User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.3)
Gecko/20030312
>X-Accept-Language: en-us, en
>MIME-Version: 1.0
>To: LITAK Tadeusz Michal <litak@...>
>CC: univalg@yahoogroups.com
>Subject: Leo Esakia
>Content-Transfer-Encoding: 7bit
>
>Dear Tadeusz,
>
>Do you have references for Esakia's proof of the result you mentioned
>(i.e. that if in a complete Heyting algebra every element is a join of
>completely join irreducibles then the cHa is spatial)?
>
>Results like this came to me as part of the computer science folklore of
>algebraic dcpos (directed complete partial orders), and their origin is
>obscure to me.
>
>Mind you, with hindsight I suspect it's not hard to deduce this
>particular result from Raney's work (1953) on completely distributive
>lattices. (Completely distributive lattices are topologies for the more
>general continuous dcpos.)
>
>On a related point, your characterization of spatiality (every element
>is an inf of meet irreducibles) for complete Heyting algebras is not
>constructively valid. Constructively you need to find points as
>completely prime filters instead of meet irreducibles. (Classically they
>are in bijection - given a completely prime filter, take the join of the
>elements not in it.) Then the criterion becomes that, for any elements a
>and b, if every completely prime filter containing a also contains b
>then a <= b.
>
>Regards,
>
>Steve Vickers.
>