September 10: Zlatan Damnjanovic: A New Framework for Formalist Foundations of Mathematics
16.30--18.00
We present and philosophically motivate a formal framework for reconstructing fundamental concepts of ordinary mathematics based on an elementary theory of concatenation. We show how ordinary arithmetical operations usually defined recursively can be recovered within a first-order theory that does not presuppose the legitimacy of definitions by primitive recursion, and how the familiar properties of these operations such as associativity, commutativity and distributivity, usually established by inductive reasoning, can be derived without taking induction principles for granted. As a by-product, we establish mutual interpretability of Robinson Arithmetic, Q, and Adjunctive Set Theory with Extensionality, AST+EXT.

October 8: Marta Bilkova: Uniform Interpolation in Provability Logics via Proof Theory
16.00--17.00
Craig interpolation is the property that says that every provable implication of a logic can be interpolated by a formula in the common language of its antecedent and consequent. Uniform interpolation is a strengthening of this property: the interpolant only depends on one of the two formulas and a choice of its variables which it should not contain (it is sometimes called forgetting variables). In this talk, we concentrate on modal propositional logics, namely provability logics GL and Grz. The uniform interpolation property for GL was first proved by Shavrukov, and later for GL and Grz by Albert Visser via simulation of propositional bisimulation quantifiers, using semantical methods. Looking at the simulation proof theoretically, one observes that the uniform interpolation property relates to existence of analytical proof calculi allowing for terminating proof search (such method was first used by Pitts who proved uniform interpolation for intuitionistic logic). We show how to use such calculi in proving the uniform interpolation property for modal logics. The proof can be seen as a recursive construction of formulas simulating propositional bisimulation quantifiers, but also as a construction of a certain normal form of a given formula and then erasing the unwanted variables.

March 17: Matteo Acclavio: A proof of coherence for symmetric monoidal categories using rewriting
15.30--17.00
A symmetric monoidal category is a category equipped with an associative and commutative (binary) product and an object which is the unit for the product. In fact, those properties only hold up to natural isomorphisms which satisfy some coherence conditions. The Mac Lane coherence theorem asserts the commutativity of all linear diagrams involving the left and right unitors, the associator and the braiding.

We prove the coherence for symmetric monoidal categories using a homotopical method based on rewriting. After proving the convergence of Lafont's string diagram rewriting system, we use it to prove the commutativity of every diagram in a symmetric monoidal category.

April 15: Jeffrey M. Keisler: Observing, reporting and deciding in networks of agents
13.00--14.00
We define an observation network as a network of agents who each have a vocabulary, a knowledge base in first-order logic, and a set of potential observations. Agents can make inferences and report them to other agents to whom they are linked, but communication is restricted to the common vocabulary of the reporter and recipient. Agents add to their knowledge bases by making observations, receiving reports from other agents, and making inferences, and share useful statements with other agents who have different vocabularies. A well-known result from mathematical logic, the Craig Interpolation Theorem, can be interpreted in terms of knowledge sharing between pairs of agents. It is a starting point for our formal results. Certain agents called deciders are faced with alternative statements, and must decide which one is true. We consider various questions about when the network is rich enough to ensure that decisions can be made successfully if the knowledge to do so exists somewhere in the network. We obtain some easily checked completeness conditions that ensure that this is so. The focus of the presentation will be on explanation, interpretation and application of the framework and results, rather than on their derivation. Observation networks are general enough to model many situations. We conclude by considering the example of junction tree algorithms for solving Bayes nets. Joint work with H. Jerome Keisler, University of Wisconsin.

Biography. Jeffrey Keisler is currently Visiting Professor and Fulbright Distinguished Chair in the Mathematics and Systems Analysis Department at Aalto University in Helsinki. A Professor of Management Information Systems at the University of Massachusetts Boston, he has two books and over fifty journal articles and book chapters in decision analysis and related fields. Professor Keisler is past-President of the INFORMS Decision Analysis Society and has received its Publication Award. His PhD in Decision Sciences is from Harvard University. He will present joint work with H. Jerome Keisler who has been a leader of mathematical logic for over fifty years.

March 17: Fabio Pasquali: Choice in Triposes
16:00--17:00
Maietti and Rosolini generalized the notion of exact completion of a category with finite limits to that of elementary quotient completion of hyperdoctrines. A hyperdoctrine will be denoted by (C,P) and can be thought of as a many-sorted logic P where sorts are objects of the category C. The elementary quotient completion of (C,P), denoted by (Cq,Pq), is a new hyperdoctrine whose base Cq is closed under effective quotients of equivalence relations expressed in the logic of Pq. In this talk we focus on triposes, a special class of hyperdoctrines, introduced in by Hyland, Johnstone and Pitts with the purpose (among others) of freely creating an elementary topos out of any given tripos. This mentioned construction is known under the name of tripos-to-topos construction. We characterize when the tripos-to-topos construction factors through an elementary quotient completion. We will show that this happens if and only if the starting tripos validates a form of choice, which we call rule of epsilon choice as it is inspired by Hilbert?s epsilon operator.