Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
It is often stated in the CS folklore that Turing was inspired by Gödel's incompleteness theorem, more specifically the diagonalization proof and the isomorphism between axiomatically generated statements (Gödel numberings).
Are there other such links between model theory and computer science? Should a computer scientist be interested in model theory?
A special case of model theory is finite model theory which is closely related to complexity theory and database theory. However the methods being used in classical model theory (e.g. types, stability theory, forcing, large cardinals etc) are geared towards infinite models and assume compactness. Hence they don't appear to be useful in computer science.
A second connection that is not well-known is with program verification and program logics. Model theoretic techniques like quantifier elimination and skolemisation come from model theory, but are now at heart of verification tools. Questions of importance in program logics like Hennessy-Milner theorems are in the language of model theory simply model-theoretic characterisations of the elementary equivalence (a model theoretic concept) on models of the logic. In many logics coming from program verification, the elementary equivalence is some variant of bisimulation, a concept invented independently in computer science. More examples along those lines could be given.
In summary, there is a lot of overlap, but the communities have been developing separately, use different terminology and have different focus (model theory: infinite, CS: finite and efficient), so currently both communities don't have much to say to each other.
