The present report is a, somewhat lengthy, addendum to "A new deconstructive logic:
linear logic," 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 interpre-
tation 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.