Re: topos logic arising nicely

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Steve,
>
> Coincidentally, for quite different reasons I have just been looking at
> the Fourman/Scott theory as a way to deal with partial functions.
>
> Scott's system for existence and identity is given a Hilbert style
> presentation, and I suppose - I may be wrong - that that is why
> Fourman's interpretation makes such heavy use of the higher order
> structure of toposes. Do you know of any sequent presentations?

I think it is straightforward to give a sequent style formulation of the
Fourman/Scott interpretation. BTW one has to take care of inhabitedness
of types (in the general case) because variables of type A range over A
whereas terms of type A receive there interpretation in \tilde{A}, the partial
map clasifier of A. See e.g. Troelstra and van Dalen 2nd Chapter for a
traetment of what they call E-logic. Just as example the rules for \forall
look as follows

     \Gamma |- A(x)  x \not\in FV(\Gamma)
   ---------------------------------------
          \Gamma |- \forall x. A(x)

       \Gamma |- \forall x. A(x)  \Gamma |- t\downarrow
    ------------------------------------------------------
                    \Gamma |- A[t/x]


where  t\downarrow  stand for "t defined".

What I meant with my remark is that if one allows partial terms then one need
not have subtypes.

Best, Thomas

PS Fourman and Scott exploit higher order aspects already at first order level
because \tilde{A} is a subobject of P(A) , namely the subsingletons.