Dialogue Games and Logical Proofs in String Diagrams

Video thumbnail (Frame 0)
Video in TIB AV-Portal: Dialogue Games and Logical Proofs in String Diagrams

Formal Metadata

Title
Dialogue Games and Logical Proofs in String Diagrams
Title of Series
Author
Contributors
License
CC Attribution 3.0 Unported:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
2021
Language
English

Content Metadata

Subject Area
Abstract
After a short introduction to the functorial approach to logical proofs and programs initiated by Lambek in the late 1960s, based on the notion of free cartesian closed category, we will describe a recent convergence with the notion of ribbon category introduced in 1990 by Reshetikhin and Turaev in their functorial study of quantum groups and knot invariants. The connection between proof theory and knot theory relies on the notion of ribbon dialogue category, defined by relaxing the traditional assumption that duality is involutive in a ribbon category. We will explain first how to construct the free such dialogue category using a logic of tensor and negation inspired by the work by Girard on linear logic. A coherence theorem for ribbon dialogue categories will be then established, which ensures that two tensorial proofs are equal precisely when their underlying ribbon tangles are equivalent modulo deformation. At the end of the talk, we will show how to understand these ribbon tangles as interactive Opponent/Player strategies tracking the flow of negation functors in dialogue games. The resulting diagrammatic description of tensorial proofs as interactive strategies is performed in the 3-dimensional language of string diagrams for monoidal 2-categories (or more generally weak 3-categories) initiated in the mid 1990s by Street and Verity, McIntyre and Trimble.
Axiom of choice Group action Tensorfeld Correspondence (mathematics) Equaliser (mathematics) Invariantentheorie Inverse element Open set Cartesian product Group representation Invariant (mathematics) Negative number Monoidal category Descriptive statistics Proof theory Algebraic equation Stress (mechanics) Infinity Maxima and minima Hopf algebra Sequence Modulo (jargon) Category of being Arithmetic mean Angle Ring (mathematics) Symmetry (physics) Duality (mathematics) Order (biology) Triangle Summierbarkeit Abelian category Arithmetic progression Spacetime Point (geometry) Three-dimensional space Free group Rule of inference Element (mathematics) Product (business) Morphismus Goodness of fit Latent heat Term (mathematics) Manifold Modulform Energy level Nichtlineares Gleichungssystem Symmetric matrix Associative property Combinatorics Focus (optics) Chemical equation Model theory Commutator Theory Algebraic structure Basis <Mathematik> Mortality rate Linear algebra Cartesian coordinate system Rectangle Braid Formal power series Algebraic closure Network topology Cartesian closed category Game theory Family Funktionenalgebra Transfinite Induktion Greatest element Musical ensemble Beta function Differential (mechanical device) Multiplication sign Modal logic Direction (geometry) Propositional formula Parameter (computer programming) Function (mathematics) Permutation Mathematics Positional notation Strategy game Analogy Diagram Arrow of time Körper <Algebra> Category of being Algebra Representation theory Intuitionistische Mathematik Counterexample Mass flow rate Closed set Moment (mathematics) Computability String theory Variable (mathematics) Time domain Coalgebra Connected space Proof theory Symmetric algebra Isomorphieklasse Funktor Vector space Linearization Quantum Configuration space Normal (geometry) Right angle Identical particles Bounded variation Classical physics Computer programming Trail Functional (mathematics) Finitismus Existence Vapor barrier Quantum group Link (knot theory) Adaptive behavior Knot Dual space Graph coloring Theory Tensorprodukt Hypothesis Power (physics) Thermodynamisches System Well-formed formula Natural number Operator (mathematics) Theorem Genetic programming Abelian category Set theory Module (mathematics) Noise (electronics) Multiplication Shift operator Projective plane Variance Division (mathematics) Calculus Pivot element Numerical analysis Cartier-Divisor Invariant (mathematics) Doubling the cube Logic Topostheorie Bijection Object (grammar) Pressure Thetafunktion Maß <Mathematik>
[Music] uh well i'm very grateful for this invitation to speak a little bit about this connection between proofs and and nuts and uh i think there is a lot to explore still so i will just uh you know explain a little bit the basic ideas and i love this picture that i you know in a way summarizes the talk so it's about you know how a proof can be seen as some kind of naughty structure it has to do with the structure of dialogue okay and so uh it's a long question you know about what is a logical proof how should we should represent it describe it and how we could have a properly you know mathematical notation for for proofs and my starting point in this talk is the idea of game semantics so the idea is that every proof of form of a formula a initiates a dialogue where proponent tries to convince opponent an opponent tries to refute proponent and this is really a nice interactive understanding of proofs and so uh here is a typical proof in uh let's say some some kind of genson notation traditional notation it's a little bit cryptic a bit difficult to understand what's behind so uh but the uh i mean what it proves uh it's so-called drinker's formula which says that in any uh open cafe in paris okay with at least so we need one one drink i mean one customer okay so uh in the cafe so there exists a specific customer y which is so sober it's very sober customer-wise such that if a of y which means that y is drinking then all the other customers in the cafe are also drinking okay and clearly this is counter-intuitive but this is proved by this short proof in classical logic okay this property is not true is not valid in uh intuitionistic logic or constructive logic but it is valid in classical logic and and here is the proof and i said that the proof gives a strategy uh some interactive strategy to convince you so we could i mean i could play it with you so okay imagine i want to convince you of this property which you think is a little bit strange well we opened i mean we entered together in the cafe and then i say okay i i know the customer was uh i mean was very sober so i could pick someone so for instance i don't know uh gerrard if you allow me i wish okay there are your you're very sober so i know that okay if ever you drink everybody else will be drinking in the cafe yes and then uh the point is uh well i may be wrong okay so uh you may be drinking uh jera but then someone else in the cafe is not drinking and so my opponent will refute me and say come on paul you're just wrong this customer so i don't know nikolaj you're allowed to be you know the counter witness uh so okay say okay come on you know here i see nikolai is is not uh i mean he's not so it's so it's a counter example to your claim and so the proof what it does interactively is to allow me to backtrack and so this is a little bit hidden here in the fact that there is two existential here introductions in the rules it allows me as you know prover to backtrack and say oh sorry i was wrong i shouldn't have picked uh you know gerard at the beginning i should have picked nicola okay and so the idea is that the fact i mean the reason why the existential here is not constructive okay uh has to do with the fact that i did use the witness from the interaction i have with the with the opponent okay so in a way i cheat okay but this is exactly the way classical logic works uh interactively and i mean you can you know instead of speaking about the drinker formula you can say that this formula says that every every uh you know proposition uh is either true or as a counter example i mean you can think of the way here as a counter example and of i mean and clearly you know before property is proved uh well this still this this property holds because if someone finds a counter example then we have the counter example i mean this is the same story i've told you here uh okay and so in a way this syntax is a little bit uh you know uh difficult to understand while the game semadix gives a more much more uh intuitive understanding of it and so let me speak briefly about you know the way you know game semantics and algebra are connected so this is through linear logic and a number of connectives which in fact are really adapted or are really uh consistent with linear linear algebra okay and so here we have negation which is really like a dual in and i will come back to that in linear algebra between the game a played by uh you know the player and the game not a same game but played now seen from the point of view of the opponent and so negation permeates the rules of opponent and proponent uh the sum here uh is uh what it does it says okay let's give let's start with two game so there is a game a and a game b there are some so imagine this is chess and poker for instance okay the sum of the game is the game where i as a player decides whether i want to play chess or i want to play a poker and then once it's decided we carry on we never come back to the other board okay uh and so this is understood as here as this disjunction okay it's a choice i do as a player but there is a dual uh connective which is just the same but where opponent makes the choice and this is understood has a form of conjunction because if i let the opponent you know the environment choose then clearly i should be a master in chess but also a master in poker if i want to to you know win the game because i don't know what the opponent will choose and so this is really a notion of constructive you know conjunction it's the end okay so this is this little symbol used for and but there is also a tensor product where the two games are played in parallel but but only opponent is allowed to switch board okay and so player will just play where opponent has just played and this is understood as a classical conjunction when i say classical i mean in the sense of classical logic and there is a dual we're same but now player is allowed to switch board okay and the nice thing is that this is can be understood as a form of classical disjunction and so i will show you how to establish uh the fact that uh for every formula so for every game so here for instance let's let's take a determined you know version of uh chess uh well we have the property that a let's call it the chest it's called property a or here not a so not a remember is just you swap the board and so i will give you an interactive strategy which wins in that game um and so really the idea is that we are playing i mean i am playing two boards uh here in parallel and here in front of me there is a tensor product and the tensor product can be seen of a amino strategy or a counter strategy of type tensor can be seen as a pair of strategies so let's say i'm playing against two you know uh famous russian uh you know chess masters and i will show you how i i can win by playing here white and here playing black okay and of course i mean winning i you know i'm not crazy i i cannot win against both or if i want to win against both i need to to be a very strong master myself but here is by pure logic okay so there is no uh i mean it's just by some kind of logical let's say manipulations or logical you know truth okay so i want to prove that a or not a and the strategy to do that is just uh to let uh it's very simple and it's like cheating really so it's to let course noise start here and so a cautionary plays a move like this or here okay and then copycat what caution has done on this board and i can do that because as because this connective now enables me to play i mean to switch board when because uh uh whenever a move has been playing on one board i'm allowed to move to the other board like this okay and so i have copycat the move by cautionary karpov answers and then i move to the other board and i play like karpov okay so and then cautionary answers and i then i i just move like cautionary has just moved and in that way uh i just by copy you know some kind of copycat strategy i i mean kart karpov really believes he's playing against koshner and karshner really believes he's playing against karpov and in the end one of the two wins and i uh so that means that i will lose maybe karpov wins so i i lose on this board but i win on this board and after all i want to prove that a or not a and so that means that i only need to win on one of the two boards okay so the idea is that we you know we can understand uh you know the fact that property is true or it's uh negation uh something purely interactive and purely linguistic which doesn't have to do with the you know outside world it's not about whether today it's you know cold or hot weather it's really about just pure linguistic phenomena okay and so uh i mentioned that uh there is also this exponential modality which is very nice i will not speak about it anymore uh in this talk but it's nice to know that there is something which enables opponent to reopen to reopen uh balls whenever the opponent is unbehaved and this is what happened in the drinker formula thing at some point i was embarrassed as a player so i reopened a new board and i won on the new board on the second board using information i knew from the first the fact that uh i mean nikola was the good witness and not jr okay and this i learned on the first board and then i used this information on the second board and so uh and by the way this uh maybe i will have the time to mention it but this has to do with co-free constructions of co-algebras or commutative co-algebras in vector spaces and uh uh okay i try to come back to this but now what i will try to show you is that there are connections between these ideas of uh you know game thematics and ideas coming from linear algebra and representation theories so okay i will i will move uh that okay so but before i do that there is this uh important uh let's say tool coming from categories and ideas by lombeck in particular which is to give a functorial approach to proof in variance in the same way that we will see there is a functional approach to not invariance okay so um so i will uh speak about the uh uh in particular i will start from this either coming from brewer hating kolmogorov that a proof of a conjunction okay really is a pair consisting of a proof of a and a proof of b okay so and the idea is that i mean from the game semantics point of view is that someone you know if i claim a and b my environment my opponent could attack me on a or on b so i need to be able to prove a and to prove b so i should have a proof of a and a proof of b okay and uh so this is fine and we will see that this will be interpreted by the existence of a cartesian product in in categories but then there is this more mysterious uh uh description of a proof of a formula from a to b in in logic uh as an algorithm which is able to turn any proof of a uh phi into a proof of b psi of phi so this algorithm phi the question is what does i mean what does it mean an algorithm and this was a i mean this is still a question that people i mean it's not so clear whereas here it's quite clear what it means okay a pair is a pair but an algorithm is something like saying okay i have a notion of algorithm somewhere in the air but i don't know exactly what it means and so the the the notion of cartesian close category is an attempt to answer that question by saying come on okay an algorithm will be a map in in a specific category but this category should be cartesian so it should have a cartesian product and it should be closed in the sense that we should have uh i mean a family of adjunctions between the functor a times and the functor a implies uh and what this means is that we have a natural bijection between the set of maps from a times b to c and the set of maps from b to a implies c and we can think of this as some kind of implication so clearly a basic example is the category of sets and functions okay but there are many many other examples uh and we spend a lot of time uh you know when we study proofs to construct cartesian close categories of many shapes okay um okay so i mean just i mean a typical example is every topos is such and uh you know every every every category of thieves is such and there are many many other examples that we can analyze it's a it's very rich and interesting topic but here i want to focus on the free construction okay and so and you will see it's very symbolic and so if you want to say okay i know i start from a category and now i want to construct the free cartesian closed category and you think about it you say okay i should start by the objects and the objects they should be constructed from the objects of the original category and then the products and the implications okay so there should be this grammar of objects and so the objects of the category of the free catalan clues category are constructed by this grammar okay of uh so you can think of them as formulas or as types constructed by this this this very simple grammar with cartesian product and implication and here again cartesian product is some you can understand it as some kind of conjunction and implication here okay and so the the the now the morphisms in this category they are not as i mean they are a bit subtle to define to describe and i will just say a word about them so they are longer terms and so uh just to say a little bit uh you know a word about lambda terms so lambda terms are terms in the calculus which is a pure calculus of functions okay and i will say a word on that now uh more but then these uh terms of this calculus should be considered modulo some some notion of beta eta conversion and what i claim here is that the situation is very similar to what we have in nut theory where we have like this tangle diagrams okay and then up to uh deformation of diagrams okay typically hydromaster moves okay so so how is the lambda calculus defined i mean there is some kind of i mean some kind of um calculus where you uh describe functions in a given context so typically you said that there is for instance a function x okay this is just a variable in a context where x is of type a and then x will be here this term will be of type a and the most important two rules is the abstraction rule we say that if you have a term p of of type b okay in a given context where the variable has been declared of type a then you will construct a function which is written lambda x dot p and the function here you can think of it as the function which two x associates p of x and so this is the notation here and its type is the type of functions from a to b and so i said implication but you can also think of it as description of uh you know some kind of uh function function space okay all the functions from a to b okay since the variable here is of is of type a and the output is of type b then lambda x dot x this function is of type from i mean a implies b and we can once we have constructed such a function from a to b we can apply it to an argument so this is the notation so p is applied to the argument to get something of type b so the argument is of type a applied when we apply the function of type a in place b or a to b and then we get something and then there are three basic rules here that uh organize i mean they deal with the context and so then what are the beta and ita rule so they're very cute rules i mean they're very beautiful and powerful so the first one says okay if i have constructed the function which 2x associates p of x and then i apply it to an argument then i will get uh i mean i can rewrite it into the same i mean the p but now it's p of q and this is the way it's written here so the because it's a pure calculus of functions we have uh variables x appearing in p and so we can then substitute them by q okay and similarly here there is a rule which says that every term of this calculus can be seen as a function lambda x which 2x associates the term applied to the argument x okay and this is completely formal completely symbolic uh but at the same time uh uh it's known to be connected deeply connected to a longer i mean a language of proofs and so these lambda terms here uh these lambda terms in red they can be seen as proofs of some propositions which are written with implication here and and conjunction uh so there were this uh you know little uh logic i mean calculus here of uh which you can see think also as a calculus of of formulas and here this is the description of the proofs of these formulas but what is important i mean okay i don't ask you to understand all these details about proofs and formulas but what i want to stress is that there is a completely algebraic construction of the free cartesian close category and what this means is that whenever i take a category c here and i have a functor into a cartesian clause category d i can lift this functor to uh because this is cartesian closed i can lift this functor uh from c to d to a functor which preserves up to coherent isomorphism uh the cartesian product and the uh implication arrow okay from this free cartesian clues category into d and so this gives so so this construction is extremely important in the construction of what we call proof in variance uh and uh i mean uh you know i work in a in a like computer science lab and the reason is that in fact this lambda calculus can be seen also as a language of programs so there is a nice correspondence between proofs here and program so you can think of it as a very simple programming language here if you like that you transport you interpret all the so the morphemes are programs and you interpret them into some category and so here the category typically will be uh it could be a category like the category of sets and functions could be a you know a progressive pressure or shift category or the topos or whatever as long as it is cartesian close category we have this beautiful little uh functor okay and the okay this is the story for for you know what what what i would do you know all my day okay constructed this kind of of things okay but then uh uh people in i mean studying not in variance and this is the connection with with nuts they do something extremely similar where instead of constructing so so they start from the functors let's say i mean it's one way to think about uh the construction of not environments there are many ways to construct not in variance but here i will describe the functorial approach which is to say okay if i'm able to to to associate to every color you know an interpretation in a ribbon category and i will explain briefly how to construct such ribbon categories uh using representation theory of quantum groups so when we have such a ribbon category and a functor into into that we can lift the functor to a functor which preserves uh the the structure of ribbon categories but this uh i mean this free ribbon category is a is a category where the morphisms are framed angles so in particular we can study like ribbon nuts and we can associate invariants uh to each ribbon nut because this category is is is yeah um typically the morphism from the uh unit object to to to itself are uh are ribbon uh i mean ribbon diagrams which are closed and so they are they are really like ribbon uh nuts and so you see there is this very i mean kind of fascinating uh uh analogy between what we do with proofs uh in the functional semantics of proofs and the functional you know variance of of nuts and so i will try to explain the connection so i will go very briefly just to explain this uh ribbon categories on string diagrams so uh so it's a notation for monoidal categories and so the idea is that the morphism from eight answer bit answer c to d tensor e will be described as some diagram with three inputs and two outputs okay so abc here as input and d e as output so so the flow i mean it goes in that direction from from the bottom to top okay so this is the arrow here and so composition is described by vertical composition so the composition in the category and the tensor product as horizontal i mean putting side by side f and g so typically here is an example we have f tensor identity so f here identity here and then f tensor identity composed with identity tensor j okay so i mean if you i mean if you interpret this morphism here uh in the string diagram notation you get this picture but then if you interpret this other morphem you get this picture where you see here uh f and g have been kind of uh i mean we play with the the order in which they appear here and the point is that in uh in a monoidal category these two morphisms are equal so really we can be i mean we can trust our eyes up to deformation of diagrams and indeed this diagram here and this diagram here describe the same morphism okay and this is really the beginning of a beautiful story where you try to make you know this topological intuition uh valid up to the point where you can say okay i have a nut and i is described as a morphism in a specific category and the morphism is invariant up to deformation okay so this is what i will explain now now okay so a braided category of monoidal category is just a monoidal category equipped with a braiding so it's a family of isomorphisms from eight and seven to b tensor a so and this is the way i will uh draw them okay i think many people here know this old story but i i felt that it's good to uh to tell it um again anyway so this is the way the the braiding is described but of course we there is an inverse which is described as a negative breading whereas here it's a positive breading uh and our coherence diagrams so this one for instance says that these two uh sequences of arrows are equal in in the braided monoidal category and then grammatically it says this okay that if we permute a with b tensor c is the same as permuting a with b and then permuting a with vc okay another diagram which is essentially saying the same but for for the other uh i mean configuration uh and so this is like braided monoidle category but then we can define i will and i will be very much interested in the notion of balanced monoidal category so it's just a braided monoidal category with a twist which is defined as a family of isomorphisms and which i will depict as a twist like this okay so there is a little like we twist the ribbon and this is why i work with ribbons rather than just strings okay so we can see this little action here on the on the ribbon and so it should satisfy that tti equals the identity so when we twist the unit uh the unit of i mean uh we just do nothing and then this very nice equation we said that when we twist the tensor so when we twist the tensor it's the same as braiding twisting braiding okay and so this is the way to see it so if you want so a tan sub b is really a and b in parallel and so if you twist uh a tensor but this is what you get you need to twist a and b independently but also brace them twice okay uh so you see this is a typical example where uh purely algebraic you know coherence property which says that this map should be equal to this sequence of three maps uh coincides with a very topological intuition okay about how we twist uh ribbons okay and so uh now uh i carry on you know what i'm trying to do now is really to build uh what i what i uh we'll call a ribbon uh category so uh we have we need a notion of duality so a dual pair between an object and a and an object b where we say that a is left dual to b is defined as a pair of morphisms so one morphism from the unit object to a tanzabi and and the other morphism from b tensor a to the unit so you can think of it as some kind of identity here that we are building and here are some evaluations so this is sometimes called co-evaluation map and evaluation map okay so typically we have that when a imagine that a is a finite dimensional vector space and this is b is the vector space of its dual vector space of forms okay so like this is v and v star okay uh and so we ask that these equations are zigzag equalities are satisfied okay which uh are represented uh like this and we say that uh yeah so so in that case we said that a is the right dual of b and yes so anyway the ribbon category is simply defined as a balanced category so if you remember it means braiding twisting okay uh but moreover every object airs a high duel and there is a further requirement that when i take a star tensor a and i twist a and then i evaluate so i get this map from a star tensor a into i or i twist a star and then i evaluate i should get the same okay uh and uh the nice thing is that once we i mean in any ribbon category the object a star is also left dual to a and so you can use the twisting and the braiding to to build i mean the i mean a unit uh so a co-evaluation map and an evaluation map but where you see a star is on the right now okay or yes or here so a star is it's not it's not anymore just a right duel it's also a left draw thanks to this uh uh structure of twist and this equation okay uh and so in particular we have this nice uh equation satisfied in every ribbon category that twisting is the same as braiding and then doing this uh you know playing between the uh here evaluation and co-evaluation but this is the original uh evaluation and then this is the uh the one that we did use from the twist but we can also define the twist from that fact that a star is at the same time a right dual and a left dual of a okay and i will come back to that later because we see the similar phenomena appearing in in logic and i claim that this is of course topology but in fact and this is really the purpose of you know i mean my my work but also this this talk okay is to show that this kind of phenomena can also i mean it's interesting to look at them from a logical point of view and there are some kind of maybe projections uh or uh of of some more um uh i mean like let's say purely logical structures about negations okay because of course when i say duality i have in mind some kind of of negations and we will see that these dualities can be seen as particular instances extremely interesting and rich but instances of a more general pattern where negation is not involutive anymore so uh so something important here in this ribbon category is that when we dualize twice an object we come back to the original object uh which is true for instance for finite dimensional vector spaces or we will see representations which is not true anymore for general vector spaces because typically the map from v to v is double negation or this by dual is not an isomorphism and so um i mean what we see here this phenomena okay i mean it's kind of very nice typically here reconstruction uh of the uh i mean the the twist here from uh dualities so you know these equations can be also played and i will come back to that at the logical level and i will explain how to do that okay anyway we have this free ribbon category so there's this beautiful theorem by shum which says that the free ribbon category can be constructed and uh it has okay so it's a free ribbon category generated by a given category so the objects are signed sequences of objects of c so sine means that epsilon 1 epsilon k are plus or minus to indicate the direction of the links and the morphisms are framed angles uh so frame triangles means they are ribbon you can draw them with ribbons with links labeled by maps in c so this is a typical example so this is a map from a plus to b plus c minus d plus and so you see a plus this is the input so the map goes in that direction and the output is b plus i mean i could say b plus tensor c minus tensor d plus and the c minus here the minus means that the flow of you know of the computation goes in that direction okay so this is typically a map in this free ribbon category okay and so clearly i want to you remember that in the free cartesian clause category the maps were proofs they were longer terms they were very symbolic objects whereas here is purely topological and so my my purpose in the next uh 15 minutes is to show you that there is a way to think about lambda terms at least uh in in good situations where the lambda terms are are linear uh i will explain that okay and you can think of of of this uh you know in connection to the next talk by uh noem zeilberger so when the lambda terms are linear then we get a very i mean slightly mysterious but also very natural i mean the two connections between proofs and nuts and so uh as i was saying okay this category here for the free ribbon category has this beautiful property that it defines the free ribbon category so every time we have a category with braiding twists and good dualities we can take any functor from c to d so here really you should think of this functor as giving an interpretation to each of the links here okay so so we give an interpretation to each of the links and then uh just from the fact that this category is ribbon we can lift this functor to uh to a functor where the tangles of course it's very important here the frame tangles but in the topological sense okay so really modular deformation if you like them are interpreted as morphisms of this category and uh it's it's a way to construct uh many invariants of of of nuts in in topology and so uh uh so uh i will i will try to explain how this can be uh adapted but maybe before that i will say i mean i think it's nice especially here uh to spend maybe five minutes explaining how we construct such ribbon categories okay before i move back to proof because i want to show also that the fact that i look at proof has to do with finite dimensional versus like in possible infinite dimensional representations of of quantum groups uh so uh the idea is that one way to construct these ribbon categories uh is to define them as categories of modules over half algebras so uh suppose given like a symmetric monodole category v so you can for instance take the category of vector spaces of a field okay so by algebra is an object h of the category v equipped with a multiplication and a co-multiplication okay so i use this diagram here for blue for multiplication remember i always drew up sorry i go from below to top so this is multiplication of h and uh and unit and co multiplication and co unit and we should ask these equations so that uh that you know okay so typically this is the by algebra equation which is which says that multiplication and community application are compatible in this way okay and then similarly for i mean unit and co-multiplication multiplication and co-unit and unit and co-unit then an antipode is is defined as the morphism from h2h which satisfies this uh these two equations and whenever we have uh such uh okay so half algebra which is a barrier right with an antipode then we can construct a minority or close category of left modules where the action on the the home okay the internal home is defined by this formula so i wrote it in the swiddler uh style okay uh and this generalizes the the usual construction for groups okay where so you can think uh you know of the your office label as a group and then what you're asking i mean here this says that you should multiply each input by the inverse of h apply the function and then multiply by h and so this is just the quantum conversion but there's the diagrammatic representation of it okay that i just show you here so that means that this object the right negation has has i mean is a is an h module similarly there is a also a way when the anti-pod is reversible to define a closure on the left okay and so similarly except that we need to use this inversible i mean inverse of the antipode and we'll get the good properties required properties so this is a way to get uh you know this implication um here uh i mean so so it's what we get is monorail close category on the two sides left and right but now maybe we want that uh to have also a braided monoidal category so for that purpose uh we introduce a notion of braiding under hop algebra which is uh in fact a vector of h tensor h which satisfies the number of properties which can be represented diagrammatically like this and now the important point uh here is that every braiding okay induces a braiding so a braiding on the help of algebra induces the braiding on the category of left h modules okay and the idea is that you just take v i mean like a vector like v tensor w you swap w and v and you apply uh your uh i mean you multiply the breading okay of your upper algebra at the same time as you permute the vectors v and w okay and so uh then uh what we uh get from that is is a way to relate the uh let's say height negation with the left negation and this is extremely uh important from you know my angle like logical angle because it's really saying that this breading will induce a map from the left negation or right negation to the left negation uh and that this can be understood in a very like logical way as i will as i will uh explain on this map in fact can be uh i mean if we compute it this map it what it does it associates to any uh form here this form where uh we pre-compose uh the form with an action of uh u and u is is is equal to this uh vector here and can be represented uh in this way okay and this is an extremely important uh uh vector in the theory of uh quantum groups uh the thing is that it's as a bad property that it's not a group-like element and so in order to obtain a group-like element in the hopf algebra uh the i mean the very er natural ways to define a twist so this is where we get back to ribbons which is just a vector of h satisfying these equations that i i draw here they are there grammatically and then when you multiply the u with this uh twist about its inverse well suddenly you get a group-like element okay and there is an element of magic i mean uh in this uh thing uh this is something i try to understand in the let's say uh from the outside looking at at uh let's say braided monoidle categories and so on and the reason why it's very important is that in fact it's related to this i mean i mean all the work here that i'm describing was i mean really developed by richette kin and two iaf in the 90s and they're i mean they're they're really the full amount i mean the fundamental observation is that if we take the finite dimensional modules this defines the ribbon category okay so if i go back to my little picture before okay uh sorry for that but here i have this category of finite dimensional representations of my uh you know uh half algebras with with structure and so i can interpret ribbons as morphisms between such representations okay and then uh using that we can construct uh invariants of the of the ribbon so it's a beautiful recipe and i try to think about what i mean it's logical meaning and so to that purpose i will introduce the notion of dialogue category so you know like ribbon is about ribbons and since i want to speak about dialogue games uh i've found it's nice to call my categories like dialogue categories but you will see uh they are extremely stupid category i mean the way they are defined is absolutely uh obvious okay so the the the important thing here is the connection with game thematics the thing i was telling you before and the idea that there are you know proofs are are based on interactions uh and so uh the uh yes so uh so a dialogue category is just defined as a category with an object button and a natural bijection so i mean we ask that there is a way to uh turn any map from a tensor b to this object which i will call bottom uh and you can think of it for instance as the base field uh into a map from b into a implies bottom okay so this is a very uh familiar situation in i mean let's say linear algebra so we can do that on the left or on the right and this is just a definition of a dialogue category so it's very stupid and primitive uh the important thing is that then we can look at introduce the notion of pivotal dialogue category which is a category where we can play with the inputs of forms so whenever i have a map from a tensor bit to bottom i can turn it into a map from b tensor and to bottom and this is the way i like to represent that so it's going i mean like this and we i mean and then when as a coherence diagram which says that if i you know turn a and then turn b it should be the same as turning eight and the b and this can be understood as some kind of coherence property are coherence properties of a map between the two negations that is here the coherence properties here but what is important here is that we get from this i mean a notion of dialogue category with uh you know um so okay so this was the pivotal uh dialogue category but we could also say okay i will define a balanced dialogue category just as a dialogue category with these two negations a breading and a twist and the important property is that every balanced dialogue category is defined the pivotal category and what is i mean an important observation is that we really need the twist to do that so the idea is that whenever i have a map from eight answer b to bottom i can pre-composite with a braiding but also with a twist on on an a here and really the intuition is that the i mean this operation of wheel i was describing here can be described at the same time as a br i mean you see here there is a twist and the braiding so the braiding would not be sufficient and this is the same i mean this is really related to what happens with algebras so um in the case of uh office revise if you remember we needed a little theta to make uh to construct a group-like element in edge and here it's the same story that i mean in that okay i mean when we have a good ribbon of algebra in fact the uh the category of general representations so finite dimensional and infinite dimensional defines such a balanced dialogue category okay and now from this uh structure so in particular i mean so it satisfies this pivotal coherence property and from that uh what we get is that uh when bottom is uh the unit object of this i mean dialog category then that the finite dimensional h modules define a ribbon category so b forwards i mean it was i mean here it can be deduced from a purely for i mean a purely category and formal way that we have this property uh so uh i will uh so i don't have too much time so i will just uh uh show you a little i mean connection between proofs and nuts that makes it even more uh i mean meaningful so the observation is that you know in a ribbon category every object bottom in fact defines a left and the right negation where whenever you dualize the object you tensor it with this um bottom okay and so uh now uh in the same way as we constructed the free cartesian close category we can construct the free balance dialogue category so i will show you the way it's constructed is very similar as the construction for free cartesian plus category so it's just the objects are let's say formulas constructed with the tensor product left negation and right negation and then the maps are proofed okay and so proofs of a logic that i call tensorial logic because it has to do with tensorial algebra and the proofs are constructed exactly in the same way you know using the same that's against unlike you know against unlike constructions of proofs but there is of course a little care about uh uh so the so-called exchange rule so uh of logic okay so we need to care a little bit because this this is really about i mean we we're manipulating the hypothesis of of a proof and so we manipulate them with with nuts and ribbons so we need to have a little bit of information about that but this can be very nicely uh done using i mean the traditional proof theory is just a very basic adaptation of it and from that we get the free dialogue category with a ribbon structure and now we know that uh every time we have a ribbon category and we fix an object bottom uh this defines a dialog category here so where we have uh you know two negations on the left and on the right and so just because it's the free dialogue category we can construct this functor and the main theorem and i will stop uh here is that the functor is faithful okay and so what that this means is that two proofs here in this uh uh logic i mean this is the world of logic this is the world of topology two proofs are equal in this category if and only if the underlying ribbon structure is the same and so i will just show you an application of that because this can be seen as a coherence theorem for dialog categories so imagine i take a an object in the dialog category and i map it here to it's double negation and this map is not involvative since for instance you know you're working in the category of general representations of you know quantum group for instance so this is not i mean this is not uh invertible and then we can also take this other negation to uh to where we take the left and right negation and we change the order then we can apply you know the two turns here that enables to connect these two negations to these two negations and the point is that we don't i mean if we do that we it's not equal to this one we need to twist also the output and to see why in fact so this commutative diagram i mean imagine we want to prove that it's commutative in any dialogue category and so we need only to prove that it's commutative in the free dialogue category and how do we do uh well we construct we see the two maps as proofs okay so there are here are the two maps this is uh this one is here and this this composition is here and then we look at their images through these ops through this functor here and the images are just tangles okay and the tangles what they do they follow the track the manipulations we do on the formulas and in particular on this bottom so they track the bottoms and then the two tangles here are equal and we know that the proofs are equal yes so i'm i i mean i could speak more but i think i'm finished with time uh yes maybe you could leave maybe i should just say one word that these rectangles here where they represent and maybe i will just show you this picture that okay what they represent is the flow of negations in the dialogue between the opponent and the player so if you remember at the very beginning we had this interaction between the prover and the refutation and in fact these tangles here uh they can be also under i mean they can be understood as little strategies where opponents ask a question or maybe i should a good player opponent ask a question and then the player answers here yeah and so there is this interesting uh relationship that i think it would be i mean it's worth exploring more between proofs and and topology thank you very much thank you very much paul andre let us let the place for the dialogue i'm not sure we can hear you at least i cannot yes cannot do you hear me paul andre i can hear you okay good does anybody hear me yes yeah sorry it was my fault yeah it is it is because now you are on the dialogue dialogue mode yeah but i realized that during all that talk i had to sound off i didn't realize that so if you wanted to stop me i was like you know a raging ball i don't know like okay so uh um are there questions actually i have a question it's maximum concern yes i got lost a bit when you discuss this all this breading do you introduce because there's so much literature it's kind of polluted by readings or oh it's really in this dialogue thinks it's you don't introduce brain breeding by hand and it appears by itself ah um well the thing is uh there is this this dream we have to to understand the topology of proofs yes and so in the traditional uh uh you know logic uh we have this so-called exchange rule so where we need i mean clearly when we describe this comes from genson it's an old tradition we need to permute the hypothesis in the proof yeah so uh and so the the thing is usually we don't track we don't track the permutations okay we say symmetry but then it makes sense to uh say that whenever we have such uh uh it's just kind of generalization in yes yes by national briefing but i would not say i mean yeah it's generalization but i would say it's a more refined picture because this can be done but now with hack we remember and so now in the proofs so okay so typically just to show you a proof we will remember the permutations traditionally we don't read because we don't care uh but now because we track them we can get uh this okay free construction which is which is uh which has the let's see some kind of grammar like a category called grammar for infinite dimensional vector spaces with braiding so i mean and so the braiding yes yeah by the by the hopf algebra action and that's the idea yeah maybe i just want to give you a comment if you because it's bragging seems to be it's kind of a bit artificial like fashion instance yeah but if you can see just notion of by algebraia without anti-port unit community just very simple product and co-product yeah and look how many this is the basis of map from n sparrow to m's power uh yeah of course there's some kind of normal form but in intrinsically there's also some three-dimensional manifolds with some some colorings here so yes it's even this already contains three-dimensional picture yeah yeah so that's that's that's uh uh that's indeed uh and maybe okay you know really all this work started from this more uh i mean you know no brain i mean but but where where i manipulate trees yeah so uh i i agreed i mean uh but what i wanted to show you that this phenomena that i i i agree with you there i mean they're they appear and it's they're a bit questionable okay what what are they doing that in fact from the they have they have some kind of they can be understood at a logical level that's what i mean before because the thing is when we look at free bonds uh diagrams we see a lot of phenomena it's difficult to understand what is really coming from the topology and what is coming from the fact that we can negate i mean we can turn things on and so the story that i want to tell so for instance i mean just to say very briefly uh this thing which i mean which would have emerged anyway in proof theory without we didn't so this operation that i was describing here of permuting you know two i mean by by doing this kind of operation of of you know if we think of a proof as something very concrete not not something you know in the air but something that people manipulate and in space and time you know like like we discuss then we see that that this operation is very natural and then we see that the twist appears here so so there is this i would say uh uh surprising and slightly i mean we want to understand it's not okay these connections and maybe just yeah that's that's but i i i agree and i i would need you know i think we need many faults i mean at some point to avoid maybe these uh braidings and yeah yeah my suggestions really to avoid reading make something simple yeah yeah that's it yeah and in other things which is uh all these games uh uh also relate to logic in some different way when you consider a statement with which sequences for any this for any exists it's like a game yeah like different oh yes we exist but uh so there is yes so maybe i should mention very briefly i mean just this last uh there is something that i i wanted to say that there is an interesting open problem i mentioned the exponential modality which you can think of of it as a co-free commutative commonerid okay generated by you know uh and i for the moment i mean so uh recently not not very long ago uh uh like i mean people like daniel murphy have you know studied uh this construction uh in in the category of uh vector spaces so uh and so in fact i mean i have shown that it's connected to the you know sweetest finite dual construction that uh you know and this is when i mean uh i mean this this construction is far f i mean for i mean far far from obvious for me uh i would be interested to see how uh this construction which we know now on vector spaces could be lifted to representations maybe it's exists but i don't know it and this is the kind of things i like to discuss with gerard and the connection with automata theory uh here and i you know all the story i've told was about uh linear so let's say arguments where we cannot repeat hypotheses uh and so in the case of the drinker formula the point is that we can we can construct a coup free i mean the algebraically the story is explained like this that we can construct a co-free commutative commonoid above the existential so we have the existential and this is what enables us to backtrack and change the weakness so if you remember the first time i was taking the gerard as a existential and then i moved to nikola and algebraically this corresponds to the fact that i can construct this bank so here so the co-free commutative commonoid on top of a formula which contains an existential and and honestly i don't fully understand how this could be you know expressed in the language of uh you know uh this hopf algebras but i'm i mean i would love to have lms because that helps me to understand the uh material nature of proofs i mean this is really the point in the way the idea uh i take the opportunity to speak to you directly uh disregarding maybe questions but we will i will ask for questions afterwards uh paul andrei dear paul andre you know that the sweet lost you all constructed for for the scholars being in the field which for as you mentioned the vector spaces uh encounters problems even when the scholars from form a division from not a division from a domain ring without zero divisors but i have uh been aware of a paper by burst p oh yeah yes you know it maybe oh yes so i i don't have to send you no but it's uh uh so so i okay i tried to uh adapt i mean this this construction to a situation where i mean some some shift like precious theoretic construction where i changed the base ring commutative ring uh and so i needed to to generalize this yes to so i used but it's very categorical yes and uh and the question is then is we would like to understand better the combinatorics behind uh and that's what i mean yes so i mean for for very you know kind of general reasons there exists such such a recovery commutative common rate for like any commutative ring but it's not a clear why i mean no what i find fascinating is that you guys all this connection with with your work and differentiation things that i i would need to understand better and so i just wanted to mention this um we can interact in a way yeah of course i would i would love to other questions please sorry if i missed it but why exactly do you need to find a dual here do you need it to define exclamation point mark a or do you need to dualize it uh well it's it's about this um so i mean when you get to uh when you want to work with um um so okay so what hap okay i will uh so what happened is traditional models of uh because this has to do with linear logic so what happens with traditional models of linear logic is that in fact we are able to build using topological uh you know vector spaces or these kind of things we're able to define the co-free commutative commonoid by some kind of variation on the uh general i mean symmetric algebra uh construction so uh and so we get something like uh you know uh i mean powers i mean tensor all powers of a uh to the n uh we symmetrize it we we do some some clever you know uh co-limit construction it's not anymore sum and we get something when we dualize it uh this gives the coffee commutative commonoid uh in the case of vector spaces like you know with no topology there is this construction which i find extremely i mean mysterious where you use the fact that every core algebra induces an algebra structure on the dual and then you do some kind of clever uh clever uh restriction of the on the double double uh uh on the by duel so that you get the co-free commutative criminal i'm not sure it answers your question but i just wanted to to say that to me i kind of understand it but honestly i don't understand it i mean i understand it from the outside but i don't have a completely clear combinatorial and this is what i hope i unders i will i will get from you know this kind of uh work by fear and chris sorry sorry i i i we could discuss offline and i i would be happy but i wouldn't thank you very much so we we resume at 13 30. thank you
Feedback