Surely you're joking, Mr Martin-Löf?...

Many, many years ago, when I was a young postdoc I gave a talk in Uppsala about Dialectica categories and Full Intuitionistic Linear Logic. I was pretty pleased with how the mathematics of my thesis had panned out and when question time came and I had a question from a distinguished Swedish professor, I thought I was on safe grounds. He asked "ok, this is all very well, the categorical constructions are nice, I can see why you might want to consider a more intuitionisitic version of a multiplicative disjunction, but...what does it all mean? How do you tell a man in the street what you do?" And yes, the distinguished professor whom I had not met till then, was prof Per Martin-Löf (second from the right in the picture above) and it took me several years to get at least preliminary answers to his (very reasonable we all agree) questions.

Now the question is in Twitter, pestering me again, and I still do not have a proper answer. But I have a suggestion, given to me by Luiz Carlos Pereira, a good friend and collaborator. (It took me more than 3 hours ransacking my old notebooks to find it, so I feel that I should write it down, as well as I can, in this week of drowning-by-reviews...)

Now, everyone knows and some of us do enjoy shopping. The earlier Linear Logic examples were all about Camels and Malborough packets. Some people decided to change them to chocolate and coffee, but the vending machines stayed. Now in this era of Amazon and Walmart, let us describe a "FashionMall Semantics". (In Rio, "fashion mall" is not a common noun compound, but a proper noun. It's a sophisticated shopping center in one of the most unequal, on your face, terrible, parts of town, where the `favela'  and the uber-consumption face each other, in threatening ways. still...)
Anyways the FashionMall in Sao Conrado has all kinds of stores you might want to buy nice things from. So if the mall issued tickets for shopping, you could think of these tickets as ways of satisfying consumers' orders:

•  If the mall gave you a ticket marked A\otimes B, then the mall has to have both A and B in stock and when you use your ticket, you  take both A and B  home.

• If the mall gave you a ticket marked A&B, their stock has to have both, but you, the customer, can only take one of them home. You can choose which one A or B  you take home.

• If the mall gave you a ticket marked A\oplus B, the stock only has to have one of A or B and the seller will choose which one it will give you. 

So far so good and similar to other explanations of Linear Logic using commercial transactions. But what can we say about A\par B?  Well, if the mall gives you a ticket marked A\par B they must have both in their stock,  you, the customer can only take one home, but you can take it back to the mall and swap it for the other one, if you want to do it. (The par operator is commutative, in the way that linear implication is not...)You do have to keep one of the two (A or B), though.

So more interesting still, if the mall gave you a ticket marked A\lollipop B what can we say?  Then we have a complicated transaction: if the buying of the antecedent  A is satisfied, then the buying of the consequent B has to be satisfied, whatever these buyings may be.  (some might use  "higher-order rule" to describe this transaction, but this  is somewhat familiar from  BHK-style interpretations.) Following this line of reasoning, a transaction A\lollipop \bot could be a transaction that cannot be satisfied.

And the units of Linear Logic, what happens to them? Well some "buys" cannot be satisfied, because the mall does not have the required stock. Other buys cannot be satisfied independently of the stock, just relating to what the costumer and the seller want to do.

There is much more that we need to work out to make  sure these intuitive notions  agree with the mathematics of Full Intuitionistic Linear Logic, but I hope this is enough to start the conversation. (and it gives me the chance to post a picture of friends Per, Steve and Richard, as well as the late Vladimir Voevodsky whom I had never had the pleasure of meeting: he really seemed a nice guy.)