This paper solves some puzzles in the formalisation of logic for discontinuity in categorial grammar. A ‘tuple’ operation introduced in [Solias, 1992] is defined as a mode of prosodic combination which has associated projection functions, and consequently can support a property of unique prosodic decomposability. Discontinuity operators are defined model-theoretically by a residuation scheme which is particularly ammenable proof-theoretically. This enables a formulation which both improves on the logic for wrapping and infixing of [Moortgat, 1988] which is only partial, and resolves some problems of determinacy of insertion point in the application of these proposals to in-situ binding phenomena. A discontinuous product is also defined by the residuation scheme, enabling formulation of rules of both use and proof for a ‘substring’ product that would have been similarly doomed to partial logic. We show how the apparatus enables characterisation of discontinous functors such...