proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...

, ludics is an analysis of the principles governing

inference rule Rules of inference are ways of deriving conclusions from premises. They are integral parts of formal logic, serving as norms of the logical structure of valid arguments. If an argument with true premises follows a rule of inference then the co ...

s of

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

. Key features of ludics include notion of compound connectives, using a technique known as ''focusing'' or ''focalisation'' (invented by the computer scientist Jean-Marc Andreoli), and its use of ''locations'' or ''loci'' over a base instead of

proposition A proposition is a statement that can be either true or false. It is a central concept in the philosophy of language, semantics, logic, and related fields. Propositions are the object s denoted by declarative sentences; for example, "The sky ...

s. More precisely, ludics tries to retrieve known

logical connective In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the ...

s and proof behaviours by following the paradigm of interactive computation, similarly to what is done in

game semantics Game semantics is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on Game theory, game-theoretic concepts, such as the existence of a winning strategy for a player. In this ...

to which it is closely related. By abstracting the notion of

formulae In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...

and focusing on their concrete uses—that is distinct occurrences—it provides an

abstract syntax In computer science, the abstract syntax of data is its structure described as a data type (possibly, but not necessarily, an abstract data type), independent of any particular representation or encoding. This is particularly used in the represent ...

for

computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

, as loci can be seen as pointers on memory. The primary achievement of ludics is the discovery of a relationship between two natural, but distinct notions of

type Type may refer to: Science and technology Computing * Typing, producing text via a keyboard, typewriter, etc. * Data type, collection of values used for computations. * File type * TYPE (DOS command), a command to display contents of a file. * ...

, or proposition. The first view, which might be termed the proof-theoretic or

Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died o ...

-style interpretation of propositions, says that the meaning of a proposition arises from its introduction and elimination rules. Focalization refines this viewpoint by distinguishing between positive propositions, whose meaning arises from their introduction rules, and negative propositions, whose meaning arises from their elimination rules. In focused calculi, it is possible to define positive connectives by giving only their introduction rules, with the shape of the elimination rules being forced by this choice. (Symmetrically, negative connectives can be defined in focused calculi by giving only the elimination rules, with the introduction rules forced by this choice.) The second view, which might be termed the computational or

Brouwer–Heyting–Kolmogorov interpretation In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, is an explanation of the meaning of proof in intuitionistic logic, proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogor ...

of propositions, takes the view that we fix a computational system up front, and then give a

realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...

interpretation of propositions to give them constructive content. For example, a realizer for the proposition "A implies B" is a computable function that takes a realizer for A, and uses it to compute a realizer for B. Realizability models characterize realizers for propositions in terms of their visible behavior, and not in terms of their internal structure. Girard shows that for

second-order Second-order may refer to: Mathematics * Second order approximation, an approximation that includes quadratic terms * Second-order arithmetic, an axiomatization allowing quantification of sets of numbers * Second-order differential equation, a d ...

affine Affine may describe any of various topics concerned with connections or affinities. It may refer to: * Affine, a Affinity_(law)#Terminology, relative by marriage in law and anthropology * Affine cipher, a special case of the more general substi ...

linear logic Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the ...

, given a computational system with nontermination and error stops as effects, realizability and focalization give the same meaning to types. Ludics was proposed by the

logician Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure of arg ...

Jean-Yves Girard Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the Éc ...

. His paper introducing ludics, ''Locus solum: from the rules of logic to the logic of rules'', has some features that may be seen as eccentric for a publication in

(such as illustrations of skunks). The intent of these features is to enforce the point of view of

at the time of its writing. And, thus, it offers to readers the possibility to understand ludics independently of their backgrounds.{{cn, date=October 2024

External links

# Girard, J.-Y.
''Locus solum'': from the rules of logic to the logic of rules
(.pdf), ''Mathematical Structures in Computer Science'', 11, 301–506, 2001.
Girard reading group
at

Carnegie-Mellon University Carnegie Mellon University (CMU) is a Private university, private research university in Pittsburgh, Pennsylvania, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became t ...

(a wiki about Locus Solum) Mathematical logic