Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz <lietz@mathematik.tu-darmstadt.de>]

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