Re: Realizibility and Partial Combinatory Algebras

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

On Fri, 7 Feb 2003 jvoosten@math.uu.nl wrote:
>
> I think the relevance of this condition (Sxy defined) is explained in the
> Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization
> Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they
> have a definition of "c-pca" which is just omitting this requirement.
> They show that the standard P(A)-indexed preordered set, for a c-pca A,
> can fail to be a tripos. So the condition IS used.
>
I hope Jaap and Peter will forgive me for saying that I think they
missed the point of my message. (Perhaps it's my fault -- with hindsight,
I wasn't as clear as I should have been. I really ought to stop trying
to reply to things like this late at night -- although, as you'll see
from the header of this message, I'm doing it again.)

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. So, whilst a tripos-theorist (if such a creature
exists) may indeed have cause to worry about whether Sxy might be
undefined, there seems to be no reason why a topos-theorist should do so.

[Yes, yes, I know that I was responsible for inventing the term
"tripos", and therefore that if anyone can legitimately be called a
tripos-theorist then I can. But I don't believe that I am a
tripos-theorist (which implies that no-one is).]

Peter Johnstone