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	Success
⊥	U+22A5	Orthogonal	Interacts successfully
ξ	U+03BE	Locus	Address
G	—	Behavior	Type-like set
⟨·⟩	—	Action	Positive action
⊗, ⅋	U+2297, U+214B	Connectives	Emergent connectives

Metatheory. Logic as orthogonality: types are behaviors. Full completeness: all strategies are definable. Symmetry: proofs and counter-proofs dual. Linear logic connection: reconstructs LL. Incarnation: canonical representatives.

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

Limitations. Highly abstract. Steep learning curve. Small community. Limited tools. Far from applications. Girard's notation idiosyncratic.