What is behind Girard's idea of distinguishing implication ( ⇒) and entailment (⊢) without separating language and meta-language?

Question

How should we understand the distinction between ⇒ and ⊢ ?

I often see that A ⇒ B lives in the object language and A ⊢ B in the meta language. But I need a different interpretation, without any reference to "meta-logic".

An interesting text, What the Tortoise Said to Achilles (Lewis Carroll) seem to provide an implicit answer. How should we interpret that to understand the distinction ?

Some interesting points of view suggested by J.Y Girard that I don't fully understand :

• The distinction is not accessible to realism because they have the same semantic. Inspired by Kant, he often says that ⊢ refers to "implicit", "synthetic" and ⇒ refers to "explicit", "analytic".

La nuance entre imbrication ⊢ et l'implication ⇒ est inaccessible au réalisme : elles ont, en effet, la même sémantique. L'acte fondateur de la logique moderne est ainsi franchement déréaliste. Alors que ⊢ réfère au synthétique d'usage, l'implicite et son substrat analytique performatif, ⇒ ne réfère plus qu'à l'usine explicite et son substrat analytique constatatif.

J.Y Girard, le fantôme de la transparence.

• About Lewis Carroll's text, the Tortoise is said to be "without cut" while Achilles use "cut" (The Blind Spot, Part 3.A.2, J.Y Girard).

• ⇒ is said to be "incremental" while ⊢ is said to be "destructive"

• ⇒ is said to be "terminated" while ⊢ is said to be "non-terminated"

• Logic lies on the dialectic between ⇒ and ⊢

Answer 1

Briefly, the distinction is not Girard's, it is already present in Frege's work in the late 19th century. If logic is the science of deduction, then entailment is the expression of deducibility, of a conclusion from hypotheses.

Entailment is not at all a "meta" concept; that is simply incorrect. It is, however, prior to implication in that implication internalizes entailment as a connective. That is, an implication is true exactly when one can deduce the consequent from the antecedent.

Analogously, in categories the Hom is prior to the exponential. That is, we have maps before we have objects that classify them.

Analogously, in type theory we have open terms (with free variables) before we have lambda's, which are elements of function types.

Analogously, in school you learned to use polynomials before you learned that one could define, say, a differential operator.

Answer 2

I am not sure if Le Fantôme de la Transparence is translated into English but the themes from the quote are familiar from Girard's Transcendental Syntax, which is. Here is the full quote in my translation:

"The nuance between imbrication ⊢ and implication ⇒ is inaccessible to realism: they have, indeed, the same semantics. The founding act of modern logic is thus frankly derelict. While ⊢ refers to the synthetic use, and implicitly to its performative analytic substrate, ⇒ refers only to the explicit use, and its declarative analytic substrate."

The "founding act of modern logic" is Frege's predicate calculus with logical consequence based on semantics. This last part, a.k.a. "realism", is, according to Girard, fatally flawed. Here are some of his reasons why:

"The fact is that semantics — whatever quality they may have — are all incomplete: they fail to catch the specificity of language. We can indeed see "the" reality as a way of quotienting the language; there are various styles of quotients, of variable quality; this variability may even be linked to the freshness of the interpretation... In the same way, the experience of philosophical logic is that of ad hoc realities, monkeying the syntax, typically Kripke models: semantics as prejudice, so to speak. One interprets the language (written in italics) by the same thing (written in boldface), thus making (almost) no quotient at all... To sum up, there is no ultimate reality the language is referring to. There are, however, a few pseudo-realities of interest, all of them exploiting some aspect of the language. Anyway, since the semantic construction takes place in the language of mathematics, semantics is eventually an internal interpretation of the language!"

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also Why is Tarski's notion of logical validity preferred to deductive one? I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

"The Fregean opposition between sense and denotation is philosophically extremely naive and part of the totalitarian regression of thought, possibly linked with the abominable political opinions of Frege... for the technical reasons just expounded, but also from a common sense remark: the language formats the reality. Frege’s description of logic reminds me of this explanation of vision of my childhood: the landscape is projected on the retina of an ox. OK, so what? It still remains to understand how this retinal image is analysed."

The distinction on which Fregean logic is "derelict" can perhaps be manifested differently. I can only speculate that "analytic substrate" probably refers to the substrate of Girard's self-sufficient language, and "performative"/"declarative" dichotomy is related to the two sides of Curry-Howard correspondence between logical proofs and typed λ-terms, "execution" and "construction". This is the basis of Girard's idea of justifying syntax from within syntax, by uncovering (Kant inspired) conditions of the possibility of its practical functioning without infinite loops. On this I find Abrusci-Pistone's expose of Girard's program somewhat easier to follow :

"Research on typed λ-calculi usually privileges, indeed, an approach directed to the dynamical features of logic: proofs, as isomorphic with programs, are taken as mathematical objects that must not only be constructed following the rules, but also be executed following the dynamics of those rules. The duality construction/execution is made explicit by the so-called formulae-as-types correspondence, by which logical formulas are associated with types, that is, with sets of proofs satisfying the norms associated by logical rules to those formulas... Logical syntax can thus be seen both as a constructive tool, enabling the formation of (normalizing) typed terms, and as a constraining one, imposing a custom on pure terms (and their socialization) in order to force termination. In analogy with Kant’s transcendentalism, indeed, the program tries to raise the issue to deduct, that is, to legitimize the authority exercised by logical languages... without reference to those entities whose representability crucially relies on the use of what is charged of being justified."

For a more detailed commentary see Rouleau's 2013 thesis Towards an Understanding of Girard's Transcendental Syntax: Syntax by Testing.

Answer 3

After some researches I think I have a quite satisfying answer.

Suppose we're in the Sequent Calculus (we don't care whether it is classical or intuitionistic). We know that the cut rule act on ⊢ while the implications rules act on ⇒.

The turtle tells us that we have the premises ⊢ A and A ⊢ B and asks us to get ⊢ B. We have two possible things we can do:

• Use the cut rule to infer ⊢ B (that's one should answer to the turtle)
• Use the left-implication rule to infer A ⇒ A ⊢ B (that's what Achille does)
  • In that case, with another cut (that's what the turtle want) with ⊢ A ⇒ A which is indeed provable we can have have ⊢ B
  • Or you can also use the left-implication rule again (that's what Achille does) to get (A ⇒ A) ⇒ (A ⇒ A) ⊢ B. That rule can be repeated as much as we want.

Conclusion

• The usual model-theoretic interpretation of sequents is associated to realism. The sequent ⊢ A ⇒ B and A ⊢ B have the same interpretation in term of truth values. So no distinction can be seen.

• The distinction lies in the computation behaviour of ⊢ and ⇒:

  • ⊢ moves the reasoning forward, that's why it is destructive. It is a real computation. We reach an information we didn't have, that's why it is implicit (close to the synthetic).
  • ⇒ is static because A ⇒ B is a mere frozen object we can manipulate without performing any activation of computation. The implication rules can be seen as a way to "freeze" computation (or unfreeze when reading from bottom to top). That also explains why it is explicit, terminated.

• Through the Curry-Howard isomorphism we can also have a simple interpretation with programs. The cut-rule is related to the process of computation while the implication rules simply manipulates application of functions f(x) as a frozen object.

EDIT : I edited my answer to a new one without mentioning Linear Logic.