nLab
transcendental syntax

Contents

Contents

Idea

“Transcendental syntax” (Girard 13) is the name of a proposal (or maybe a pamphlete) by Jean-Yves Girard which means to rethink fundamental aspects of formal logic, of syntax/semantics. According to Girard, linear logic and Geometry of Interaction are but exercises in transcendental syntax (Girard 13b).

While Girard’s prose is notoriously demanding, exegesis may be found in (Abrusci-Pistone 12, Rouleau 13).

Girard describes four levels of semantics: alethic, functional, interactive, and deontic. They descend into the depths of meaning, and thus are numbered from -1 to -4. The negatively first, alethic, is the layer of truth or models. The negatively second, functional, is the layer of functions or categories. The negatively third, interaction, is the layer of games or game semantics. The negatively fourth, deontic, is the layer of normativity or formatting. (Equivalent eXchange)

Philosophical interpretation

The Transcendental Syntax starts from the strong claim that formal logic makes a lot of arbitrary choices such as the rules of logic (see deductive systems) and that it should be possible to study the mechanisms of reasoning without these assumptions (to which Girard refers to as “prejudices” hiding the “blind spots” of logic).

The solution presented by the Transcendental Syntax can be understood as an update of Kant‘s epistemology by taking computation into account through recent works in linear logic and the Curry-Howard correspondence. It suggests the division of the whole logical activity into four concepts (Girard 16):

Analytic / AnswersSynthetic / Questions
A posteriori / ExplicitConstatUsine
A priori / ImplicitPerformanceUsage

The point of view of the Transcendental Syntax is that logic studies the relationship between questions (formulas) and their answers (proofs) by means of finite objects. In order to do so with as less assumptions about logic as possible, we should start by defining the answers, seen as neutral and objective. Then we study the sufficient conditions making the logical concepts (proofs, formulas, logical correctness) emerge from the meaningless. In reference to Kant, Girard talks about the conditions of possibility of language.

The answers corresponds to a space of computational objects called epistates which can be evaluated (performance) into a normal form (constat). This is the space where proofs are formulated but not yet considered logically correct.

The space of questions considers two alternative definitions of meaning corresponding to formulas or types called dichology:

  • the use (usage): it corresponds to Ludwig Wittgenstein meaning-as-use. The computational behaviour of epistates and their potential interaction with other ones induces a classification into dichologies.

  • the factory (usine): we want our computational objets to pass a specific set of tests in order to accept them in the corresponding type.

This is related to the distinction between existentialism and essentialism in philosophy. The logical certainty corresponds to the adequation between usine and usage: we would like the usine to be finite and sufficient to ensure what we consider a right use of epistates.

Technical interpretation

Technically speaking, the Transcendental Syntax is basically a finitary version of the Geometry of Interaction. Some preliminary works include flows (Girard 95, Bagnol 14) or interaction graphs (Seiller 16). The Transcendental Syntax generalises and extends both by taking into account proof nets' logical correctness in a more general setting.

The elementary objects are constellations defined as multisets of clauses containing first-order terms. Two constellations can interact by using the dynamics of Robinson’s resolution (Robinson 65). We use constellations to encode proof structures, their cut elimination but also the correction graphs asserting logical correctness.

We can obtain two alternative notions of typing:

  • By using realizability techniques for linear logic as in ludics? or Seiller’s interaction graphs, we can define formulas called behaviours. This corresponds to types “à la Curry” where untyped computational objects are typed.

  • Inspired by the logical correctness of proof nets, we can define a type as a finite set of tests (encoded as constellations). If a constellation passes all tests, it is considered as part of the corresponding type. This corresponds to types “à la Church” where types exist before the computational objects being typed. In the context of proof nets, it corresponds to testing proof structures against correction graphs.

References

  • JA Robinson?, A machine-oriented logic based on the resolution principle, 1965.

  • Jean-Yves Girard, Geometry of interaction III: accommodating the additives, 1995 (pdf).

  • Marc Bagnol?, On the Resolution Semiring, PhD Thesis 2014 (pdf)

  • Thomas Seiller?, Interaction Graphs: Full Linear Logic, 2016 (pdf)

  • Jean-Yves Girard, Geometry of Interaction VI: a Blueprint for Transcendental Syntax, 2013 (CiteSeer)

  • Jean-Yves Girard, Transcendental syntax 2.0, 2013 (pdf)

  • Jean-Yves Girard, Transcendental syntax I: deterministic case, 2016 (pdf)

  • Jean-Yves Girard, Transcendental syntax II: non-deterministic case, 2016 (pdf)

  • Jean-Yves Girard, Transcendental syntax III: equality, 2018 (pdf)

  • Jean-Yves Girard, Transcendental syntax IV: logic without systems, 2020 (pdf)

  • Vito Michele Abrusci, Paolo Pistone, On Transcendental syntax: a Kantian program for logic?, 2012 (pdf)

  • Vincent Laurence Rouleau, Towards an understanding of Girard’s transcendental syntax: Syntax by testing, PhD thesis 2013 (pdf)

The beginnings of an attempt to formalize Transcendental Syntax is given in

  • Boris Eng?, Thomas Seiller?, Multiplicative Linear Logic from Logic Programs and Tilings (hal-02895111)

  • Boris Eng?, Stellar Resolution: Multiplicatives - for the linear logician, through examples (hal-02977750)

Last revised on April 7, 2021 at 08:56:53. See the history of this page for a list of all contributions to it.