From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2157 Path: news.gmane.org!not-for-mail From: Peter Lietz Newsgroups: gmane.science.mathematics.categories Subject: Re: Realizibility and Partial Combinatory Algebras Date: Sun, 9 Feb 2003 20:09:26 +0100 (CET) Message-ID: References: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241018454 2765 80.91.229.2 (29 Apr 2009 15:20:54 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:54 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Sun Feb 9 15:50:14 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 09 Feb 2003 15:50:14 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18hxOX-0000XN-00 for categories-list@mta.ca; Sun, 09 Feb 2003 15:45:41 -0400 In-Reply-To: Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 12 Original-Lines: 64 Xref: news.gmane.org gmane.science.mathematics.categories:2157 Archived-At: On Fri, 7 Feb 2003, Prof. Peter Johnstone wrote: > Of course I know about the Hyland--Ong paper: indeed, I reviewed it for > Zentralblatt. However, the point I was trying to make was that the > construction of the quasitopos of A-valued assemblies, and the proof > that its effectivization is a topos, make no use whatever of the > condition that Sxy is always defined. The fact that the tautology > ((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to > be realized by S when p is empty has no effect on this construction, > because one never has to deal with "propositions" having an empty > set of realizers. Dear Professor Johnstone, I obviously assumed strongly that you know the Hyland-Ong paper and was hence rather puzzled by what I mistakenly took for your question. As to the question regarding A-valued assemblies when A is a c-pca, I think I can give a justification for the axiom "Sab exists" as well. I claim that if the axiom "Sab exists" is absent, then the resulting category of A-valued assemblies is not a quasi-topos. One can form the category of A-valued assemblies and it is regular and cartesian closed. However, the realizers for the evaluation maps and also the construction of a realizer for the transpose of a map may exist, but one has to make a case analysis as to whether the source object is inhabited or not. Therefore it seems unlikely that the category is locally cartesian closed, as these operations cannot be carried out in a uniform manner. If this is the case then the category's exact completion is not a topos. I am aware that this argument is pretty vague. For a rigorous proof I would try to show that IF the subobjects of the threefold product of Nabla(P(A)) do form a Heyting-algebra, which if I am right is one of the requirements for a quasi-topos, THEN "Sab always exists". I would go about it as follows. 1. Show that the exponent subobject of two subobjects of an object is - if it exists - constructed as in the "unconditional" pca case. 2. Define the subobject m:S->Nabla(P(A)) with S = {M\subseteq A | M inhabited} and the set of realizers of M w.r.t. S being M (and m being the obvious map). 3. Interpret the S-tautology of intuitionistic propositional logic taking u,v and w as the pullbacks of m along the 1st, 2nd and 3rd projection of Nabla(P(A)) x Nabla(P(A)) x Nabla(P(A)), respectively. 4. Observe that it is the full subobject and use the reasoning of the Hyland-Ong paper to show that "Sab always exists". Should I be wrong, this would also be good news in a way, because it would imply that the standard construction of A-valued assemblies could be used for semantic strong normalization proofs instead of the more complicated construction of modified assemblies. Best regards, Peter Lietz