Multiplicative UnitFailure of HarmonyAlternative ConjunctionAdditive UnitDisjunctionDisjunctive UnitPersistent TruthOf Course!Example: Beggars RevisitedExample: Two NickelsExample: MenuExercisesReferencesLecture Notes onHarmony15-816: Linear LogicFrank PfenningLecture 3January 23, 2012In the last lecture we started developing the propositional connectives oflinear logic. Specifically, we introduced simultaneous conjunction A ⊗ Band linear implication A ( B. Each connective is determined by giving leftand right rules in the sequent calculus that specify how to use a resource orprove a goal with that connective. We also explicated two tests we apply todetermine if the logical connectives are meaningful: identity expansion andcut reduction. If they both hold we say that the left and right rules for theconnectives are in harmony. We continue to develop additional connectives,and also explore some consequences of a failure of harmony between leftand right rules.1 Multiplicative UnitWhenever we have a binary operator, A⊗B in this case, we should considerif it has a unit. In this case, the unit is written 1, and has the property thatA ⊗ 1 and 1 ⊗ A are equivalent to A. We can try to derive the rules for 1systematically, by thinking of it as a multiplicative conjunction with zerocomponents. Below, we show the binary rule first, and the nullary rulesecond.∆ ` A ∆0` B∆, ∆0` A ⊗ B⊗R· ` 11RA ⊗ B has two components, so ⊗R has two premises. Correspondingly, 1has no components and no premises. This also means that we require thatthere are no resources, indicated above by writing ‘·’. In summary, 1 holdsas a goal if we have no resources.LECTURE NOTES JANUARY 23, 2012Harmony L3.2Looking at the left rules:∆, A, B ` C∆, A ⊗ B ` C⊗L∆ ` C∆, 1 ` C1LA ⊗ B has two components, so they both appear as new resources in thepremise. 1 has no components, so no new resources appear in the premise.The left and right rules for 1 are in balance. First, the local expansion:1 ` 1id1−→E· ` 11R1 ` 11Land then the reduction· ` 11R∆0` C∆0, 1 ` C1L∆0` Ccut1−→R∆0` CWe should verify that A⊗1 is equivalent to A. But what does this mean?We take it to mean that both A ⊗ 1 ` A and A ` A ⊗ 1. We just give a shortexample proof, the other direction and other versions are similarly easy toprove.A ` AidAA, 1 ` A1LA ⊗ 1 ` A⊗LThe multiplicative unit is useful in specifications to eliminate resources,using the idiom A ( 1.2 Failure of HarmonyWe investigate the consequences of a failure of harmony in one case. Let’sassume had replaced the left rule for simultaneous conjunction with thefollowing two rules:∆, A ` C∆, A ⊗ B ` C⊗L1??∆, B ` C∆, A ⊗ B ` C⊗L2??LECTURE NOTES JANUARY 23, 2012Harmony L3.3First we note that identity expansion indeed fails. We show one attempt;others fail similarly.A ⊗ B ` A ⊗ BidA⊗BA ` AidA??· ` BA ` A ⊗ B⊗RA ⊗ B ` A ⊗ B⊗L1??It turns out that with these the two incorrect left rules, weakening∆ ` C∆, A ` Cweakenbecomes a derived rule of inference. This, of course, violates the basic prin-ciple that ephemeral resources must be used exactly once, because A is in-deed not used. Before reading on, we suggest you try to prove this yourself.LECTURE NOTES JANUARY 23, 2012Harmony L3.4A ` AidA· ` 11RA ` A ⊗ 1⊗R∆ ` C∆, 1 ` C1L∆, A ⊗ 1 ` C⊗L2??∆, A ` CcutA⊗13 Alternative ConjunctionUsing our rules for coin exchange, we can prove q ` d⊗d⊗n and also q ` q.But clearly we can not prove q ` (d ⊗ d ⊗ n) ⊗ q, because we would haveto use q twice in the proof. Still, with the resource q we can actually proveboth! To express this situation inside the logic as a connective we writeA N B, pronounced “A with B”. It is variously called alternative conjunctionor additive conjunction. With this connective we can prove q ` (d ⊗ d⊗n)N q.We can achieve this as a goal from resources ∆ exactly if we can achieve Afrom ∆, and also B from ∆.∆ ` A ∆ ` B∆ ` A N BNRThis appears to be a violation of linearity: the resources in ∆ seem to beduplicated. But we are saved, because when we have a resource A N B wehave to choose between A and B. We cannot get both. This means that ∆ isnot really duplicated, since only one of the two premises will ever be used,as we will check shortly.∆, A ` C∆, A N B ` CNL1∆, B ` C∆, A N B ` CNL2The informal reason that the “duplication” of ∆ does not destroy linearityis reflected in the identity expansion and cut reduction. It is most clear inthe reduction, so we show this first.∆ ` A ∆ ` B∆ ` A N BNR∆0, A ` C∆0, A N B ` CNL1∆, ∆0` CcutANB−→R∆ ` A ∆0, A ` C∆, ∆0` CcutALECTURE NOTES JANUARY 23, 2012Harmony L3.5In fact, there is another symmetric reduction, when the second premise ofthe cut is inferred with the NL2rule. The identity expansion isA N B ` A N BidANB−→EA ` AidAA N B ` ANL1B ` BidBA N B ` BNL2A N B ` A N BNR4 Additive UnitAs for multiplicative conjunction with unit 1, there is a nullary version ofadditive conjunction. The unit is > (pronounced “top”). Again, its rulescan be derived systematically from the rules for additive conjunction. Theright rule has zero premises, propagating the resources ∆ to all of them.A N B has two conjuncts and therefore two left rules; > has zero conjunctsand therefore zero left rules.∆ ` >>Rno >L ruleOf course, there is now no cut reduction since there is no left rule for >. Butthere is still an identity expansion.> ` >id>−→E> ` >>R5 DisjunctionWe have seen that alternative conjunction stands for a kind of choice. If wehave a resource A N B we have a choice wether to use A or B in our proof.If we have a goal A N B we have to account for both uses.Disjunction is symmetric to this. If we have a resource A ⊕ B the envi-ronment must provide either A or B, so we have to account for both possi-bilities. Conversely, if we have a goal A ⊕ B we can satisfy it by providingA or by providing B.∆ ` A∆ ` A ⊕ B⊕R1∆ ` B∆ ` A ⊕ B⊕R2∆, A ` C ∆, B ` C∆, A ⊕ B ` C⊕LWe leave the identity expansion and cut reduction to Exercise 5.LECTURE NOTES JANUARY 23, 2012Harmony L3.66 Disjunctive UnitThere is also a unit of disjunction 0, which is a form of falsehood. We canobtain its rules as the nullary versions of disjunction.no 0R rule ∆, 0 ` C0LWe leave its properties to Exercise 6.7 Persistent TruthThe most difficult connective to add is one to internalize