Simple Type Theory: A Practical Logic for Expressing and Reasoning about Mathematical Ideas

This unique textbook, in contrast to a standard logic text, provides the reader with a logic that actually can be used in practice to express and reason about mathematical ideas.

The book is an introduction to simple type theory, a classical higher-order version of predicate logic that extends first-order logic. It presents a practice-oriented logic called Alonzo that is based on Alonzo Church's formulation of simple type theory known as Church's type theory. Unlike traditional predicate logics, Alonzo admits undefined expressions. The book illustrates, using Alonzo, how simple type theory is suited ideally for reasoning about mathematical structures and constructing libraries of mathematical knowledge.

Topics and features:

• Offers the first book-length introduction to simple type theory as a predicate logic
• Provides the reader with a logic that is close to mathematical practice
• Presents the tools needed to build libraries of mathematical knowledge
• Employs two semantics, one for mathematics and one for logic
• Emphasizes the model-theoretic view of predicate logic
• Includes several important topics, such as definite description and theory morphisms, not usually found in standard logic textbooks

Aimed at students of computing and mathematics at the graduate or upper-undergraduate level, this book is also well-suited for mathematicians, computing professionals, engineers, and scientists who need a practical logic for expressing and reasoning about mathematical ideas.

William M. Farmer is a Professor in the Department of Computing and Software at McMaster University in Hamilton, Ontario, Canada.

這本獨特的教科書與一般的邏輯教材不同，它提供讀者一種實際上可以用來表達和推理數學思想的邏輯。

這本書是對簡單型理論的介紹，它是一種古典的高階述詞邏輯，擴展了一階邏輯。它介紹了一種實用導向的邏輯，稱為Alonzo，它基於Alonzo Church對簡單型理論的形式化，也被稱為Church的型理論。與傳統的述詞邏輯不同，Alonzo允許未定義的表達式。本書使用Alonzo來說明簡單型理論如何適合於推理數學結構和構建數學知識庫。

主題和特點：

• 首次提供了簡單型理論作為述詞邏輯的介紹


• 為讀者提供了一種貼近數學實踐的邏輯


• 提供構建數學知識庫所需的工具


• 使用兩種語義，一種用於數學，一種用於邏輯


• 強調模型論觀點的述詞邏輯


• 包含一些重要的主題，如確定描述和理論映射，通常在標準邏輯教材中找不到

本書適用於研究生或高年級本科生的計算機和數學學生，同時也適合需要一種實用邏輯來表達和推理數學思想的數學家、計算機專業人員、工程師和科學家。

William M. Farmer是加拿大安大略省漢密爾頓麥克馬斯特大學計算機與軟件系的教授。

William M. Farmer has over 35 years of experience working in industry and academia in computing and mathematics. He received a B.A. in mathematics from the University of Notre Dame in 1978 and an M.A. in mathematics in 1980, an M.S. in computer sciences in 1983, and a Ph.D. in mathematics in 1984 from the University of Wisconsin-Madison. He is currently a Professor in the Department of Computing and Software at McMaster University. Before joining McMaster in 1999, he conducted research in computer science for twelve years at The MITRE Corporation in Bedford, Massachusetts, USA and taught computer programming and networking courses for two years at St. Cloud State University.
Dr. Farmer's research interests are logic, mechanized mathematics, mathematical knowledge management, and formal methods. One of his most significant achievements is the design and implementation of the IMPS proof assistant, which was done at MITRE in partnership with Dr. Joshua Guttman and Dr. Javier Thayer. His work on IMPS has lead to research on developing practice-oriented logics and set theories and on organizing mathematical knowledge as a network of interconnected axiomatic theories. He and Dr. Jacques Carette are currently leading the MathScheme project at McMaster with the aim of developing a framework for integrating axiomatic and algorithmic mathematics. On this project Dr. Farmer has focused on how to reason about the interplay of syntax and semantics, as exhibited in syntax-based mathematical algorithms like symbolic differentiation, within a logic equipped with global quotation and evaluation operators. Dr. Farmer has had a career-long interest in using simple type theory as a practical logic for expressing and reasoning about mathematical ideas. He is the author of "The Seven Virtues of Simple Type Theory", Journal of Applied Logic, 6:267-286, 2008, one of the leading references on simple type theory.

William M. Farmer在計算機和數學領域擁有超過35年的工業和學術經驗。他於1978年獲得聖母大學的數學學士學位，並於1980年獲得數學碩士學位，於1983年獲得計算機科學碩士學位，並於1984年獲得數學博士學位，這些學位都是在威斯康辛大學麥迪遜分校取得的。他目前是麥克馬斯特大學計算機和軟件系的教授。在1999年加入麥克馬斯特之前，他在美國麻薩諸塞州貝德福德的MITRE公司從事計算機科學研究長達十二年，並在聖克勞德州立大學教授計算機編程和網絡課程兩年。

Farmer博士的研究興趣包括邏輯、機械化數學、數學知識管理和形式方法。他最重要的成就之一是與Joshua Guttman博士和Javier Thayer博士合作，在MITRE公司設計和實施了IMPS證明助手。他在IMPS上的工作引發了對發展面向實踐的邏輯和集合論以及將數學知識組織為相互連接的公理理論網絡的研究。他和Jacques Carette博士目前在麥克馬斯特大學領導MathScheme項目，旨在開發一個整合公理和算法數學的框架。在這個項目中，Farmer博士專注於如何在具有全局引用和評估運算符的邏輯中推理語法和語義的相互作用，例如在基於語法的數學算法（如符號微分）中。Farmer博士一直對使用簡單類型理論作為表達和推理數學思想的實用邏輯感興趣。他是《簡單類型理論的七個優點》（The Seven Virtues of Simple Type Theory）一文的作者，該文發表於2008年的《應用邏輯學》（Journal of Applied Logic），是簡單類型理論的主要參考文獻之一。