Suppose we start with a sequential 'base theory' B formulated in a language L (such as B = Peano arithmetic, or B = Zermelo-Fraenkel theory), and we extend B to a new theory B+ consisting of B plus T, where T stipulates that S "resembles" a Tarskian satisfaction predicate. Here T is formulated in the language L+ consisting of L plus an extra binary relation symbol S. For example, T might only express "S is a full satisfaction class" (note that in this case B+ does not include the scheme of induction for
formulae of the extended language L+).
I will give an overview of the status of our current knowledge of the relationship between B and B+ in connection with the following four questions (for various canonical choices of B and T):
1. Is B+ semantically conservative over B? In other words, does every model of B expand to a model of B+?
2. Is B+ syntactically conservative over B? In other words, if some L-sentence is provable from B+, then is it also provable from B?
3. Is B+ interpretable in B?
4. What type of speed-up (if any) does B+ have over B?
This talk reports on joint work with Albert Visser.