## Jean-Baptiste Joinet, Harold Schellinx, and Lorenzo Tortora de Falco.
SN and CR for free-style *LK*^{tq}: linear decorations and
simulation of normalization.
*Journal of Symbolic Logic*, 67 (1):162-196, 2002.

The present report is a, somewhat lengthy, addendum
to citeDanJoiSche97, where the elimination of cuts from derivations
in sequent calculus for classical logic was studied `from the point of
view of linear logic'. To that purpose a formulation of classical logic
was used, that - as in linear logic - distinguishes between *
multiplicative* and *additive* versions of the binary
connectives. The main novelty here is the observation that this *
type-distinction* is not essential: we can allow classical sequent
derivations to use *any* combination of additive and
multiplicative introduction rules for each of the connectives, and still
have strong normalization and confluence of *tq*-reductions. We give a
detailed description of the simulation of *tq*-reductions by means of
reductions of the interpretation of any given classical proof as a proof
net of **PN2** (the system of second order proof nets for linear
logic), in which moreover all connectives can be taken to be of *
one* type, e.g. multiplicative. We finally observe that dynamically
the different logical cuts, as determined by the four possible
combinations of introduction rules, are *independent*: it is not
possible to simulate them *internally*, i.e. by only *one*
specific combination, and structural rules.

[ bib |
.html ]

Back

*This file has been generated by
bibtex2html 1.60*
>>> BackToHomePage(Protocollo) <<<