Tuesday, 11 December 2001 2:30 - 4:00 Luigi Santocanale Fixed Point Logics and Circular Proofs ABSTRACT: Fixed point logics and $\mu$-calculi are obtained from previously existing logical or algebraic frameworks by the addition of least and greatest fixed point operators. The propositional modal $\mu$-calculus or modal $\mu$-logic, useful for model checking, arises from modal logic exactly in this way. A proposition-term in a $\mu$-calculus has a circular structure: it is possible to travel along subformulas and come back to the starting point using regenerations of fixed point. The circularity is inherited by proof-terms. Normally cut-free proofs in sequent calculi are finite because premiss sequents are always strictly smaller than conclusions. However, in settings where the propositions themselves can be circular, there exists the possibility of having circular or infinite proofs as well. Remarkably, in the theories of fixed points, these kind of proofs happen to be the most useful. Thus, the mathematics suggests that we are indeed allowed to make circular reasonings. In this talk I'll explain this apparent paradox, using the concept of initial algebra (and final coalgebra) of a functor. I'll point out the sense for which initial algebras of functors are a generalization of least fixed points and the relationship to inductively constructed sets (such as lists, finite tress, etc.). I will interpret circular proofs as sort of functions (more precisely, arrows of a category) having as domain an inductively constructed set. Recall that recursively defined functions are uniquely determined by their defining system of equations. Similarly it is possible to transform a circular proof in a system of equations and then prove that this system admit a unique solution. NOTE: Luigi will also be talking at UQAM: Pavillon Prisident-Kennedy, local PK-4323 Friday December 14 13h15 Jouer avec l'induction et la coinduction: les jeux de pariti. Un jeu de pariti est joui sur un graphe fini de positions et de mouvements. Dans ce graphe on peut bien avoir des cycles, et pourtant on difinit l'ensemble des chemins inifinis gagnants pour un des deux joueurs ` l'aide de la ``condition de pariti''. Cette condition est bien connue dans la thiorie des automates qui reconnaissent les objects infinis. En effet tout automate est iquivalent ` un automate qui utilise la condition de pariti. Nous allons difinir cette condition et lui donner une interpritation algibrique ` l'aide des notions d'alghbre initiale et coalghbre finale d'un foncteur, c-`-d., ` l'aide des formulations catigorielles de l'induction et de la coinduction. Nous allons associer une expression algibrique ` chaque jeu de pariti et montrer qu'elle dinote (dans la catigorie des ensembles) l'ensemble des stratigies gagnantes pour un des deux joueurs. Nous montrons aussi que les expressions associis aux jeux sont iquivalentes aux expressions qu'on peut engendrer par les operations de produit fini, de coproduit fini, d'alghbre initiale et coalghbre finale, c.`-d aux 5-termes catigoriels. Nous obtenons cette fagon une caractirisation explicite de tous les foncteurs qu'on peut difinir par des 5-termes dans la catigorie des ensembles. (Apologies for any effects of bad character coding!)