From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2352 Path: news.gmane.org!not-for-mail From: Galchin Vasili Newsgroups: gmane.science.mathematics.categories Subject: re: More Topos questions ala "Conceptual Mathematics" Date: Tue, 10 Jun 2003 14:23:50 -0700 (PDT) Message-ID: <20030610212350.52749.qmail@web12205.mail.yahoo.com> References: <000701c2d910$a0faa480$39a14244@grassmann> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1241018598 3722 80.91.229.2 (29 Apr 2009 15:23:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:18 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Jun 12 13:02:13 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Jun 2003 13:02:13 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19QUPZ-0006Fn-00 for categories-list@mta.ca; Thu, 12 Jun 2003 12:54:49 -0300 In-Reply-To: <000701c2d910$a0faa480$39a14244@grassmann> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 43 Original-Lines: 130 Xref: news.gmane.org gmane.science.mathematics.categories:2352 Archived-At: 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 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" > To: > 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 > 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