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.

To main page

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.

To main page

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.

To main page

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.

To main page

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.

To main page