Incarnation in Ludics and maximal cliques of paths

Ludics is a reconstruction of logic with interaction as a primitive notion,in the sense that the primary logical concepts are no more formulas and proofsbut cut-elimination interpreted as an interaction between objects calleddesigns. When the interaction between two designs goes well, such two designsare said to be orthogonal. A behaviour is a set of designs closed underbi-orthogonality. Logical formulas are then denoted by behaviours. Finallyproofs are interpreted as designs satisfying particular properties. In thatway, designs are more general than proofs and we may notice in particular thatthey are not typed objects. Incarnation is introduced by Girard in Ludics as acharacterization of "useful" designs in a behaviour. The incarnation of adesign is defined as its subdesign that is the smallest one in the behaviourordered by inclusion. It is useful in particular because being "incarnated" isone of the conditions for a design to denote a proof of a formula. Thecomputation of incarnation is important also as it gives a minimal denotationfor a formula, and more generally for a behaviour. We give here a constructiveway to capture the incarnation of the behaviour of a set of designs, withoutcomputing the behaviour itself. The method we follow uses an alternativedefinition of designs: rather than defining them as sets of chronicles, weconsider them as sets of paths, a concept very close to that of play in gamesemantics that allows an easier handling of the interaction: the unfolding ofinteraction is a path common to two interacting designs.Comment: 33 pages, revised and corrected versio