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
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
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
participants (2)
-
Galchin Vasili -
Stephen Schanuel