The annual meeting of the British Logic Colloquium will take place at
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
|4.30-5.30||Zilber||Kempson and Meyer-Viol||-|
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.
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.
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.
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.