### Mathematical Logic in The Netherlands

19-20 May 2011

Click here for a PDF version that contains the schedule and all abstracts.

### Thursday, 19 May

10.00-11.00 |
Invited talk: Henk Barendregt (University of Nijmegen) Obtaining results accidentally |
---|---|

11.00-11.15 | Coffee |

11.15-11.40 |
Contributed talk: Wim Veldman (University of Nijmegen) Two equivalents of the fan theorem |

11.40-12.05 |
Contributed talk: Merlin Carl (University of Bonn) Simplified fine structure for applications of constructibility |

12.05-12.30 |
Contributed talk: Yurii Khomskii (University of Amsterdam) Regularity and definability |

12.30-13.30 | Lunch |

13.30-14.30 |
Invited talk: Jaap van Oosten (University of Utrecht) Type theory and homotopy theory |

14.30-14.55 |
Contributed talk: Benno van den Berg (University of Utrecht) A functional interpretation for non-standard arithmetic |

14.55-15.20 |
Contributed talk: Vieri Benci (University of Pisa), Leon Horsten (University of Bristol), and Sylvia Wenmackers (University of Groningen) Axioms for non-archimedean probability |

15.20-15.50 | Coffee |

15.50-16.15 |
Contributed talk: Paula Henk (University of Amsterdam) A new perspective on the arithmetical completeness of GL |

16.15-16.40 |
Contributed talk: Kohei Kishida (University of Groningen) A forgotten trio: Classical semantics for first-order non-classical languages |

16.40-17.05 |
Contributed talk: Frank Roumen (University of Nijmegen) Obtaining the syntactic monoid via duality |

17.05-17.15 | Break |

17.15-18.15 | Plenary discussion session about OzSL |

19.00/19.30- | Conference Dinner |

The conference dinner takes place on Thursday, 19 May, from between 19.00 and 19.30. Click here for the venue. *Registration requested.*

### Friday, 20 May

10.00-11.00 |
Invited talk: Alessandra Palmigiano (University of Amsterdam) Algebraic modal correspondence |
---|---|

11.00-11.15 | Coffee |

11.15-11.40 |
Contributed talk: Johannes Marti (University of Amsterdam) Relation liftings in coalgebraic modal logic |

11.40-12.05 |
Contributed talk: Wouter Stekelenburg (University of Utrecht) Necessary conditions for the construction of a category of assemblies |

12.05-12.30 |
Contributed talk: Dion Coumans (University of Nijmegen) and Sam van Gool (University of Nijmegen) Free algebras via partial algebras for a functor |

12.30-13.30 | Lunch |

13.30-14.30 |
Invited talk: Bas Spitters (University of Nijmegen) Efficient real computation in constructive type theory |

14.30-14.55 |
Contributed talk: Lorijn van Rooijen (University of Nijmegen) Generalised Kripke semantics for the Lambek-Grishin calculus |

14.55-15.20 |
Contributed talk: Jesse Alama (New University of Lisbon) Proof analysis using fine-grained dependency information in formal mathematics |

15.20-15.50 | Coffee |

15.50-16.15 |
Contributed talk: Matteo Bianchetti (University of Milan) Logical consequence |

16.15-16.40 |
Contributed talk: Tonny Hurkens (University of Nijmegen) Logic in easy form: Four labels explaining inference |

16.40-17.05 |
Contributed talk: Paniel Reyes Cardenas (University of Sheffield) Peirce's mathematical structuralism as pragmatistic realism |

### Abstracts of the Invited Talks

Henk Barendregt (University of Nijmegen), **Obtaining results accidentally**

In this talk two examples will be given. Alonzo Church was asked to prove for his dissertation that a certain problem was decidable. He could not do it, but came up with the notion of computability. On a more modest level it will be shown how I tried for my dissertation to make a recursion-theoretic model of the lambda calculus. I did not succeed, but came up with the notions of solvability and the omega-rule in lambda calculus. The latter turned out to be related to Cartesian closed categories having enough points. The former turned out to be essential for understanding Scott's models and Boehm-trees, which was an early example of co-induction.

Jaap van Oosten (University of Utrecht), **Type theory and homotopy theory**

In recent years, there has been a renewed interest in Martin-Löf's type theory, and most emphatically for the interpretation of Identity types as Path spaces. Around this theme there was a meeting in Oberwolfach featuring Fields medalist Vladimir Voevodsky, who is now championing a homotopy theoretical approach to type theory (and the foundations of mathematics in general). The talk will give a sketch of these developments.

Alessandra Palmigiano (University of Amsterdam), **Algebraic modal correspondence**

Sahlqvist correspondence theory is among the most celebrated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. Traditionally developed in a model-theoretic setting (cf. [3], [4]), it provides an algorithmic, syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames.
Sahlvist result can equivalently be reformulated algebraically, via the well known duality between frames and complete atomic Boolean algebras with operators (BAO's). This perspective immediately suggests generalizations of Sahlqvist's theorem along algebraic lines, e.g. to the cases of distributive [2] or arbitrary lattices with operators.
We illustrate, by way of examples, the algebraic mechanisms underlying Sahlqvist correspondence for classical modal logic [1], after having discussed the appropriate duality with the relational semantics. We show how these mechanisms work in much greater generality than the classical setting in which Sahlqvist theory was originally developed. Next we present the newly developed algorithm ALBA [2] which effectively extends the existing most general results on correspondence.

Bibliography:

[1] W. Conradie, A. Palmigiano, S. Sourabh, Algebraic Sahlqvist Correspondence, in preparation.

[2] W. Conradie and A. Palmigiano, Algorithmic Correspondence and Canonicity for Distributive Modal Logic, submitted.

[3] H. Sahlqvist, Correspondence and completeness in the first and second-order semantics for modal logic, in Proceedings of the 3rd Scandinavian Logic Symposium, Uppsala 1973, S. Kanger, ed., 1975, pp. 110-143.

[4] J. van Benthem, Modal logic and classical logic, Bibliopolis, Napoli, 1983.

Bas Spitters (University of Nijmegen), **Efficient real computation in constructive type theory**

In 1967 Bishop proposed to use constructive analysis as a language for exact real computations. Martin Löf proposed constructive type theory as an actual programming language. This language now forms the base of both proof assistants and programming languages. I will report on our effort to actually carry out this research program: we provide an efficient computer verified implementation of exact real numbers in the Coq proof assistant.