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.
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.
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.
This is a concluding talk by Jesse Alama and Patrick Girard (Stanford) on decision methods for arithmetical universal-existential sentences.
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.
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.
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.