From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5065 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Sheaf toposes and chain-complete posets Date: Mon, 27 Jul 2009 14:45:38 +0200 Message-ID: Reply-To: Andrej Bauer NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1248731600 31676 80.91.229.12 (27 Jul 2009 21:53:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 27 Jul 2009 21:53:20 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Mon Jul 27 23:53:13 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MVY88-0002Dn-Vd for gsmc-categories@m.gmane.org; Mon, 27 Jul 2009 23:53:13 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MVXIQ-0005XO-Br for categories-list@mta.ca; Mon, 27 Jul 2009 17:59:46 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5065 Archived-At: Dear categorists, I am trying to wrap my mind around the concept of an (internal) chain-complete poset in a sheaf topos. I am failing to come up with an example of a poset that is chain-complete but is not complete. The precise definitions of "chain-complete" in the internal language are as follows. Suppose (P, <=) is a poset in a topos. For C in Omega^P, let chain(C) be the statement forall x, y : P, (x in C and y in C) ==> (x <= y or y <= x) Then P is chain-complete if forall C : Omega^P, chain(C) ==> exists x : P, x is the supremum of C where "x is the supremum of C" means the usual thing. So what does a chain-complete poset which isn't complete look like? Since I am used to arguing intuitionistically, it would help a lot if there were some (possibly infinitary) logical principle or schema that is typical of sheaf toposes -- something expressing the local nature of validity. Such a principle ought to be invalid in realizability toposes, so perhaps it should express or imply cocompleteness (with respect to Set). But would that be of any help for arguing in the internal language? With kind regards, Andrej Bauer [For admin and other information see: http://www.mta.ca/~cat-dist/ ]