I did my PhD thesis in Girard's team in Marseille (my supervisor was Laurent Regnier, himself a student of Girard's) so I have quite a bit of experience with his "excentric" way of communicating and I can attempt an exegesis ( :-) ) of this particular sentence (besides, I am quite familiar with both the philosophical and technical contents of what Girard calls "geometry of interaction", or GoI).

First of all, the concept of time Girard is talking about is *computational time*, i.e., the step-by-step evolution of a computational process. This is where his words make the most technical sense. Any broader interpretation of the word "time" in this context may (or may not) lead to futile and meaningless musings. Now, the three "intuitions" Girard is talking about correspond to three different views of logic, the first two belonging to the proof-theoretic tradition, the third more model-theoretic:

- logic as proof search;
- logic as functional programming;
- logic as a descriptive tool.

In logic as proof search, one step of computation corresponds to one inference rule (read bottom-up). Certain inference rules commute, which means that they may possibly be applied in parallel, whereas others are related by causal dependencies, yielding a sequential evaluation. These latter are the ones that make the time "tick", so one may see computational time in proof search to be given by the successive application of clusters of mutually independent rules. This idea finds a technical realization in the notion of *polarity* and *focusing proofs* in linear logic, which was unknown at the time Girard wrote "Towards a GoI". Polarity in linear logic was introduced in the early 90s by Jean-Marc Andreoli and today is an essential aspect not only of linear proof search but of games semantics and the theory of programming languages in general.

The second view is the simplest to explain: it is the well-known Curry-Howard correspondence, under which a proof may be seen as a program, the execution of which corresponds to cut-elimination. So computational time is just the succession of cut-elimination steps, i.e., rewriting steps leading to a result, which is fairly standard and intuitive I would say. The relationship between evaluation time in this sense ($\beta$-reduction/cut-elimination) and the usual notion of time defined using Turing machines (or other low-level machines) has been the direct or indirect subject of countless papers from the 90s onwards (google "implicit computational complexity", or take a look for example at this paper by Blelloch and Greiner or this very recent paper by Accattoli and Dal Lago).

The third view is also very standard: logic is seen as a language in which we may state facts/propositions about some kind of world. There is a whole class of logical languages (known as temporal logics) which are taylored so as to be able to speak of worlds in which there is a notion of time. Here, Girard is suggesting that non-commutative logic, with its non-symmetric connectives distinguishing "left" from "right" (hence, presumably, "before" from "after") may provide a language with a built-in notion of time. This latter point is the most hand-wavy and, in fact, it is the only one that has had no technical development so far (at least as far as I know).

think. Such people, are usually called "controversial" (sometimes even "excentric") by the community. For sure, Y.J. Girard is one of the greatest logicians of our time; yet he is a bit "controversial" :-) $\endgroup$2more comments