The annual meeting of the British Logic Colloquium will take place at
the
University of East Anglia in Norwich from Thursday 7 September to Saturday
9 September 2000, starting after lunch on the Thursday and finishing
before lunch on the Saturday.
The following invited talks have been arranged:
There will also be a session for contributed talks on the Friday
afternoon.
| Thursday | Friday | Saturday | |
|---|---|---|---|
| 9-10 | - | Otto | Ketland |
| 10-11 | - | Rathjen | Prest |
| 11-11.30 | - | Coffee | Coffee |
| 11.30-12.30 | - | Hodkinson | Moore |
| 12.30-2 | - | Lunch | Lunch |
| 2-3 | Pitts | Contributed | - |
| 3-4 | Morgan | Contributed | - |
| 4-4.30 | Tea | Tea | - |
| 4.30-5.30 | Zilber | Kempson and Meyer-Viol | - |
| 5.40- | BLC meeting | - | - |
| 7.30- | Reception | Conference Dinner | - |
Ian Hodkinson
Decidable fragments of first-order temporal logics
This talk concerns first-order temporal logic, obtained by augmenting
classical first-order logic with temporal operators (such as Since and
Until) operating over various kinds of flows of time. Though some
axiomatizations of first-order temporal logics are known, a series of
incompleteness theorems started by unpublished results of Scott and
Lindström in the 1960s show that most standard first-order temporal
logics are not even recursively enumerable. Indeed, the extremely weak
expressive power of the temporal formulas required to prove undecidability
left little hope that any useful decidable fragments located `between'
propositional and first-order temporal logics could ever be found.
We will describe recent joint work with Frank Wolter and Michael
Zakharyaschev on a new kind of decidable fragment of the first-order
temporal language, called the monodic [sic] fragment. Roughly speaking,
monodic fragments are obtained by:
1) restricting the pure classical (non-temporal) part of the language to an
arbitrary decidable fragment of first-order logic, and
2) restricting the temporal part of the language to the `monodic' formulas
whose subformulas beginning with a temporal operator have at most one free
variable.
Condition 1 allows the use of classical decidability results to select a suitable first-order part of the language, while (2) leaves enough room for non-trivial interactions between quantifiers and temporal operators (as in the Barcan formula). Thus, we can talk about objects in the intended domain using the full power of the selected fragment of first-order logic; however, temporal operators may be used to describe the development in time of only one object (two are enough to simulate the behaviour of Turing machines or tilings, causing undecidability).
Decidability of monodic fragments can be proved in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps, which can prove decidability over real-numbers time when the first-order part is evaluated in constant finite domains.
Paper available at http://www.doc.ic.ac.uk/~imh/papers/hwz.ps.gz
Ruth Kempson and Wilfried Meyer-Viol
The Logic of Tree Growth: Dynamic Syntax for Natural Languages
This talk introduces a formal model of the left-to-right process of
language understanding
(Dynamic Syntax) as a novel grammar formalism. The framework uses a modal
logic of finite
trees (LOFT) with interpretation defined as the development of a labelled
tree, each node of
a completed tree annotated with a subterm of a logical formula. Central is
a concept of
monotonic tree growth across partial labelled trees. The framework will
be introduced
as a specialisation of Propositional Dynamic Logic where the states are
structured objects
(decorated trees) and the state space is partially ordered (the ordering
representing the
relation of `tree growth'). The potential of the framework as a grammar
formalism
will be illustrated by providing a characterisation of the interaction
between ``movement"
processes and pronoun construal across a range of languages, while
sustaining a unitary
account of anaphora.
Jeffrey Ketland
Some philosophical issues concerning axiomatic truth theories
In the 1930s, Tarski's work significantly clarified the concept of truth,
its relationship
with the notion of proof, the construction of truth theories free of
inconsistency, and
led to the development of basic concepts of model theory. Embodied in
Tarski's work
(as Convention T) is the central idea that any definition of 'true' must be
governed by
the so-called T-scheme: 'p' is true if and only if p. Recent interest in
axiomatic truth
theories has led to a constructive interaction between philosophical debates
about
truth (e.g., deflationism, redundancy theory, minimalism, the correspondence
theory,
etc.) and certain properties of axiomatic truth theories. In particular, I
have argued
(Ketland 1999, 'Deflationism and Tarski's Paradise', MIND 108) that the
question
whether a system of axioms for truth generates conservative extensions is
related to
arguments for and against deflationism (which is roughly the idea that the
concept of
truth is redundant or theoretically superfluous). For example, the addition
of a
(restricted) T-scheme: T[#p] <-> p (with p an arithmetic sentence) yields
a
conservative extension of PA. The addition of Tarski's satisfaction axioms
to PA
yields a non-conservative extension (known as PA(S)) if the induction scheme
is
expanded, and a conservative extension otherwise. I argue that understanding
the
properties of axiomatic truth theories can lead to valuable insights
regarding
philosophical debates about the concept of truth.
Martin Otto
On guarded logics
Guarded logics have, since the introduction of the
guarded fragment GF of first-order logic FO by Andréka,
van Benthem and Németi, seen a rapid career as a most
promising intermediary between basic modal logics and FO.
Not only do they offer a much more satisfactory explanation
of the good behaviour of modal logics, in regard to their algorithmic
model theory, but they also promise to extend some of the power of
algorithmic and model theoretic techniques from the modal domain to
much richer settings.
In this survey talk I shall try to review some of the recent history
of this development and to illustrate the
major parallels between the modal and guarded scenarios,
in the light of some paradigmatic results.
A guiding idea is the observation that families of logics - like the
rich family of modal logics, the family of bounded-variable logics, and also
the family of guarded logics - are best understood as families in the
light of their semantic invariances (or preservation properties).
On the one hand, these semantic invariances are highly characteristic
of typical domains of applications for respective logics;
on the other hand they account for the specific model theoretic tools
that can be brought to bear.
Andrew Pitts
A computer science application of permutation models of set
theory
The permutation model of set theory with atoms (FM-sets) devised by
Fraenkel and Mostowski in the 1930s supports notions of
`name-abstraction' and `fresh name' that provide a new way to
represent, compute with, and reason about the syntax of formal systems
involving variable-binding operations. Inductively defined FM-sets
involving the name-abstraction set former (together with cartesian
product and disjoint union) can correctly encode syntax modulo
renaming of bound variables. In this way, the standard theory of
algebraic data types can be extended to encompass signatures involving
binding operators. In particular, there is an associated notion of
structural recursion for defining syntax-manipulating functions (such
as capture avoiding substitution, set of free variables, etc) and a
notion of proof by structural induction, both of which remain
pleasingly close to informal practice in computer science.