Ludics¶

Reconstruct logical propositions and proofs from address-based designs, polarized actions, and successful interaction, defining meaning extensionally through orthogonality rather than presupposed formulas.

Version: v1 · 2026-08-30 · History
Domain-specific #: 2214
Origin domain: proof theory
Subdomain: linear logic
Aliases: Ludics logic

Core Idea¶

Ludics is Jean-Yves Girard's proof-theoretic program for deriving logical meaning from interaction before taking formulas and connectives as primitive. It replaces ordinary proofs with designs built from polarized actions occurring at loci or addresses. A design interacts with a counterdesign through normalization. When their interaction terminates successfully—often at the distinguished terminating action called the daimon—the designs are orthogonal. A behaviour, playing the role of a proposition or type, is then characterized extensionally as a set of designs closed under biorthogonality.

The reversal is central. Traditional proof theory begins with formulas and inference rules and asks which proofs inhabit them. Ludics begins with possible situated actions and their observable interactions; logical connectives and proof behavior are recovered from regularities in those interactions. Girard's Locus solum develops the framework as a move “from the rules of logic to the logic of rules.”^[1]

Focalization supplies the proof-theoretic bridge. Positive phases make active choices; negative phases respond to all admissible challenges. Polarity organizes proof search into maximal focused phases and exposes the interaction structure otherwise hidden among commuting rule permutations. Ludics also connects this rule-based view of propositions with a realizability view, where meaning is given by the observable behavior of computational objects against tests.

Structural Signature¶

base — a finite interface of signed loci specifying where a design can engage;
locus/address — a finite address naming a concrete occurrence rather than a formula symbol;
positive and negative actions — polarized moves with a focus and a finite ramification of subaddresses;
chronicle — an alternating justified sequence of actions obeying address and polarity constraints;
design — a coherent, prefix-closed family of chronicles representing a proof-like strategy;
counterdesign — an oppositely polarized compatible object supplied as a test;
interaction/net — designs are connected along dual loci;
normalization — matching actions cut against one another and execution moves through their ramifications;
daimon — a special positive termination action marking successful completion or concession;
orthogonality — a design is orthogonal to a counterdesign when their normalization succeeds under the declared criterion;
orthogonal and biorthogonal closure — tests define inhabitants and repeated orthogonality yields stable behaviours;
behaviour — a biorthogonally closed set of designs functioning as a proposition or type;
incarnation/materiality — the part of a design actually visited by interaction with all tests in its behaviour.

The invariant is extensional logical meaning reconstructed from polarized address-based designs and their normalization against counterdesigns.

What It Is Not¶

Not game theory about entertainment. “Ludics” evokes play, but the players and moves are proof-theoretic structures.
Not game semantics generally. It is closely related but has its own objects, loci, orthogonality, behaviours, and reconstruction program.
Not a logical connective. Ludics is a framework in which connectives can be recovered or analyzed.
Not ordinary sequent calculus with renamed formulas. Formula-free addresses and interaction-first semantics are constitutive.
Not proof search alone. Focalization organizes proof search, while ludics adds designs, tests, normalization, and biorthogonal meaning.
Not realizability alone. It relates realizers to observable interaction and focalized proof structure through a particular formal apparatus.
Not informal dialogue logic. Alternation is rigorously constrained by bases, justifications, polarity, and normalization.

Scope of Application¶

Ludics belongs to proof theory, linear logic, semantics of computation, realizability, game semantics, type theory, and formal analyses of interaction. It is used to investigate what makes an inference rule logical, how propositions can be reconstructed from their possible proofs and refutations, and how syntactic proof normalization relates to operational behavior.

The framework has several variants and presentations. Exact definitions of designs, chronicles, convergence, totality, and behaviours can differ with additives, repetitions, exponentials, or computational effects. Reference-grade use must declare the version rather than treating every paper carrying the label as one fixed calculus.

Its literal scope is formal. Applications to language, dialogue, or computation require an explicit encoding into designs and interaction. Casual metaphors about debate or games do not instantiate ludics.

Clarity¶

A recognition test asks whether formulas have been displaced by located actions and whether semantics is defined through testing. If an object is merely a proof tree over formulas, it is not yet a ludics design. If “type” is assigned without orthogonality or an equivalent interaction criterion, the characteristic reconstruction is absent.

Polarity has operational force. A positive action selects one finite ramification; a negative side must be prepared for admissible responses. Alternation and justification link each new focus to an address generated earlier. Coherence ensures chronicles can inhabit one design without incompatible positive choices.

Normalization is an execution, not only a syntactic rewrite. Matching focused actions direct the interaction to subaddresses. The observable outcome determines orthogonality. Sets of tests then define which designs count as inhabitants; biorthogonal closure prevents accidental examples from being mistaken for a stable semantic class.

Manages Complexity¶

Ordinary proof systems contain many bureaucratic permutations of independent rules. Focalization compresses these into polarized phases, revealing canonical interaction structure. Loci detach occurrences from formula identity, allowing the framework to study how concrete uses compose without assuming a global formula tree.

