I only gave one rule for zero and it was supposed to be symmetric so that there should be two

rules for if there are two rules for one there should be two rules for zero. What have we

done? We have done so far multiplicative conjunction. So linear logic continuous. We did also the

additive conjunction. We did multiplicative disjunction I think. So this is written as

star tensor star fusion times. This additive conjunction is written as this is the Girard

notation. And this is the square cap and sometimes the lattice meet. Multiplicative disjunction

written in our notation I propose writing plus in Girard's notation should be ampersand

and upside down. Let me have another look. Right I think I got it better. So par, unit

multiplicative. Actually we did also the truth constants so we did both multiplicative and

additive unit. So I am writing it as one. I think that was one of the few connectives

that he didn't write in a strange way. Yes, yes that's the only one which was just one.

Sometimes written as I. Multiplicative unit, additive unit or truth constant. These rules

we all have left and so for all these guys we have left and right rules in this case

we have just right rule. Maybe I should have a look what is written in those. So I would

just write it as I am writing it here as top. Sometimes written as true. Girard's own notation

or Girard's notation was again here it was I think consistent with general logic of constants.

And then the first rule that was missing in what we wrote yesterday was zero. The name

that Girard was using was well. Unit for par or dualizing element. I don't know how to

call it otherwise. So I am going to use notation zero. Girard's notation confusingly enough

was bottom even though it wasn't the smallest element of the lattice. There was a good convention

proposed by Costa-Dozen to write for the additive constants like for the additive truth capital

T and here is small t. Well to an extent we are following this. And then for the additive

zero write small f and sorry capital F and for multiplicative zero small f which at least

has the advantage of being maybe easier to digest for somebody accustomed to Girard's

notation. So neutral maybe less simply write it neutral element for par. And then I gave

you only one rule right? Can I have a look at what was written so far? I only gave left

rule for this and there should be of course right rule for this. So we had and this is

the empty thing. So this is the left rule and the right rule was dual to of course the

rule for unit. So as I said this is neutral element. So comma on the left hand side is

really metalinguistic expression of this multiplicative conjunction tens or times or whatever and

comma on the right hand side is metalinguistic expression of this multiplicative disjunction.

And now we are still missing the disjunction right? Wait wait wait wait wait wait wait

yes actually yes yes yes yes sorry. The problem is that I am already starting to think like

linear classical linear logitian in terms of single sided sequence. So we will see single

sided version of sequence calculus for linear logic today because you see it in almost every

reference on linear logic so it would be rather hard for you to read or to look up in any

book or chapter without knowing why they are writing single sided sequence. And it is actually

useful exercise to work out why this formulation is equivalent to the two sided one. Right

so that is it for constants and well we still need also additive bottom. So let us call

it multiplicative zero. I do not want to call it false but bottom element actually what

was the name Jirard himself was proposing for this yeah it is smallest element simply.

Neutral element for aha I did not write what this bottom no no no before I introduced neutral

element for additive disjunction I introduced additive disjunction itself. So maybe let

us do this first. And then the rules for additive disjunction should be simply dual forms duals

of the rules that we have for additive conjunctions of normal lattice connectives. This is Jirard

notation this is the one that we are going to be following for example the book by Trelstra

lecture or linear logic. What was the name being used apart from plus for this plus or

for this. So obviously you have this so these are the right rules.

And just like in case of conjunction we were seeing the difference between the way you

accumulate information on the right hand side with disjunction we should see the difference