A SHEAF REPRESENTATION AND DUALITY FOR FINITELY PRESENTED HEYTING ALGEBRAS

A. M. Pitts in [Pi] proved that HA(fp)(op) is a bi-Heyting category sa tisfying the Lawvere condition. We show that the embedding Phi : HA(fp )(op) --> Sg(P-0,J(0)) into the topos of sheaves, (P-0 is the category of finite rooted posets and open maps, J(0) the canonical topology on Pg) given by H --> HA(H, D(-)) : P-0 --> Set preserves the structure mentioned above, finite coproducts, and subobject classifier; it is al so conservative This whole structure on HA(fp)(op) can be derived from that of Sh(P-0, J(0)) via the embedding Phi. We also show that the eq uivalence relations in HA(fp)(op) are not effective in general. On the way to these results we establish a new kind of duality between HA(fp )(op) and a category of sheaves equipped with certain structure define d in terms of Ehrenfeucht games. Our methods are model-theoretic and c ombinatorial as opposed to proof-theoretic as in [Pi].