Orthogonality replaces intensional inspection with behavioral tests. Instead of comparing every internal branch of two proof objects, one asks whether each survives the same counterdesigns. Behaviours package potentially infinite test relations into type-like objects. Incarnation then removes parts of a design never visited by any relevant interaction, isolating materially observable content.

This supports modular reasoning: bases specify interfaces, designs specify strategies, normalization specifies composition, and behaviours specify extensional meaning. Each layer answers a different question and blocks category mistakes between syntax, execution, and semantic classification.

Abstract Reasoning¶

Meaning is test-relative. A design belongs to a behaviour because of how it interacts with the behaviour's orthogonal counterdesigns, not because of a presupposed formula label.
Biorthogonality stabilizes semantics. Closing twice under tests produces the largest behaviorally indistinguishable class consistent with the tests.
Polarity predicts proof-search phases. Positive choice and negative responsiveness determine where nondeterminism and obligation appear.
Addresses preserve occurrence identity. Repeated formula shapes at different loci remain distinct concrete uses.
Normalization is composition. Compatible designs yield an observable interaction, making cut elimination computational.
Unused structure is semantically suspect. Incarnation identifies the fragments actually elicited by counterdesigns.
Types can be reconstructed. When stable behaviours reproduce logical connectives, proof-theoretic and realizability meanings coincide under the framework's hypotheses.

Knowledge Transfer¶

Within logic, ludics transfers between proof normalization, realizability, focused calculi, linear logic, and game-semantic analysis because all can be recast around interaction and observation. Loci resemble memory addresses, which makes the framework suggestive for programming-language semantics, but a genuine transfer must preserve polarity, designs, normalization, and testing.

The broader pattern—define an object by the adversarial tests it passes—also appears in observational equivalence and specification. Those are related primes, not literal ludics without the formal apparatus.

Historical and terminological care matters. “Ludic” in philosophy, art, or game studies is not an alias. The capitalized research program is tied to Girard and subsequent proof-theoretic developments.

Examples¶

Positive choice. A design focuses on a locus and selects one ramification, committing to a branch of interaction.
Negative response. A counterdesign at the dual locus accepts the admissible ramifications and continues at generated subaddresses.
Successful cut. Matching actions normalize through their shared locus until the daimon is reached, establishing orthogonality.
Failed interaction. Mismatched or divergent execution prevents orthogonality and separates designs behaviorally.
Behaviour construction. Begin with a family of designs, collect every counterdesign orthogonal to all of them, then take the orthogonal again.
Incarnation. Remove chronicles never visited against any test in the orthogonal; the remaining material design captures observable use.

Structural Tensions¶

Formula-free syntax vs. recovered logic. Ludics discards formulas initially so their connective structure can re-emerge behaviorally.
Internal proof structure vs. external tests. Designs have rich syntax, but membership is extensional.
Positive choice vs. negative obligation. One polarity commits; the other accommodates possible challenges.
Convergence vs. divergence. Terminating interaction supports orthogonality; nontermination can carry semantic information.
Complete design vs. incarnation. A written design may contain branches no valid opponent ever visits.

Structural–Framed Character¶

Ludics is structural. Once a formal variant is fixed, legal actions, designs, reductions, orthogonality, and closure are mathematical. Philosophical interpretations of meaning motivate the framework but do not make membership subjective.

Structural Core vs. Domain Accent¶

The core is dual testing: entities and counterentities interact, observation defines compatibility, and closure under indistinguishable tests forms semantic classes. Its proof-theoretic accent—loci, polarized actions, designs, normalization, daimon, orthogonality, and behaviours—is indispensable.

Duality — designs and counterdesigns occupy complementary polarities.
Interaction — meaning is exposed through execution against an opponent.
Normalization — cuts reduce to observable outcomes.
Closure — biorthogonality constructs stable behaviours.
Interface — bases expose signed loci for composition.
Observational Equivalence — shared tests determine semantic indistinguishability.

The prospective DAG edge uses composition under prime:duality.

Relationships to Other Abstractions¶

Current abstraction Ludics Domain-specific

Parents (1) — more general patterns this builds on

Ludics is part of Duality Prime

shared tests determine semantic indistinguishability.

Hierarchy path (1) — routes to 1 parentless root

Ludics → Duality

Neighborhood in Abstraction Space¶

Ludics sits in a sparse region of the domain-specific corpus (94^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Formal Patterns & Indiscernibility (6 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

Linear Logic — a source framework and recovered logic, broader than ludics.
Game Semantics — related interaction semantics with different primitives.
Focusing — an essential technique but not the whole theory.
Realizability — a semantic tradition connected by ludics but not identical.
Dialogue Games — other logical game formalisms.
Ludology — study of games and play.

References¶

[1] Jean-Yves Girard, “Locus solum: from the rules of logic to the logic of rules,” Mathematical Structures in Computer Science 11 (2001), 301–506, https://girard.perso.math.cnrs.fr/0.pdf. registry ↩

[2] Jean-Yves Girard, “From foundations to ludics,” https://girard.perso.math.cnrs.fr/bsl.pdf. registry

[3] “Ludics,” Wikipedia, frozen revision 1318125608 (2025-10-22), https://en.wikipedia.org/wiki/Ludics. registry