塔斯基对计算机科学的影响 [pdf]
本文探讨了阿尔弗雷德·塔斯基（Alfred Tarski）在逻辑学和元数学方面的开创性工作对计算机科学发展的深远影响。塔斯基的模型论、可定义性理论以及尤其是他对真理的形式化定义，为数据库理论、编程语言语义学、可计算性理论和形式化验证等计算机科学核心领域奠定了理论基础。文章详细梳理了塔斯基的思想如何通过多位学者间接塑造了现代计算机科学的关键分支。
背景速读
- 阿尔弗雷德·塔斯基（Alfred Tarski, 1901–1983）是波兰裔逻辑学家和数学家，20世纪最伟大的逻辑学家之一。他与哥德尔、丘奇等人共同奠定了现代数理逻辑的基础。
- 塔斯基在1930年代提出的"真理的语义学定义"（即"塔斯基T-模式"）以及"模型论"的基本框架，后来成为计算机科学中形式语义学、程序验证和数据库理论的逻辑基石。
- 这篇论文由著名逻辑学家所罗门·费弗曼（Solomon Feferman）撰写，梳理了塔斯基的工作如何直接影响了计算机科学的多个子领域——特别是自动定理证明、类型论、关系数据库的数学基础、以及程序语言的指称语义学。
- 对于技术读者来说，塔斯基的"不可定义性定理"（truth undefinability theorem）也深刻影响了计算理论中对可判定性与完备性的理解，是理解哥德尔不完备定理与计算极限之间关系的关键节点。
- 这篇文章合著者的背景——费弗曼曾是塔斯基的学生，也是《哥德尔全集》的主编，这使得他对这段思想传承有第一手的权威视角。