6
$\begingroup$

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?

$\endgroup$
11
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.