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 rather 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 the “prejudices” 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) which are subjective and their answers (proofs) which are objective, by means of finite objects (because of the intuition that reasoning should be finite). 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 adequacy between usine and usage: we would like the usine to be finite and sufficient to ensure what we consider a right use of epistates. According to Girard Girard 16, the separation between constat and performance comes from the notion of undecidability (for instance through the Halting Problem) because the potential of program, for instance, cannot always be reduced to its result (which is not necessarily defined). The separation between usine and usage comes from Gödel’s incompleteness theorem which intuitively mean that the possible use of a logical object may go beyond what we expect (think of Gödel formulas which are rare and not so problematic in practice).

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.

Getting rid of semantics

An important ambition of the Transcendental Syntax is to make assumptions computationally explicit, to “put everything on the table”. In the Transcendental Syntax, it is no more possible to write a proof as usual. A proof comes as a hybrid object (Φ,𝒯)(\Phi, \mathcal{T}) where Φ\Phi is a constellation (elementary computational object) and 𝒯\mathcal{T} is a set of constellations corresponding to tests asserting the logical correctness of Φ\Phi. The constellation Φ\Phi has to satisfy a given criterion of orthogonality when interacting with Φ𝒯\Phi' \in \mathcal{T}, written ΦΦ\Phi \bot \Phi'. Logical objects only exist as computationally justified constructions.

Following this approach and by choosing a right notion of orthogonality, it is possible to construct axiom-free systems. In Transcendental Syntax’s fourth paper (Girard 20), Girard sketches a reconstruction of Peano arithmetic. An essential point which allows us to actually get rid of semantical explanation is that both tests and tested are of the same kind, have the same role and interact in a symmetric way. The “boundaries” of logic then rely on a given notion of orthogonality and not on a semantical system deciding what is logical or not.

This might be compared with other approaches in type theory such as computational type theory or cubical type theory where some logical constructions are not primitive anymore but reconstructed. A major difference seems to be the starting point and the primitives considered. It is also very similar to approaches in classical realizability.

All these approaches, including Girard Transcendental Syntax start from the assumption that computation can fully explain logic and are thus extensions of the Curry-Howard-Lambek correspondence.

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 June 27, 2021 at 16:02:02. See the history of this page for a list of all contributions to it.