Re: More Topos questions ala "Conceptual Mathematics"

[Vaughan Pratt <pratt@CS.Stanford.EDU>]

>From: Stephen Schanuel
>you'll learn why Boolean algebra, so familiar in sets, needs
>to be replaced by Heyting algebra in more general toposes.

I would expand this beyond Heyting algebras to quantales, residuated monoids,
etc.  See http://boole.stanford.edu/pub/seqconc.pdf for an example of a
situation, namely event structures as a model catering simultaneously to
concerns of branching time and "true" concurrency, that has traditionally
been handled in a Boolean way.  That paper extends event structures to three-
and four-valued logics of behavior.

This particular extension (expansion, augmentation) doesn't generalize the
two-valued Boolean logic of event structures to Heyting algebras.  There are
exactly two three-element idempotent commutative quantales.
Obviously the three-element Heyting algebra is one of them, and this HA
does find application in drawing a distinction between accidental and
causal temporal precedence, a topic Haim Gaifman looked into around 1988.

The other, which isn't a Heyting algebra, is at the core of the notion of
transition as the intermediate state between "ready" and "done," more on
this in the above-cited paper.

This is not to say that there is no topos-theoretic approach to this
extension.  In particular the above paper briefly mentions the presheaf
category Set^FinBip where FinBip is the category of finite bipointed sets,
as a notion of cubical set.  Cubical sets certainly provide one algebraically
attractive model of true concurrency that works roughly the same way as
the one based on this 3-element quantale---both of them entail cubical
structure---but I've been finding the latter a more elementary and natural
tool for working with cubes, at least for my purposes---homologists may
find limitations that I don't seem to run into.  An advantage of Set^FinBip
is that it accommodates cyclic structures (iterative concurrent automata),
whereas the one based on 3' as I've been calling this 3-element quantale
works with acyclic cubical sets, calling for iteration to be unfolded, much
as formal languages "are" unfolded grammars.

(Come to think of it, I don't know anything about the subobject classifier of
Set^FinBip.  If someone has a succinct description of it I'd be very grateful.)

The main point here is that there *is* a logic of behavior that is
close to but not quite intuitionistic, at least not in the strict Heyting
algebra sense.  Furthermore it is not a question of just finding the smallest
Heyting algebra in which the above quantale embeds, since there isn't one that
preserves the ordered monoid structure: a Heyting algebra must have its monoid
unit at the top, which 3' as "the other three-element quantale" doesn't.  So
whatever relationship obtains between the subobject classifier of Set^FinBip
and 3', it's not an ordered-monoid embedding of the latter in the former.

See http://boole.stanford.edu/pub/seqconc.pdf for more details.

Vaughan