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.