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.
