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

To main page