Linear logic: Difference between revisions

Revision as of 21:53, 3 January 2024

Revision as of 09:37, 12 March 2024

Line 278:

===Exponentials===

The exponentials are used to give controlled access to weakening and contraction. Specifically, we add structural rules of weakening and contraction for {{math|?}}'d propositions:<ref>Girard (1987), p.25-26, Def.1.21</ref>

{| style="margin:auto"

Line 328:

|}

One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives, resembling the inference rules governing modalities in sequent calculus formalisations of the [[normal modal logic]] [[S4 (modal logic)|S4]], and that there is no longer such a clear symmetry between the duals {{math|!}} and {{math|?}}.

This situation is remedied in alternative presentations of CLL (e.g., the [[Logic of unity|LU]] presentation).