God also made the continuum: Representation of the reals as a final coalgebra

One elegant definition of the nonnegative integers standardly ordered is as the initial algebra of the functor 1;X, ordinal sum (concatenation) with the singleton. We give a construction dual to this for the nonnegative reals standardly ordered, namely as the final coalgebra of the functor X.w, ordinal (lexicographic) product with the natural numbers. This gives a sense in which analysis is dual to enumeration. Baire space and Cantor space are similarly obtained as final coalgebras of elaborations of this functor, respectively X'.w (order dual) and 1;(X.w), sitting on either side of the continuum. When combined as 1;(X'.w) the two elaborations cancel to restore the continuum.

Full completeness of the multiplicative linear logic of Chu spaces.

Linear logic was introduced by Girard in 1987 as a resource-sensitive "logic behind logic". Chu spaces are a common generalization of topological spaces/finite dimensional vector spaces/abelian groups, etc. represented in terms of the relationship between their points and open sets/functionals/group characters, etc.

We put the syntactic proofs of the theorems of multiplicative linear logic in one-one correspondence with their semantic proofs defined as logical transformations between operations on Chu spaces. One can view a result of this nature as a refinement of ordinary completeness to a characterization of proofs rather than of mere provability.

Joint work with Harish Devarajan, Gordon Plotkin, and Vaughan Pratt.

Full completeness of the multiplicative linear logic of Chu spaces (end)

Second half of talk on Chu spaces (see previous abstract).

Last modified: Fri May 28 00:06:44 PDT 1999