Linear logic: Difference between revisions

Revision as of 03:38, 13 October 2022

Revision as of 18:34, 15 December 2022

Line 9:

===Syntax===

The language of ''classical linear logic'' (CLL) is defined inductively by the [[Backus–Naur form|BNF notation]]

Line 34 ⟶ 35:

|}

Here {{math|<VAR>p</VAR>}} and {{math|<VAR>p</VAR>^⊥}} range over [[Atomic formula|logical atoms]]. For reasons to be explained below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and ⊥ are called ''multiplicatives'', the connectives &, ⊕, ⊤, and 0 are called ''additives'', and the connectives ! and ? are called ''exponentials''.

We can further employ the following terminology:

over [[Atomic formula|logical atoms]]. For reasons to be explained

below, the [[Logical connective|connectives]] ⊗, ⅋, 1, and

⊥ are called ''multiplicatives'', the connectives &,

⊕, ⊤, and 0 are called ''additives'', and the

connectives ! and ? are called ''exponentials''. We can further

employ the following terminology:

{| class="wikitable"

|+

Line 73 ⟶ 70:

Binary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &.

Every proposition {{math|<VAR>A</VAR>}} in CLL has a '''dual''' {{math|<VAR>A</VAR>^⊥}}, defined as follows:

{| border="1" cellpadding="5" cellspacing="0" style="margin:auto"

|-

Line 108 ⟶ 106:

| & ⊤ || ⅋ ⊥ || ?

|}

Observe that {{math|(-)^⊥}} is an [[Involution (mathematics)|involution]], i.e., {{math|<VAR>A</VAR>^⊥⊥ {{=}} <VAR>A</VAR>}} for all propositions. {{math|<VAR>A</VAR>^⊥}} is also called the ''linear negation'' of {{math|<VAR>A</VAR>}}.

The columns of the table suggest another way of classifying the connectives of linear logic, termed '''{{em|{{visible anchor|polarity}}}}''': the connectives negated in the left column (⊗, ⊕, 1, 0, !) are called ''positive'', while their duals on the right (⅋, &, ⊥, ⊤, ?) are called ''negative''; cf. table on the right.

''{{em|{{visible anchor|Linear implication''}}}} is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by {{math|<VAR>A</VAR> ⊸ <VAR>B</VAR> :{{=}} <VAR>A</VAR>^⊥ ⅋ <VAR>B</VAR>}}. The connective ⊸ is sometimes pronounced "[[lollipop]]", owing to its shape.

==Sequent calculus presentation==

Line 120 ⟶ 119:

We now give [[Sequent calculus#Inference rules|inference rules]] describing how to build proofs of sequents.<ref>Girard (1987), p.22, Def.1.15</ref>

First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [[exchange rule|exchange]]:

[[exchange rule|exchange]]:

{| style="margin:auto" border="0"

Line 132 ⟶ 130:

|}

Note that we do '''not''' add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present.

absence of propositions in a sequent, and the number of copies present.

Next we add ''initial sequents'' and ''cuts'':

{| style="margin:auto"

|-

Line 159 ⟶ 157:

|}

The cut rule can be seen as a way of composing proofs, and initial sequents serve as the [[identity element|units]] for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof.

for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this [[canonical form]] property (which can be divided into the [[completeness of atomic initial sequents]] and the [[cut-elimination theorem]], inducing a notion of [[analytic proof]]) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware [[lambda-calculus]].

Now, we explain the connectives by giving ''logical rules''. Typically in sequent calculus one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification).

In a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗).

one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning

So, we should expect a certain [[Logical harmony|"harmony"]] between the rule(s) for a connective and the rule(s) for its dual.

about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective

(say ⅋) effectively play the role of left-rules for its dual (⊗). So, we should expect a certain [[Logical harmony|"harmony"]]

between the rule(s) for a connective and the rule(s) for its dual.

===Multiplicatives===

The rules for multiplicative conjunction (⊗) and disjunction (⅋):

{| style="margin:auto"

|-

Line 195 ⟶ 192:

and for their units:

{| style="margin:auto"

|-

Line 218 ⟶ 216:

|}

Observe that the rules for multiplicative conjunction and disjunction are [[Admissible rule|admissible]] for plain ''conjunction'' and ''disjunction'' under a classical interpretation

plain ''conjunction'' and ''disjunction'' under a classical interpretation

(i.e., they are admissible rules in [[Sequent calculus#The system LK|LK]]).

Line 225 ⟶ 222:

The rules for additive conjunction (&) and disjunction (⊕) :

{| style="margin:auto"

|-

Line 257 ⟶ 255:

|}

|}

and for their units:

{| style="margin:auto"

|-

Line 273:

|}

Observe that the rules for additive conjunction and disjunction are again admissible under a classical interpretation.

But now we can explain the basis for the multiplicative/additive distinction in the rules for the two different versions of conjunction: for the multiplicative connective (⊗), the context of the conclusion ({{math|Γ, Δ}}) is split up between the premises, whereas for the additive case connective (&) the context of the conclusion ({{math|Γ}}) is carried whole into both premises.

under a classical interpretation. But now we can explain the basis for the multiplicative/additive distinction

in the rules for the two different versions of conjunction: for the multiplicative connective (⊗),

the context of the conclusion ({{math|Γ, Δ}}) is split up between the premises, whereas

for the additive case connective (&) the context of the conclusion ({{math|Γ}}) is carried whole into both

premises.

===Exponentials===

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

structural rules of weakening and contraction for ?'d propositions:<ref>Girard (1987), p.25-26, Def.1.21</ref>

{| style="margin:auto"

|-

Line 306 ⟶ 302:

|}

|}

and use the following logical rules:

{| style="margin:auto"

|-

Line 329 ⟶ 327:

|}

|}

One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives,

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, and that there is no longer such a clear symmetry between the duals ! and ?. This situation is remedied in alternative

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

==Remarkable formulas==

Line 436 ⟶ 434:

Multiplicative disjunction {{math|(<VAR>A</VAR> ⅋ <VAR>B</VAR>)}} is more difficult to gloss in terms of the resource interpretation, although we can encode back into linear implication, either as {{math|<VAR>A</VAR>^⊥ ⊸ <VAR>B</VAR>}} or {{math|<VAR>B</VAR>^⊥ ⊸ <VAR>A</VAR>}}.

== Other proof systems ==

=== Proof nets ===

{{main|Proof net}}

Introduced by [[Jean-Yves Girard]], proof nets have been created to avoid the ''bureaucracy'', that is all the things that make two derivations different in the logical point of view, but not in a "moral" point of view.

Line 475 ⟶ 474:

The goal of proof nets is to make them identical by creating a graphical representation of them.

== Semantics ==

=== Algebraic semantics ===

{{See also|Quantale}}

Line 504 ⟶ 503:

{{Portal|Philosophy}}

* [[ProofChu netspace]]s

* [[Linear type system]], a [[substructural type system]]

* [[LogicComputability of unitylogic]] (LU)

* [[Proof net]]s

* [[Geometry of interaction]]

* [[Game semantics]]

* [[Geometry of interaction]]

* [[Intuitionistic logic]]

* [[ComputabilityLinear logic programming]]

* [[Linear type system]], a [[substructural type system]]

* [[Logic of unity]] (LU)

* [[Ludics]]

* [[ChuProof spacenet]]s

* [[Uniqueness type]]

* [[Linear logic programming]]

==References==

{{Reflist}}

==Further reading==

* Girard, Jean-Yves. ''[http://girard.perso.math.cnrs.fr/linear.pdf Linear logic]'', Theoretical Computer Science, Vol 50, no 1, pp.&nbsp;1–102, 1987.

* Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. ''[https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html Proofs and Types]''. Cambridge Press, 1989.

Line 535 ⟶ 536:

==External links==

* {{Commons category-inline}}

* [http://bach.istc.kobe-u.ac.jp/llprover/ A Linear Logic Prover (llprover)], available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan

{{Non-classical logic}}