Ludics

Origin. Girard introduced ludics (2001). Foundation for logic via interactive games. Designs as basic objects, not formulas. Orthogonality defines behavior/type. Unifies logic, computation, and game semantics. "Logic from interaction."

Models. Interactive foundations of logic. Traditional: formulas, proofs, models. Ludics: designs (strategies), interaction, orthogonality. No a priori formulas — behaviors emerge from interaction. Symmetry between programs and tests.

Formalism.

Designs: Tree-like strategies with addresses (loci). Actions: positive (output) or negative (input). Daimon †: signal for success/termination.

Loci: ξ, ξ.i, ξ.i.j, ... — addresses in a tree. Positive locus: owned by design. Negative locus: opponent's.

Design structure: D ::= † | ξ⟨N₁,...,Nₖ⟩.D₁ | ... | Dₙ

Positive action: output at ξ, choose branch i. Negative action: input at ξ, handle all branches.

Orthogonality: D ⊥ E: designs D and E interact successfully. Normalization: interaction reduces to †.

Behavior (type): G = G⊥⊥ (bi-orthogonal closure) Behavior: set of designs closed under bi-orthogonality.

Connectives emerge: ⊗, ⅋, etc. defined via behaviors. Formulas = behaviors, not primitive.

Incarnation: Material part of design (strip away †). Identity of designs.

Symbols.

Symbol	Unicode	Name	Meaning
†	U+2020	Daimon	The give-up action; success of an interaction
⊥	U+22A5	Orthogonality	D ⊥ E: the interaction normalizes to †
ξ	U+03BE	Xi / Locus	An address in the tree of a design
⊗	U+2297	Tensor	Multiplicative conjunction, defined as a behaviour
⅋	U+214B	Par	Multiplicative disjunction, defined as a behaviour
⟨	U+27E8	Left angle bracket	Opens the list of subaddresses in an action
⟩	U+27E9	Right angle bracket	Closes it
·	U+00B7	Locus separator	Extension of an address, as in ξ.i.j
₁	U+2081	Subscript one	First component in ξ⟨N₁,...,Nₖ⟩
ₖ	U+2096	Subscript k	Last component of the ramification
ₙ	U+2099	Subscript n	Index of the last alternative in a design
D, E	—	Designs	The primitive objects: strategies over loci
N	—	Negative part	A subaddress set in a positive action
G	—	Behaviour	A bi-orthogonally closed set of designs, a type
G⊥⊥	—	Bi-orthogonal	Closure operator; behaviours are its fixed points
::=	—	Grammar production	Formation rule for designs
Inc	—	Incarnation	The material designs of a behaviour, its canonical core

Metatheory. Girard's "Locus Solum" (Mathematical Structures in Computer Science, 2001) proves the two results the theory is built to deliver. Separation: two designs with the same orthogonal are equal, so a design is determined by the interactions it survives, which is the ludics analogue of Böhm's theorem for the lambda calculus and the reason orthogonality can serve as the definition of type. Internal completeness: the behaviour obtained by bi-orthogonal closure of a connective's defining set contains nothing beyond that set, so the connectives need no separate completeness theorem — soundness and completeness coincide by construction, unlike in denotational semantics where the two are proved apart. Full completeness holds for polarized multiplicative-additive linear logic: the winning designs of the behaviour interpreting a formula are exactly its proofs, so there are no undefinable strategies. Incarnation picks canonical representatives, the material part of a design, making behaviours sets with a distinguished minimal core. Terui's "Computational Ludics" (2011) recast designs as a term calculus and reproved separation there.

Applies to. Foundations of logic. Game semantics. Realizability. Program semantics. Interaction-based computing. Dialogue systems.

Limitations. The theory covers the multiplicative-additive fragment; the exponentials, and with them repetition and infinite behaviour, are not part of the original construction and the extensions handling them are not settled. Separation requires the daimon: designs must be allowed to give up, so the objects of the theory are paraproofs rather than proofs, and provability is recovered only by restricting to winning designs afterwards. Loci are absolute addresses, so designs are not invariant under renaming and an explicit delocation operation is needed before behaviours can be compared; this is why ludics does not present itself as a category in the ordinary way. Normalization of designs is partial, since designs may be infinite and interaction may diverge, so orthogonality is a relation that can fail to be decided. Quantification is outside the original theory, which is propositional.