From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4334 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: The internal logic of a topos Date: Tue, 18 Mar 2008 11:19:00 -0700 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019878 12799 80.91.229.2 (29 Apr 2009 15:44:38 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:38 +0000 (UTC) To: Categories mailing list Original-X-From: rrosebru@mta.ca Tue Mar 18 19:03:06 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 18 Mar 2008 19:03:06 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Jbjlv-0007L8-6F for categories-list@mta.ca; Tue, 18 Mar 2008 18:55:03 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 98 Original-Lines: 77 Xref: news.gmane.org gmane.science.mathematics.categories:4334 Archived-At: Dear Peter, Your answers come as something of a relief, in that on the one hand it seemed unlikely that every morphism \Omega^n --> \Omega would arise as a Heyting polynomial, yet I didn't see why that should be taken as grounds for calling such counterexamples nonlogical. This was the nature of my concern about Heyting algebras, that they might feature somehow in the antecedent of someone's definition of logicality. I'm more than happy to have Heyting algebras arise as a natural consequence of something even more natural such the notion of topos. I've known and loved Heyting algebras much longer than I have toposes, yet I now see toposes as being prior to Heyting algebras in the causal chain of things, and would be most uncomfortable with a definition of logicality in a topos that arbitrarily took the notion of Heyting algebra as a criterion in any essential way. So I find the thought that there could be logical morphisms in a topos that aren't Heyting polynomials quite comforting, as it tends to put Heyting algebras in their place as themselves a natural *part* of the internal logic of a topos thus understood without however being the whole of it. In a private reply Andrej Bauer made the nice point, obvious in retrospect, that the logical morphisms as the morphisms \Omega^n --> \Omega shouldn't assume n is finite or even discrete, to allow quantification over any type. He also brought up the matter of higher order logic which hadn't been on my agenda but probably should be at some point. Vaughan Prof. Peter Johnstone wrote: > Dear Vaughan, > > I don't think one can give a straight answer to this question: it all > depends on what you mean by `the logic of a topos'. I presume you're > thinking of the fact that, in Set, any function 2^n --> 2 is a polynomial > in the Boolean operations (i.e., is the interpretation of some n-ary term > in the theory of Boolean algebras). One could ask the same question about > a general topos, with `Heyting' replacing `Boolean'; but the answer > would mostly be `no', even for Boolean toposes. On the other hand, one > might well *define* `the internal logic of a topos' as meaning the > collection of all natural operations on subobjects -- that is, the > collection of all morphisms \Omega^n --> \Omega. > > Incidentally, there is nothing unnatural or counterintuitive about `the > notion of internal Heyting algebra: it is a very natural consequence of > the definition of a subobject classifier, see A1.6.3 in the Elephant. > > Peter > > On Sun, 16 Mar 2008, Vaughan Pratt wrote: > >> As I understand the internal logic of a topos it consists of certain >> morphisms from finite powers of Omega to Omega. In the case of Set it >> consists of all such morphisms. For which toposes is this not the case, >> and for those how are the morphisms that do belong to the internal logic >> best characterized? >> >> I do hope it's not necessary to start from the notion of an internal >> Heyting algebra, that sounds so counter to mathematical practice and >> intuition. >> >> If the internal logic consists of precisely those morphisms preserved by >> geometric morphisms this will give me the necessary motivation to go to >> the mats with geometry. >> >> Vaughan >> >> >> > >