From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2176 Path: news.gmane.org!not-for-mail From: Peter Lietz Newsgroups: gmane.science.mathematics.categories Subject: Re: Realizability and Partial Combinatory Algebras Date: Thu, 13 Feb 2003 18:34:40 +0100 (CET) Message-ID: References: <1045047509.3e4a28d50d86b@mail.inf.ed.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241018467 2870 80.91.229.2 (29 Apr 2009 15:21:07 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:21:07 +0000 (UTC) To: categories Original-X-From: rrosebru@mta.ca Thu Feb 13 14:55:15 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 13 Feb 2003 14:55:15 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18jOTp-00071L-00 for categories-list@mta.ca; Thu, 13 Feb 2003 14:53:05 -0400 In-Reply-To: <1045047509.3e4a28d50d86b@mail.inf.ed.ac.uk> X-MailScanner: Found to be clean Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 31 Original-Lines: 68 Xref: news.gmane.org gmane.science.mathematics.categories:2176 Archived-At: Dear John, would you please fill me in on either (or better yet, both) of the following points, as I failed to figure them out by myself: 1.) Let A be a c-pca. If I understand correctly, you say that the indexed poset that maps a set I to the set of maps from I to P(A), endowed with the usual entailment relation [ for phi,psi: I -> P(A), phi |- psi iff there is an r in A such that for all i in I and for all a in phi(i), ra exists and ra is in psi(i) ] is indeed an indexed Heyting-Algebra and that the implication of phi,psi : I -> P(A) is given by (phi=>psi)(i) = {r in A | forall a in phi(i). rka in psi(i)}. My question is: given phi, psi and theta such that theta /\ phi |- psi over I via some realizer r, what would be a realizer witnessing theta |- phi => psi with => defined in the way you indicated? 2.) Given a c-pca A, you say that A equipped with the application function a.b := akb is a (proper) pca. What exactly would be a good S combinator for the new algebra ? (You wrote that some additional care is needed to construct S) Many thanks in advance, Peter ps: in an attempt to give the shortest possible of the many reasons, why Heyting algebras do not form a CCC I suggest: The one-element poset is the terminal Heyting algebra. Therefore, every object has at most one global section. Hence, there can only be one morphism between each two Heyting algebras, as the global sections of the exponent correspond to the morphisms (which is absurd). pps: The one-element poset *is* a Heyting-algebra, in fact all topologies are. On Wed, 12 Feb 2003, John Longley wrote: > As far as I can see, Peter Johnstone is essentially correct. > Even without the condition "sxy is defined", Asm(A) is locally cartesian > closed (though the correct construction of local exponentials is not quite > the "obvious" one), and its exact/regular completion is a topos. Peter > Lietz's argument (which is the one that occurred to me too) seems to fail > at his point 1: to get a realizer for the mediating morphism from the > true local exponential to the object he constructs, one actually needs > the condition "sxy is defined". For the record, in Peter L's example, > the true exponential m^m in the slice over Nabla(P(A)), for instance, ....