Jean-Yves Girard writes at the end of his paper
"[Towards a Geometry of Interaction](http://jb55.com/linear/pdf/Towards%20a%20geometry%20of%20interaction.pdf)", page 105, that we have three intuitions about the nature of time: 


1. time is logic modulo the order of rules,
2. time is the cut elimination process,
3. time is the contents of noncommutative linear logic.


Can anyone explain what these means? 
Does anyone know if Girard has developed these thoughts any further?



Time in Girard's Geometry of Interaction
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:


1. logic as proof search;
2. logic as functional programming;
3. 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](http://www.pps.univ-paris-diderot.fr/~mellies/tensorial-logic.html) and the [theory of programming languages](http://existentialtype.wordpress.com/?s=polarity) 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](http://www.cs.cmu.edu/~blelloch/papers/BG95.pdf) by Blelloch and Greiner or [this very recent paper](https://sites.google.com/site/beniaminoaccattoli/Accattoli%2C%20Dal%20Lago%20-%20Beta%20Reduction%20is%20Invariant%2C%20Indeed.pdf?attredirects=0) 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](http://en.wikipedia.org/wiki/Temporal_logic)) 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).


