modified realizability topos and so on

14 Feb 1992

      It is well known that one can build toposes from realizability.
This has been done quite successfully for Kleene realizability and  
for extensional realizability.
An excellent survey on these topics is contained in the Thesis by  
Jaap van Oosten.

There he also suggests how to give higher order variant of MODIFIED  
REALIZABILITY - although only of that variant of modified  
realizability called the "HRO variant" in Troelstras book (SLNM 344).

I want to suggest an - I think more adequate - version.

Jaaps approach :  propositions are modelled as as pairs  (p,P)
                  where  p  is a subset of  P  which is a set of 

                  natural numbers containing  0

                  (p,P) |- (q,Q)   ("entailment")

                  iff there is a natural number  n  such that

                    for all m in P :  {n}(m) terminates  and 

                                      {n}(m) is in Q   and

                                      {n}(m) is in q  if  m  is in p 

It is felt - and also explicitely expressed in Jaaps Thesis - that  
the requirement " 0  in  P " is a very liberal way of expressing that  
the set P  of  "potential realizers"  is NOT EMPTY.

The intuition behind modified realizability is much stronger :

a proposition should be a pair  (D,P)   where  D  is a  "domain of  
potential realizers"  and  P  is an arbitrary subset of  D .
Of course, the requirement that  D  is a domain is much stronger than  
the claim that it contains a specified element (namely 0).

Now my suggestion is that 

PROPOSITIONS are  pairs  (D,P)  where  D  is an effective domain    
and  P  is an arbitrary subset of  D .
By "domain"  we either mean a complete Sigma extensional per or a  
Sigma replete per with a least element (realized by the code of the  
totally undefined function from N to N ).

Now one does know that families of pers form a hyperdoctrine over SET  
and so do families of domains in the sense specified above.

NOW THE POINT IS that this holds also for families of pers with a  
predicate on it.
We give the skeleton of a definition below.

We construct the following posetal hyperdoctrine over  SET .

Let DOM be any of the subsets of PER mentioned above.

An object over  X  is a pair  (F,P)  where  F : X -> DOM  and  P   
associates with any  x  in  X  a subset  P(x)  of  F(x).

Now if  (F,P)  and  (G,Q)  are objects over  X  then  (F,P) |- (G,Q)   
iff there is a natural number  n  such that

  -  for any  x  in  X :  n realizes a morphism f(x) : F(x) -> G(x)

  -  for all x in  X  and  d  in  P(x) :  f(x)(d)  is in  Q(x)   .

Obviously, any fibre is a pre-Heyting algebra and it is complete in  
the sense that right adjoints to reindexing exist and are themselves  
preserved by reindexing.

We also have a generic element over

  Prop := { (D,P) |  D  in  DOM  and   P  is a subset of  D }

where the generic object in the fibre is given by  (F_gen,P-Gen) :

  F_gen(D,P) = D    and    P_gen(D,P) = P  .

Now from this MODIFIED REALIZABILITY TRIPOS one can construct the  
associated  MODIFIED REALIZABILITY TOPOS .

It remains as an open problem whether it is very different from the  
one Jaap proposed.

REMARKS  One could as well consider the triposes arising from 

         families of predomains or families of extensional pers.

         Our considerations were directed towards 

         domains of partial elements.

         Of course it is also possible to consider the collection of 

         domains of total elements, e.g. all Delta replete pers
         (where Delta is the 2-element discrete per) 

         s.t. any constant total function with value  0  or  1  

         realizes some element .

    QUITE GENERALLY ANY SUBCOLLECTION OF PERS CLOSED UNDER PRODUCTS 

    OF FAMILIES OVER UNIFORM omega-Sets  ALLOWS TO DEFINE A   

    CORRESPONDING REALIZABILITY TRIPOS and ITS ASSOCIATED 

    REALIZABILITY TOPOS.

P.S.  Maybe all these facts are already well known to Martin Hyland !   

      In his Como paper he says that he has checked several topoi 

      arising from several versions of realizability or functional   

      interpretation in form of "back-side of an envelope 

      computations" .
      Nevertheless the remarks above - I hope - might be interesting 

      for some people (as e.g. me) who have not had such a close look 

      at the backside of Martins envelopes.

   For toposes derived from functional interpretation at first sight 

   there is the problem that Dialectica categories are not ccc-s but 

   categorical structures suitable for interpreting classical linear  

   logic. But if one looks at the Kleisli coalgebra associated with 

   the  !-comonad  on ecan again get a tripos corresponding to 

   functional interpretation !

Thomas Streicher
=========================================================================