TY - JOUR

T1 - Entailment systems for stably locally compact locales

AU - Vickers, Steven

PY - 2004/1/1

Y1 - 2004/1/1

N2 - The category SCFrU of stably continuous frames and preframe ho-momorphisms (preserving ¯nite meets and directed joins) is dual to the Karoubi envelope of a category Ent whose objects are sets and whose
morphisms X ! Y are upper closed relations between the ¯nite powersets FX and FY . Composition of these morphisms is the \cut composition" of Jung et al. that interfaces disjunction in the codomains with conjunctions in the domains, and thereby relates to their multi-lingual sequent
calculus. Thus stably locally compact locales are represented by \entailment systems" (X; `) in which `, a generalization of entailment relations,is idempotent for cut composition.
Some constructions on stably locally compact locales are represented
in terms of entailment systems: products, duality and powerlocales.
Relational converse provides Ent with an involution, and this gives a simple treatment of the duality of stably locally compact locales. If A and B are stably continuous frames, then the internal preframe hom A t B is isomorphic to e A B where e A is the Hofmann-Lawson dual.
For a stably locally compact locale X, the lower powerlocale of X is shown to be the dual of the upper powerlocale of the dual of X.

AB - The category SCFrU of stably continuous frames and preframe ho-momorphisms (preserving ¯nite meets and directed joins) is dual to the Karoubi envelope of a category Ent whose objects are sets and whose
morphisms X ! Y are upper closed relations between the ¯nite powersets FX and FY . Composition of these morphisms is the \cut composition" of Jung et al. that interfaces disjunction in the codomains with conjunctions in the domains, and thereby relates to their multi-lingual sequent
calculus. Thus stably locally compact locales are represented by \entailment systems" (X; `) in which `, a generalization of entailment relations,is idempotent for cut composition.
Some constructions on stably locally compact locales are represented
in terms of entailment systems: products, duality and powerlocales.
Relational converse provides Ent with an involution, and this gives a simple treatment of the duality of stably locally compact locales. If A and B are stably continuous frames, then the internal preframe hom A t B is isomorphic to e A B where e A is the Hofmann-Lawson dual.
For a stably locally compact locale X, the lower powerlocale of X is shown to be the dual of the upper powerlocale of the dual of X.

UR - http://www.scopus.com/inward/record.url?scp=2442624815&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2004.01.033

DO - 10.1016/j.tcs.2004.01.033

M3 - Article

VL - 316

SP - 259

EP - 296

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -