这是一本结合逻辑在计算机科学中的应用来介绍数理逻辑的教科书，书中强调了演绎作为计算的一种形式的概念。虽然本书覆盖了所有传统的逻辑主题(语法、语义、完备性和紧致性)，但是书中大部分讨论的是其他主题，诸如消解定理证明、逻辑式程序设计和非经典逻辑(模态逻辑和直觉主义逻辑)，而这些主题在现代计算机科学中变得越来越重要。另外，本书还系统介绍了集合论基础知识，并对该主题提供了历史综述。

本书不要求读者具备逻辑基础知识，适合计算机科学和数学系高年级本科生以及低年级研究生使用。

This book is a rigorous elementary introduction to classical predicate logic emphasizing that deduction is a form of computation. We cover the standard topics of soundness, completeness and compactness: our proof methods produce only valid results, all valid sentences are provable and, if a fact is a logical consequence of an infinite set of axioms, it is actually a consequence of finitely many of them. The need for soundness seems obvious but, as we see in our discussion Of PROLOG, even this requirement of simple correctness is often sacrificed on the altar of efficiency in actual implementations. Completeness, on the other hand, is a remarkable result connecting proofs and validity. We can prescribe an effective proof procedure that precisely captures the semantics of first order logic. A valid sentence, i.e., one true for every interpretation of the relations used to state it, always has a proof in a particular formal system and there is an algorithm to find such a proof. Compactness also has surprising applications that deduce results about infinite structures from results about finite ones. To cite just one example, it implies that every planar map is colorable with four colors as every finite planar map is so colorable. We also prove that validity is undecidable: no single algorithm can decide if any given sentence is valid. Thus, although we can, using a particular algorithm, search for a proof of a given sentence φ and be assured of finding one if φ is valid, we cannot know in general whether we are searching in vain.

Preface

Introduction

I Propositional Logic

1  Orders and Trees

2  Propositions, Connectives and Truth Tables

3  Truth Assignments and Valuations

4  Tableau Proofs in Propositional Calculus

5  Soundness and Completeness of Tableau Proofs

6  Deductions from Premises and Compactness

7  An Axiomatic Approach*

8  Resolution

9  Refining Resolution

10 Linear Resolution, Horn Clauses and PROLOG

II Predicate Logic

1  Predicates and Quantifiers

2  The Language: Terms and Formulas

3  Formation Trees, Structures and Lists

4  Semantics: Meaning and Truth

5  Interpretations of PROLOG Programs

6  Proofs: Complete Systematic Tableaux

7  Soundness and Completeness of Tableau Proofs

8  An Axiomatic Approach*

9  Prenex Normal Form and Skolemization

10 Herbrand's Theorem

11 Unification

12 The Unification Algorithm

13 Resolution

14 Refining Resolution: Linear Resolution

III PROLOG

1  SLD-Resolution

2  Implementations: Searching and Backtracking

3  Controlling the implementation: Cut

4  Termination Conditions for PROLOG Programs 

5  Equality 

6  Negation as Failure

7  Negation and Nonmonotonic Logic

8  Computability and Undecldability

IV Modal Logic

1  POssibility and Necessity; Knowledge or Belief

2  Frames and Forcing 

3  Modal Tableaux 

4  Soundness and Completeness

5  Modal Axioms and Special Accessibility Relations 

6  An Axiomatic Approach*

V Intultionistlc Logic

1  Intuitionism and Constructivism

2  Frames and Forcing

3  Intuitionistic Tableaux

4  Soundness and Completeness

5  Decidability and Undecidability

6  A Comparative Guide

VI Elements of Set Theory

1  Some Basic Axioms of Set Theory

2  Boole's Algebra of Sets

3  Relations, Functions and the Power Set Axiom

4  The Natural Numbers, Arithmetic and Infinity

5  Replacement, Choice and Foundation

6  Zermelo-Fraenkel Set Theory in Predicate Logic

7  Cardinality: Finite and Countable

8  Ordinal Numbers

9  Ordinal Arithmetic and Transfinite Induction

10 Transfinite Recursion, Choice and the Ranked Universe 

11 Cardinals and Cardinal Arithmetic

Appendix A: An Historical Overview

1  Calculus

2  Logic

3  Leibniz's Dream

4  Nineteenth Century Logic

5  Nineteenth Century Foundations of Mathematics

6  Twentieth Century Foundations of Mathematics

?  Early Twentieth Century Logic

8  Deduction and Computation

9  Recent Automation of Logic and PROLOG

10 The Future

Appendix B：A Genealogical Database

Bibliography

Index of Symbols

Index of Terms