September 10: Alexander Leitsch: CERES: Cut-Elimination by Resolution.
16.00--17.00
Abstract:
We present a cut-elimination method for Gentzen's LK which is based on the resolution calculus. The first step consists in a structural analysis of a proof P of a sequent S and the extraction of a clause term X(P). X(P) encodes an abstract structure of the derivations of cut formulas and represents an unsatisfiable set of clauses C(P). A resolution refutation R of C(P) then serves as a skeleton of an LK-proof P' of S with only atomic cuts. P' itself can be obtained from the resolution refutation R via so-called projections of the proof P w.r.t. the clauses in C(P).
The main algorithmic advantage of this method, called CERES, lies in the integration of efficient theorem provers (constructing the resolution refutation R). Moreover the clause term of the proof paves the way for an algebraic analysis and a mathematical comparison of cut-elimination methods. E.g. it can be shown that CERES asymptotically outperforms a large class of ``traditional'' cut-elimination methods including this of Gentzen.
To main page

September 24: Andrés Perea: Minimal belief revision leads to backward induction.
16.00--17.00
Abstract:
In this paper we present a model for games with perfect information in which the players, upon observing an unexpected move, may revise their beliefs about the opponents' preferences over outcomes. For a given profile P of preference relations over outcomes, we impose the following three principles: (1) players initially believe that opponents have preference relations as specified by P; (2) players believe at every instance of the game that each opponent is carrying out an optimal strategy; and (3) beliefs about the opponents' preference relations over outcomes should be revised in a minimal way. It is shown that every player whose preference relation is given by P, and who throughout the game respects common belief in the events (1), (2) and (3), has a unique optimal strategy, namely his backward induction strategy in the game induced by P. We finally show that replacing the minimal belief revision principle (3) by the more modest requirement of Bayesian updating leads exactly to the Dekel-Fudenberg procedure in the game induced by P.
To main page

October 8: Robbert Brak: Theorem provers and Agent Interaction Protocols.
16.00--17.00
Abstract:
The many problems arising from the communication between two or more (software) agents in Multi-Agent Systems are all actively researched. At first, it was thought that conversations between agents would emerge naturally as a byproduct of building inside the agent a message exchange ability and a powerful reasoning mechanism. Soon, however, it appeared that this ideal would not be attainable in practice. Instead, agents should be assisted, for example by recording standard conversations in a so-called interaction protocol, in which the number of possible messages that can be send in one 'conversation step' is drastically restricted.
A large number of more or less formal languages has been developed to describe interaction protocols. One such language is Agent-Negotiation Meta-Language or ANML for short. An important goal of this language (which is based on dynamic logic) is, to deal with the lack of formality in existing protocol languages.
To see how much of this goal has been reached, I have tried to formalize ANML using the interactive theorem prover Isabelle. As I will show, it soon appears that this is not an easy task. It even turns out to be necessary to significantly change the language. This 'debugging' process leads to a new language - ANML2, in which rules of a protocol are abbreviations for sets of logical formulae. In this new framework, which I have implemented in Isabelle, protocols can now easily be expressed. Moreover, it is possible to verify ANML2-protocols with respect to properties such as termination and consistency.
To main page

November 19: Rineke Verbrugge: Strong completeness for non-compact hybrid logics
16.00--17.00
Abstract:
Hybrid logic is a well-known extension of modal logic. Special propositional variables called nominals, which are true in exactly one possible world, are added to the language. One of the pleasant features of hybrid logic is that its correspondence theory is very straightforward: hybrid logic can be translated into first-order logic, where nominals are interpreted as constants. The link is so strong that it is very easy to obtain complete proof systems for classes of frames that satisfy additional properties. This works not only for the usual properties such as transitivity, reflexivity, and symmetry, but also for irreflexivity, asymmetry, and many others that cannot be characterized by modal formulas. Blackburn and Tzakova have provided complete proof systems for many hybrid logics.
One would like to prove strong completeness also for non-compact logics where the relevant properties are not characterized by axioms, but by infinitary rules.
Thus, we extend Blackburn and Tzakova's results by providing a strongly complete infinitary proof system for hybrid logic. This proof system can be extended with countably many sequents, not containing any propositional variables, and each with possibly infinitely many premises. Thus completeness proofs are provided for infinitary hybrid versions of non-compact logics like ancestral logic and Segerberg's modal logic with the bounded chain condition. The completeness proofs look considerably different from the usual one, especially because the usual Lindenbaum Lemma cannot be straightforwardly generalized.
The lecture is based on work with Barteld Kooi and Gerard Renardel de Lavalette.
To main page

December 3: Agatha Walczak-Typke: Stable structures and their non-choice analogues
16.00--17.00
Abstract:
A weakly Dedekind-finite set is is a set X which cannot be mapped onto omega. If the Axiom of Choice is assumed, all weakly Dedekind-finite sets are finite. If the Axiom is not assumed, it is possible for infinite weakly Dedekind-finite sets to exist. The parallels between various classes of weakly Dedekind-finite sets and certain structures explored by model theorists have been noted in the past. We explore these parallels in greater detail, focusing on aleph_0-categorical structures.
To main page

December 10: Guram Bezhanishvili: MacNeille completions in modal logic
16.00--17.00
Abstract:
I will discuss MacNeille completions of modal algebras and present new results about normal modal logics (not) closed under MacNeille completions. The talk will have an algebraic flavour.
To main page

