Abstrakt
The theory of definability, initiated formally by Alfred Tarski
but incorporating earlier informal work in analysis, general
topology, and other fields, is an attractive, important, and in some
respects central branch of logic. It cuts across most of the
standard divisions of research in logic such as set theory, recursion
theory, and model theory, even makes some contact with proof theory,
and increasingly becomes involved with theoretical computer science.
It provides a convenient framework for the (horizontal) unification
of the theories of definability for seemingly unrelated areas and for
the (vertical) integration of the theories of definability for
first-order and higher-order languages.
Here we highlight some of the important
landmarks from past
research with an emphasis on looking at the similarities and
differences of the methods used in the several areas, with special
attention focused on proofs of undefinability and inseparability.
We
take a look at some current examples from finite-universe logic as
an
illustration of the critical problem of how to "finitize" results
from the classical to the finite-universe setting and of the role of
finite combinatorics in making this transition.