Dynamic Topological Logic. Past Results, Recent Counterexamples

The theme of Stanford Logic Seminar in spring quarter is Logics of Space. There will be occasional special presentations by visitors. In the first two talks (by Grisha Mints and Johan van Benthem) we begin with preliminaries: modal logic and the topological interpretation up to Tarski's Theorem on completeness of the real line for S4. At the beginning we discuss organizational questions.

Topological logics on product spaces

This is a joint work with G. Bezhanishvili and J. van Benthem

The most basic logic for spatial reasoning we looked at in the seminar
is
S4 interpreted over a topological space. In this study we look at
several
slightly stronger spatial
logics. The logics are stronger in both that their languages have
slightly more expressive power, and in that their intended
interpretation has some additional spatial structure. We will
study several multi-modal languages interpreted in various
topologies of the direct product space. On the side of
interpretation, we are interested in grids and topologies on
grids. If we are starting with two spaces X and Y equipped
with respective topologies tau_X and tau_Y, the product
space obtained as a Cartesian product of X and Y contains
several topologies interesting from the point of view of modal
reasoning about space. There is of course the product topology
obtained as a product of topologies tau_X and tau_Y; there
is the vertical topology tau_V and the corresponding horizontal
one tau_H which are obtained as transfer of tau_X and
tau_Y onto the products space. There is also something like a common
knowledge topology.
We will look at modal interpretation of these topologies and their
interaction on products of some standard topological spaces.

Tarski's Elementary Geometry

We shall study a first-order theory of plane geometry, due to Tarski, which is based on the notion of betweenness and outdistance of points. We will begin with some historical comments and describe (with pictures) the axioms. About Tarski's theory we will investigate four questions: what are its models like (they are planar); whether it is complete (it is); whether it is decidable (it is); and whether it is finitely axiomatizible (it is not).

References:Tarski, Alfred. "What is elementary geometry?" In

Tarski, Alfred and Givant, Steven. "Tarki's system of geometry", Bulletin of Symbolic Logic 5 (2) (1999), 175-214.

Provability algebras and combinatorial independence results

We suggest an approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional modal "provability" operators. We use this structure to analyze Peano arithmetic (PA) and show that an ordinal notation system up to $\epsilon_0$ can be recovered from the corresponding algebra in a canonical way. This method naturally leads to some interesting statements of combinatorial nature independent from PA. We also formulate a simple theorem in the area of propositional modal logic that cannot be proved in (a conservative extension of) PA.

Martin-Lof's type theory with permutative reduction

A system of Martin-Lof's type theory with permutative reductions is investigated. Strong normalization and subformula property are proved.

Lambda logic

Lambda logic is, roughly speaking, the union of lambda calculus and first-order logic. Church originally intended lambda calculus to serve as a foundation of mathematics. This aim foundered on paradoxes, and lambda calculus is now usually regarded as a theory of computation. Nevertheless, since functions play an important role in mathematics, it is often more natural to formulate theorems using lambda-terms for functions than to use the set-theoretic definition of functions. This is especially true if we want to use computers to find or check formal proofs. Typed lambda calculus has been used in some computer proof-checking systems, but the most successful theorem-provers have used pure first-order logic, usually in a clause-language formulation. The author has written a theorem-prover, Otter-lambda, which is based on the well-known first-order prover Otter, but supplements it with a new algorithm for untyped lambda-unification. This permits the prover to instantiate variables with lambda-terms defining functions. For example, one can state the Peano axioms with a variable for the predicate in the induction axiom, and Otter-lambda can instantiate that variable based on the given goal, thus "finding the right instance(s) of induction". The prover will be demonstrated on a number of examples from different areas of mathematics. Lambda logic is the theoretical foundation for Otter-lambda: it answers the question, "In what theory does Otter-lambda find proofs?" Theoretical results have been obtained guaranteeing the soundness of Otter-lambda, but the lambda-unification algorithm is necessarily incomplete, so its usefulness must be judged on its practical results.

Internalised Kripke semantics and proof analysis in modal logic

We present a general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics. The method covers all modal logic characterised by Kripke frames determined by universal or geometric properties and it can be extended to treat also Godel-Lob provability logic.

Last modified: Tue Oct 07 09:26:10 PDT 2003