So I think we can start then.

There are two things that I should clarify.

First, I realized that the rule that I gave following book of Pym and several early references for left introduction rule for this junction was mistaken in all of these references.

And I only realize it now when I try to prove for myself soundness result that we want to do today in respect to this resource monolayer solution last time.

I started and of course I got stuck in the clouds for the left of this junction.

I started to look for it and then I realized, I found out something that I read long ago.

Only one paper from 2005 there is a small footnote saying that Pym made a paper cover by Pym himself.

That he made a mistake in this book but he forgot to edit it before they went to print.

The mistake was copied in several papers and now they can give the proper form of that rule.

So, funny enough what he says there is that the left rule for, there are no consequences of that mistake.

These are disingenuous for me because either this rule is sound or not.

I realized it only when I was comparing with you last time so I didn't have time to try to find a good example.

But just for... All the errors in the erratum are without known consequences strangely, right?

Errors in what? In the erratum, I mean, why are you not referring to the erratum to Pym's book?

Yes, yes, yes, yes, yes.

So, Ruzik has mentioned that the erratum actually gave wrong definition for the leftist ranking. Have you seen it? I didn't check the erratum.

No, I didn't check that. I mean, there are lots of errors regarding the completeness of the book apparently.

Yeah, so the leftist sanction rule that we can use is actually then much, much simpler.

In fact, this is exactly the rule that we derived, I think. Let me double check if this is the rule that we derived.

The left side.

Yes, this is the rule that we derived for the disjunction. So now this is not a derived rule but from now on we have to call this rule simply that rule for the leftist sanction. So just for...

Let me write this in words. This is from now on, this is...

The one given in the lectures following Pym's book and other early references.

Well, I don't want to blame that this is not sound, not having an example, but it is mistaken.

It's actually good question if regardless of the statement that this is without known consequences we can find an example of derivation which shouldn't even sound with respect to our intended semantics.

But...

Okay, so this is one thing and the other thing was pertaining to the definition of our resource monoid, the proper way of defining partial... the associativity law for partial operations.

We had some discussion during the last lecture about this. I checked how it is set up with the reference. In some of the references it is completely glossed over.

So it just says that it's a natural definition or whatever. And in some of the references I was able to find an explicit definition and it indeed seems to postulate less than what was postulated last time.

So, correction number two.

Definition of partial pre-order resource monoid clause for associativity.

So, what was stated at least in the... in one of the paper by Galen and Kalemyshyn co-authors was simply that if mn times o is defined,

then mn times o is equal to mn times n o.

But actually if you look at this, then this thing defined must mean that this thing is defined in particular.

So we could as well state that this thing has to be defined and then we could derive as a consequence in particular if this thing is defined, then this thing must be defined as well.

It doesn't make sense otherwise to speak about m times o otherwise.

So in the end it seems to me that all those definitions that one can reasonably write are redefining one and the same thing, but if we need one fixed definition then probably it's best to stick to the definition that we see explicitly in some of the references.

This definition couldn't it be that in this equation the right hand side is defined and the left hand side is busy?

No, this is a commutative.

So indeed we are using the fact that our resource monolinks are commutative ones and just like in the linear case we never dealt in fact with the situation where our operations were not commutative.

It is sometimes considered, this is really what this thing called full number calculus that I was telling you about when introducing the idea of substractural logic is all about.

And for some applications for example in linguistics I think that I even mentioned at that time is not even a good thing to insist that this multiplicative conjunction or fusion or whatever it is, is always a valid define.

Right, so we had a bunch of structures, partial pre-order resource monolinks, total pre-order resource monolinks, partial discrete resource monolinks and total discrete resource monolinks.

And now we are going to see some of them in real life.

So of course the trigger thing to do is to pick any commutative monoid at all and impose them in the discrete order.

Then all the other clauses in the definition would be trivially satisfied.

Maybe let's start with this.

And then, standard mathematical because of course we will see some other example of monolinks in what follows.

But for the time being let's make it clear that here I mean in terms of natural, rational, real, commutative one of course.

With the discrete order.