In his 1958 paper, ``Mathematical Significance of Consistency Proofs", G. Kreisel suggested the following research program: ``To determine the constructive (recursive) content or the constructive equivalent of the non-constructive concepts and theorems used in mathematics, particularly arithmetic and analysis." Following this program, Kreisel asked whether model-theoretic independence proofs for arithmetic could be made constructive by using recursive models of arithmetic. In 1959, S. Tennenbaum gave a negative answer for first-order Peano Arithmetic (PA), by showing that no nonstandard model of PA is recursive. This result suggested a battery of other questions about the Turing complexity of models and complete extensions of PA. One line of questioning was continued by C. Jockusch, who asked for a characterization of the degrees of models of True Arithmetic (the theory of the standard model of PA), and of other specific complete extensions of PA. R. Solovay answered both of Jockusch's questions, in theorems made widely known by J. Knight. Knight later asked whether Solovay's theorems could be simplified in one of three natural ways. We discuss why all three of Knight's questions have negative answers. Our discussion rests on some independence results that are interesting and useful in other contexts.
At the beginning we discuss organizational questions. The theme for this quarter and possibly next is decidable theories. We'll begin with a review of papers on decidability by automata methods for some theories formulated in weak second order logic. There will be occasional special presentations on other topics by visitors.
The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures over integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these ``little engines of proof'' and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modern reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.
I will present the theory of continuous pair-colorings on Polish spaces and its relation to the problem of covering the plane by graphs and inverses of graphs of Lipschitz-continuous functions. I will present in detail the classification of such coloring, ans show that there exists a minimal coloring, whose homogeneity number is equal to the number of Lipschitz continuous functions from the Cantor set to itself necessary to covery the square of the Cantor set; and there exists a maximal coloring, whose homogeneity number is consistently larger than that of the minimal one.
Among the consistency results I will survey is the following one: there is a model of set theory in which the Euclidean plane can be covered by $\aleph_1$ graphs and inverses of graphs of continuous real function, but cannot be covered by any $\aleph_1$ graphs and inverses of graphs of Lipschitz-continuous real functions.
These results were obtained with Stefan Geschke and Martin Goldstern.
In the automata-theoretic approach for solving the satisfiability problem of a logic one develops an appropriate notion of automata and establishes a translation from formulas to automata. The satisfiability problem for the logic reduces to the automata emptiness problem. Most prominently, decidability of the (weak) monadic second-order logic of one successor (W)S1S is proved by a translation of formulas to word automata and decidability of the (weak) monadic second-order logic on binary trees (W)S2S can be shown by a translation to tree automata. Despite the non-elementary worst-case complexity, these automata-based decision procedures for WS1S and WS2S have recently been found to be effective for reasoning about a wide variety of computation systems.
We briefly review the basic concepts of the classical connection between finite automata and WS1S, and demonstrate the resulting decision procedure using the Mona tool (developed at BRICS, Denmark) and its integration into the PVS theorem proving system. Furthermore, we study extensions of weak monadic second-order logics on words and trees with linear cardinality constraints of the form |X_1|+...+|X_r| < |Y_1|+...+|Y_s|, where the X_i and Y_j are monadic second-order (MSO) variables. Although these logics are undecidable in general, we identify decidable fragments.
Presburger arithmetic is an important theory for practical formal verification of programs. Their are two important classes of decision procedures (DP) for Presburger arithmetic, namely the automata based and the ILP (integer linear programming) based methods. Buchi was the first to propose an automata based DP which uses translation of Presburger arithmetic into WS1S and subsequently uses an automata based DP for WS1S. A more efficient method was later proposed by Hubert Comon, and Wolper et al. This part of the talk will focus on the current state of the art in automata based DPs for Presburger arithmetic.
The feasibility part of the ILP problem is precisely the satisfiability problem for a conjunction of Quantifier-free Presburger formulas. Considerable amount of research has been done in the last few decades on the ILP problem. Solvers for ILP extended to handle quantifiers and boolean combination of presburger formulas can act as a DP for Presburger arithmetic. There are many methods to solve the ILP problem, namely the Omega test, simplex with branch and bound etc. This part of the talk will focus on the Omega test which is a complete method as opposed to simplex with branch and bound. Some comparisons between the automata methods and ILP methods will be provided followed by a brief discussion on how to write practical decision procedures.