# Logic Seminar Abstracts Autumn 2003

G. Mints, T. Zhang (Stanford)
Propositional logic of continuous transformations

At the beginning we discuss organizational questions. The theme for this quarter and possibly next is decidable theories. We'll begin with detailed reviews of new papers on decision procedures for arithmetical formulas with small number of quantifiers (Shih Peng Tung) as well as decidable fragments of set theory (Harvey Friedman). There will be occasional special presentations on other topics by visitors.

Dynamical topological logic studies models of the form (X,T), where X is a topological space, T a transformation on X. Application in computer science include hybrid systems, there is a hope to treat mathematically interesting models. Propositional formulas are constructed from variables (atomic formulas) by Boolean connectives, necessity \Box and a monadic operation o. Variables are interpreted by subsets of X, Boolean connectives act in a natural way, \Box is the interior and o is the pre-image under operation T. Under this interpretation the axiom schema o\Box A->\Box oA called (C) expresses continuity of T. J. Davoren proved completeness of S4+C [including o(A&B)=oA&oB, o(~A)=~oA] for the class of all topological spaces, in particular for finite spaces derived from Kripke models. We prove completeness of S4+C for Cantor space. The proof uses a continuous and open map W from the Cantor space onto a suitable Kripke model (K,T) [with T continuous in order topology on K] and a continuous map S on Cantor space satisfying condition: WS=TW.

Jesse Alama, Patrick Girard (Stanford)
Decision Methods for Arithmetical Universal-Existential Sentences

First order arithmetic is very expressive. Truth of very simple classes of sentences is well known to be undecidable (non-recursive). In this series of talks a much less known (and potentially useful) fact is presented: the class of arithmetical universal-existential sentences is decidable by an efficient procedure. At the first meeting necessary definitions and main results are stated. The only prerequisite is the knowledge of the arithmetical language.

Jesse Alama, Patrick Girard (Stanford)
Decision Methods for Arithmetical Universal-Existential Sentences II

At this and next meeting Jesse Alama and Patrick Girard (Stanford) discuss in detail decision methods for arithmetical universal-existential sentences. Necessary definitions will be repeated. Note new room.

Jesse Alama, Patrick Girard (Stanford)
Decision Methods for Arithmetical Universal-Existential Sentences III

This is a concluding talk by Jesse Alama and Patrick Girard (Stanford) on decision methods for arithmetical universal-existential sentences.

Makoto Tatsuta (National Institute of Informatics, Japan)
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction

This paper points out an error in Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.

G. Mints (Stanford)
Computerized Exercises to a Course of First Order Logic

We describe a software package and a web server allowing several formats of administering exercises to students and automated answer checking using three computer programs: OTTER, MACE and PRESBURGER. Currently available exercises cover the material corresponding to sections 2.1-2.3 of the textbook by H. Enderton and to a certain degree the Chapter 1. The section 2.4 (Deductive Calculus) can be easily covered by existing software for natural deduction (Fitch or Epgy Proof Editor). Remaining section 2.5 (Soundness and Completeness Theorems) presents a challenge for next stages of the project. A part of the challenge is discovering new efficiently decidable classes of formulas.

Harvey Friedman (Ohio State University, Columbus)
Boolean Relation Theory

We discuss the state of the art in Boolean Relation Theory, and a draft manuscript concerning the following statement from BRT.

Let f,g be multivariate functions from N into N of expansive linear growth.
There exists infinite sets A,B,C contained in N such that
A U. fA contained in C U. gB
A U. fB contained in C U. gC.

It is necessary and sufficient to use Mahlo cardinals of finite order to prove the above statement.