Incarnation in ludics and maximal cliques of paths

DOI10.2168/LMCS-9(4:6)2013zbMATH Open1319.03063arXiv1307.1028OpenAlexW1984267738MaRDI QIDQ2851674FDOQ2851674

Authors: Myriam Quatrini, Christophe Fouqueré 

Publication date: 16 October 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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 proofs but cut-elimination interpreted as an interaction between objects called designs. When the interaction between two designs goes well, such two designs are said to be orthogonal. A behaviour is a set of designs closed under bi-orthogonality. Logical formulas are then denoted by behaviours. Finally proofs are interpreted as designs satisfying particular properties. In that way, designs are more general than proofs and we may notice in particular that they are not typed objects. Incarnation is introduced by Girard in Ludics as a characterization of "useful" designs in a behaviour. The incarnation of a design is defined as its subdesign that is the smallest one in the behaviour ordered by inclusion. It is useful in particular because being "incarnated" is one of the conditions for a design to denote a proof of a formula. The computation of incarnation is important also as it gives a minimal denotation for a formula, and more generally for a behaviour. We give here a constructive way to capture the incarnation of the behaviour of a set of designs, without computing the behaviour itself. The method we follow uses an alternative definition of designs: rather than defining them as sets of chronicles, we consider them as sets of paths, a concept very close to that of play in game semantics that allows an easier handling of the interaction: the unfolding of interaction is a path common to two interacting designs.

Full work available at URL: https://arxiv.org/abs/1307.1028

Recommendations

• Study of behaviours via visitable paths
• Computational ludics
• scientific article; zbMATH DE number 1948178
• Ludics and natural language: first approaches
• scientific article; zbMATH DE number 1948179

zbMATH Keywords

game semanticslinear logicnormalizationcut-eliminationludicsincarnation

Mathematics Subject Classification ID

Abstract deductive systems (03B22) Logic in computer science (03B70) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cited In (3)

• Study of behaviours via visitable paths
• Title not available (Why is that?)
• Computational ludics

This page was built for publication: Incarnation in ludics and maximal cliques of paths

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851674)