UCLA LOGIC COLLOQUIUM
                        Friday, January 19, 2001
                               4:00 p.m.
                       Mathematical Sciences 6627
                                 UCLA

                             DREW MOSHIER

                           (Chapman College)

       "MULTI-LINGUAL SEQUENT CALCULI: PROOF THEORY AND TOPOLOGY"

We introduce Gentzen-style sequent calculi where the formulas on the
left and right of the turnstile need not come from the same logical
system.  In such calculi, sequents can be seen as consequences between
different domains of reasoning.  We discuss the ingredients of proof
theory needed to set up calculi generalized in this fashion.  The
result is the category MLS (multi-lingual sequent calculus) in which
the morphisms are generalized calculi and objects are calculi that
capture "domain internal" reasoning.

To develop a semantic theory for MLS, we turn to spectral theory,
showing that the MLS objects give rise to spectra (spaces of prime
filters) that are, up to homeomorphism, exactly the locally compact,
strongly sober spaces (aka Nachbin spaces).  Such spaces, studied first
by Nachbin in the 1940′s, are arguably the natural T_0 generalizations
of compact Hausdorff spaces.  The morphisms of MLS correspond to
"continuous relations" between these spaces.  In turn, a continuous
relation from X to Y corresponds to a continuous function from X to the
Smyth powerdomain of Y.  Thus we establish category equivalences: MLS
to N^* (the category of Nachbin spaces and continuous relations) and
MLS to the Kleisli category for the Smyth powerdomain monad on N
(Nachbin spaces and continuous functions).

Several useful topological concepts, such as the Hausdorff condition,
zero-dimensionality, functionality of a relation, and properness of a
function (f^-1 preserves the "well-below" relation on opens), have
interesting characterizations within MLS as proof-theoretic properties
of the corresponding sequent calculi.  As time allows, we will discuss
some of these characterizations and demonstrate how proofs within MLS
of familiar topological results shed light on the topological concepts
involved.

_________________________________________________________________________

                           http://www.math.ucla.edu/~hbe/logic.html