Logic Seminar Abstracts Spring 2004

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.

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.

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).

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.

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

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.

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.