Okay, ready to go. Okay, first of all, sorry for canceling the class last week. Okay, any questions before we start? Because I know you guys have... I saw a couple of you sent me the exercise on Petrinet and linear logic. but any discussion, philosophical, computer science, whatever, before I start talking a little bit what we are going to do this session. I saw your outline of the course, the map that you made.
I thought that was really cool. Oh, good, good, thanks. Is that a particular form of graph? it's quite familiar for making concepts and ideas to... No, no. It was completely improvisation, no. But I was just... I mean, obviously, it's a very selective diagram in terms of both the style, but also, more importantly, about the chronicling certain events that we have been talking. Obviously, this is extremely selective. So many people, if you show this to a, you know, I don't know, a physicist or even a computer scientist,
they might object to parts of it. Any thoughts, any particular thoughts on this? I was also hoping that you could sort of position us in it because I thought it was a pretty good outline. Okay. It was sort of like a review. for me of the ideas that we've talked about and how they join together? Sure. Actually, I planned to put a hand we are here, but then I thought that, hmm, I'm not sure if we are here really. Yeah, sure. I will open it and I will talk a little bit about it. The thing is that also there were a couple of things that I really, you
know, even if I didn't visualize it diagramatically like that, but I was thinking this is basically the outlines of how I was going to put this whole course in order. And there were a few topics that I really didn't cover that much, but I think I talked to Adam and I think I talked to Colin about a couple of these stuff, which I think are really, really important fundamental problems in complex design, problems as problematics, as stuff that I think if
they are being invalidated or going through revision, they can throw out a lot of the stuff that is happening in the complex sciences or philosophy of science, especially related to physics, biology, complexity, science. Concept of invariance, regularity, pattern, the concept of causality. We talked about a little bit of causality, especially when we talked about time, but invariance especially, invariance and regularities. What's the relation between regularities and invariance?
Well, you see, I use them, most times they are used interchangeably. When I use invariance, I mean it's mathematical model of invariance. And when I mean it's a regularity, I take it to be the realistic account of regularities of pattern in whatever system. But obviously, the first one is a mathematical epistemic claim. The other one, I take it to be more of a metaphysical claim and belongs to the metaphysical debate. Obviously, so many people do not believe in the reality of patterns and hence regularities
in nature. some do so but I never does when I use these two terms I use the invariance more of as a mathematical conception logical mathematical conception and the other one more as a physical conception robust so regularity to me I guess speak somewhat to this concept of biased or pre-observed structure. So you believe that a curve is going to be smooth or that a simple solution in terms of less sort of modalities in a curve is going to be a more likely model than one with lots of modalities.
I machine learning you call it regularization smart right if I I guess that me they usually selects more robust models a robust annoyance that is if you have some observation that is a idiosyncratic it's not gonna turn the whole thing inside out because it it just naturally prefers a simpler models that's regular rise a shun it's a regular model I And I guess that is, as you say, a form of invariance, because you become invariant to noise at that point. But I think you're- Sure, sure. I mean, they almost, at some point, the boundary becomes extremely blurred.
And that becomes also, that's, I think, quite an interesting topic to talk about. You know, based on the kind of mathematical conception, the mathematical concept of invariance, and the model of invariance you are using, you're also, of course, biased toward detecting and observing certain regularities, certain, as you say, features that appear to be robust or invariant from mathematical sense. And these are, I think, interesting questions. A couple of good books on this, I think. James Ladyman, Everything Must Go is a good book,
although I'm not convinced by his arguments. I'm still trying to think about it. Another book that is controversial but very interesting, Making Things Happen by James Woodward. He teaches at Pittsburgh, the Department of Blot, Blot, and History of Science. This is directly connected, you know, to the reason that I brought the idea of causality and causation. You know, he, in his book, he develops what he calls a manipulationist account of causality. It's some sort of complex heuristic schema.
It's the idea, very, very briefly, that what is exactly a cause? I think I talked to you about this too, that causes have explanatory input because they explain phenomena. And so, kind of like in fill you in about this background of whole debate, when it comes to the explanation, usually description is, there is a clear cut between description and explanation. Very traditionally, this also has something to do with the distinction between appearances
than reality in a classical, philosophical discourse. So when we describe a phenomenon, we are not explaining it. To explain it means that to find basically what has caused it. For example, and what is it? So the manipulation, it's a counter-causation, says a good example that can illuminate this trivially a bit, is that for example a pole casts shadow on a wall. In order to, when we look at the shadow, at the effect, we are describing the phenomena. In order to explain
it we need to understand the correlation between the pole and whatever has made this shadow appear and the effect on the wall, the shadow on the wall. Now the manipulation is a constant of causation, is this understanding that using manipulation conditionals, if we manipulate the size of, for example, the pole, move it within a threshold, within certain constraints of heuristics, if this relation between the pole and the the shadow on the wall doesn't change. We call this an invariant relation. And this invariant relation is a causal relation. So causation always defined for Woodward as
invariance under heuristic manipulations. And these heuristic manipulations, of course, a systematic formalization. So this is a kind of like, these are interesting. And of course, to me, this is a controversial claim. First of all, I think this whole idea of cause and effect, the way that it's being classically understood is itself problematic, and a very, very good critique of this given by the guy I named in one of the earlier sessions, Wolfgang Stegmuller. I think it's in the first volume
of his epistemic papers that he criticizes this account of causation as simply something causes something to happen, and we call that effect of that cause, and then make a one-to-one correlation between the two, and simply define true invariance or causal correlation, so on and so forth. Sorry, going back a little bit to where the conversation started, I was trying to
work through a little bit of Tom, Rene Tom. And it's very interesting though, the maths doesn't make it very casual reading. This relationship of morphogenesis and discontinuities was very insightful, I thought. But then there was this really interesting comment about structural stability and computability being at odds. And I wasn't, which I thought was an interesting idea, but I wasn't quite able to follow how he got there. Yes, okay. You need to know about this Frenchies a little bit. The whole idea is that people
who come from this, I think I mentioned this, coming from this kind of a French philosophical background, which is, you know, their father is Poincare, the dynamicists, and Tham, his a student and later colleague Jean Petitou, the one that Robin put in his article on collapse on Lothman. Who else? Gilles Chatelet, even. They are really brilliant people. But there is this whole idea of discretization, computation. They take it quite actually a very... In fact,
I think the critique of computation basically falls in the trap of the most unsophisticated accounts of computation and computability. There is, I think there is a bias, an inbuilt bias in French philosophical tradition, starting with Poincaré, and then later you go see philosophy of science in 1960s in France. This has been constantly repeated, but without any kind of argument as why this is the case. And you see the ramifications of this in later social commentaries on computability comes
from French theory. I mean, Jean Dupuy, even the neuroscience parts, like Jean-Pierre Changou, all of these new stuff in content of philosophy. There are, I think, the ramifications of this. Really trying to go on. Sorry. No, that helps, actually, that it's computability in that very narrow sense, or calculability in that very narrowly characterized sense that he's like. SUBJECT 1-Super mechanistic, but not in a good mechanistic sense. Not in a, for example, or vector mechanistic sense, but super mechanistic, this kind of. And it really, when you look at it,
it seems that it has influenced quite a lot of people down the road, this kind of bias toward computer science. And both it's applied and theoretical. It's all of the stuff that people talk about, especially it's kind of like a pseudo-Marxist take on French philosophy, has something to do with computability, algorithms, these kinds of stuff. I think there are, they, one of the things that I think is really important is that, I briefly, you know, address this, is that when you start to look into computer science,
with computer science I take it to be even more relative foundational, even more fundamental to mathematics, precisely along these lines that we have charted, you know, the constructivist program, then you see that it absolutely brings some really wild ideas and concepts, that there is no corresponding philosophical concepts for these. And I think that any person who tries to append these concepts of theoretical computer science to pre-existing philosophical concepts. For example, this idea of negation in the sense of proto-logics and computer science
to negation in the sense of Hegelian. I mean, Lukács does a great job, but I think it's still problematic. I think any person who tries to append these fundamental concepts of computer science to to pre-existing philosophical concepts, they're simply doing massive amounts of reduction. And that's kind of a, to me, it's a theoretical opportunism. Rather than appending them to the pre-existing philosophical concepts, why not develop completely new philosophies that are synchronic, genuinely synchronic to these concepts? the
makes sense and the other really interesting quote you are really related to on what you've been talking about or others this whole idea with Gerard and linear logic and the idea of making cost an explicit part of the system resource constraint I guess a very explicit part of logical systems. There's this throwaway quote in another paper, like it was a Q&A, and they're talking about what's the measure of complexity, and they're talking about sort of, well, what's the point of a measure of complexity, and so on, and so on said, well, perhaps the unit
should be money. Perhaps the unit of complexity should be money. It sort of takes costs to do something, and that's kind of fundamental to what is part of these phenomena. So it's sort of a throwaway comment, but I also thought it was a really interesting sort of possible entry point or intersection to the stuff that you're talking about with linear logic and so on. Yeah, I mean, it's kind of like, I have thought, in fact, I have thought about this, this whole idea that a resource, it is not a key. It's the most fundamental concept, really, in theoretical computer science and, you know, new logics. And it is the whole idea that if you can simply abstract semantic complexity from simply resources, once put into interactional mode,
And basically, resources being the building blocks of interaction and arising complexity. Then what would be the implication of this for simply money, really, as a resource that you can simply make abstraction out of it? I'm worried about pulling the whole group off topic now, but I've seen a reverse criticism of money in that the problem with it is it's just a scalar unit. When it should be a more complex data structure, that would be more useful.
Yeah. And it sort of, yeah, ties to what you're saying as well. But the, yeah, anyway, the same very related ideas, they're interesting ones to throw in there, but I don't want to derail the whole discussion. Yeah, in any case, I'm going to start to talk about this idea, just kind of a little bit bring this whole idea of why interaction is important and resources and why is that you know this constructivist crypto constructivist move that goes to study these deep proteological
to say computational phenomena is important because I think that's why I think computer science then becomes, as so many even logicians and mathematicians claim, computer science simply becomes the most fundamental in terms of relative fundaments, relative as trotter fundamental science for studying abstract phenomena and abstract construction. And I think this has, this is something that I'm trying to research and think about more coherently. And this whole idea that language computes, I mean, in linguistics, even in a traditional
linguistic sense, not in computational linguistics. People say meaning computes, language computes. What does that mean exactly? This whole idea that language, once language, even natural language, which is kind of a complex phenomenon, but nevertheless loaded with junk, really, biological junk, biological biases. Even in that sense, the natural language, once it evolves and it allows for this explicitization of this logical and computational phenomena, it absolutely contributes to evolution of
intelligence from a certain perspective. Without it, we can't imagine, we can't even talk about intelligence, really. That's the whole point, this idea that there is a correlation, explicit correlation, an implicit correlation between language and thought. In fact, Sellars says that thought is nothing but language. And this is the whole idea, that even private thoughts are modeled on explicit public linguistic practices in a society. And Brandon, you know, basically just refines this claim through the program of no pragmatism. So if that's the case, if thought is language, even understood simply as natural language
and not any other kind of language, what does this mean in terms of how can we really computationally talk about it without falling in the trap of the old philosophy of language in which, for example, we say language has an essence. Language is natural objects or all sorts of these ineffability discourses. Go on Tal. In Hebrew, the language, it's also very close. The word thinking and computing, it's the same word, . This has come. I mean, I understand that people have talked about this.
As I said, people talk about language from mid-20th century when you look into philosophy of language. People say that language computes. But what is, I think, important and makes the whole claim non-trivial and even more consequential than what it appears to be, is really once you understand in what context exactly we mean language computes and this whole idea of interaction and the role of interaction, how basically it develops from basic axiomatic confrontation of acts, symbolic acts, to these extremely massive and sophisticated computational phenomena
through which agents simply can gain traction on the real world. But also it has, I think, ramifications for the artificial languages and artificial intelligence, precisely because once you formulate even formal languages on the level of interactive theory of computation, and this is the goal of a couple of the people that I've already mentioned, is that you can think about developing artificial languages that are no longer the
adjective artificial is not a, is not diminutive, is not used diminutively. It's not artificial, is not used in the sense as being inferior to natural language. But natural language simply becomes a fraction of these formal languages, precisely because these formal languages can index both the formal explicitly, they can index the formal properties, computational and logical properties of formal languages, their accuracy, efficiency, explicit behaviors, but also index
the cognitive dimensions of natural language, like concept views, like discourse, like the feasibility, so on and so forth. Talks, comments, Aaron, Juan, Steven. Okay, if you guys don't have any comments, thoughts, I will start.
So I think that's actually, that was a very good discussion. I will start precisely from this point. This idea that interactive theory of computation and the fundamental correspondences between in logics, mathematics, and computer science structures, proofs, and programs? Why is it important? How does it enable us? I think the whole idea of this whole new trends in
enable us. I think the whole idea of this whole new trends in computer, theoretical computer science and logic and mathematics, especially computer science and logic, after, especially after Girard's contribution to linear logic and its subsequent developments, rectifications and revisions can be summed up as this, under this general idea, to relocate foundation of logic upon a computational approach to logic.
understanding what we, for example, what we understood as negation in a logical sense, and hence its philosophical, the philosophical interpretation of the function of negation, now goes even into a deeper level, that negation simply becomes the effect of a protological computational phenomena. So in order for us to understand what really negation is in the first place, we need to understand phenomena responsible for it, the computational porto-logic phenomena, or for that matter, any kind of logical idea, logical connectives, operators, proof behavior, so on and so forth, judgments.
Within this context, the general idea of foundations of logic, relocating foundations of logic upon a computation of particular logic, then, of course, even the concepts of computer science undergo, you know, reinterpretation, one of them being the concept of programming of languages, or programs for that matter, or language. Then to define, for example, a programming language, once we make this deepening move from logic to logic, from logic to computation, then a programming language becomes equal
to a set of axioms for elementary acts. To combine these axioms, namely to write down a program, is to describe, one, a possible complete generic action ready to be actualized when confronted to the next environment looming of. Simply that environment is a context. And such an environment is itself composed by acting processes, so that rather than by an action, the computational process must be thought as the confrontation of actions, interactions. We can think about it in terms of what we talked about in terms of that in order for
us to precisely describe what really an algorithm is, you know, one of the most fundamental problematic questions in computer science is that we need to understand how an algorithm interacts with its environment. And the system environments, the players, and according to this, so the program of axiomatization, which is one of the main fundamental dimensions of the development of computability theory, before that matter, any systematic form of language, undergo also a kind of a shift from
that kind of axiomatization simply as, you know, kind of zero-interactive premises and and how they hold sway over conclusions to axiomatization in the sense of interaction between a system, an algorithm, and an environment. And I will talk about this, how can this be done and what does exactly the sense of this a new axiomatization program.
So we know that programming languages are system of axioms for elementary kinds of interaction, as it is proposed in Interactive Theory of Computation. And we know that program is an open notion. Axioms first have to be chosen. So in fact, this is basically a general principle that you can find it in any axiomatic system. First, you choose the axioms. And of course, axioms are not neutral entities. They have properties. And these properties says a lot about their fundamental underlying behaviors.
They come basically even at the most basic level. we are trying to understand syntactically in axiomatic systems, axioms always come with an implicit semantical dimension. And I will talk about the implication of this coming with an implicit semantic dimension for development of one of the more prominent revisions of the Girard system. And that's Japparit's idea of computability logic, which we are going to talk about later in this session. So program is an open notion. Axioms have to be chosen. It's also a plural notion. Any choice for axioms determines a given kind of dynamic with its own complexity, its own properties.
So depending on how you choose, what axioms you choose, how you choose them, you determine and you import you ascertain kind of dynamic schema, and hence ascertain type of complexity with its own set of properties. So this is a, you know, as I said, once we make this move from logic to protocol, logic or computation, the program, this open notion and plurality, openness and plurality of programs becomes prominent. This is about programs. Computation also, the concept of computation
undergoes change. Computation becomes a plastic notion. Interactions could be performed in parallel or not, one. Two, interactions could be performed following various strategies. An elementary interaction, basically the fundamental elementary axiomatic components of computation also become extremely diversified. No longer is required, it's mandatory for them to be deterministic.
And we talked about this in terms of our games and how basically game brings the concept of non-determinism into a system. So the move toward, as we have seen it in linear logic, the whole idea of multi-agent concurrent systems. Once we make this move from logic to proto-logic, essentially we are, our concept of computation becomes interactive, our interactives becomes concurrent in the general sense, parallel, especially our case. Interactions being both deterministic can
to be both deterministic and non-deterministic, hence our computation, the concepts of computation that we are talking about covers a broader range of basically phenomena, whether deterministic or non-deterministic. So this is the kind of a computation, concept of computation becomes a plastic notion, but it also becomes a wild phenomenon. computation possibly becomes infinite, possibly non-deterministic, possibly even inconsistent. So and I will talk about these, how can the concept of computation can incorporate inconsistency
can incorporate infinite processes or infinite games in terms of games simply being for us as an elementary computation. I will talk about this, especially this is something that is highlighted prominently in Japerits' computability logic. So with the qualities or with the change in our concepts, in our primary concepts of computation,
programs, axioms, undergoing change, obviously these are ramifications for the application of computer science to different domains as well. One of them is that we know that is correlated with artificial intelligence, but even more as simply as a branch of cognitive science. Is that then how can we computationally describe thought processes? In traditional computer science or in traditional cognitive science, this whole idea that computationally described thought processes in the sense of classical sense of
computation is methodically, for a good part, is considered to be methodologically problematic claim. But with our notion of computation becoming plastic, wild, plural, then we can broaden the scope. And we know that the idea, the interactive model of computation is really about processes and behaviors. So with this idea of open, plural, plastic, wild processes, we already break away from
kind of that natural or non-natural deductive computation as deductive systems in the classical, very conservative sense. Obviously, we can track a broader range of processes responsible for cognition. So in this sense, one of the research ambitions of theoretical computer science, or for that matter computer science in general, becomes constructing
modeling or computational simulation of semantic phenomena. And this obviously is not only as significant within computer science, but also have ramifications for cognitive sciences are artificial intelligence. To construct computational models, computational simulations of semantic phenomena at different levels of complexity, different levels of complexity simply being modeled as different interactions between processes, between various processes,
having different semantic behaviors. And then there is a question, and this is what exactly why we need to go look deeper into interactive theory of computation that's a little bit more formal, to see under which condition semantic can grow up from such axiomatic accounts, from these axiomatic acts from these elementary computational acts. How can we imagine the evolution of semantic complexity from these protologic computational phenomena? So this is the kind of motivation behind this
move toward interactive theory of computation, describing it in more formal details. Another Another thing that is interesting, I think, is, as I said, the revision of the concept of the program. And this has more significance for computer science for development of new artificial languages and also, of course, as import for the project of artificial intelligence. Within this interactive context, the programs are no longer like, can be described like
monads, like big sim monads. precisely because the meaning of the program is determined by its interaction with its context, namely the context sensitivity of programs, which is a fundamental computational aspect of programs from this point onward. The meaning of the text of a program does not first depend on the usual semantic question, What is that text referring to? What does it denote? Hence the notational semantics. The meaning of it. What is the notational semantics?
The meaning of the program is simply its function. So with this move toward this interactive dimension toward this proteological fundamental computational behaviors, the meaning of the program is now its interaction with its context. This is the underlying idea behind the shift from denotational semantics of programming in computer science to operational semantics. What is operational semantics? The meaning of the program is its interaction with its context, with its environment, rather than being its function. So the meaning of the program in this sense depends on a preliminary question.
What does this program do? How does it act? With the idea of this doing or action is simply being constrained by its context, determined in part through this interaction by its environment, by its context. So very intuitively programs in this sense can be thought as acting text, texts whose meanings is paradigmatically actionable. And this is one of the things that, one of the basic ideas in this move from logic to proto-logic is that acting is primitive, semantically understood. Acting itself is axiomatic. So
rather than founding so-called fundamental or establishing so-called fundamental axioms, Why not take acting, formally understood, and I will talk about this, we know a little bit about this in linear logic framework. Why not take acting and interacting as axiomatic, interacting simply being confrontation of these elementary acts, and see how different axioms with different properties can rise, can evolve from different confrontations of different actions.
Hence, classical axiomatic systems simply becomes of the byproducts, you know, special cases and byproducts of axiomatic interactions, confrontation of axiomatic elementary acts. And this is the whole idea that axiomatic systems and logics can now be studied at a deeper computational level. they are being produced through these interactive axiomatic computational
interactions Also, another thing that is important in the move, in the deepening move from logic to proof to logic or computation is this almost metaphorically put, the explosion or the bursting force of the notion of the program into semantics, precisely because it pushes back the artificial limits, namely extensionality of the definition of the domain of sense. Those of you who are
familiar with this idea of sense and reference, this is, I think, an extremely interesting philosophical question. The realist in logic, the realist claim that logic is based on reference and of course when we look into this claim we see how it unfolds to another claim and that, for example, at the level of the language, that linguistic components actually have a reference to the real world. We talked about this, and this is what Sellar's theory of meaning, non-relational theory of
meaning, tries to refute. So this is kind of a realistic position in logics that when you translate at the level of linguistics, it becomes relational, referential theory of meaning. And sense, in the sense of, becomes simply secondary to reference. Reference a realistic concept in logics comes first and sense, and artificial one comes the second, hence artificial language precisely because they diversify the sense understood
inferior as to the referential accounts. So, as I said, another ramification of the move As I said, another ramification of the move to protocol logics is the bursting of the notion of program into semantics that pushes back the artificial limits, namely extensionality of the definition of the domain of sense. Practically, it is only through one particular among various algorithms that, for instance, arithmetic function is given to us. A given operation allows for multiple modes of being given various algorithms, aliases for multiple senses. Semantically, the bursting of the
notion of program or action therefore corresponds to the desirable extension of the domain of sense, namely multiple algorithms for ascertain multiple algorithms being basically another word for different senses of a program. How to understand this? As I said, Frigge is a realist, and in the realist context of logic, the reference of terms is primitive and independent of sense. sense is put forward only as a way to designate the reference, to designate reference. Once
we move toward this proto-logic where we have interaction, namely operational semantics, action semantics, there is an interaction between the program and the context or its environment, there is a radical revision of the Friedian position going on as well. And That's the revision of the Freedian relationship between sense and reference. Sense becomes primary. Reference becomes secondary. For example, the computational evaluation is nothing but a transformation of sense. For instance, 2 plus 2 and 4. 2 plus 2 and 4.
same reference but not the same sense. They both have four, but they have different senses, different algorithms for the same reference. The computing process converts the first sense, 2 plus 2, into the second one, 4. So in this sense, again intuitively understood, the reference becomes the invariant of transformation of sense, namely algorithms. The sense now comes first, and this opens us toward a non-trivial reconstruction of reference
as second. So this was another interesting aspect, interesting consequence of the move to art-prudter logic that also renegotiate and revise the traditional, realist, Fregean philosophy and logic. And
And again, this also, as I said, can be computationally reinterpreted for programs, which is again correlated to this shift from denotational semantics, simply being a realist account the level of logic and computation to an operational semantics in which we have multiple senses, multiple interactions that can account for how a program acts, how a program functions. No, not necessarily.
I ate you, this cocktail party effect, right? Where you can spot your name. I was following most of it, but one thing I wasn't quite following was how much of this re-situation of Frege was like your take on it, or whether it was via another thinker. Because the interesting thing, I guess, to me is historically, in terms of the history of ideas, he's sort of predating computers, right? So he's laying these interesting logical foundations that various people take up, but studied
systematically. But it's definitely predating like curing. So I was curious about that aspect. Yeah, I mean, well, I think we talked about this when we were talking about formal languages, especially I think I remember that I talked about Frigga and Tarski. Yeah, definitely, I mean, in fact, Frigga, I think, is a constructivist when you look at it more carefully, and there is a lot in common. But I think when it comes to the philosophy of logic, he's a realist. He's a provenant of the referential dimension, which is ultimately
a metaphysical account, and hence can be reinterpreted very sloppily, as it has been by so many linguistics, or by computer science, or by logicians, or by philosophers. The idea that once, even though I think Frigge, we shouldn't really push this too far, because Frigge is rather innocent when he defends his realist account or referential. But nevertheless, it's still, you know, once you put the claim, this can be reinterpreted in different ways. And this had led to linguists, for example, saying that according to this, if there is,
in fact, a correspondence between, for example, these behaviors and phenomena that govern linguistic behaviors between these and logic, and especially classical logic, the kind of conservative framework, then according to this referentialist claim or realist claim, then we can say that There are, in fact, there is a realist correspondence between a natural object and a linguistic object. This is the relational theory of meaning. Then we go, for example, to logic.
And we see that how it affects people like Russell in the sense that they develop, you know, an atomistic metaphysical account of logic. And of course it's powerful, but just too powerful that it's too weak, you know, when it tries to be pushed outside of its boundary. Yeah, so it has, I think, even though I think Frigge, to my mind, and I genuinely need to read more of his stuff, is that even though the way that at least Frigge formulates this is innocent in his own framework, the claim.
But once it's taken out of the context, precisely through this correspondences between language and logic, computation, mathematics, so on and so forth, then it can lead to really kind of grotesque claims in various domains in logics and computation and stuff. grotesque in the sense that it's wacky, but simply quite questionable, quite debatable. And of course, classical philosophy of language, for example, never question these things.
It always takes them for granted, the realist account or the referential account of language. And only through the assaults of people later in the 70s and late 60s, there were divergences from these classical referential accounts in language. In the 80s only in logics. only in late 90s and early 20th century with serious divergences from these in computer science. Okay, thanks.
Welcome. So again, as I said, this is the topic of our third module. And this is basically how we can be visualized in that diagram that I posted on the classroom page. The core thought behind it is this move toward protocol logic or theory of computation being the most
fundamental. The move itself, the move from logic to prontologic or theory of computation, itself can be chronicled in a way, starting from, you know, early constructivist programs, you know, Brower and Hayting and Kolmogorov, and then Curry Award correspondence, where typed programs are equal to proofs.
Then logic, according to this constructivist program, is already within the intuitionistic framework, then refinement of both classical logic and intuitionism, we see this move is being made from logic to logic. For example, when we see Corey-Hawart correspondence doesn't have this move toward this interactive theory of computation explicitly made in the Corey-Hawart correspondence, but it already implies this. And how is that? As I said, if the Corey-Hawart corresponds to simply type programs or equal to proofs. So what does this imply? It implies that logic is selecting a subset from a computational proof to logic,
the considered set of programs. This is the idea that you were, for example, in a Hayting framework. You have how to construct a proof from judgments, or how to solve a problem constructively understood. Now, of course, you can construct the proof in different ways. You can solve the problem in different ways, different senses, different senses being different computational problems,
different following different computational schemes or interactive schemes. So this is how, basically, this constructive mode simple intuitionistic framework implies, as I said, already a move toward logic as the theory of computation. And logic in this schema, as Jean-Baptiste Jeunet puts it, simply comes to taming of wild processes, control of dynamic interaction, or a study of these computational intractive phenomenon undergirding logical behaviors, connectives and proofs.
Logic now is the taming of wild processes. But then epistemologically, the question arises epistemologically, which justification do we have for the taming rules? then how can we extrapolate logic from these axiomatic elementary computational phenomena? Obviously, if the taming rules are predefined, then we are again making a kind of an elicit move that reestablishes logic first, computation second.
Which is precisely what this move initiated and drove people to actually reverse this position. Computation comes first, logic comes second. Precisely, we do not want to predefine rules. That's a dogmatic move. Semantic, this is part of the semantic success of the enterprise, that we should not define procedural rules first. But let them arise through the course of the interaction itself. The rules of logic themselves, the taming of the processes, should themselves arise
from interaction, from computational interaction, rather than being predefined, rather than being pre-existing. So this also makes another shift in the landscape. In typical, again, theoretic account of logical behaviors and computational behaviors, you have something called procedural rules, pre-existing rules of how, basically, axioms interact and then make something, they construct something. But if the rules themselves are predetermined, that's already a kind of like an illicit semantic move. We should let the semantic of rules themselves be generated through interaction rather than
pre-defining them. And this is the move that's highlighted specifically in two of the further developments of linear logic, Girard's ludics and Japaregzi's computability logic, where you do not have predefined rules as opposed to in a traditional concept of gaming logics or, for example, in game theory. You do not have predefined winning strategies. You do not have payoff functions. Basically, everything, as I said, it comes from this confrontation of axiomatic acts. else is simply a corollary or a byproduct to this whole constructive program.
And so what is exactly then the, if, as I said, we need to have a taming of these wild processes to understand logic, what is a program, how from these really complex interactional schemas, computational interactional schemas, for example, something like a proof comes through. So obviously for that we need taming, taming processes, you know, a kind of a, and That's why we call it a kind of a proto-logic, where at the same time you have taming process, but you do not have procedural rules, predefined rules. So what is exactly this?
Then how can we define these taming processes, how proto-logic? This is really, the whole idea is really encapsulated in the concept of negation, especially the computational mathematical interpretation of negation. As I said, negation in logic is you have all those philosophical interpretations of this in Hegel and these things and stuff. But negation is really a duality. Negation itself is the interchange of roles, is the interaction. That's how basically it's formulated, that interaction of duality, namely negation, itself should organize basically the phenomena or the behaviors that are arising through the
course of the confrontation of these axiomatic acts. For example, at the level of proof and the construction of proof, negation is the intractional duality between proofs of A and proofs of not A. We saw this can be represented as you have a player that tries to prove to verify and a player tries to falsify and they both have their own strategies. And these strategies interact. The proof itself is the interaction,
winning strategy that emerges out of the interaction of these strategies, of the verifier and the thalsifier. And this move, this reinterpretation of negation as interaction of duality can be traced back to trivial, it can be traced back to De Morgan's duality in mathematics. But really, the main person who's behind this is Godel's completeness theorem, which establishes dualities for the first time
in proofs of A and models of not A. to confront algorithms or proofs in our current award framework, in interactive theory of computation. Now, according to this account of negation as interaction of duality, to face algorithms, proofs inhabiting type A, one also needs algorithms or proofs inhabiting type not A of the falsifier. Bad proofs are necessary. Falsifying proofs are necessary. Precisely, you see that this
This is already, we have the concept of validity and truth has been completely shifted from that zero-intractional framework of classical logic and classical proof theory to an intractional one, where there is no, in order to construct or validate a hypothesis, you need to have its dual. And this dual is represented by the environment, by the context, by the falsifier, and so on and so forth. You cannot posit the validity without this program for validation, without the context, without an opponent, without an environment, without a falsifier,
the proof of type not A. And this is something that we saw that linear logic already started to formulate other than being a resource sensitive logic was the logic of dualities, logic of symmetries. The symbol of it was the orthogonal bottom, M orthogonal P, model and program,
and the environment. And the way that this duality is expressed is that we can generalize the concept of duality as sets of argumentations, as sets of argumentations between an algorithm and this environment, between a proof of A and proof of not A. So this duality itself is implicitly a dialogue, dialogue being computationally understood.
So, in this sense, we saw that, you know, through this move from logic to pro to logic or theory of computation, a lot of things happened. A lot of revisions, reinterpretations. And probably one of the most important ones, if not the most important one, is reestablishing the architectonic foundational value of negation in any logical computational system. And what is this architectonic foundational value of negation?
Negation, it has an algorithmic duality. That's the whole point. Negation is a most fundamental computational concept. And this is something that we will talk about. We will look into it how it basically works, especially once it's being coupled with the logic of resources. I'm going to talk about this architectonic foundational value of negation, computationally understood as an algorithmic duality, especially particularly in two frameworks.
One is Girard's ludics that have been developed by way of Andreoli, Jean-Baptiste Genet, Girard himself, and the other one is Georgian philosopher and computer scientist, Georgi Jaffaretsi, Computability Logic. This session I'm going to talk about computability logic first. So before moving forward, any questions, discussions, stuff? Thank you. Reza.
Hello. I'm only getting this in the broadest strokes. Some of these moves have been covered in Olivia Luca Fraser's Go Back to An Fang. Yes, yes. I got to read that on the plane, but just again, just getting the general broader sense of direction here. I think that article is really superb. It's fantastic. I love it. But I think, as I said, one of the things, and that's not Lukas thinks, I think that's
really a flaw that philosophers usually are very predisposed to, and that's trying to hijack novel concepts coming from sciences, and in this case, logics and computer science, and interpret them by using pre-existing philosophical concepts. And in that case, I think negation is one of the flaws, the way that Luca is trying to reinterpret the concept of duality and the concept of winning from a dialectical Hegelian
perspective, which he does a fantastic job, but I think you can only go so far with this schema of interpretation, precisely because as an algorithmic duality, negation can lead to really wild processes and wild forms of interaction that no longer can be seen through the lens of Hegelian dialectics. Basically once we see, as we will, that duality, algorithmic duality, and the idea of negation
as duality is itself a special case of a wider computational phenomenon. And that's permutation of rules. You see, duality is simply, you can see it as a switch of roles in a game of chess. I move the black, you move the white, and you see my moves from your perspective, I see your moves from my perspective. This is the switch of the roles, and we are trying to counter one another. This is simple duality as an interchange or switching of roles. This itself is a special case of duality or negation as permutation of rules.
That itself covers a broader range of logical computational phenomena. As I said, they are extremely hard to really interpret them in terms of pre-existing philosophical concepts, particularly dialectics. Oh, yes, I can see that. Comments, Adam, Sean, Aaron, Steven, Tal, anyone? I think my questions are on the centrality of negation, but that's what you're diving
into next, right? Go on. Put one more. Implicit. I'm sort of surprised to see negation at the heart of things. instead of branching of some kind. But that's probably a real- BRANCHIN RASMUSSENBAUM GASPALAVANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJANIRAJ
we can see that branching, in fact, can be understood as how the history of this negation is preserved to the system. For example, am I going to, for example, if we are, you know, a zero branch game is the one that, as I will talk about this, if, for example, when I turn off the computer, I lose basically all of the histories of our interaction, comes zero, And then I have to start a new game, so no branching. Or a more sophisticated example, I turn on the computer, it allows me to resume from our interaction history moving toward a more elementary branch.
or even a more sophisticated interaction would be that it allows me to play multiple sessions, multiple scenarios of our chess game at the same time, different branches. So histories, how basically how this history of interaction is preserved, how the history of dualities or algorithmic dualities are preserved can lead to different complex branching in the game. But the most elementary thing is really that the negation is itself the interaction. That's the whole point. That's the algorithmic duality.
That's interaction itself is the negation. Negation not classically understood, but simply as an algorithmic duality, the interchange of rules, which is again itself, as I said, a special case of permutation of rules in more general sense of concurrent systems. Cool. Okay. So, the content of today's session is a little bit scary. I think there's too much formalism, but it's nevertheless, I think, it's necessary to slowly move toward these formalism precisely because of two reasons.
One, not only to understand a bit of technical definitions and stuff, but also precisely because of these intuitive biases that I know that all of us are involved with, especially because some of these concepts have intuitive connotations. You can have intuitive impressions of negation, of intraction, of so many of these stuff, So the first move before I introduce computability logic, some really, really general remarks on game semantics.
and maybe semantics of interaction or semantics of games and how you approach. This is basically the idea that how you can, if you have your interactive framework at the level of syntax, as Girard does, then semantics autonomously arises from interaction at the level of syntax. This is kind of the computational interactive formulation of the syntax-semantics interface. Luca talks about it in her paper. She says the imanogenesis of semantics from syntax
within this interactive framework. So this is usually aligned with the classical accounts of game semantics, where you have first the syntax, and then you study how semantic arises from interaction of your formulas at the level of syntax. Now the thing is that who developed computability logic thinks this should not be the case, and in fact this is an erroneous move. He tries to preserve the idea of classical logic that semantics should always come first.
We need to first anchor the semantics, the minimal semantics, coherent but minimal semantics or truth, then fix the syntax, rather than fixing syntax and then trying to see how a semantics can be generated for it. So this difference of computability with linear logic in a Girardian sense can be understood as two different attitudes to classical logic and intuitionism. Classical logic, as I said, semantic comes first, syntax,
you know, first you put the semantics of value, semantics of truth first, and then you try to analyze that a little bit of syntax. The whole point of linear logic development was break away from this, precisely because when you fix semantics, you become predisposed to use kind of pre-existing dogmas about how to determine, for example, semantics, so on and so forth. That's the idea of what I said in terms of procedural rules and taming of processes. So pre-existing semantics also for Girard implies existing of pre-existing procedural
rules that restrict the scope of interactions or logical behaviors. Now, Jafaridzis thinks that while this is true, but in doing, in breaking away from the classical framework of semantics first and syntax you essentially sacrifice a lot of useful information useful rules that are
basically are implicit in classical logic also once you have syntax even in the intractional level, then really nothing guarantees that a corresponding semantics can come out of it, namely the semantics of validity comes out of it. Because really the semantic of validity is really the ultimate criteria. Hence he says that usually the people who are, you know, the linear logicians fall in the trap of this finding a semantic system
that arbitrarily matches their syntactical system. Hence it becomes again a kind of, you know, a sloppy, you know, reinterpretation of syntax semantics interface. That simply you try to find a semantic system for your syntax. But what does guarantee this matching between your semantic systems and your pre-existing syntactic system? And he talks about it most of the time, the development of semantic system for a syntax system. not only is arbitrary, but also is fundamentally inadequate and insufficient.
So what Japparizze very briefly, how he frames this question, how he tries to solve this, is that he tries to come up with a minimal semantics of validity and truth, constructively understood. So while he stays true to the main idea of classical logics, namely the priority of semantics, but nevertheless he wants to reinterpret it according to the constructivist program of intuitionism. As I said, semantics of truth or validity, but constructively understood. So for that, he basically does two things.
One is that he drops similar but in a different way than Girard's linear logic. He drops procedural rules from interaction. And from this point, computability logic is similar to linear logic. They both draw procedural rules, or at least ludics, rather linear, traditional linear logic. Computability and ludics both draw procedural rules for pre-existing, predefined rules in attraction. But also he reinterprets the logic of resources that are present in linear logic.
His point is that the way that logic of resources are formulated in Girard's linear logic and subsequently in spur of development like Ludix is that they are extremely casual or naive for that matter precisely because the idea is that interaction when we deal with resources, are not only about the quantity of resources that's in linear logic, the choice of how many copies of something you have or you can put together, but also the types of these
resources. Are they weak types of resources in terms of how I can reuse a resource. In terms of types of resources, so there are strong, medium, and weak types of resources, of resources. And this quality of resources can, in fact, lead to different kinds, covering different kinds of logical behaviors and schemas of construction. So these are some of the stuff, motivations behind this idea of new computability logic. But I will talk about this more in detail and then start to talk about why is that it's called computability logic. it's computability logic because it reinterprets church theory thesis, theory of computability
in the classical sense. So the philosophies of computability logic and linear logic overlap in their attempt to develop a logic of resources, but the ways these philosophies materialize are rather different. logic starts with mathematically strict semantics, minimal coherence, but only after that, as the second step, asks what the corresponding logic and its possible axiomatizations are, namely fixing the syntax. Semantic comes first, syntax comes second. As a formal theory of
resources, a linear logic has been motivated and introduced syntactically rather than semantically. essentially by taking classical sequent calculus and deleting or suspending the rules that seemed unacceptable from a certain intuitive, naive resource point of view. And we looked at them. They were the rules of eigenpotency and monotonycy of entailment, weakening and contraction. But nevertheless, the problem remains. In the absence of a clear, formal concept of resource semantical truth or validity, How can the question about whether the resulting system was complete could be even meaningfully asked?
In this process of syntactically rewriting classical logic, some innocent, deeply hidden and fundamental principles of classical logic that have computational, fundamental computational properties are also getting victimized, thrown away along with the more monolithic, the more kind of dogmatic aspects of classical logic. Many retroactive attempts have been made by Girard and his colleagues, Andrew, Jonet, and many others, to find semantical, often gained semantical justification for linear
logic. And we will talk about this in terms of Linux. Technically, it is always possible to come up with some sort of formal semantics that matches a given target syntactic construction. But the whole question is how natural and meaningful is. Sorry? Did I get disconnected? No, it was Tony talking to me. No, it was me. Sorry, I was signing in to check on my other device. Okay. So, technically it's always possible to come up with some sort of formal semantics as much as a given targetic syntactic construction. But the whole question is how natural and meaningful such a semantic is in its own rights and how adequately it corresponds to the logics
underlying philosophy and ambitions. Unless by good luck, the target system really is the right logic. The chances of a decisive success when following the other scheme from syntax to semantics would be rather slim. We know that intuitionistic logic is a logic of problems constructively understood in the sense presented by Hayting and Kolmogorff that I mentioned. I think not the previous session, the session before it. Just as the resource philosophy of computability logic overlaps with that of linear logic, does its algorithmic philosophy with the constructivistic philosophy of intuitionism.
The difference, again, in this way, is that this philosophy is materialized. Intuitionistic logic has come up with a constructive syntax without having an underlying formal semantics. Formal semantics, namely semantics of validity, semantics of how truth should be constructed. So, yes, intuitionistic logic has come up with a constructive syntax without having an underlying formal semantics, such as a clear concept of truth in some constructive
sense. This sort of syntax was essentially obtained from the classical one by banning and suspending the law of the excluded middle, the offending law for an intuitionist constructivist. But as in the case of linear logic, the critical question immediately comes up, where is it guarantee that together with excluded, some innocent principles that have fundamental computational properties and giving rise to logical behaviors are not sacrificed as well.
Now the constructive claims of computability, Jafariz, the computability logic, on the other hand, is based on the fact that it defines truth as algorithmic solvability. Hence also you should expect a different interpretation of negation, really, as the architectonic foundation, fundamental concepts of computation and logic. In other words, it does not find the term constructive syntax meaningful unless it is understood as soundness with respect to some constructive semantics, for only a semantic
may or may not be constructed in a reasonable sense. So the whole idea that how syntax, you have construction at the level of syntax, with the idea that supposedly semantics would have an imminent genesis from the syntax at the interactive level, that even that construction has already an implicit semantic import, how they should interact, how this construction goes about, has already a semantic import. And if you are not, you know, basically does not have a, if you cannot, if you can't make
explicit the semantical import of the construction itself, then this whole idea of syntax-semantic correspondence is dubious and questionable, becomes arbitrary. The reason for the failure of P disjunct not P, law of exclusion middle, sorry, P conjunct not P, or how in computability logic this is formulated is P disjoint union not P. Disjoint
union, people who are familiar, can be compared with this junction in classical logic, but also it can have an equivalence in category theory, so it's represented usually by a co-product symbol in categories here. I will talk about this, the why, what is the significance of use of this joint union symbol. The reason for the failure of p conjunct, not p, p is joint union, p, p co-product, p in computability logic is not that this principle is not included
in its axioms. Rather, the failure of this principle is exactly the reason why this principle or anything else entailing it would not be among the axioms of a sound system for computability logic. Here, failure has a precise semantical meaning. It is non-validity, i.e., existence of a problem A for which A disjoint union and not P is not algorithmically solvable. So this was a little bit commentary on the difference between computability logic and
linear logic, even though at the level of notations and at the level of resources, interpretation of duality, logical operations, they are very similar. But the similarity needs shouldn't be blown out of proportion. They are quite distinct precisely because their underlying principles, their motivations are distinct, fundamentally distinct. Another thing that is important, but also in ludics as well, but even more important so in computable logic, is the concept of game.
We know that game has a kind of special significance in theory of computation. In computability logic, the game itself is the most fundamental computational concept that represents the semantics or logics of behaviors, again being simply a schema of construction, hence representing the semantics or logics of behaviors.
you know, kind of a concept in when they talk about the concept of game in computation logic, it's usually taken as to be a two-player game. It is the trivial concept, or not trivial, this is the predominant concept of duality in mathematics, logics, and computation, a A two-person game symbolizes interchange of roles, as we said, negation as a special case of permutation of roles. So we have a two-person game. The action of these players are interpreted as moves.
So when we are saying moves in a game from now on, it's basically referring to the actions of these players. These action of the players can be simply processes, can be basically proof of A or proof of not A. Then situations arising in the course of interactions between these two players are called positions. So their actions are called moves, situations arising in the course of interactions are called positions, and success or failures of these players in their game are called
wins or losses. An agent and its environment, hence the way that they interact can be formalized in terms of moves, positions, moves or runs, positions, and winnability or failure strategies, win win or loss strategy, win or loss scenarios. So basic stuff about computability logic.
Now what is exactly the primary motivation behind computability logic? Because we talked about the motivation that lead it to, for it to diverge from linear logic. But we really didn't talk about the exact motivations behind the development of computability logic. So algorithmic activities are synonymous to computations. In a game semantic or game theoretic framework, games accordingly represent computational
problems, namely interactive tasks performed by computing agents with computability meaning winnability, i.e., existence of a machine that wins the game against any possible behavior of the environment. So in the interactive theory of computation, particularly in computational logic, which based on a bit of this game semantics. Computability is synonymous to the win scenario, the winnability. Existence of a machine that wins the game against any possible behavior of the environment.
This environment can simply be a context, abstract context. We know that in the 1930s, Church and Turing came up with what has been perceived as an ultimate mathematical definition of the precise meaning of algorithmic solvability. But such a definition was set forth and embraced before really having attempted to answer the seemingly more basic fundamental question about what computational problems are, the very entities that may or may not have algorithmic solutions in the first place. The tradition established since then in theoretical computer science by computability simply
meaning Turing computability of functions as the tasks performed by every Turing machine is nothing but receiving an input x and generating the output fx for some function f. As I mentioned in previous sessions, Turing himself, however, was more cautious about making overly broad philosophical conclusions about this, acknowledging that not everything one would potentially called a computational problem might necessarily be a function or reducible to a function. Traditionally construed computational problems correspond to interfaces in transformational
programs where the interaction between a system and its environment is simple and consists of two steps, querying the system and generating a reply and answer, corresponding to input and output. So this is how basically you can model a typical Turing model or algorithm or classical notion on the state transition as itself as a simple elementary interaction. Input is environment asking a question from the system, and output is the answer of the
system to the environment, query and reply system that we have talked about in details. The computational problems that interactive theory of computation, particularly Jappariz's computability logic deals with, are more general in that the underlying interfaces may have arbitrary complexity. We talked about that, you know, the core reply scenario in, I think, one of the first sessions. I think it was the last session of the computation module that behind this simple schema of query reply input output,
there are many arbitrary complexities of interaction where the query reply becomes extremely convoluted concepts. That was part of the whole idea of breaking the impressionistic intuitions behind the concept of interaction. So OK, so again, to repeat, I forgot where I was. The computational problems that interact the theory of computation, particularly Jafariz's computability logic deals with are more generally that the underlying interfaces
may have arbitrary complexity. Such problems and the corresponding computations can be called interactive as they model potentially long dialogues, interactions between the system and the environment. From the technical point of view, then computability logic is a game logic because it defines interactive computation as games. As we have discussed, there is an extensive literature on game-style models of computation in theoretical computer science, alternating, you know, Turing machines, interactive proof systems, etc., whose main focus is usually computational complexity. Jafariz's system, on the other hand, is concerned with computability rather than complexity,
and deals with deterministic rather than non-deterministic choices. There are, unlike the majority of other game semantics or interactive accounts of games in theoretical computer science, computability logic is not an attempt to use games to construct robust models for Girard's linear logic, or Hayting's intuitionistic calculus, or any other syntactic targets. This was part of the main divergences of computability logic from linear logic.
As I said, rather than the syntax to semantics, computability logic follows the scheme from semantics to syntax. In other words, it views games as foundational entities in their own right, and then explores the logical principles validated by them. What rules can be validated by games constructively and interactively understood within the framework of a minimal coherent semantics, namely semantics of construction co-ogames.
The concept of computability on which the semantics of computability logic is based is a natural and a non-trivial generalization of Church-Turing computability from simple to a step, namely question-answer or input-output problems, the problems of arbitrary degrees and forms of interactivity, where in the course of interaction between the machine and the environment, input and output can be multiple and interlaced, perhaps even taking place throughout the entire process of computation rather than just as the beginning, namely input or the end output, as is the case with simple problems. Technically, the concept is defined in terms of games.
An interactive computational problem or task is a game between a machine and the environment. Where the dynamic input, the steps, are called environment's moves and output steps are called the machine moves. The environment always queries the system and the system responds. Complexly interactive tasks are not generally reducible to well-modeled, well-studied two-step tasks or problems as being covered by classical theory, the Church-Thering theory of computability. For example, tasks involving multiple concurrent sub-tasks naturally generate situations or
positions where both parties may have meaningful actions to take, and it may be up to the player whether to try to make a move or wait to see how things evolve, perhaps performing some vital computations while waiting and watching. It is unclear whether the steps corresponding to such situations should be labeled as machine to move, or environment to move, namely output and input, which makes it then impossible to break the whole process into consecutive pairs or alternately label the steps between inputs and outputs. A standard game semantical approaches that understand players' strategies as functions
from position to moves can't adequately capture the substance of interaction in full generality. They are based on games, but they can't really get into the fundamental aspects of the game itself, game being the minimal semantics of construction. they essentially try to reduce interactive processes to simple chains of queries and replies or input-output events. This is so because in the context of games, the strategy equals function approach inherently
only works when at every step of the play, the player who is expected to make a move is uniquely determined. In this sense, such games can be called strict games. Strictness is typically achieved by procedural or predefined rules or equivalent rules strictly regulating who and when should move. The most standard procedural rules being the one according to which players should take turns in alternating order. So computability logic tries to even suspend and relax even
what we perceive as the most innocent procedural rule, predefined rule. Then to see precisely how the interaction can be reinterpreted, how the game of construction, how the semantics of truth and validity can be reinterpreted. It's suspended in what appears to be the most innocent of procedural rules, simply taking turn when we are playing against one another, when the algorithm and environment or the proof of A and proof of not A can simply take turn in kind of a classical game scenario, even if it's suspend that kind of alternating order. So this is one of the main features distinguishing
computability logic from now CL games from more traditional games, game rules, that strictly regulate which players to move in any given situation are absent. So rules that strictly regulate which players to move in any given situation are absent in computability logic. And it is exactly this feature, the conclusion of suspension of the most innocent procedural rules that makes players' strategies no longer definable as functions, namely functions from
positions to moves. You see, again, an idea of how you can really intuitively understand this in the classical game scenario, function being interpreted as positions to moves. Think about it moving a pawn from one cell to another cell. Introducing pawn to a cell can be interpreted as an input. It creates a counter move and then according to that how you shift it again can be understood as an output or alternatively the more sophisticated still functional thing is that I move my pawn
according to your move. Your move is simply the input that triggered my move. So I put it in a cell. The move that I make is precisely the position to move can be understood as input to an output regime, a function. You can see it in terms of cells, one cell to another cell, according to, I mean, whether just by itself or according to, in reply to a move that has been made by the other chess player. So, computability in the traditional Church-Turing sense is a special case of winnability.
Winnability restricted to two-step input-output question and answer attractive problems. So is the classical concept of truth, which is nothing but winnability restricted to propositions viewed by computability logic as zero-step problems, i.e. games with no moves that are automatically won or lost depending on whether they are true or false. This way, the semantics of computability logic is really the generalization of that of classical logic. Thinking of a human user in the role of the environment, computational problems then, as I said, are synonymous to computational tasks, tasks performed by a machine for the
user or the environment. What is a task for a machine is then a resource for the environment. That's important and vice versa. is a task where a machine is then a resource for the environment and vice versa. Hence, why computability logic drives heavily, again, on a logic of resources, but similar, but a different interpretation as of linear logic. So the computability logic games at the same at the same time formalize our intuition of computational resources. Logical operators are understood as operations on such tasks, resources or games.
Atoms as variables ranging over tasks, resources or games. And validity of a logical formula as being always winnable, i.e. as the existence under every particular interpretation of atoms of a machine that successfully accomplishes, provides or wins the corresponding task or resource or game, no matter how the environment behaves. The idea of algorithmic solvability, how to play against a behavior of the environment, regardless of the specificity of that behavior.
With this semantics, computability logic is a formal theory of computability in the same sense as classical logic is a formal theory of truth. Furthermore, as mentioned, classical concept of truth is a special case of winnability, eventually translate into classical logics being a special fragment of a more general computability logic. So before we start to talk, formalize and talk about the system and notations of computability logic and how it relates, how it really reinterprets some like chair-tearing computability,
hearing reducibility, halting problem, stuff in theory of computation, I think the best way is to give a formalization of the concept of game that can capture the generalizations that has made to this concept. Because as I said, the whole idea is that the game, if we posit the game as a fundamental object of computation, then the game itself needs to be generalized.
Not only that, but also the concept of we need to make explicit the implicit semantic dimensions of game, namely the interactive framework, the constructive framework itself. Any questions, anything if we move forward? Nothing? Okay.
I'm going to share this screen in a while, a short while. So, as I mentioned in computability logic and to some extent even in Girard's ludics, procedural rules are absent and hence the games are called free. But, you know, one of the main differences between Jafaridze and computability logic and Girard's ludics is that in Charinze's system, even the most innocent one, the one that simply accounts for alternating moves, even the two players, are suspended.
it. So in these games, either player is free to make any move at any time. Instead of having procedural rules common for all games, each particular game comes with its own what is called now structural rules. These are structural rules of games. Don't confuse it with structural rules of classical logic. These are rules telling what moves are legal for a given player in a given position. Making an illegal move by a player is possible,
but it results in a loss for that player. The difference between procedure and structural rules is that unlike the standard procedural rules that allow only one player to move, at least move without penalty in every given situation, a structure of rules can be arbitrarily lenient. In particular, they do not necessarily have to satisfy the condition that in every position at most one of the players may have legal moves. When however this condition is satisfied, the result would be a strict type game. Namely, the structural rules of such a game can be thought of as procedural rules according
to which the player that is expected to move in a given non-terminal position is now uniquely determined, one that has legal moves in that position. Quick games are therefore a special case of more general free games, where basically the estructural rules become procedural rules. The latter, namely general free games, present a more adequate and seemingly universal modeling tool for interactive tasks.
So in free games as opposed to strict games, in games that involve structural rules rather and procedural rules. A strategies for playing games can and should no longer be defined as functions from position to moves. That's what I briefly mentioned. So before moving further into computability logic and its formalism, it would be best to provide a formal definition of game, as I said. that is more aligned with free games of computability logic,
games in which procedural rules are suspended and have structural rules, arbitrary lenient. To define the game formally, first, we have to fix several classes of objects and dedicated meta variables for them. By placing the common name for objects between brackets, we denote the set of all objects of that type. So whenever we have brackets, we are denoting the set of all objects of that type. For example, variables in solid. Brackets stands for set of all variables. Now these objects are, let me, oh.
it gave me some sort of... Okay, I can see it now. Well, can you see it? Because it gave me some sort of... I see it, but can you try to change the slot, or move it so I can see if it updates? Yes, okay, one second, sorry, okay. Can you see it? One second. I can see your mouse. I think you went back. Now I see you.
Can you see it now? Yes? Yes. Yes. For some reason, ask permission to share this screen. So objects. First variables, variables in bracket, meaning that all variables, set up all variables. Then letters x, y, z are used to define meta-variables for variables. of variables. Then constants 0, 1, 2, letter C will be used as meta variable for constants.
So variable for constants are, you know, by letter C. Then terms, with terms being, you You know, for variables and constants, letter t will be used as a meta variable for terms. Valuation is defined as any function of the type. The valuation is important. Valuation is defined as any function of the type that takes variables to constants. And that's a variable for valuation called e. I will talk about this and exemplify this a little bit.
Each valuation, e, extends to a function of the type terms to constants by stipulating that for every constant c, there is e of c that equals c. So, moves, you know, so those are basically the variables, terms, and valuations, the more abstract properties of the game. And then there are more familiar components of the game, moves, defined as any finite strings or standard alphabet, plus the symbol heart.
Is it a heart of time? What is that? A special, I can't, my PDF is quite, OK. A special status move. So basically, what is the symbol? It represents a special science move. It's basically a move that is always illegal to make. So it denotes the illicit move. In games, even in the traditional how games are sketched, you have legal moves and illegal moves. Illegal moves, as I said, do not immediately lead to loss, but in competition logic, they do. And you can see there is a reason for this. Because when they don't do lead to loss, it's
precisely because the presence of procedural rules. There are other rules that are already in place that's kind of like specify these illicit moves. But illicit move in computability logic is more general precisely because you have already suspended procedural rules. And hence, illicit move in the framework corresponds to a loss situation, namely an algorithmic unsolvability.
Then players. Players are denoted by top and bottom symbols. You see it's kind of like a linear logic notation symbols. The top and bottom are two orthogonal signs. The T1 and the inverse T. Here and from now on, T or top and bottom are symbolic names for the machine and the environment. T is the machine, T is the one who replies, and bottom is the environment, the one that questions. And the reasons that the notation bottom is the inverse
the word the Gunal Batum, is that it really corresponds to, as I said, corresponds to the idea of negation duality. Because in linear logic, or in, you know, we cite Currie-Howard isomorphism, the whole idea was that if the architectonic foundational concept is really negation, negation is algorithmic duality, then the algorithmic duality is always defined, is always represented by the environment, the one who is the opponent, the one who is the falsifier, one who negates, hence represented
by the symbol of negation in linear logic. And respectively, the letter inverse ampersand will range over players with not inverse ampersand meaning ampersand's adversary, i.e. the player that is not ampersand. Then we have labeled moves. In games you always, because you need to define the transitions, you always label the moves. These are called lab moves. They are defined as any moves prefixed with either the system or environment, top and
bottom. With such a prefix, label indicating who has made the move to determine whether it's a machine move or an environment. Then you have runs defined as any finite or infinite sequence of lab moves or labeled moves, align you to the player and the machine and the environment. And then you have meta variables for runs. Positions are defined as any finite runs in the game. A meta variable for position is fine. A run is a finite or infinite sequence of lab
moves and a position is a finite run. Runs and positions will often be delimited with the tuples and brackets, well-written sets. Denoting the empty run, the one that you just have a two pole without anything in it, it just denotes an empty run. The meaning of an expression such as that, the position phi is appended to the position and then the run. Now again, according to all these definitions,
is a pair A equals to parentheses LR, superscript A, comma, win superscript A, parentheses closed, where LR A is a function that sends each evaluation into a set of runs such that the following two conditions are satisfied. One, a run is in if and only all of its non-empty finite initial segments are in. B, no run containing the whatever labeled move symbol of the illegal move is in.
So in a nutshell, what is LR? What does it really denote? It's basically the structural component of the game, that's arbitrary linear rules. In the sense of structural rules that I mentioned. LR, so it stands for structural rules, about runs, which is, again, a function that sends each valuation into a set of runs. elements of LR, sorry, LR is missing here. Elements of LRA are called the legal runs of A with respect to E.
And all other runs are called illegal. LR, legal run, function that sends valuations and that correspond to a structure of rules. Elements of LRA are called legal runs of A with respect to each, and all other runs called illegal. In particular, if the last moves of the shortest illegal initial segment is inverse ampersand labeled, then it's said to be an inverse ampersand illegal run of A with respect to E. So this is your legal law. So in a game you have all of these things and then you have the legal run. And the legal
run can lead to a winnability position. You know that I said illegal runs automatically, basically, a loss situation for the player. So the next component of this formal definition of free games is winnability situation. And that's symbolized by WN superscript A. It's a function of a type, valuation times run, to players, such that writing for the following condition is satisfied. If, again,
the WNA is missing. If WNA is an ampersand illegal run of A with respect to E, then not inverse ampersand, namely the move of the adversary, the position of the adversary. So the whole idea is that basically the adversary wins. So this is just a very formalized account of a very trivial fact in compatibility logic, that if you make an illegal run as the player, as a verifier in your construction of proof or in your algorithm,
then the adversary, the proof of not A, the falsified fire, wins. And this is the next paragraph is just what I said. Now a game is said to be a static if and only if whenever something is missing here. Let me see if I can, because I should have this in the, some of the, I see that some
of, when I was converting my Word doc to PDF, seems that some of the equations haven't been Let me see if I can open my Word doc instead. Sorry, I didn't check this because I just converted this this morning. Let me see. Let's see. Yeah, okay.
Why does this happen? Does any of you have any clue why some of the symbols are not converted to PDF? Is it because of the embedding? It could be the creation of the PDF doesn't have the fonts. doesn't have the fonts or you don't have no it shouldn't be there I mean this converts the PDF from the machine fun so it should be fine no what well anyway I'm going to share the doc because the best way the best way is to use latex that's the way the best way to preserve symbols yes but to make it fast word is
the best one. Yeah, no, no, no, it's actually quite easy now. Is it? No, I have done that, but sometimes it's just like for very simple, and I'm really, really elementary at the text. Yeah, I get that. Run into problems that delays the whole thing for a long time. Anyway, I'm going to share the doc with you. I mean, the other trick is sometimes if you print to PDF instead of... Okay, yes. Okay, so I need to download a PDF writer. It goes through the print driver and you have a better chance of getting the formatting exactly right. Okay, okay. Without contradicting Tony's comment on Latex, I'm sure he's right.
But yeah, if you print to PDF, sometimes the formatting is cleaner, for sure. Okay. Sorry for all of this. Okay. Okay. Here. We are here. So win a is a function of the type valuation times run to player such that writing win
A for the valuation E, for gamma the following condition is satisfied. If gamma is an illegal run of A with respect to E, then we have winnability condition for the adversary, for the environment. When winnability for the player A for the valuation E is illegal, we say that gamma is
is won by the inverse ampersand run of A with respect to E and respectively when basically the illegal move is made by the adversary. We say that the run with respect to E is won by the adversary. Now a game is said to be static if and only if whenever we have the inverse ampersand
symbol, basically the range or intuitively like the turn of the player, the turn of the player. It's not even the turn of the player, but we can understand intuitively at the turn but it's really the range of, range over players. So if the range of the player is the moved and runs player, made by the player, if it is just inverse ampersand, it means that of the machine, and if it is the negative inverse ampersand, it means that it turns or runs and moves by the adversary.
As I said, if illegal moves won by the player, we show it as a winnability condition with just inverse ampersand. And if you are a player and make an illegal move, basically this winnability condition is for the adversary, which is represented by a negation sign, inverse ampersand. So no, and now, again, A is said to be a static if and only if, whenever winnability condition for A valuation E of gamma
equals to ranges of the player. And the run delta is inverse ampersand delay of gamma. We have the ability condition for delta. So this corresponds with this intuition that, as I briefly mentioned that basically the whole idea of taking turn, taking turn being simply the
idea of the most basic procedure or rule is that it needs to be satisfied. And taking turn can be understood as a delay condition, a delay of how you respond in terms of the query action framework. And once the delay condition, in terms of when the condition is interpreted, you can basically have, when it satisfies taking turn, alternating moves between the player and the environment, between the rare fire and the falsifier, then you have a strict game. Sorry, a static game.
Roughly in a static game, a player can succeed when acting fast. It will remain equally successful acting the same way but slowly. This releases the player from any pressure for time allows it to select its own pace for the game. The following fact is rather a straightforward observation. All elementary games are static." we have when we are working at the interactive level the whole idea is that so many of the interactive
scenarios involve with delays, waiting periods in response to a query made by the environment or the opponent. What is exactly, you know, this, behind this intuition, behind this idea of the static games and the idea of, you know, if a player can succeed when acting fast it will remain equally successful, acting the same way but slowly, is that winnability conditions are
speed independent. This is one of the main ideas in computability logic, that the idea of algorithmic solvability for general computational problems are speed independent. Now, we are ready to clarify what is meant by computational problems. In this context, we can use the term intractive computational problem, or simply problem as synonymous with a static game. The general, the central point of computability logic with regard to the definition of computational problem is that it requires the agent top, we said that it's a machine, be implementable
as a computer program with effective and fully determined behavior. On the other hand, the behavior, including a speed of the agent's bottom, which is the environment, and that quite literally can represent environment in the most general sense, like a completely blind force of nature, a contingent, in terms of how it decides how it questions, where it comes from, so on and so forth. This intuition is captured by the model of interactive computation where machine, agent one, is formalized in what is called HPN in computability logic, a hard play machine.
H is a Turing machine with the capability of making moves. At any time, the current position of the game is fully visible to this machine, as well as it is fully informed about the valuation with respect to which the outcome of the play will be evaluated. This effect is achieved by letting the machine have, along with the ordinary read-write work tape, two additional read-only tapes, the valuation tape and the run tape." And we saw this whole idea introducing those new components into the formal concept of
gain, free gain, can correspond. Evaluation can correspond. Evaluation and the run. Basically, your two only retapes correspond to the valuations at once. Valuation tape and run tape. The former espels some valuation E by listing concepts in the lexicographic order of the corresponding variables. Its contents remain unchanged throughout the work of the machine. As for the run tape, it serves as a dynamic input, espeling at any time the current position of the game. Every time one of the players makes a move, that move with the corresponding label is automatically appended to the contents of the runtime.
So you know this idea of labeling and introducing additional variables and then the corresponding meta-variables in computability logic is precisely because the whole idea of the computability is to not only model a basic fundamental framework of interaction, core game, but also represent the game in this full behavioral complexity, namely the histories of interaction. And this So this is the intuition, the idea behind introduction
of these variables, read-only tapes, the valuation and the runtime, to capture basically histories of interaction, captured the games in its full computational complexity. As always, the computation proceeds in discrete steps, also called clock cycles. How the hard play machine H makes a move alpha are done by constructing alpha in a certain section, say, the beginning of the work tape
and then entering one of the especially designated states called the move states. Therefore, H can make at most one move per clock cycle. On the other hand, as mentioned earlier, there are no limitations to the relative speed of the environment. So the layer can make any finite number of moves per cycle. We assume that the run tape remains stable during a clock cycle and is updated only on a transition from cycle to another. Again, there is a flexibility in arranging details regarding what happens if both of
the player, system and the environment, machine and the algorithm and the context, make moves simultaneously. Another kind of interactive scenario that is important but nevertheless usually not covered in strict game scenarios, but this can be covered by free game scenarios. For clarity, we can assume that if during a given cycle, H makes a move alpha and the environment makes moves beta 1, beta n, then the notion is spelled on the run tape throughout
the next cycle will be the result of appending environment move beta1 to environment move beta n, system making the move alpha to the current position. So again, the idea, as I said, of how you can, too, defining a formal system of game in which you can track the history of moves and interaction, you can in fact cover interactive
scenarios where you can formalize the idea of simultaneity of queries and replies. A configuration of a hard play machine is defined in the standard way. This is a full description of the current state of the machine, the location of its three scanning heads and the contents of its tapes, with the exception that in order to make finite descriptions of configurations possible, we do not formally include a description of the unchanging content of the valuation tape as a part of the configuration, but rather
account for it in our definition of computation branches as this will be seen shortly when I'm talking about the operations and logical operators in computability logic. A configuration C prime is said to be an E successor, valuation successor of a configuration C if and only if when valuation E is spelled on the valuation tape, C prime can legally follow C in the standard, the standard for multi-tape tiering machine sense based on the transition function of the machine and accounting for the possibility of the above
described non-deterministic updates of the contents of the run tape. And E-computation, computation for value E, valuation E branch of H is a sequence of configurations of H where the first configuration is the initial configuration and every other configuration is an E successor of the previous one. Thus, the set of all E-computation branches capture all possible scenarios corresponding to different behaviors by the environment or the opponent, the pulsifier. Each e-computation branch B of a hard-play machine incrementally spells, in the obvious sense, some run of gamma on the run tape, which is called the run spelled by B player,
branch B. And for a game A, when we write H implies or entails A according to valuation E, it means that H wins A on E according to valuation E. If and only if whenever B is an E-computation branch of H and gamma, the run spelled by B, we have winnability condition for game A, evaluation E, run gamma for the player, for the system, for the machine. And we write
H implies A if and only if H implies for gain A at the valuation E for every valuation E. The meaning of H implies A entails A, constructs A, determines A. is that H wins or computes solves A. So, you know, within this interactive free, you know, the concept of free game in this in computability logic, we see that this is basically how it
becomes isomorphic and correspond with kind of, not superficial and not trivial, but in an intuitive way it becomes very similar and fits with the intuitionistic framework. Actually the interactivities, this is just the intuition behind the idea of the algorithmic solvability for general computational problems, general games, free games, becomes a winnability position. The above hard play model of interactive computation seemingly strongly favors the environment
in that the latter may be arbitrarily faster than the machine. What happens if we start limiting the speed of the environment? As I talked about, the answer is nothing as far as computational problems are concerned. The model of computation is the whole idea of speed independency. The model of computation called EPM, Easy Play Machine, takes the idea of limiting the speed of the environment to the extreme, yet it yields the same class of computable problems. This is the whole idea why Jafarizze adds this speed independency condition.
Is to show that the interaction, the computational interaction, the fundamental computational interaction captured by the fundamental concept of gain correlates and covers computational problems in general. As I said, that was the whole point of computability theory, understanding the nature of computational problems in general. And to do that, he shows that there is a speed
in dependency in terms of who waits and who the delays between basically your player and opponent. by suspending the procedural rules of game, namely turning the concept of a strict game to a general game, and then showing that this general game can, in fact, cover general computational problems, precisely because when we drop this speed dependency from the equation in terms of an idea that is captured by existence of procedural rules.
Nothing really happens. the notion of algorithmic solvability doesn't change. We say that an e-computation branch B of a given easy play machine is fair if permission is granted infinitely many times in B. A fair EPM is an EPM whose every computation branch or every valuation E is fair. For an EPM E and valuation a small e, we write E wins,
provides, solves, entails, constructs, based on how you interpret this symbol, according to which framework, in which context. E wins A on E, on valuation E. If and only if, whenever B is an E-computation branch of E and gamma, the run spelled by B, we have the winnability condition for gain E at the evaluation E for the run gamma belonging to the player. Basically the player wins. And B is fair unless gamma run is an environment illegal run of A with respect to E. Just as
with hard playing machines for an EPM, E wins, computes, or solves. A means that the formula, the next formula, E wins A for every valuation of E. In other words, we deal with fair, easy easy playing machine. The idea of algorithmic solvability, the idea of winnability, solvability, construction is precisely the same as hard playing machines, basically the idea of speed independency.
general, yes? Am I still connected because I can't see you guys? You are. Okay. So the whole idea is that the general free games which you have of speed, namely the absence of procedural rules, cover basically the winnability or algorithmic solvability at the level of strict machines, and machines that have procedural
rules. That's the whole idea of generalization. Generalization of the concept of a game does not change the definition of algorithmic solvability as a winning situation. It just leads to a broader computational phenomena and proteological phenomena that capture winnability situation, but it does not change the winnability situation as such.
So that was a little bit above generalization of the concept of game, especially the concept of free game and its relation to strict games that cover the classical church-tiering computability before moving forward into computability logic to end this session, just introducing some of the basic logical operators on games in computability logic. And seeing basically we introduced the notations of linear logic, and we
saw how they function at a very elementary level. And now we can do that same thing with the logic of computability. So we know that computational problems in the traditional church-turing sense can be seen as a strict depth to gain of the special type shown in the following figure. The first level arcs of such a game represents inputs, i.e. environments moves.
And the second level arcs represents outputs, i.e. the system, machine moves. The root of this sort of game is always a machine label, as it corresponds to the situation when there was no input, in which case the machine is considered the winner, because the absence of an input removes any further responsibility from it. All second-level nodes, on the other hand, are environment-labeled, bottom, orthogonal of us were labeled, since they represented situations when there was an input, but the machine failed to generate an output. So hence the environment wins. Finally, each group of siblings of the third-level nodes has exactly one machine-labeled member.
This is so because traditional problems are about computing functions, as famous, and We talked about in Church Turing paradigm, meaning that there is exactly one right output per given input. What particular nodes of those groups will have labeled machine, and only this part of the game tree depends on what particular function is the one under question. The game of the following figure is about computing the successor function, computing n plus 1. So this is kind of like a branching in a strict machine that is about computable functions,
with functions being about the right output. Once we agree that computational problems are nothing but games, and more broadly, general free games, the difference in degrees of generality and flexibility between traditional approach to computational problems and computability logic becomes apparent. What we see in the figure below is indeed a special case of games with strict limits. Staying within these limits would impede any more or less advanced and systematic study
of computability, precisely because of what I said, the situations, different senses, you see, those situations that give rise to winnability condition, namely computability, algorithmic solvability, construction, can be understood as senses, precisely because the strict gains restrict senses in that idea of sense versus reference that I mentioned in terms of programming languages. They restrict the situations, namely protological computational behaviors that can give rise to the same winnability situation.
Hence, they cannot be called to be able to cover general computational problems. As we know, at least in that figure, they simply cover winnability condition for functions. First of all, one would want to get rid of one machine-label node per sibling group restriction
for the third-level nodes. Any natural problem, such as the problem of finding a prime integer between n and 2n, or finding an integral root of exponent 2 minus 2n equals 0, may have more than one, as well as less than one solution. That is, there can be more than one, as well as less than one right output on a given input n. You can, again, think about this stuff that we were talking at the beginning of the session
in terms of algorithmic algorithms constructively understood, correspond to different algorithms, respond to different senses. And that's the whole idea, diversification of the sense, namely broadening the range of algorithms that can yield the winnability condition is the key idea here in interactive
theory of computation. And why not further get rid of any remaining restriction on the labels of whatever level nodes and whatever level arcs? One can think of natural situations when, say, some inputs do not obligate the machine to generate an output, and thus the corresponding second-level nodes should be machine-labeled instead of environment-labeled. An example would be the case when the machine is computing a partially defined function f and receives an input n on which f is undefined. In the depth to restriction, this is the depth to restriction of branching.
This is the view of computational problems as very short dialogues. As I said, the whole idea was that even at the level of computable functions and a strict machine as provided by church-tearing paradigm of computability, we still can model it as an interaction. these are very short dialogues, or two-depth branching, between the machine and its environment, permitting longer than two or even infinitely long branches would allow us to capture problems with arbitrarily high degrees of interactivity and arbitrarily complex interaction protocols. The task performed by a network server is a tangible example of an infinite dialogue
within the server and its environment, the collection of clients, or let us just say the rest of the network. Notice that such a dialogue is usually properly free-gamed with a much more sophisticated interface between the interacting parties than the simple input-output interface offered by the ordinary Turing machine model, where the whole story starts by the environment asking a question, querying, making an input, and ends by the machine generating an answer output with no interaction whatsoever is in between these two steps. Hence the idea that I mentioned in previous sessions, the shift from inter-step sequential
algorithms to intra-step sequential algorithms. Again captures this idea. Removing restrictions on depths yields a meaningful generalization, not only in the upward, but in the downward direction as well. It does make sense to consider dialogues of lengths less than two, constant gains of depth zero. We call them elementary. There are exactly two elementary constant games, building blocks, for which the same symbol, machine and environment, as for the two players are used.
This is a zero, basically, a depth. This can be identified with two propositions of classical logic. machine, T-labeled, true, and orthogonal duality representing the environment being false. And precisely, a classical prepositional framework, traditional prepositional framework of classical logic in fact represents a depth zero game. A snow is white is thus a moveless game automatically won by the machine. But the snow is black is automatically lost. So not only traditional computational problems are a special case of more general gains in
computability logic, traditional propositions as well. This is exactly what eventually makes classical logic a natural elementary fragment of computability logic, a special case of it. However, propositions are not sufficient to build a reasonably expressive logic. For higher expressiveness, classical logic generalizes propositions to predicates. And you can also, this is something that I'm trying to think more carefully, but something that you guys, those of you who are into random and inferentialism can think about.
This is why I think using classical propositional logic, even though it is strong and elegant, is fundamentally inadequate and in fact misleading when used to map inferential conceptual role semantics, the whole idea of linguistic turn or the confrontation of speech acts and how how to determine the role of the concepts in a discourse, in a dialogue.
And that's why I think that's one of the major flaws in Brandone's systems that Wendou O'Doé is inferential role semantics, where concepts, the role of the concept is determined through kind of a pragmatic dimension of dialogues, interaction of speech acts, which is already an interaction game, but is formulated using classical logic. Classical logic is elegant to describe this, but fundamentally it filters out the most important information, most important aspects of really what exactly the role of the concept
is determined through a linguistic interaction. And that is the interaction itself. You do not have a logic that can capture the interaction itself. In fact, position the interaction as a fundamental proteological computational object, then there is a good chance that basically this whole philosophy of language, no matter how sophisticated it is, again falls in the trap of classical philosophies of language. Language simply being a medium of communicative discourse, you know, in a Habermasian sense,
or different kinds of conservative philosophies of language. So I just, so back to the introduction of logical operators and logical operation on free games and computability logic. Logical operators in CL stand for operations on games. There is an open-ended pool of operation in computability logic. Yet, there is a core collection of the most basic and natural game operations. The propositional connectives, negation, conjunction, disjunction, reduction or implication, product,
co-product, and these weird symbols that you see that I will talk about. And the quantifiers, which look like quantifiers of classical logic. Among these are operators of classical logic, and this choice is intentional in computable to logic precisely because comfortable logic is also a generalization of classical logic. And the whole idea of semantics comes first, which is the characteristics of classical
logic. Indeed, after analyzing the relevant definitions, each of the classically shaped operations, restricted to elementary games can be easily seen to be virtually the same as the corresponding operator of classical logic. For instance, if A and B are elementary games, then A, then so is A disjunct B. And the latter is exactly the classical
a and b understood as an elementary game. The whole idea is that one thing is still far from clear in computability logic. Precisely because of this move from a zero-depth game to infinite-depth game, purely interactive framework,
is radical, is in fact so radical, that an asymmetry opens up between the syntactic-semantic interpretation of these notations in classical logic and semantic interpretation of them in computability logic. So you can go only so far with this connecting these isomorphisms between these notations and that of the classical logic. And even though it is useful to intuitively make these comparisons,
but any person who is interested to further go into these areas, it starts to prove less and less useful and more and more confusing if you make these comparisons. Not only with classical, these notations with classical logics, but also with linear logic, precisely because of these fundamental shifts in terms of classical logic, you know, the shift from the zero branch, zero depth to infinite branch, infinite depth, and also in terms of linear logic precisely because of the switching of the syntax semantics priority. Since semantics comes first here, whereas syntax comes first in linear logic, you can
only make so much comparison between the notations of the two, even though they function at a superficial level similarly. Negation, I haven't written this down, negation in computability logic is notated by really the negation symbol in classical logic. But if you have noticed
that we have already have a more fundamental concept of negation built in the semantics of the system itself. And that's really the players, you know, denoted by bottom and top, or top and bottom, machine and the environment, that already indexes the architectonic fundamental concept of algorithmic duality. And negation simply, the negation, the classical notation of negation in computable logic is simply tries to make explicit the algorithmic duality that is already inbuilt within the
system between the notations of the player A and player B, the machine and the environment. Then the choice operations, another class of operations on games in computability logic. These you see, you know, I have seen them being named in various ways, you know, as with and plots, big with and plots as product, co-product, or in terms of conjunction, disjunction,
and union intersection. It really depends on the context of interpretation. So these are a little bit less straightforward than how they are named in linear logic. A1, a small product, A2, is the game. When we are talking about product-co-product, we are taking the category theoretical interpretation. When we are talking about conjunction, disjunction, we are talking about the classicological interpretation and making that kind of comparative move. So A1 product, a small product, A2 is the
same, is the game where the initial position, in the initial position environment has two legal moves or choices, one and two. Once such a choice, I, is made, the game continues as a chosen component AI, meaning that environment with choice I, A1, small product A2, equals to AI. This is how it's formalized. Basically it's the idea of branching, really.
main operator that results in branching in games, the choice operator. Which legal move can I take? As you see, the choice operators, in linear logic, if you remember, the additive multiplicatives, conjuncts, disjuncts, linear logic, where simultaneously gave us an interpretation of resources and who makes the choice. You know, it's the seller that gives you the choice or determines the choice, or it's you
who can freely choose which resource to use. So this has been refined in computability logic. Now resources and choices are two different classes of operators of games. If a choice is never made, environment loses. A1 co-product, a small co-product, A2 is similar, symmetric with machine and environment interchange. That is, in A1 co-product A2, it is the player, the machine who makes an initial choice and
who loses if such a choice is never made. below can give us a clue how to visualize the way a small product, a small co-product combine two games, A and B, as choice propositional connectives. The game A of this figure can be seen to be parenthesis, player, co-product, small co-product, environment, a small, parenthesis, clothes, small product, environment, co-product, machine.
And its negation to be, as you see, the negation distributes over, would be the inverse of that equation. The symmetry duality, familiar with classical logic, persists, we always have the distribution of negation, or are basically choice operators, or in this case, logical operators, and in this case choice operators. So negation distributes in computable logic, and negation, remember, negation is duality, and interchange of roles. Negation distributes over our choice operators.
The whole idea, what does that mean? It means that there is an intimate entanglement between the interchange of role, whose move is that, who plays the game, you know, environment or the machine, there is an entanglement between this and the choice that is being made, whether it's the choice of the environment or the machine. But also within, and that can be even more refined and can be extended to the choice
that is being made within a specific branch, within the specific strategies of, for example, the machine versus the environment. But always interpreted through this entanglement with duality, namely the interactive aspect of the game in the sense that how actions of the machines are in response to the actions of the environment. In addition to the operational, sorry, choice operators, we have quantifier counterparts of them. In computability logic, it's denoted by big product, big co-product of a small
product and small co-product in the sense that when we have this notation, it's nothing but the infinite conjunction or product of A1, A2, A3. So this is just, again, very, very intuitive. It can be understood that the quantifier counterparts for choice operators tells you how much, you know, basically they quantify the conjunction, the conjunction of these choices, as you see in the figure below. So when you have product, if interpreted within category theory, understanding of the symbol,
or if you interpret in terms of conjunction, the classical thing, when you have the big symbol as opposed to the smaller one, you have a quantifier counterparts. You have conjunctions, a1 conjunct, a2 conjunct, a3 and so on and so forth. Then you have parallel operations. This is something that is missing in linear logic, Nevertheless, the whole idea was one of the reasons that interactive theory of computation was introduced, because we captured the parallel concurrent aspects of interaction, precisely
because concurrent, asynchronic concurrent games are general cases of, you know, just simply synchronic, strict gains. Sorry, these operations, some of these, they need to be small, and some of them need to be big, exactly like the ones that we have with our choice operators. So these parallel operations respond to the intuition of parallel computations.
They have been introduced in computability logic to capture the idea of parallel computations. These are called parallel operators. Playing A, disjunct A2 and respectively A1 conjunct A2 means playing the two games simultaneously where in order to win. A machine needs to win in both, respectively at least one of the components, A1. In a chess example, the two-board game, not chess, you see, you can think of this as being
the proof of not A, of type not A. And then the conjunct chess can be easily won by just mimicking in chess the moves that the adversary makes in, you know, not chess, negation chess and vice versa. This is very different from the situation where negation chess, not chess, and co-product chess, winning which is not easy at all. In that game, the machine needs to choose between not chess
and chess, i.e. between playing black or white, and then win the chosen one-word game. So you see, again, the choice operator operators that initiated the branching in our diagrams, in our games. Now, navigating these branches, which corresponds to the computation being done, and the parallel computations, few occupied branches is captured by parallel operations, navigation of branches, corresponds
to the intuition of parallel computation. And again, very similar to the trace operators, duality or negation distributes over. Basically once you apply negation, namely duality, algorithmic duality, to these operators, you can extract their dual notation, their dual function.
When A and B are finite or finite depths, the depths of A disjoint B and A conjunct B is the sum of the depths of A and B, which signifies the exponential growth of the breadth. Figure below illustrate this growth, suggesting that once we have reached the level of parallel operations, parallel computation, so that recurrence operations that I will talk about shortly, continuing drawing trees in the earlier style becoming unfeasible. Basically once you have both branches and parallel operations in games, in both you have shifted from a zero depth or a two depth game to infinite depth game and have moved
non-parallel to parallel computation or parallel operators navigating different sessions of branches at the same time in comfortable logic they don't make trees anymore because drawing trees and understanding how the game is evolving And who wins, basically, is completely unfeasible. And precisely, parallel operators have been designed to make this feasible, to compress the idea of branching and parallel computation.
Then two more, and then we conclude this session. Then another basic, probably the most basic operation on games in computable logic is reduction. Reduction is denoted by classical logic of implication, but is not introduced as a primitive operation as it can be formally defined by classical logical implications of the following formula. From this definition, we see when applied to elementary games, reduction has its ordinary
classical meaning because so do negation and conjunct intuitively B reduces to A is the problem of reducing, B, sorry, implies A is the problem of reducing A to B, solving B for the problem A. So this completely corresponds with the intuitionistic framework of Kolmogorov The idea of how you can reframe proofs in terms of construction of solutions for a given
problem. Which as we talk about, this also captures the idea of, and then once we go into details about this, is also captures the idea of Turing reducibility in Church-Turing thesis. So intuitively, B implies A is the problem of reducing A to B. Solving B for the problem A means solving A while having B as a computational resource. So solution reduction solving a problem, which is a problem of reduction, is essentially
a problem of a resource. Again, corresponding to linear logic intuitionistic framework. Resources are symmetric to problems. is a problem to solve for one player is a resource that the other player can use and vice versa. We talk about this, that the input is a resource provided by the environment. Since B is negated in the following formula, and negation means switching the roles, B B appears as a resource rather than a problem for machine in B implies or reduction sign
A. So the idea that we have in computability logic, we have interactivity, we have choices, We have parallel computation, but also we have the pure Brouwer-hating Kolmogorov constructivist program, which is now being reframed in terms of resources, quite similar to linear logic.
resources are endemic to construction of proofs or solving problems. Then finally we have recurrence operations. And these recurrence operations are the ones that fine-grained the concept of resource in linear logic and more traditional forms of resource sensitive logics. But the difference between linear logic approach to resource is that computability logic also captures the quality or type of resources rather than just the quantity and the number
of copies and the reusability versus non-usability of resources. And these qualities are divided into three classes of the strong, medium, and weak types of resources. What is common to the members of the family of game operations called recurrence operations is that when applied to A, they turn it into a game playing, which means repeatedly playing A. In terms of resources, recurrence operations generate multiple copies of A, thus making
A a reusable or recyclable resource. The difference between various sorts of recurrence is how re-usage is exactly understood. For example, imagine a computer that has a program successfully playing chess. The resource that such a computer provides is obviously something stronger than just chess, for it permits to play chess as many times as the user wishes, while chess as such only assumes one play, basically terminate once it's done. The simplest operating system would allow to start a session of chess, then after finishing or abandoning and destroying it, start a new play again and so on. The game that such a system plays, i.e., the resources it supports or provides, and you
can think about this play again as our verifier, falsifier, a schema of proof of type A and proof of type not A. The game that such a system plays, i.e. the resource it supports or provides, is that a weird sign. Actually the line and the triangle needs to be connected. I had to improvise in that type. which assumes an unbounded number of plays of chess in a sequential fashion.
The single is called sequential recurrence. Now a more advanced, a different type or quality of operating system, however, would not require to destroy the old sessions before starting new ones. Rather, it would allow to run as many parallel sessions as the user needs. branches of chess that can be simultaneously played and you can choose to play them. This is captured by this symbol, meaning nothing but the infinite parallel conjunctions. Chess, chess, chess, conjunct, conjunct, heads. It's called parallel recurrence. As a resource,
recurrence chess is obviously a stronger than sequential recurrence chess as it gives the user more flexibility. So these operators are introduced to capture not just the quantity of resource as in linear logic, but the semantic of resource in the construction, construction being interactive understood. So they capture the semantic of resources within the interaction between the environment and the machine, between the verifier and the falsifier. A really good operating system would not only allow the user to start new sessions of chess
without destroying old ones, it would also make it possible to branch, replicate each particular stage of each particular session, i.e. create any number of copies of any already reached position of the multiple parallel plays of chess. Imagine if this, not only you could branch and play multiple sessions of the game, but also you could save them, all these branches. Basically pure, persistent, you know, history. You can save your histories of interaction. What corresponds to this intuition, semantic intuition of resource, is this simple chess where it's a kind of an invert vertical lollipop. It's called branching recurrence.
As all of the operations except negation and reduction, each sort of recurrence comes with, again, with this dual. And once you apply the negation to them, the duality, you get basically another notation. It's dual notation called corecurrence. recurrence. Say for example, the branching co-recurrence with the vertical lollipop, A is nothing but the branching recurrence of not A, seen from the environment. Seen
seen from the environment. Seen from the environment, that's the whole idea of switching the roles in interaction, the function of duality or negation. Like when basically my moves is your moves from my, sorry, basically the whole idea of interchange of roles or perspectives like for example in a game of chess that you know we see each other's position and strategies from our perspective and accordingly interpret perspective and accordingly interpret or devise strategies of how to move in accordance to
basically your perspective or your role, the function of negation or duality. So basically, once you apply these, apply negation or duality, interchange of role, to this, to the recurrences, you get corecurrence. And the same thing for, you know, you have parallel co-occurrence and sequential corecurrence. And again, these corecurrence can be exactly like the way that our big notations for choice
operators were basically the infinite conjunct or disjunct. These also can be understood as infinite parallel disjunction of resources. So it's the dualities of recurrence operators are basically a study, semantically a study, the availability and interactive behavior of resources throughout the branches, throughout the branches, not only within the interactive context, but also throughout the branches. So this is basically why now we see that what does this mean, what are the consequences
of semantics comes first in computability logic, that basically once you prioritize and minimal coherent semantics, and that semantics constructively understood within the concept of game as the ultimate computational framework, like protocological framework, then you need to refine and redefine resources, choices semantically, and they come with different shades of semantic complexity within this framework. So I don't go forward to computability logic and ludics, but that was just kind of a basic
introduction to the computability logic and what it tries to do and what sets it apart from linear logic, classical logic, but also the way that it tries to generalize computational problems from computable functions to the idea of general computational problems and hence gives a reinterpretation of Church theory and computability. Any questions, answers, comments, stuff? Quiet group today.
Nothing. MALE SPEAKER 1 OK, well, I mean, you have his email, and we can do a classroom if nobody has any questions. No. I never know how long to wait on the silence yet.
MALE SPEAKER 1 So yeah, I think I'd probably just have to digest that stuff. I think it's useful, but I don't think I have any immediate questions. I just have a meta question about, is this the last instance? Sorry, I did drop for a little bit, so I'm not sure if it was already covered. MALE SPEAKER 1 The last instance of what? MALE SPEAKER 1 Oh, sorry, of the seminar. MALE SPEAKER 1 Oh, the last module, yes. The last module. MALE SPEAKER 1 I think, are you wondering if we're in the last module, or is this the last seminar? Is that what you're wondering? JOHN MUELLER
engineering especially design of artificial languages for which natural language simply would be a small fraction okay okay cool okay thank you Reza thank you everyone