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.

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.

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.

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.

Abstract Reasoning

1. 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. 2. Biorthogonality stabilizes semantics. Closing twice under tests produces the largest behaviorally indistinguishable class consistent with the tests. 3. Polarity predicts proof-search phases. Positive choice and negative responsiveness determine where nondeterminism and obligation appear. 4. Addresses preserve occurrence identity. Repeated formula shapes at different loci remain distinct concrete uses.

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.

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

• Combinatory Logic — 0.78
• Random-Access Machine — 0.77
• Disjoint-Set Data Structure — 0.77
• Indiscernibles — 0.76
• Turing Machine — 0.76

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