[For the entire collection see Zbl 0667.00009.]
The author’s general style has been familiar since the Greeks, especially in periods of stagnation, both of ultimately successful projects and of duds. He uses cozy clichés from past and present: contemporary “underlying structures” or “dynamics”; Kant had “all possible behaviours”; “intuition of time” is perennial. A common element of the style is summarized in an aphorism of Heraclitus, which the author takes as his motto (for example, in his book on proof theory). For good or ill, the style is unusual in comtemporary mathematics, but the author’s job is not. Specifically, his no longer very-recent linear logic, LL, is an attractive addition to the arsenal of proof theory; at least, for this reviewer [cf. J.-Y. Girard, Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)]. It has been related to other parts of mathematics like \(C^*\)-algebras; so general that almost anything can be related to them. The particular formal properties of LL, which he singled out for attention originally, were quickly found to be familiar in various marginal parts of proof theory [cf. A. Avron, ibid. 57, 161-184 (1988; Zbl 0652.03018)] for partial (orthodox) documentation. So, what next? besides, of course, giving LL a rest. One option, suggested by the author’s reference to computation, is to take genuine, but possibly isolated contributions of proof theory - for example, to the unwinding of proofs -, and see where, if anywhere, LL does better. (As long as only generalities are involved, familiar experience is at least as suitable as electronic computation). Another is described by the author in the abstract. In simple terms - less breezy than his, but also less reverent (on what Hilbert and Brouwer “still have to say”, tacitly, in their traditional vein) - it is admitted that (a) the ideas of the pioneers are woefully inadequate for - data processing in - ordinary mathematics at the time, and even more today. But (b) just because computation, especially, of the electronic kind, is special, the ideas may have special potential here. So (c) at least some formal properties of LL should be interpreted in terms of (some of) those ideas. Of course, this is not a blue print since, for example, (c) is all too easy if mere coherence is the principal constraint on the interpretation (and the ideas must not be taken too literally since - as the pioneers meant them - they may not fill the bill). But it is quite precise enough to present - what seem to the reviewer - most rewarding questions. For example, on p. 92, a matter of terminology - the choice between “operational semantics” and “geometry of interaction” - immediately recalls 50 years of experience with (set-theoretic) semantics for ordinary (classical) mathematics: What has it contributed to those areas where even the most stringent demands on semantics are satisfied impeccably? Whatever the implications for the author’s particular option, for logicians such reminders may be grist to their mill. At least, in the forties - not the seventies, of course - when looking back on his work Gödel interpreted his marvellous theorems as correcting similarly grotesque blind spots; of accepting (or rejecting) without a moment’s thought the equation: truth \(=\) (formal) derivability or the fuss about the alleged absurdity of the reducibility axiom.