hour. Well, we have people coming in late sometimes because of the time change. Also, it's super early, so maybe Greg and... Maybe Greg will come a little bit later because he'll get an hour longer sleep. Okay, okay. Sure. People trickle in. This is like the main... Steven, Adam, Aaron, Juan have been here every session mostly. Yes. So... OK. Let's just start from the end of last session. And I really, really need to put, I have been going through the slides trying to kind of
organize them because I noticed that they're kind of like really all over the place. They need to access some sort of a structure. And they're kind of embarrassing. So I've been starting working on the slides from first session to our current status. And we'll definitely put them in the Dropbox and in Google Drive. As soon as I have done some of them, structured some of them. but I will do the rest and put all of them at once. Because especially it's important as we are moving forward, the amount of formalism that it involves, it requires some going back over the materials
that we have been discussing every week. So we know what we are talking about when we are talking about formalisms and the logical connectives, et cetera. So, before moving forward, as usual, any questions, discussion? I think it's really important for you guys on your own when I'm talking about linear logic because from now on basically everything that we are going to work with has some components of symbolic notations in linear logic, if not other stuff. So it's really important to go on your own and look at the massive amount of text on
linear logic. Look at the introductory text. If you want me to introduce books or introductory essays, I can do that. But definitely make sure that you get at least the meaning of the logical connectives in linear logic right. That's why I'm going to sign today. Last session I talked about some of the symbols and some of the meaning of them, their interpretation, multi-agent system, interactive theory of computation.
I will go again over them to make sure that you can grasp the basic fundaments. But nevertheless, any kind of problem, any kind of discussion, comment that you have, if you have any question about the philosophical aspect of these kinds of stuff, linear logic included, I would be happy to answer. Where did we leave off last week? Because I've had like a 2.30 cut off every day. Oh, okay. Okay.
We... You saw the PetriNet parts, right? Yeah. After the Petri Nets, we moved to—you remember there were what I call the triadic landscape of interactive theory of computation. It was multi-agent system, concurrency, and logical problems. So we moved to the logical problems. Then I introduced the most important part, refinement of Brouwer-hating constructivism on Coldmogor, respectively. The idea that proofs as propositions, this whole trinity between mathematics, computation
and logic where you can have one discovery, you can have discoveries in other branches. And then I talked that in order for us to grasp the fundaments of this constructivism between logic, mathematics, and computation, we need to look at linear logic. So I started to introduce the basic notations of linear logic and gave interpretation of them within that framework of interaction with some stuff about what is exactly the substructure of logic. You suspend the role of weakening and contraction, idempotency and monotensity of entailment in classical logic. And that makes your logical framework resource conscious.
And this resource consciousness, it sounds simple, but it has massive ramifications for the way both classical logic and Brauerian intuitionism are renegotiated. And a little bit talked about why is that it is connected to computationalism. I mean, you can reinterpret Church's lambda definability simply through resource sensitivity of a proof, proof understood as a program or construction. in order to generate this output, what kind of input do you need?
How many times are you allowed to use it? Are you allowed to duplicate it freely or not? So now I will, again, come back to this linear logic and talk about interpretation a little bit more subtly. Great, yeah, that's helpful. I guess I have two notes here that maybe it would be good to clarify. First was with regard to this kind of resource consciousness, because yeah, I have here the linear logic having two sort of important innovations. On classical logic, the first being resource consciousness. The abilities. That is a sort of like hypothesis tracking. The resource in question is argumentation itself and like a method of tracking. Yes, yes.
I mean, the intuitive idea is like when you are making a building, simply construct a building, you need to account for every material and building block that you are using. According to how many times or how many bricks you put in a wall, your structure is completely different. So it's quite an intuitive idea. And one of the things that people always say is that So there is this, because sequence calculus, Gensen's sequence calculus, the way that he transforms 3DN implication entailments to this line by line construction already implied
proofs are programs. But it needed to wait at least a decade or so to some people to make this explicit, to say proofs are programs. It is quite, in fact, so intuitive that all the computer scientists are saying that all these ramifications of this, they were so blind to it. Because from an intuitive perspective, it is quite simple. Any construction need to take to account its building block, its resources, types of inputs, how many times the inputs are used, so on and so forth. And the sort of method for tracking.
Yes. Yes, because you see, and that's where interactive dimension comes to this. you remember this whole idea of interaction that if you decompose your monoidal structure of inference to at least two players, it means that the input that I have, I can decide, but not all of the inputs. So basically this idea that what resource do you choose or you are allowed to choose, some of them are not completely, we do not have the free choice over those resources.
Those are the resources that can be introduced via the interactive framework precisely because an opponent who is playing against us, environment, another machine, another agent, is deciding. Hence, if the choice is made by the opponent, then it means that we have restrictions and constraints over which resources we can use, how many times can we use them. Hence, all of those notations in linear logic that the conjuncts in classical logic is instantly, Once you weaken and suspend the structural rules of weakening and contractions, the conjuncts
in classical logic, they become two. One is the one that you have the choice and the other one that you can have both. But you can have both and one you have the choice but you can either go for this one or that one. Then also it bifurricates the disjuncts, the ones, the inputs that, for example, the opponent or the environment decides for you which of these you can get, you can receive. Like a good example that I will talk about is thinking about this is are these restaurant
menus, specials, you know, specials on the restaurant menu. For example, it says that you can get a burger with fries with coleslaw on one, and the other one is saying that, or you can, for example, get a steak with salad. And you have limited choice of, for example, side dishes or appetizers. And you cannot mix these together. The choice is being made by the restaurant, by the menu. You are free, for example, to combine the side dishes, but you cannot decide, for example, to mix. You cannot simply mix, for example,
burger with salad, because salad comes with a steak. And then I guess the second point for clarification, linear negation, I guess was that second. Yes, linear, you see linear negation, did you read Luca's Go Back to Anfang? No, I don't have any access from here. That was in the glass, Pete. No, no, no, no. It's on her academic page. Okay. Yeah, I recommended that because it puts the whole linear logic and its development in a philosophical perspective.
However, okay, let me tell you this. Linear negation is simply in logic, is generalization of dualities in mathematics, like Duhm-Morgan dualities. And it implies polarity, player opponent. negation is simply behind the function of negation we can see a more fundamental behavior. And that's the interchange of role between interlocutors in a dialogue.
You go, I go, I go, then you counter my move, I counter your move. So what makes negation negation in the first place is this interchange of rules. If it is a two-player game or permutation of rules, if it is a game that involves many players, you know, multiplayer. Now, philosophically, you can think about linear negation simply in terms of Hegelian dialectics. But, and this is, you know, Girard makes this very brief, almost impressionistic reference to the link between Hegel and linear logic as a general framework, particularly linear
negation. And Luca talks about this. Now when I have been going through Girard and all the commentaries about it, it seems that it would be a little bit of a rather opportunistic move, opportunistic philosophical move to interpret linear negation simply as dialectics. Because it's just too easy. I think linear negation has more properties that dialectics cannot index, and precisely is the idea that dualities are special cases of permutation of rules, meaning that only
when polarities, dialectical polarities, between interlocutors happen, we are talking about a two-person game, where we have interchange of roles. Hence, it is very easy to frame as dialectical in the Hegelian sense. But given the fact that the two-person game is itself a special case of many persons' game, then it is harder to define linear negation as a dialectic. So yeah, I genuinely need to think about this more carefully, but I'm still not convinced that it's in fact, yes, it is in fact useful to intuitively think
about this philosophically as Hegelian dialectics, but I would think that it is really just a trivial superficial isomorphism between the two. And even if Girard makes the connection, that just doesn't mean anything. Yes, it is a dialogue, so what? But what is it exactly tells us about the fundamental aspect of the phenomena that are at the stake, dialectics and linear negation? Yeah, great. Yeah, and I'll take a look at that and then we can come back to it. Sure. Go on, Adam.
Just following on from the resource consumption type formulation of the axioms, right, so you sort of have to consume these axioms, and so I found that fairly intuitive if you think of it as like execution of a program or whatever, well, the axiom doesn't come for free, you have to sort of execute through it. Yes. and prove it in some way. But what was a little bit unintuitive was the default sort of aspect to it where once you consumed an axiom, you couldn't use it again. You can't use it again. In linear logic, you can't use it again. It's in classical logic. It has to be, it's consumed, right?
It's consumed. And if you want to use it again, you either need to have a free context so you can use exponentials in linear logic, like that exclamation mark, of course, which allows you to use them because they are context free or you need to be permitted again by the environment or whoever has provided you with that resource. So everything, yes. So it's not that linear logic completely suspends arbitrary infinite resources, or reusable
resources. It just restricts them. It makes their tracking possible. So yes, you can in fact use it even in linear logic framework, reuse a resource, but then you need to have a reason, a good reason to do so. That only happens if your axioms, for example, in certain cases are context free, hence you can reuse them. But if they are context sensitive, then you can't reuse them. You need to come back again to that context in order to be able to adjudicate whether I can use this resource or not based on this context that I have been given.
For example, the environment makes the move. Am I free to make this choice or not? At this part, for example, at this step of the program or a step of the proof. Okay, so that aspect of context sensitivity I guess makes more sense to me. Because I guess the way I was thinking of it before is you have an axiom, okay sure it costs resource, the obvious analogy is computing time to me, but you sort of compute the axiom