# zbMATH — the first resource for mathematics

Geometry of interaction. I: Interpretation of system F. (English) Zbl 0686.03030
Logic colloq. ’88, Proc. Colloq., Padova/Italy 1988, Stud. Logic Found. Math. 127, 221-260 (1989).
[For the entire collection see Zbl 0673.00007.]
The author provides an explicit formula for cut elimination from Gentzen- type derivations. To each derivation $$\Pi$$ in second order linear logic, two matrices u, $$\sigma$$ are assigned, and the proof of the following fact is sketched. The normal form of $$\Pi$$ under the standard cut elimination procedure is given by the matrix $$EX(u,\sigma)=(1-\sigma^ 2)u(1-\sigma u)^{-1}(1-\sigma^ 2)$$ provided the final sequent of $$\Pi$$ does not contain the connectives ?, $$\exists$$. Coefficients of the matrix u are bounded operators in Hilbert space, and coefficients of $$\sigma$$ are 0, 1, describing in a straightforward way cuts present in the proof $$\Pi$$. Intuitionistic and classical logic probably can be treated via the author’s embedding in linear logic [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)]. A specific $$C^*$$-algebra $$\Lambda^*$$ is introduced to model linear logic. The author makes a lot of optimistic comments concerning possible future applications of functional analysis to the study of linear logic, and of linear logic to the study of interactive computations.
Reviewer: G.Mints

##### MSC:
 03F05 Cut-elimination and normal-form theorems 03B70 Logic in computer science