Tarski's influence on computer science [pdf]

This paper examines Alfred Tarski's foundational contributions to computer science, particularly his work on model theory, decision procedures, and semantics, which influenced areas such as database theory, programming language semantics, and automated theorem proving.

Background

Alfred Tarski (1901–1983) was a Polish logician and mathematician whose work on the concepts of truth, logical consequence, and formal semantics laid the theoretical foundation for much of modern computer science. This paper, authored by the late Stanford logician Solomon Feferman, traces how Tarski's ideas directly shaped the development of programming languages, database theory, type systems, formal verification, and the semantics of computation. Key Tarskian concepts that became CS tools include: the distinction between object language and metalanguage, the definition of satisfaction and truth in formal structures (model theory), the fixed-point theorem for defining recursive functions, and the theory of relation algebras (which underpins relational databases). The paper is aimed at a mathematically literate audience but is historically important for anyone wanting to understand why logic is not just an abstract branch of philosophy but the actual backbone of computing.