re: More Topos questions ala "Conceptual Mathematics"

[Galchin Vasili <vngalchin@yahoo.com>]

Hello,

   I have been reading up on the Curry-Howard
isomorphism. In the last chapter of "Conceptual
Mathematics" Lawvevre and Schanuel say that the
logical connectives are completely analogous to
categorical operations x, map object and +. Is this an
oblique reference to the Curry-Howard isomorphism?

Regards, Bill Halchin

--- Stephen Schanuel <schanuel@adelphia.net> wrote:
>     Probably it's easiest to try to define
> implication yourself, and then
> you'll see that it is just what 'Conceptual
> Mathematics' says -- but if you
> need more help:
>
>     'Implication' is supposed to be a binary
> operation on Omega, i.e. a map
> from OmegaxOmega to Omega. How can we go about
> specifying such a map?
>
>     Well, a map from any object X to Omega amounts
> (by the universal
> property) to a subobject of X, so we're looking for
> a subobject of
> OmegaxOmega, i.e. a monomorphism with codomain
> X=OmegaxOmega. Now how can we
> go about specifying a nonomorphism with a given
> codomain X? Perhaps the
> simplest way is to specify two maps with domain X
> and common codomainY; then
> the equalizer of these will do.
>
>     See if you can think of two maps from
> OmegaxOmega to Omega whose
> equalizer seems to capture the intuitive notion of
> 'implication'. It might
> help to start with a simple case, the category of
> sets, where Omega is just
> the two-element set with elements called T (true)
> and F (false). (If you
> have ever seen 'truth tables', you will see that
> what you are looking for is
> also called the 'truth table for implication', but
> if you haven't seen
> these, please ignore this remark.) If you succeed in
> specifying the pair of
> maps, you will have learned much more than you can
> by reading further; but
> if after trying you are still stuck, then read on.
>
>     The desired two maps from OmegaxOmega to Omega
> are:
> (1) projection on the first factor, and
> (2) conjunction, which was defined in the paragraph
> just preceding the one
> you're stuck on.
>
>     I hope you managed to find these maps, but even
> if you didn't, you can
> now have fun by looking at the maps conjunction,
> imlication, negation, etc,
> in irreflexive graphs (and other simple toposes) and
> comparing these with
> those in sets; you'll learn why Boolean algebra, so
> familiar in sets, needs
> to be replaced by Heyting algebra in more general
> toposes.
>
>     Good luck in your studies!
>
> Yours,
> Steve Schanuel
> ----- Original Message -----
> From: "Galchin Vasili" <vngalchin@yahoo.com>
> To: <categories@mta.ca>
> Sent: Wednesday, February 19, 2003 7:16 PM
> Subject: categories: More Topos questions ala
> "Conceptual Mathematics"
>
>
> >
> > Hello,
> >
> > 1) In the very last chapter (Session 33 "2:
> Toposes and logic" of
> "Conceptual Mathematics"  where the authors cover
> topoi, they define  '=>'
> for the internal Heyting algebra of Omega:
> >
> > "Another logical operation is 'implication', which
> is denoted '=>'. This
> is also a map Omega x Omega->Omega, defined as the
> classifying map of the
> subobject S 'hook' Omega x Omega determined by the
> all those <alpha, beta>
> in Omega x Omega such that alpha "subset of" beta."
> >
> > Starting from "subobject S 'hook" ......" I got
> totally lost. I am
> frustrated because I know this is crucial to
> understanding why Omega is an
> internal Heyting algebra, so any help would be
> appreciated. (I am assuming
> that alpha and beta are subojects of Omega???).
> >
> > 2) In the same Session 33 on pg 350 is a set
> "rules of logic". These are
> exactly the axioms for a Heyting algebra, yes?
> >
> >
> >
> > Regards, Bill Halchin
> >
> >
> >
> >
>
>


__________________________________
Do you Yahoo!?
Yahoo! Calendar - Free online calendar with sync to Outlook(TM).
http://calendar.yahoo.com