Time:  12  1:20 p.m. 

Room: 
OSC 201


Speaker:  Yimu Yin Department of Philosophy Carnegie Mellon University 

Title:  Quantifier elimination and real closed fields with a monadic predicate 

Abstract:  We review the model theory of quantifier elimination (QE). In particular I shall prove that, for countable theories, the Strong Shoenfield QEtest is equivalent to the van den Dries QEtest. Using this latter test van den Dries showed that the theory of the reals with a predicate for the powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a modeltheoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not elementary. In particular, we show that it is possible to eliminate a single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is the length of the input formula and $2_k^x$ denotes $k$fold iterated exponentiation. Some immediate consequences on decidable recurrent relations will also be discussed, if time permits. 