One of the most fascinating examples of the failure of Beth’s definability theorem and, consequently, of Craig’s interpolation theorem, is quantified S5. In this paper, we intend to establish the interpolation property for fragments of quantified S5 using a formulation of the semantics of quantified S5 as an analytic calculus in its own right. This is especially straightforward for S5, because necessity (possibility) in S5 means for all worlds (there exists a world), and we have simply to extend every predicate by a world position (worlds and objects are to be considered as separate entities).