Okay, Reza, now you can go to the screen again. For some reason, it doesn't allow me to get the... No? OK, one second. Yeah. Can you see this? Yes. So our starting point to this idea that test comes within the syntax itself in linear logic
and the idea that Girard gives an autonomy to syntax, is to identify a proposition A in bold with a set A, it's in italic, where we can think of the elements as observations, explanations, models, proof, et cetera, for the proposition. Now, these elements are determined by a testing process. A belongs to set A if and only if successfully, if A, that A
needs to be in italic, successfully passes a set of tests or the set A. Noted test of A. A useful metaphor here is to think of A as a set of strategies or proofs for a player prover to win a game, i.e. prove the proposition, bold A. And test A as a set of counter strategies or counter models for a player refuter to prohibit the win. I exhibit a model that invalidates Proposition A." So the whole idea of testing, as we talked about, and this idea of testing, again, you
You can think of this in a constructivist style of Brouwer, Haytingham, Kolmogorov, generating input to, sorry, consuming an input to generate an output, how to solve a problem given this set of premises, how to construct a conclusion from a set of hypotheses. And as we implied at the end of the last session, the whole idea of linear logic and the way that this constructivist approach is done is within a ludic or game-oriented framework.
The game is really a testing procedure through which you can determine the meaning of syntactic compound. So again, a useful metaphor here is to think of A as a set of strategies, proofs, for a player prover to win a game, i.e. prove the proposition A, and test of A as a set of counter strategies or counter models for a player refuter to prohibit the win, i.e. exhibit a model that invalidates A. However, notice that this duality of prover and refuter is
somewhat asymmetric. The burden of proof rests upon the shoulder of the prover. Following Girard, we will ask that the duality, elements of A, test for A, be monist, i.e. that the elements and tests belong to the same universe, E. Also, we will ask that the testing process be symmetric, i.e. that tests for A are simultaneously tested by the elements of A. Informally, we have that in the following notation. And since by symmetry, the elements of A, that's the italic A, are a test for test A, we have A equals to test of test of
A. In the analogy of a game prover versus refuter, we let the strategies consist of formal proofs of proposition A against formal proofs of not A. A here is a set. Therefore, in Girard's transcendental syntax, a proposition also called a dichology is a set of elements that epistates equal to its double negation. In other words, negation is an involuntary testing process. What are these terminologies? Epistates in Girard vocabulary, which is quite outlandish, refers to some kind of judge or magistrate in ancient Greece. And dichology is a neurology that means discourse in two parts.
So you see, and Aaron, when you said about linear integration, Negation, and I said that in classical logic, negation and also double negation, all the controversies about this idea of double negation and stuff, it always comes with a kind of a a priori definition of negation, we take for granted what negation is. The thing about Girard's linear logic, or this whole Brouwer-Hating, Kolmogorov, Corey Howard, Lambeck style of
constructivism, is that it allows us to define what negation is in the first place. Negation, From a computational perspective, at the deepest logical level, is an involuting testing process. Now depending on whether it's a two-person game or a multi-person game, the idea of linear negation changes precisely because your testing process changes. interaction between refuters, opponents, or players, so on and so forth.
So to make this idea of testing and proving and the rectifications that Girard makes in classical, in both classical and intuitionistic frameworks, the best way to approach these things is to, again, have a summary account of notations in linear logic and how they are derived from classical logic. Exactly what kind of rectification Girard makes to classical logic and then what are
are the ramifications of these adjustments, or suspensions, or rectifications. As I briefly mentioned at the end of last session, we have three forms of inference. And these three forms of inference could be viewed as sorting mathematics into three levels. A arrow B implies, or the notation for implication represents a sort of implication within the statement of a proposition. Example, if A is true, then B is true. This is simple implication in logics and mathematics. A turnstile B is the sort, and if you remember,
That was the first person who came up with this notation of term style, is Gensen. There's a sort of implication between propositions. Example, assuming A can prove B. So the second level is implication is no longer simple. Implication is interpreted as truth. And that's the explicit consequence of sequential judgment, sequence calculus, basically, of Gensen.
Then the third level, A term style B over C term style B. As you see, you have two lines and two sequence that are related to one another. It's a sort of implication performed in the process of proving. Given a proof of B from A, one can prove D from C. In this sense, the rules of inference are rules for rewriting. So at the third level, your implication is not only proof, but your implication is proof
qua the program. And this is the implication within the sequence calculus. As I said, Gerhard Gensen didn't really propose proofs as programs. But within a sequence calculus system, it is already implicit that proofs are programmed precisely because of this rewriting aspect. And this is something that was elaborated further by people who came after him. As we discussed, this innocuous looting interpretation actually relates to what is known as intuitionism
that treats a proposition A as the claim that one has a proof of A, one has reduced A to a steps which intuition can verify. And you see, again, within this whole idea of implication as proofs, as programs, we have a constructivist approach, and the stuff that I talked about, Brouwer, Hayting, Kolmogorov, and Corey Howard. I.e., it is not true that one either has a proof of A or a proof of not A. For example, If A is independent of the axioms, then neither A nor not A is provable, and one may freely
decide whether to assume A or not A. Let gamma, gamma prime, delta, delta prime, etc. be finite sequences of formulas and A, B, C, etc. be formulas. A certain number of formulas should be true using the above natural language interpretation of sequence. This one means formula proves itself and also we have these. These are the rules of inference. As you see, we have these junctions within formulas on the left and right side.
applications, copying. So these are inferential rules of the sequence calculus and the classical logic. But in addition to these inferential rules, introduction of the disjuncts or conjuncts, there are also structural rules in classical logic. And the structure of rules, as I said, usually come in three types, exchange, weakening, and contraction. Exchange order does not matter, whatever are the formulas, in order to prove or construct
a conclusion or an output. addition of new premises doesn't change the conclusion and contraction. You can derive the same conclusion by freely contracting or simply eliminating one of your premises. you do not have the count of your resources, it doesn't matter.
In order to treat formulas more like resources, their spontaneous appearance and disappearance should be restricted. This is what Girard's, basically, adjustment called the Project of Classical Logic and Intuitionism. In other words, the weakening and contraction rules should be omitted. This naturally affects the other rules. In assuming weakening and contraction, the rules at eldestjunct, artistjunct are equivalent respectively to eldestjunctprime, artistjunctprime. For example, artistjunctprime and artistjunct are equivalent in the presence of weakening.
OK. Sorry. I completely misread the whole thing. My notes here, actually, I will read from the screen, because my notes here were actually a different format, and I completely misread the whole thing. So anyway. Sorry. Let me read from the screen. In order to treat formulas more like resources, their spontaneous appearance and disappearance should be restricted. In other words, the weakening and contraction rules should be omitted. This naturally affects the other rules. Assuming weakening and contraction, the rules L conjunct, R conjunct are equivalent respectively
L conjunct prime, R conjunct prime. For example, R conjunct prime and R conjunct are equivalent in difference of weakening and contraction rule. is omitted for simplicity. If you see in the first line, we have gamma prime results. It's actually that should be just turnstile. Those primes after turnstile should be, for some reason, they ended up in the formula to completely ignore them. L, gamma prime implies B, gamma implies A, then gamma and gamma prime implies B, gamma
and gamma primes implies A. Hence, we conclude that gamma and gamma prime implies A conjunct B. same one, you have two formulas that are giving two different conclusions. Hence, if you put them together, replicate them, you get the conjunct. Hence, you can easily contract them and say that one of those formulas proves the conjunct of the two conclusions. Without weakening and contraction, these are no longer equivalent.
So we could legitimately distinguish between conjunct of the first two rules and the connectives of the second two rules, called conjunct prime. That is just what we are going to do. But the first connectives will be called instead, and, or as I said, it's the additive conjunction notation in linear logic. It's the idea that I can use either this one or that one. I have a free choice, but I can't use both. The second connective will be called multiplicative conjunction, dot, circle, multiplier sign.
It's a tensor sign, where you have both. So the idea that once you suspend the structure rules of weakening and contraction, you essentially come with two conjunctions, one additive conjunction that is either or of the formulas. I can have both, but I can freely choose which one. And you also get another conjunction, another type of conjunction. It's called multiplicative
conjunctions where I can have both. So suspension of the structural rules of contraction and weakening bifurricates the classical conjunction into two types with two different interpretations of conjunction, additive conjunction and multiplicative conjunctions. And the two, these two conjunctions, they treat resources differently. The multiplicative conjunction rules apply in any context. They are context-free. As I said, you can have
not both, and it's your choice too. While the additive conjunction, the ampersand sign, while the ampersand rule, R-conjunct, requires the context of the two sequences to agree. is context sensitive, either or. Another way to divide the rules, we might attempt to divvy up the rules among the connectives differently. For example, we might define a connective with rules R conjunct, L conjunct prime. In that case, and what was that, R conjunct prime?
and L conjunct of prime, these two. In that case, as soon as we add the cut rule, I will talk about the cut rule. I don't talk about it this session, but cut rule that you can simply cut elimination means that you don't need to repeat the lines of your sequence formulas, but it has a computational interpretation. I will talk about this later. In that case, as soon as we add the cut rule, we can derive the rule of contraction. Weakening follows from the complementary choice. So if the conjunct is either replaced by two connectives
in the wrong way, or if it is not kept as it is, the rules are weakening, and contraction can be derived. Hence, linear logic is forced upon us by the single choice to suppress weakening and contraction. To sum up, we have arrived at these rules. As you see, the rules of inference that in classical logics were interpreted in sense of conjuncts are now divided into additive multiplicative conjuncts. So weakening, suspension, weakening, and contraction
gives us a different interpretation of conjunctions and also logical connectives in general in linear logic. The first thing it does, it restricts the context and resources of conjunction in classical logic, divides it to context-free and context-sensitive interpretations of conjunction in linear logic. So this was a lot of conjuncts. But what about negatives? What is exactly negation in linear logic?
Does linear logic have any negatives? The modification to classical logic multiplied connectives, but it does not multiply negatives. There will still be a single negation operator called the dual, and written using the orthogonal vector subspace notation, a bottom, or a orthogonal, or a, or simply linear negation. At this point, a few assumptions will simplify the presentation without affecting the expressiveness of the logic. One, application of the exchange rules are ignored by letting gamma, delta, et cetera, denote multi-sets instead of sequences.
A multi-set is a function f, s mapping to s greater than 0, assigning a positive number to each element of a set. 2. Right-hand side of a sequence suffices to express all possible sequence. And as you see in the following sequence. So all sequence will be assumed to be of the form implying or proving delta. Although, as I said, there are parts of linear logic where the form of linear logic where the rules of exchange, which is another structural rule of classical logic, is suspended too.
But we are not going to do that. Sorry, you guys went silent. Can you still hear me? Yes. The negation operator does not appear in the signature of the logic. Instead of being a connective, the dual is an involution on atomic formulas, which induces and involution on all formulas by a few simple rules. This removes the unnecessary bookkeeping moving between equivalent expression of a single formula. There are also new connectives.
Once you have the linear negation and also the reinterpretation of conjunction in classical logic, you get many other connectives. This is basically from Girard's original manuscript on linear logic, which I think is most comprehensive All the rest are rather unreadable. You can go, these are all quoted from his own manuscript to, at least in the framework
of linear logic, we need to be faithful to his original framework. and then talk about the refinement that he made to it, or other people developed it, and it became more sophisticated framework. But in its original intuitionistic linear logic, in the 1986, I think, paper that he wrote, this is basically how things are interpreted. The introduction of negation doubles the number of connectives in analogy with the relation not parenthesis A, conjunct B equals to not A, disjunct not B. Negating ands should give
That was, if you remember, as I said, negation in linear logic is generalization of Domorgan dualities. So negating multiplicative conjunction gives a connective which we will write par, as in parallel or. It's an inverse ampersand. And negating additive conjunction gives us plus. And I gave the interpretation of these in the previous session.
So essentially, once you have these, once you have the linear negation plus the conjunct, given the fact that the new linear logical interpretation of conjunct was arrived at through suspending the structural rules of weakening and contraction. So once you have these three components, the two conjuncts plus the linear negation, you have all of these further interpretations, further reinterpretation of logical connectives in the following manner. If you see this sign here is the invert ampersand. Sorry, the invert ampersand is actually, I have it in another letter type, but this is
usually what people put it for par. These properties determine the rules of inference for par and plus, just to reach the rules of multiplicative conjunction and additive conjunction to the left-hand side of the turnstile. They will be summarized below. The connectives differ in chiefly by how they handle the context of the formula. The context of the conclusion of the additive conjunction and plus rules agrees with the context of each premise. They are called additive connectives. On the one hand, the rules of multiplicative conjunction, in part, do not restrict the
context of the affected formulas. And the conclusion concatenates the context of the premises. These are called multiplicative connectives. So in addition to additive connectives, you have multiplicative connectives in linear logic. conjunctions and par-multiplicative disjunction, even embedding of classical logic. So you see, you still preserve the connectives of classical logic, but in a more refined manner.
in what sense, in the sense of resources and contexts. As for the choice of symbols, in my first glance, it seems better to label the negatives of multiplicative conjunction and as plus instead of par. The symbols are assigned so that the relation between multiplicative conjunction and plus is the following. I will give the interpretation of this later. But Tony has put the previous session. We went over the difference in terms of who makes available, what resource, am I free
to choose it or not, in a kind of a game theoretic framework. We gave an interpretation of plus and tensor. Implication. Using the negative, implication can be defined in analogy with the classical case where A implies B equals to not A disjunct B. In other words, implication is true when either the premise A is false or the conclusion B is true. This implies, for example, that if A is true, then B implies B is true for all B.
The truth of the statement of A implies, parenthesis, B implies A lies at the root of the strength of this formula. In any case, mimicking the definition of not A, This chunk B in linear logic gives the definition A, linear implication, with lollipop B, whose internal structure can be interpreted as linear negation of A par B. What does that mean? If you remember linear implication, the lollipop symbol is simply
the symbol of the duality, the interchange of player at least when our game is a two-person game. So obviously, and within this test framework, even our test framework in linear logic is interactive, is multi-agent. is the move or counter move deployed by the opponent, sorry, by the refuter.
as we talked about, the linear logic interpretation of implication becomes something that always involves a counter move by a refuter. And a counter move by a refuter is denoted by a linear negation symbol, a duality. So the implication, lollipop, lollipop being the linear logic symbol of linear implication.
What is exactly, we also talked about that linear implication is really a resource conversion symbol. Because every implication entails or involves a resource being consumed on the left side and something being produced or generated on the right side. So linear implication not only involves this idea of counter-move by the opponent, but also it implies consumption of a resource on one side of your sequence and generation
of another resource on the other side of your sequence on the right side, the side of the conclusions. So the implication is not a connective of the logic but a shorthand. Since the disjunct is split into plus as well as par, one might also try defining the implication at least in the classical sense. A, linear implication B under linear logical definition is equal to linear negation of
A plus B. This does not work for the philosophical reason, then the additives, par and plus, have intuitionistic properties, whereas the negation, orthogonal or bottom, used in the definition of implication has classical properties. And what is the classical properties? It's, again, the generalization of double negation. You see double negation in the classical sense gives you again A. Double linear negation again gives you A. But it's different also, the whole thing is that, we will talk about
this, this double negation within linear logic, although functions the same as classical logic, It has a different interpretation precisely because negation in linear logic is about duality, is about the interchange of role between the player and the opponent, prover and refuter. So this match would produce undesirable results if we interpret A implies B under linear logical definition as linear negation of A plus B. Generally, all of the logical symbols or logical
connectives within linear logical framework involve a form of resource awareness or resource sensitivity. Now once we have the basic logical symbols, logical connectives of linear logic, it's easy for us to put so many remodel, the remodel proofs, functions, programs, implications in different way. For example, a very intuitive example of this, which is again, as Gerard's
own example, you see in the classical logic, precisely because you don't have this kind of context sensitivity and you don't have this kind of resource awareness, you can use, regardless of context and regardless of its availability, a resource to produce a conclusion. infinitely reuse or use a given input to generate an output. But in real world, as well as in linear logic,
this is impossible. The menu example that I mentioned gives you a good intuition of these connectives and how they approach resources. You have two $10 bills. How do you write this in linear logic? You have both. When you have both, we use the notation of tensor, multiplicative
So on one side we write, on the left side we write 10 USD, 10 SOAR, 10 USD. Linearly implied, symbolized by a lollipop, salad, multiplicative conjunction pasta, additive conjunctions, rice, these are inside the parenthesis. And then multiplicative conjunctions, apricots plus carrot cape, again within the parenthesis.
So any of you can give you how does this work? what does this menu is supposed to function here. To give you a better here are the summary, the legends for the symbols, and based on what we talked about last time. Let me just make this a little bit smaller for you so you can see any of you who can tell me what this menu is supposed to do for you, how you are interacting with this menu. Anyone?
Adam, Sean, Aaron? Stephen? Yeah, sure. So if I'm reading this correctly, you have two $10 bills. Expending both of them gives you the option to...you receive a salad, you choose between pasta or rice, and you receive apricots or carrot cake depending upon the season. Is that correct? Yes. So the interpretation is that in the first one, first side before the second multiplicative conjunction, sorry, the third multiplicative conjunction in the whole sequence, the salad,
multiplicative conjunction, pasta, additive conjunction, rice. In the first one, you have the free choice between rice and salad pasta. Actually you have to parenthesis. You have free choice between pasta or rice. You can get one of these but not the other. And you can get salad on the side. And after this third multiplicative conjunction, you get either apricot or carrot cake, but
it's not you who choose, it's the restaurants. It's depending on the season, I have to say. So spending $20 to up your $10 bills, you see $20, we shouldn't even say $20. Spending both of your dollar bills, convert your dollars to this chain of, you know, your resources and produce these results. You can have both of these specials. Salad
plus either pasta or rice, you decide. You can have this and apricots or carrots, but apricots and carrots, you absolutely don't have any free choice about which one you will have. It depends on the availability from the opponent's side, the restaurants, the menu. I have a quick question. Sure. The way it's formulated, are we allowed to distribute such that we can say that if you spend one of your $10 bills, you can receive salad and pasta or rice? Or is it only assumed
if you spend both of them, you can get both salad and pasta or rice and apricots or carrot cake. Does that make sense? We'll repeat it one more time. Can we draw from this formula that salad and pasta or rice is an effect of spending $10? dollars? Or can we only get that if you spend both of your $10 bills, you get... Oh, it is both of your $10 bills, yes. It's both. Okay.
Can you see the screen again? Yes. So just I will give you more examples and stuff as we move forward, kind of intuitive examples before we get into more sophisticated ones. But if you remember I gave you one assignment one option. So the second assignment would be for you to model an interaction between a customer and a seller in any context of what you want, restaurant, coffee, an ATM
machine, whatever. Model interaction between the two, any kind of interaction that you can think of according to linear logic notations and then write what it means. should involve differently at least one logical connected that implies the choice is not being made by you. The choice being made by the seller. So that's your second exercise. You
You can either go with this one or the dining philosopher one. Sorry, what was the first one? That was the dining philosopher problem, looking at the solutions of dining philosopher and try to model it with a PetriNet and say whether that PetriNet model of designing philosophers, you can get it from online, but you need to interpret it whether it leads to race condition or whether it leads to resource starvation. Basically saying what is exactly wrong with
that model. So when a formula appears negated in linear logic, its interpretation should be reversed, received give with a double R. Since moving formulas along linear implication, or Lonely of negates them. The multiplicative conjunction on the right side should be read as giving instead of. The interpretation comes from reading the rules of inference
for each connective backwards from bottom to top. The multiplicative A tensor B saves the context of both variables. So reading upwards, we have enough resources. the context to follow both branches. And again, Stephen, that's in response to your question. We can follow both branches, $10, $10, A, multiplicative conjunction B. But the additives, additive conjunction, additive disjunction, save only one copy of the context. So there are only enough resources to follow one or
the other branch upward. In the game of chess, you can think about this in terms of branching of your moves. If you have these additives, it means that you can't follow the same branch at the same time. You will be restricted in either or fashion, either this branch or that branch. If you add this among your dollars, if you add the ampersand between your $10 bills, then it means that you can only spend one of the dollar bills, but you can decide which one of these dollar bills to spend.
If you had additive disjunction between your dollar bills, an intuitive interpretation of this is that your mom is giving you two bills. And it's not you who decide which one of them to spend. It's basically the person who gives you the money. In that case, why not view the ampersand, the additive conjunction, as a type of OR? The menu interpretation concerns the context of additive
and junction connected, whereas the interpretation of additive conjunction as a type of AND concerns the interpretation of A and B additive conjunction B in terms of true-false values. Since the formula A additive conjunction B linearly implies A is provable, additive conjunction cannot be a type of OR. It might look like the PAR symbol connected was omitted, but it hides in A linearly implies B, which as we said, its internal structure is in fact
linear negation A par B by definition. Then in addition to this diversification of connectives, you have something else in linear logic, and they are called exponentials. We talked about exponentials, and for now, we don't come into varieties. we talk about one of them, and that's the off-course operator. Of course operator, we talked about the arbitrary amount of resources are available, and it
preserves some of the characteristics of classical logic. In fact, the majority of inferential rules that you have in classical logics are in fact exponentials, meaning that you assume that you have availability of resources. What would be linear logic notations for having our cake and eating it too? That would be it, as you see. How do you interpret this? The exponentials are the unary operators resembling modals in logic.
They allow control the application of weakening and contraction rules. Because you remember that weakening and contractions are really about this resource insensitivity. Sometimes it's important, as Adam was talking about, that you should be able to use a resource as many times as you want. So you need to have these exponentials. But you need to have controlled applications, namely a context sensitive, depending on the condition of when these resources are available and how you can use them. The exponentials
in linear logic allow the following inferences. The negation operator ensures there will be two different exponentials which are related by of course linear negation, of course a. There is of course A as many times of A you want. You can use it without restriction. So linear negation of course, which you can intuitively think about as complete availability of resource, any arbitrary amount.
Although we said that it's best to avoid interpreting availability of resource as any amount of you want, rather than reusing your resource infinitely. So it's not reusing, really. The best interpretation of this is not reusing, but arbitrary amounts of A. So this, of course, operator, which is this arbitrary amount of A, is quite easy to understand. Linear negation of this produces another exponential. And that exponential is called why not? You see, the reason that Gerard coined these terms
is like this. Can I have this? Of course. Or why not? You see, why not is come from the opponent's side. Why not? I'm saying, can I have this one again? And the opponent says, why not? This is symbolizing linear logic by a question mark. Of course, is denoted by an exclamation mark. And as we said, linear negation is really the symbol of duality, the symbol of the move made by the opponent. So availability of exponential of resource, availability of resource, when
it is implied by the opponent, it becomes a question, why not? Can I have this? Why not? These are called exponentials because they convert additive connectives into multiplicative ones as the following. You see, the distributive characteristics of exponentials hold. Distribution of course operator of additive conjunction of A and B results in, of course A multiplicative conjunction of course B. And for y-not operator, y-not of A additive
disjunction B produces y-not A par y-not B. And the equivalence here in the above formula It means that the formula A linearly implies B. Additive conjunction B implies A is drivable. Some examples in how this, in more intuitive framework, how these notations and relations can work.
Buy from A, x exclamation mark, selling A x y multiplicative conjunction, having y implies having X, selling T. You can read it yourself. So basically the interpretation is that where buying from AX is the name for a resource of type selling AX multiplicative conjunction having Y, converts this to having X. There's a buying and selling. This expresses the ability to buy an object X from an agent A for the cost Y.
You have this. Now you can, like a spelled out sequential format, you can, for example, think about how to model this according to the linear logical notation. It would be easy. That's what I want you guys to do, to get any kind of interaction, a simple interaction and model it in linear logical notations. In addition to these kinds of explicitly real world, real life resource consumption scenarios
where you buy and sell something because it's very explicitly resource consumption, then it's very explicitly expressed, in fact we can model any form of interaction about beliefs, actions, about expectations, through linear logic, very elegantly. For example, action operators are resources that describe an agent's belief upon actions. Typically, they are of the form action name parameter consumed linearly implied generated. The parameters to the action, or what we call them parameters, allow us to describe classes
of actions. Their resources used up are consumed and those produced are generated. The reason actions are usually intuitionistic is that actions themselves do not get consumed when they are performed. Nevertheless, they have context sensitivity with regard to the environment that they are For example, an agent can use the following resources as action operators to describe its beliefs about asking another agent A for an object X and subsequently getting the objects from them. Ask A give X. Has A X. Linear implies has A X.
Multiplicative conjunction. Expect A to give me X, get from agent A X, expect A to give me X, multiplicative conjunction has A X implies having X. This is a real rudimentary example of expecting someone to do something for me. Take that person as, for example, this thing. I expect you to give money if you have money. The ask action here generates an expectation that another agent, A, will give the object
X to the agent who has just asked for it. The action requires the resource has AX to be present but does not remove it because it occurs on both sides of the Lollipop symbol, a linear implication. This limits asking for an object to cases when the asking agent knows the other agent has the object and is thus called a precondition resource. Sometimes we do not know what they have and hence it becomes what becomes, it needs to be modeled by a different connected. Even we know that they have in fact this resource, we can define this as a precondition resource.
The get from action in our above crypto code in linear logic format, the get from action requires the agent to be expecting to be given X from agent A. This illustrates the way conventional contexts can be built and used to structure actions and dialogues. The agent must ask to be given X from agent A before the agent can actually be given X. The get from action, again in the above example, expresses that the agent believes that the executing, the action, will remove the expectation. So expectation here can be understood as a resource that is removed once it's fulfilled.
Like you remember the linear implication lollipop symbol, you could think about it as hunger satisfied. Linear implication symbolizes the act of eating. I am hungry is an expectation, it's a desire, once fulfilled by linear implication, a function essentially, a type of function. It satisfies, changes the resource, changes the desire of eating and turns it into a satisfied condition. I'm full now. The get from action operator expresses that the agent believes that executing the action
will remove the expectation and result in having the object being asked for. Furthermore, A will no longer have the object. All actions that an agent believes can happen are specified as action operators. To allow plans to be made which involve other agents' action, the set of action operators include the actions taken by other agents. We call such actions passive because they typically involve waiting and perceiving something in the world rather than causing it to happen. And these are the ones that can be modeled in linear logic by those connectives that imply the choice made
by the opponent, by the other player, by the environment. And we talked about these also in terms of the server client queries and response. Basically, any kind of scenario that involves a waiting, involves choice being made by the environment, involves ignorance of the player about resources. These can be modeled by those connectives which implies opponent's moves.
For example, the act of getting an answer to a question is passive and can be written Get answer Q, expect reply Q implies answer QA. This says that if an agent is expecting a reply to a question Q, then the get answer action will remove that expectation and produce a new answer resource. The choice connected in linear logic allows agents to operate in non-deterministic environments, such as the semantic web, where the outcome of actions is not known in advance, but the
possible outcomes are. At the logical level, non-determinism corresponds to a resource of the form A additive disjunction B . When such a resource is the consequence of an action, either the resource A or the resource B will be produced, but not both. And as we said, it is non-determinism because this A or B, the choice, is made by the environment, by the opponent, by the refuser. For example, the action of getting an answer to a yes or no question could be written as YN, answer Q, expect reply Q, implies answer Q, yes, additive conjunction answer Q, no.
You can have the same thing about another buying and selling scenario involving dollars and buying tea and cake. And just to give you more material to work with, you can see the best way of how to, model, if you are taking this exercise, how to model an interaction between two agents or in a buying and selling scenario. First think in terms of the actions that need to be performed and the choices that are being
made in each step. Write this kind of crypto code format and then try to model this into a linear logic notation format, as we have done with the key and cake scenario. Typically, just to give you again more material, in this query reply scenarios, answer expectations In this query reply scenarios, answer expectation scenarios, we have usually two, but you can think to see if we have more.
We have in our binary format, we have ask A, get answer A. I expect from agent A something to produce something, and we write it as follows. Then we have situations that we are getting asked rather than asking. It's someone else's expectations for us to answer. And that can be symbolized again by the following notations.
So depending on whether asking or getting asked the linear implication order changes. Before I move forward, any question? But I'm sure you have already started to see, I mean, we will get into more details about the computational aspects of these logical connectives and side linear logic, but you
We can see the ramifications of this for dialogues, for rationalism, for intelligence, for modeling action in multi-agent systems, functional programming, so on and so forth. comments, Sean, Adam, Aaron, Steven, Juan, Tony.
I didn't ask, by the way, if any of you guys were familiar with linear logic. You? Okay. Well, you do logic in computer science and you don't go as far as exponentiation. I think that's usually where it drops off. You do kind of truth tables and similar problems like the one you posed. Order this or that. Okay. Well, how much did you get into linear logic? I guess up to the point where you're sort of expressing problems and answering them, or doing like D. Morgan's Law.
Okay, okay. And who was it who asked this question about distribution? Okay. These sort of questions are like, what is the distributive property? What is the commutative property? Yeah. And I guess the interesting thing for me is that all these sort of almost like algebraic structures come up in different contexts. Like the symbols are different, but the operators are actually the same, but the operands are context specific. Yes. Yes, except for the bit about resources, where you sort of introduce this sort of the left-hand
side is something to be consumed by the right-hand side. That is something that was kind of unfamiliar and interesting. I've never seen it that way. Okay. There are actually a couple of books, probably you have come across them already, that have been specifically written for computer scientists and computer students explaining linear logic for computer science, especially in functional programming domain. Yeah, but I think functional programming deploys more category theory than linear logic. Yes, but this is more of something new.
Yes, it is category theory. But again, because of that, our correspondence moves made, again, from category theory to linear logic. Because really, when you get at the end of the road, these are all the boundaries between them are blaring, category theory and linear logic. In fact, it's really interesting that you said the algebraic thing. You have already noticed the tensor sign. Basically, Girard, when he wrote his 1986 paper, one that I quoted some stuff from it, he modeled it from an algebraic perspective. Throughout the years, he has started
to move toward topology and category theory. But these sort of, I guess, tensors and matrices and in particular outer products, this operation of, it is exponentiation, isn't it? Yes. It is. Or tensor multiplication or tensor products is exponentiation, would you say? Yes, yes. Okay, that makes sense, yeah. And there is, for those of you, again, who are interested, and I especially suggest it to you, Sean. There is this woman. I remember she was, I haven't been following her blog
for a while, but she was a student at Carnegie Mellon. She had a blog called, let me see, what was the name of the It's called Everything in Context. She wrote this really nice dissertation, computer science thesis, on framing narratives and
computer games to linear logic framework and using Heverly-Petrina's linear logic. And in fact, there is a programming framework for linear logic in computer science, and she uses this heavily. It's a really interesting framework, especially interactive narratives in video games. So many of these computational problems come in a very intuitive way, but complicated, the way that things interact. And she tries to analyze them from the perspective of linear logic and category theory, in fact.
It's a really good, I think her blog is very good for any of you who are more interested in linear logic within the kind of applied domains in computer science, like designing games, designing programming, or even engineering, these kinds of stuff. It's a good resource that you should check. Lambda phone. Let me see if this is the same blog.
linear logic, is as I said, it's like the most basic, in fact, original version of linear logic. By itself, it's just elegant framework. So many of its ramifications are still shrouded. What is really interesting is how it was received in theoretical computer science by Girard's colleagues and also some British and Americans. And they developed it further and they turned it into computability logic. Then when it turns into computability logic or game semantics, semantics of information processing, like Abramskin, BLAS, it becomes extremely interesting.
Some of the notations are different. For example, in computability logic, which is the whole project was spearheaded by Georgi Jafaridze, Georgian computer scientists. The notations are different. Their interpretations are similar, even though they do not have the same exact meaning. But the ramifications of linear logic, and precisely through this whole idea of resource consumption and context sensitivities and abilities, it really gave fantastic conceptual resource to reinterpret church lambda definability. theory of computability. What is exactly a computable function once we interpret it
So I, how are we doing it? About time, we have like 30 minutes left. So it would be best, because the stuff that I have to talk about are a little bit too formal and I know that usually at the end of the sessions you guys are getting a little I think best just to talk about where we are headed and not really present the formal parts right now and leave it for the next sessions. Because what I want to do, let me share this diagram with you.
As I said, the central part of the grand unifying aspect of the holy trinity of computation between proofs, programs, and structures, mathematics, logics, and computation, is really their reinterpretation of logics, of logical problems. And that couldn't be attained through further development of Brauer's dictum. Essentially, that's due to Brauer, Hayting, Kolmogorov, Kari Howard, Lambeck, Abramsky,
and so on and so forth. So what we are doing to do, we are going to—we have already looked at this transshift from classical logic and its connectives to linear logic, and how linear logic preserves rules of inference of classical logic and the constructivism of intuitionism, but it refines both. So how we are going to approach this is we are going to look into this increasing refinement and development of Brouwer-Haythin Kolmogorov's scope of constructivism.
This landscape can be seen as coming again from two directions, at least the way it's now moving forward. is coming from the Gensen side, the shift from the classical framework of logic to a sequent calculus structuring due to Gerhard Gensen, through which we can keep track of formulas and that's what sequent calculus is famous for. It gives a bookkeeping format
of logics, entailment, implication. You can keep track of your rules of inference by keeping track of your formulas, your premises in relation to your consequences. There was of course another side to the importance of sequent calculus for the constructivist approach, which wasn't put forward by Gensen himself, even though it was implicit within
in the sequent calculus format. And that's the idea that we talked about, proofs as programs. Sequent calculus, sequence essentially, are construction of judgments. They treat judgments as constructions, proofs as programs. So this was one aspect, and this is the aspect that we briefly talked about and we try to talk about it more. And the second one, which really brought this whole sequence calculus framework to a new level, was Girard's linear logic, where formulas are resources. And it's not only about keeping track of your formulas, core resources, but how you are
spending them, where you can spend them. The context is important. And that couldn't be done unless through the advent of substructural logics, namely suspending the weakening and contraction rules of classical logic. The other important aspect of linear logic that precisely once coupled with the sequent calculus format puts us in the direction of a theory, an interactive theory of computation is the concept of dualities and symmetries of proofs.
We intuitively, but also more or less formally have talked about dualities in terms of games, terms of symmetries of verifier and falsifier, prover, refuter. So once we have these two frameworks, in fact, these are in linear logic, it already subsumes the sequence calculus format, but gives a duality interpretation, also a completely context-sensitive, resource-sensitive interpretation of sequence calculus. You have a rich constructivist approach, and this rich constructivist approach is really the heart of the interactive theory of computation, through which Church-Turing theory of computable
functions can be fundamentally reinterpreted to show that the way that a Turing machine is formulated is a special case of a general, more general theory of computability. Computability for a Turing machine is a special case of a more general theory of computability. And this is the landscape that's usually defined under the rubric of logic of computability, where you have operational semantics
versus denotational semantics of computation. What is the notational semantics of computation? It's meaning as function. Operational semantics is the best way to understand this, even though we will elaborate about this. It's not quite like this, but for now, you can think about it as meaning as use, contextuality. meaning as used versus dialogical interpretation of meaning versus monological interpretation of meaning, and which in theory of computability,
in logic of computability, this shift from monological to dialogical is discussed with regard to functions, how we understand functions in mathematical terms and in theory of computability. So in logic of computability, you have linear logic, you have reinterpretation of linear logic, you have dualities, you have proofs as programs, you have to track a bookkeeping format, which all bring us to a different interpretation
of what a computable function is, or function in general is. And that's operational semantic interpretation of function versus denotational interpretation of functions of programs. So in the notational semantics of computation, functions or programs, programs are considered to be function, and functions are considered to be monological. In operational semantics, program, the meaning of the program is not really the function. The meaning of the program is behaviorally understood. It's the context of interaction within which a function can be understood. And that's the whole point of the operational semantics,
which we talked about. So this is the further step in moving towards an interactive theory of computation and talking about behaviors, et cetera, by framing it around this development of the constructivist approach by way of sequence calculus and linear logic and logical computability. Philosophical questions.
How does this fit in your project? I'm still sort of trying to figure that out. A lot of this is pretty new to me. some, I'm still trying to figure that out. If it's not to, I guess, rewind back to the beginning, I was wondering if you could talk a little bit more about this distinction between function and behavior and the question of definitions of behavior. Okay. There are many ways of framing this question and answering it. Traditionally, at
least in the behavioralist sense, in the traditional behavioralist sense, defining behavior, behavior is an observable, explicitly observable phenomenon, which is teleologically defined. Hence, why the classical behavioralism gives rise to classical functionalism. You say, for example, let's talk about the Pavlovian behavioralism.
the intelligent behaviors of animals, first you, according to some pre-given rules of observation, rules of singling out invariances of certain behaviors, first you single out a certain behavior. And then you see what caused this behavior. This idea that according to pre-given rules and pre-given axiomatic approaches and methodologies, you are capable
of singling out an observable behavior, obviously means that you are modeling it based on your practical reasoning. Practical reasoning, like a system function versus a system that malfunctions. dogman ought to do this and if it doesn't do this then it is malfunctioning. If the dog doesn't do this when responding to, for example, these parameters, then it is malfunctioning. It's not doing its behavior. It's a behavioral anomaly. So this whole idea of behavioralism has teleological components, is heavily modeled on our practical reasoning, but it is blind
on being modeled on practical reasoning. That's the whole point of it. It takes it for granted as if there is an intrinsic component to it. Then there is also the issue of causal substrate, that every behavior you can—and again, that's the reductionistic component of traditional behavioralism. Every behavior can in fact be traced to a causal component. But by virtue that this behavior has a teleological autonomy, has a functional autonomy, we can simply abstract
extract this behavior functionally understood from its causal substrate, simply replicating it without any underlying constraints. These are the hallmarks of the classical behavioralism, which you see the appeal of classical behavioralism not only for classical functionalism but also for classical projects of AI. Functional autonomy of intelligent behavior allows us to replicate it by decoupling it
completely from its causal constraints. And if this is the case, exactly how we can find an isomorphic function, how you can find an isomorphic function to replicate what a function does, you can do the same thing for these behavioralists, namely purely functionalist accounts of behavior. All you need to reconstruct a behavior is to find an isomorphic behavior that might be driven by completely different underlying generative processes, mechanisms, causal structures, so on and so forth.
So it's really about the isomorphic, isomorphic of one behavior with regard to another behavior. simulation, technically defined in engineering, is really captures the idea of pure functionalism and pure behavioralism. You replicate without any regard for the underlying properties, underlying characteristics, whether are causal or functional or processual, or how, what is the context. Simply you have a context-freeness here. So this is the classical behavioralism. Classical behavioralism is
in fact gives us, it's very much in tune with a mathematical concept of functions. So it's very in tune with classical functionalism. And classical functionalism is in tune with a flat picture of what a function is. Basically all your levels of abstractions are flattened, hence the isomorphic, creating isomorphic functions, replicating one behavior by different structural substrate is permissible, precisely because you have a flattened picture of functions. Now behaviorism, computational or conceptual understanding of behaviors, and it's kind
of no pragmatist or computational framework, is still a form of functionalism. But a functionalism where functions do not have this flattened picture. They have different levels of abstraction that need to be taken into account. They are context sensitive. So the more sophisticated forms of functionalism through which behaviors are talked about is no longer in that kind of traditional teleological accounts. It's about regularities. It's about, but most importantly, we can't talk about simulation of behaviors in this context. We can talk about the reenactment in the sense that extended theories of mind talk about
reenactment, reenacted cognition. What is reenacted? Meaning that reproducing the parameters through which a function or a system is interacting with its environment. Simply reenact the context of interaction. We reenact the parameters that are responsible for giving rise to this behavior rather than simply replicate an isomorphic of it without any regard for these parameters. without any regard for these parameters.
Re-enactment versus simulation is, I think, a good dichotomy to frame the difference between new functionalisms, where you talk about behaviors in an interactive sense, what is responsible for them, what generates them at different levels, according to different contexts and different situations, versus simulational understanding of behavior, which is pure functionalism of the old flattened picture of the function, very much in tune with the classical mathematical understanding of function, very in tune with teleological projects of understanding of functionalism, conditioning.
Of course, they both have ramifications. Simulation aspects supposedly frees us from causal constraints, suppose us from underlying constraints to a good extent, if not completely. Hence it gives us the illusion of a powerful framework. Behavior, and you get this in classical syntactic projects of AI, classical functionalism that Putnam criticizes. and traditional behavioralism.
Another ramification of this is the multiple realizability, which is a fundamental aspect of functionalism. Because if your functions can be abstracted from the context, from the situation in which they are generated, if they can simply be replicated without any regard for substratic constraints, it means that a function can be said to be, without any constraint, multiply realizable in any context within any causal structure. Hence, you get what Putnam criticized about traditional functionalism and multiple realizability
A Swiss cheese can be said to have a mind, you know, precisely because there was a structural environmental situational constraints have been taken out. So you, if mind can be, you can find an isomorphic function or behavior that doesn't do, supposedly at the surface, at the observable surface, does whatever the mind does, and if this function or behavior that you have replicated is free from the causal constraint, free from the situational constraint, then you are capable of implementing it in whatever structure you
want. You can turn a Swiss cheese into a computer, but also you can put mind in whatever, in a piece of a stone. Padnam talks about this in terms of it essentially leads to triviality, a triviality condition, precisely because if you do not have constraints and multiple realizability, you have a trivial situation. Everything can be implemented with everything. So but once you have constraints and these kind of hierarchical contextual framework,
then it is not really about unconstrained form of multiple realizable. You still have multiple realizable. You still can talk about, for example, a distributed multi-agent artificial framework that can have a mind that can be implemented with what we call mind. But it will be according to the constraints of how this function are generated, how an And intelligent behavior is generated on different levels according to its causal and structural constraints, so on and so forth. Hence, that's why the move from classical projects of AI to more sophisticated forms
of AI was concomitant with revisitation of neuroscience, empirical science, because precisely brain puts constraints on how intelligent behavior, even rationality works. There are causal constraints, but also toward linguistics, precisely in that kind of Brandomian sense of language as a social edifice, precisely because you have environmental factors, situational factors, there are context sensitivity with different levels of context sensitivity. That's the issue of semantic complexity of behavior, semantic complexity of behavior. If you do not have an account of semantic complexity of behavior, namely the hierarchies of different
modes of intelligence, each with their respective abilities, respective level of complexity, then you can't really talk about AGI in the sense that, for example, general intelligence is being formulated as being a human level AI. Thanks. It helps a lot. Welcome. Sean, you were going to say something. Well, I found this distinction between behavior and function also interesting.
I guess this is more of a comment extension. is it behavior then that's sort of bound to context, as in it doesn't really, doesn't transpose itself well to other operands versus functions are somehow more generalized, such that they could operate on different levels or different distinct domains versus behavior is bound to the domain and bound to empiricism, like of the singular observation. Yes, absolutely.
Yes. It's the question of entanglement, that behaviors are entangled. Is there any sort of further treatment on this problem with entanglement or any literature that you would suggest? Yes, yes. Yes, I think Sellars was really the first philosopher who really talked about this. And this is basically the whole project of Sellars, Mind and Empiricism, then his later works. In philosophy, I think Sellars is responsible for it, really astonishingly formulated the kind of difficulties that arise in this once we deal with entanglement, mind and empiricism.
You need to have, and that's why it's famous for naturalism with a normative term. So you neither have dogmatic rationalism, pure rationalism, nor that kind of empiricism that so many people talk about it in the sense that, you know, you can in fact talk about observable phenomena without having concepts, without having a rational account of mind. And then this becomes a stepping, a step for CELAR's project to develop a new account of functionalisms. But all he really talks about, about functions, are really behaviors. You know, it's not the kind of, this is, and then Brandon takes this to another level
in the Tales of the Mighty Dead. I will put all of these in the Google Drive and also, so in philosophy, yes, there is It's kind of a massive landscape concentrated on this problem of behaviors and classical understanding of function. But also there is, in cognitive science, there are some good sources on this. I will share them. I think Shonju and Stanisla Dohan are two great neuroscientists
who have worked on this point. And what I like about them is that in neuroscience, especially today's on the side of people who are kind of both analytic and continental, I shouldn't just say continental, There's the tendency that neuroscience is seen as the ultimate disenchantment of the world and basically it brings the spell of doom for intelligence and mind and rationalism and this kind of stuff. And people usually tend to have this kind of really inflated account of neuroscientific discoveries and stuff. I think two neuroscientists who are extremely subtle when it comes to this idea of rationalism and an entanglement issue are, as I said, Stanislav Duhuan and Changzhou.
I put their books in the Google Drive. This is also, you know, again, back to our discussion, feedback on your paper, it essentially has ramifications for the idea of scientific explanation too and scientific progress, all of this, if irrationalism and empiricism are entangled, you know, which is again this whole idea of behavior, mind, concepts, stuff. This is again part of Solares project, refining
what a scientific explanation really is. Ultimately Solares project is quite a Platonic project, I think, rather than being Hegelian. And when I talk about Plato I do mean this kind of really wishy-washy, common sense understanding of Plato as being the father of eternal ideas and pure forms and stuff, pure rationalism. Plato is quite sophisticated when you read this stuff. Absolutely. I never realized, you know, coming from a sloppy Deleuzian background in philosophy, I always hated Plato and respectively Hegel. But I noticed in the past 10 years
absolutely, he's an astonishing thinker. Plato is really massively criminally misrepresented by philosophers who have come after him. And I think... Plato and Deleuze and other Frankfurt School philosophers were primarily in the same pursuit but using different focal points as reference. Absolutely. a world sort of condemned to religious thought. He only had so many tools to sort of express these rich ideas. Yes. But I think he was seeking more phigenesis, just as Deleuze was thousands of years later. Like, how can we transcend? Yes. Where does novelty come from?
Yes, no, Plato is... And what really set me astray about Plato, So especially with relation to this whole idea of functions, ideas, thinking, its entanglements with the world, is a piece by Sellars, a very obscure piece, written I think in the 50s. called Reason and the Art of Living in Plato. It's one text and then he wrote another text afterward called Soul as Craftsman. Especially Soul as Craftsman is really a mind-blowing
piece. You can definitely see that so many of this stuff that we are talking about programming and these levels of abstraction, contextuality, idea of realizability. It's just encapsulated in Plato's theory of forms. Sort of like a fundamental algebra, I guess. Yeah, yeah. It's a theory of constructors. forms of constructors.
So yes, this is, yeah, Sellars, Plato, Hegel, Brandon in philosophy I think are very great Again, you want to get to the subtleties of this entanglement issue, situationality, but also the ramifications of this within a much broader philosophical project. understood as this kind of massive program of how Plato formulates it, how to realize
a good life, good being adequately understood. This is the important issue, good being adequately understood. Yeah, I guess that's where I fall off the train with Plato and kind of positions him in the past, is like obsession with the virtuous, or always going back to this idea, like even before any kind of normative contemplation, but just saying there is something that is like the truest form of humanity. I found that a little bit. You should definitely then read Sola as Craftsman, because Stellars gives a really solid account
of what Plato means by the good, especially because Plato considers good to be the form of forms, the highest form, as you say. And if you aren't convinced by this argument, there is another great book that I suggested in my previous class at the New Center by Lawrence Becker called The New Stoicism, which is an stoic interpretation of Plato and Socrates and the idea of the good as virtue understood as the maximization of intelligence or rationality and the way that it's formulated. It's quite powerful book. So these are some good, but definitely Solace Craftsman should put you in a good understanding
what Plato exactly means by the good. Why he's emphasizing it as the center of his project. Okay, guys. Let's wrap up this session and you can post your exercises, the PetriNet, or modeling some interactive scenario that involves buying and selling or expecting and performing action by way of linear logic and put it on the classroom page. And then next session, we will resume the rest of our linear logic and we move to the
theory of computer logic of computability. Sorry. Okay, guys. If you don't have any questions, I will let you go. All right. This is actually a session that...