January 21, 2005: Bart Kastermans: A weak form of diamond and cardinal characteristics related to the symmetry group of the natural numbers
16.00--17.00
Abstract:
We´ll descrive a unified way of looking at certain cardinal characteristics on reals (Galois-Tukey connections). Show how from any such characteristic one gets a version of the diamond principle. And then how from this we get that consistently a_p = a_g < cof(Sym(N)). We´ll also give some open questions related to the permutation group of the natural numbers.
To main page

January 21, 2005: R. Yavorsky: Gurevich abstract state machines: theory and practice
15.00--16.00
Abstract:
The talk will discuss current developments in the area of Gurevich ASM's. A short introduction will be followed by a report on the work being recently done in this area in Moscow.
To main page

March 18, 2005: Xavier Caicedo: On implicit connectives
16.00--17.00
Abstract:
An axiomatic expansion E(C) of a deductive logic having a reasonable notion of equivalence defines implicitly a new connective symbol C if E(C)+E(C') proves C and C' equivalent. For some logics like classical propositional calculus, C is necessarily equivalent to a combination of classical connectives, but other calculi, like Heyting calculus or Łukasiewicz logic, allow implicitly defined connectives which are not explicitly definable in this manner, providindg new concepts to the logic. We discuss the general properties of axiomatic expansions of algebraizable logics by these connectives, specially in the case of Heyting calculus and intermediate calculi, and consider the problem of characterizing those logics for which all axiomatically defined implicit connectives are explicitly definable.
To main page

April 8, 2005: D.C. McCarty: An Incompleteness Argument from the 19th Century
16.00--17.00
Abstract:
Paul du Bois-Reymond was a noted mathematician and philosopher of the second half of the 19th Century, publishing on differential equations, analysis and the foundations of mathematics. His magnum opus, "General Function Theory," appeared in 1882 and contained what its author claimed to be a demonstration that mathematics is absolutely incomplete, that is, that there are mathematically meaningful and significant propositions A such that neither A nor not-A will ever be demonstrated by mathematicians. His arguments for this claim are not based on the idea of a formal system but on a detailed analysis of mathematical cognition. We will describe that analysis and assess for their cogency du Bois-Reymond's incompleteness arguments.
To main page

April 28, 2005: C. Tapp: Georg Cantor, the founder of set theory, in contact with catholic theologians of his time
15.30--16.30
Abstract:
Georg Cantor (1845-1918), the founder of set theory, had a large correspondence with some, for the most part catholic, theologians of his time. The talk offers what a careful examination of this correspondence has brought into light. Cantor contacted the theologians primarily as conversational partners for the philosophical problems of the foundations of set theory. He discussed with them the traditional (attempts to) proofs of the impossibility of actually infinite numbers. In this context an elaborate system of distinctions in the notion of infinity arose. Some other highlights of the correspondence are: Cantor's hitherto unknown use of pseudonyms, his Jewish ancestry, and, in spite of his formally belonging to the Lutheran Church, a very close relationship to Catholicism. The founder of set theory is presented both as a scientist admiring theological scholarship and as a private person interested in a broad range of practical religious affairs, in which he showed both devotion and reserve - analogous to enthusiasm and disappointment, the two characteristic extremes that drove his personality.
To main page

April 29, 2005: Emil Jerabek: Admissible rules of modal logics
Abstract:
Building on the work of S. Ghilardi and R. Iemhoff, we present explicit bases of admissible rules for several normal modal systems, including K4, GL, S4, Grz, or GL.3.
To main page

May 27, 2005: Andreas Weiermann: Analyzing Ramsey's theorem for pairs using non standard models
Abstract:
We sketch how to obtain a first order theory which has the same provably recursive functions as WKL_0+Ramsey's theorem for pairs. Moreover we provide a density version for the regressive Ramsey theorem for pairs. Proofs are based on constructions of non-standard models.
To main page

June 3, 2005: Joel Hamkins: Forcing axioms arising from a modal view of set theory
Abstract:
The subject of set theory has become the study of the diverse models of set theory, exhibiting the diverse combinations of set theoretic properties that are possible. Since these models are often constructed by the method of forcing, where a smaller model has access to the objects and truths of a larger world, there is a natural Kripke model here. A statement is possible in a model if it holds in a forcing extension of that world, and necessary if it holds in all forcing extensions of that model. These notions are expressible in the language of set theory, and it is natural to inquire about the modal properties of the situation. Under this interpretation, the S4 axioms (and more) constitute a theorem scheme of ZFC. The remaining S5 axiom (diamond box phi implies phi) results in a new kind of forcing axiom: the Maximality Principle.

The Maximality Principle asserts that any statement phi which holds in a forcing extension V^P and all subsequent extensions V^P*Q, holds already in the ground model V. This principle is equiconsistent with ZFC, though it is not forcible over every model of ZFC. A stronger version of the principle, allowing real parameters, begins to have large cardinal strength. The strongest form of the principle, asserting that it holds in every forcing extension, using the real parameters available there, has large cardinal strength, including interplay with the Axiom of Determinacy. Interesting modified versions of the principle are obtained by restricting to a class of forcing notions. For example, in recent joint work with Woodin, the Necessary Maximality Principle for ccc forcing is proved equiconsistent with the existence of a weakly compact cardinal.
To main page