Amsterdam Workshop onModal Logic, Model Theory and (Co)AlgebrasFriday February 25, 2005 |
| On the occasion of the PhD defense of Balder ten Cate (on the 24th at noon in the Aula of the University of Amsterdam), a workshop will take place on February 25, 2005, on modal logic, model theory and (co)algebras. The provisional program is as follows (abstracts below). This program might still be changed.
The lectures before the lunch break will take place in room I301 and the lectures afer the lunch break will take place in room I401. Both rooms are in building I ("the diamond factory"), Nieuwe Achtergracht 170, in Amsterdam. This schedule makes it possible for those interested to attend a talk by Keith van Rijsbergen (abstract below), which will take place from 13:30-14:30 in Room F.009, Informatics Institute, Kruislaan 403, Amsterdam. For more information, contact Balder ten Cate. |
Johan van Benthem (University of Amsterdam)
|
|
I discuss predicate minimization as an alternative to
standard fixed-point computation, and explain a new
preservation theorem for first-order formulas backing
this up. This leads to several generalizations of modal
correspondence theory. Finally, I high-light difficulties in
lifting first-order model theory to fixed-point languages.
References:
J. van Benthem, 2004, 'Modal Predicates, Fixed-Points,
and Definability', Journal of Symbolic Logic, to appear.
|
Mai Gehrke (New Mexico State University)
|
| In recent joint work with Mike Dunn and Alessandra Palmigiano we give a uniform account of relational completeness for various substructural logics based on a discrete duality and Sahlqvist-like correspondence theory for some complete (non-distributive) lattices. The approach in that work is purely algebraic, but the outcome is a two sorted type of relational structures including what we think might best be thought of as worlds and resources respectively. The talk will be an account, from the relational structures point of view, of some very preliminary views of these structures. |
Valentin Goranko (University of Johannesburg)
|
|
[Joint work with Willem Conradie and Dimiter Vakarelov]
Correspondence and completeness are key topics of the model theory of modal logic. A celebrated general result relating these two concepts for a large syntactic class of modal formulae is Sahlqvist's theorem. Sahlqvist's approach to proving first-order definability and canonicity of modal formulae was paralleled and further developed by van Benthem into the substitution method. Proving first-order definability of modal formulae amounts to elimination of second-order quantifiers. Two algorithms have been developed and implemented for elimination of predicate quantifiers in second-order logic: SCAN, based on a constraint resolution procedure, and DLS, based on a logical equivalence established by Ackermann. In this talk I will introduce a new algorithm, SQEMA, for computing first-order equivalents, and at the same time proving canonicity, of modal formulae. Like DLS, it uses (a modal version of) Ackermann's lemma, but unlike both SCAN and DLS it works directly on modal formulae and thus avoids introduction of Skolem functions and the subsequent problem of unskolemization. If successful, the algorithm produces a locally equivalent pure formula in a temporal (reversive) extension with nominals of the input language. In return for being specialized, SQEMA is more transparent and flexible, easier to use and extend, less dependent on the syntactic shape of the formulae, and apparently has a wider scope of applicability on modal formulae than either of the others. In this talk I will present the core algorithm and illustrate it with some examples. I will then discuss prove its correctness and show that it succeed not only on all Sahlqvist formulae, but also on the larger class of inductive formulae, introduced by Goranko and Vakarelov. Since all formulae on which SQEMA succeeds are provably canonical, we have thus introduced a purely algorithmic approach to proving completeness via canonicity in modal logic and, in particular, established what we believe to be the most general completeness result in modal logic so far. |
Ian Hodkinson (Imperial College London)
|
| I will describe a canonical variety of BAOs that has no canonical axiomatisation (by equations or first-order sentences). In fact, any axiomatisation of it has infinitely many non-canonical axioms. This can be seen using random graphs. |
Maarten Marx (University of Amsterdam)
|
| We show how modal ideas have shaped the development of one of the best known XML languages at present: XPath. In fact an isomorphic variant of the language was invented by three PhD students of one of Balder's promotors, one of which is now one of Balder's promotors, the other is his boss, and the third is in London. We also give a semantic characterization of the expressive power of this language in terms of first order logic. We end with showing some further developments in XML query language design: all based on tools and techniques from modal logic. |
Michael Moortgat (Utrecht University)
|
|
Lambek-style categorial grammars are modal logics of natural language
resources: the assembly of form and meaning is analyzed in terms of
n-ary connectives, interpreted via (n+1)-ary 'merge'/composition
relations; grammatical invariants are laws that do not impose
restrictions on the interpreting composition relations; language
diversity is obtained through non-logical axioms (and their frame
constraints) characterizing the structural deformations under which
the basic form-meaning correspondences are preserved (cf
Kurtonina/Moortgat 1997).
The vocabulary of constants currently employed in grammatical analysis is rather poor: it consists of families of connectives held together by residuation. As a result, a heavy burden is placed on the non-logical module (controlled structural rules). In this talk (reporting on work in progress with Rafaella Bernardi and Rajeev Gore) I extend the core vocabulary by exploiting two symmetries from Dunn's Gaggle-theoretical approach: arrow reversal and tonicity reversal. One obtains residuated and Galois connected families of connectives, together with their duals. Communication between these different perspectives on grammatical structure is channelled through weak distributivity principles generalizing work of V.N. Grishin. The broadened vocabulary makes it possible to recognize as grammatical invariants recalcitrant principles of linguistic organization that before were thought to require the introduction of non-logical axioms. I illustrate with scope construal for generalized quantifiers.
N Kurtonina and M Moortgat, Structural control, in Blackburn and de
Rijke (eds.) Specifying Syntactic Structures, CLSI Standford, 1997,
75-113.
|
Jouko Vaananen (University of Helsinki)
|
| Team logic a very simple non-classical logic where sentences describe "tasks" for "teams", like for a team of robots building a car in a factory. Its semantics is 4-valued. Inside this logic one can see the independence friendly logic as a fragment and understand better, I hope, its potential and limitations. |
Yde Venema (University of Amsterdam)
|
|
There is a strong line of research in theoretical computer science which
links fixed point logics on the one hand, and the theory of automata that
operate on possibly infinite objects on the other hand. The aim of our talk
is to advocate a coalgebraic perspective on this connection.
The main part of the talk will comprise a coalgebraic presentation of modal logic and the modal mu calculus. The key point here is to replace the box and diamond operator using the single `cover connective', the semantics of which can be defined directly in terms of coalgebraic relation lifting. This perspective immediately suggests a coalgebraic generalization of the modal mu-calculus and of the corresponding graph automata. In the last part of the talk I will then briefly sketch some of the results that we obtained for these coalgebra automata, and the consequences of these results for coalgebraic fixed point logics. Here I will focus on the closure properties of coalgebra automata. |
Keith van Rijsbergen (University of Glasgow) |
| Is there a logic for information retrieval? If there is, how does it differ from classical logic? And, what use is it? One of the most important models for IR derives from the representation of documents and queries as vectors in a vector space. I will motivate the answers to the three questions above, by showing how a logic emerges from the geometry of a vector space. As consequence of the line of argumentation an appropriate probability measure on the vector space will be constructed which can be shown to be appropriate for building probabilistic models for IR. |