Logic for Mathematics and Computer Science

Preface
Flow of Topics
PART I. QUANTIFIER-FREE LOGICS
Chapter 1 From Aristotle to Boole
1.1 Sophistry
1.2 The contributions of Aristotle
1.3The algebra of logic
1.4 The method of Boole, and Venn diagrams
 1.4.1 Checking for validity
 1.4.2 Finding the most general conclusion
1.5 Historical remarks
Chapter 2 Propositional Logic
2.1 Propositional connectives, propositional formulas, truth tables
 2.1.1 Defining propositional formulas
 2.1.2 Truth tables
 2.2.1 Equivalent formulas
 2.2.2 Tautologies
2.3 Substitution
2.4 Replacement
 2.4.1 Induction proofs on formulas
 2.4.2 Main result on replacement
 2.4.3 Simplification of formulas
 2.5.1 The standard connectives are adequate
2.6 Disjunctive and conjunctive forms
 2.6.1 Rewrite rules to obtain normal forms
 2.6.2 Using truth tables to find normal forms
 2.6.3 Uniqueness of normal forms
2.7 Valid arguments, tautologies, and satisfiability
2.8 Compactness
 2.8.1 The compactness theorem for propositional logic
 2.8.2 Applications of compactness
2.9 The propositional proof system PC
 2.9.1 Simple equivalences
 2.9.2 The proof system
 2.9.3 Soundness and completeness
 2.9.4 Derivations with premisses
 2.9.6 Generalized soundness and completeness
2.10 Resolution
 2.10.1 A motivation
 2.10.2 Clauses
 2.10.3 Resolution
 2.10.4 The Davis-Putnam procedure
 2.10.5 Soundness and completeness for the DPP
 2.10.6 Applications of the DPP
 2.10.7 Soundness and completeness for resolution
 2.10.8 Generalized soundness and completeness for resolution
2.11 Horn clauses
2.12 Graph clauses
2.13 Pigeonhole clauses
2.14 Historical remarks
 2.14.1 The beginnings
 2.14.2 Statement logic and the algebra of logic
 2.14.3 Frege's work ignored
 2.14.4 Bertrand Russell rescues Frege's logic
 2.14.5 The influence of Principia
 2.14.6 The emergence of truth tables, completeness
 2.14.7 The Hilbert school of logic
 2.14.8 The Polish school of logic
 2.14.9 Other propositional proof systems
 2.14.10 Problems with algorithms
 2.14.11 Reduction to propositional logic
 2.14.12 Testing for satisfiability
Chapter 3 Equational Logic
3.1 Interpretations and algebras
3.2 Terms
3.3 Term functions
 3.3.1 Evaluation tables
3.4 Equations
 3.4.1 The semantics of equations
 3.4.2 Classes of algebras defined by equations
 3.4.3 Three very basic properties of equations
3.5 Valid arguments
3.6 Substitution
3.7 Replacement
3.8 A proof system for equational logic
 3.8.1 Birkhoff's rules
 3.8.2 Is there a strategy to find equational derivations?
3.9 Soundness
3.10 Completeness
 3.10.1 The construction of Zn
 3.10.2 The proof of the completeness theorem
 3.10.3 Valid arguments revisited
3.11 Chain derivations
3.12 Unification
 3.12.1 Unifiers
 3.12.2 A unification algorithm
 3.12.3 Properties of prefix notation for terms
 3.12.4 Notation for substitutions
 3.12.5 Verification of the unification algorithm
 3.12.6 Unification of finitely many terms
3.13 Term rewrite systems (TRS's)
 3.13.1 Definition of a TRS
 3.13.2 Terminating TRS's
 3.13.3 Normal form TRS's
 3.13.4 Critical pairs
 3.13.5 Critical pairs lemma
 3.13.6 Terms as strings
 3.13.7 Confluence
3.14 Reduction orderings
 3.14.1 Definition of a reduction ordering
 3.14.2 The Knuth-Bendix orderings
 3.14.3 Polynomial orderings
3.15 The Knuth-Bendix procedure
 3.15.1 Finding a normal form TRS for groups
 3.15.2 A formalization of the Knuth-Bendix procedure
3.16 Historical remarks
Chapter 4 Predicate Clause Logic
4.1 First-order languages without equality
4.2 Interpretations and structures
4.3 Clauses
4.4 Semantics
4.5 Reduction to propositional logic via ground clauses, and the compactness theorem for clause logic
 4.5.1 Ground instances
 4.5.2 Satisfiable over an algebra
 4.5.3 The Herbrand universe
 4.5.4 Growth of the Herbrand universe
 4.5.5 Satisfiability over the Herbrand universe
 4.5.6 Compactness for predicate clause logic without equality
4.6 Resolution
 4.6.1 Substitution
 4.6.2 Opp-unification
 4.6.3 Resolution
 4.6.4 Soundness and completeness of resolution
4.7 The unification of literals
 4.7.1 Unifying pairs of literals
 4.7.2 The unification algorithm for pairs of literals
 4.7.3 Most general unifiers of finitely many literals
4.8 Resolution with most general opp-unifiers
 4.8.1 Most general opp-unifiers
 4.8.2 An Opp-unification algorithm
 4.8.3 Resolution and most general opp-unifiers
 4.8.4 Soundness and completeness with most general opp-unifiers
4.9 Adding equality to the language
4.10 Reduction to propositional logic
 4.10.1 Axiomatizing equality
 4.10.2 The reduction
 4.10.3 Compactness for clause logic with equality
 4.10.4 Soundness and completeness
4.11 Historical remarks
PART II. LOGIC WITH QUANTIFIERS
Chapter 5First-Order Logic: Introduction, and fundamental results on semantics
5.1The syntax of first-order logic
5.2First-order syntax for the natural numbers
5.3The semantics of first-order sentences in N
5.4Other number systems
5.5First-order syntax for (directed) graphs
5.6The semantics of first-order sentences in (directed) graphs
5.7Semantics for first-order logic
5.8Equivalent formulas
5.9Replacement and substitution
5.10Prenex form
5.11Valid arguments
5.12Skolemizing
5.13The reduction of first-order logic to predicate clause logic
5.14The compactness theorem
5.15Historical remarks
Chapter 6A Proof System for First-order Logic, and Gödel's Completeness Theorem
6.1A proof system
6.3Herbrand's Deduction Lemma
6.4Consistent sets of formulas
6.5Maximal consistent sets of formulas
6.6Adding witness formulas to a consistent sentence
6.7Constructing a model using a maximal consistent set of formulas with witness formulas
6.8Consistent sets of sentences are satisfiable
6.9Gödel's completeness theorem
6.10Compactness
6.11Historical remarks
Appendix AA Simple Timetable of Mathematical Logic and Computing
Appendix BDedekind-Peano number system
Appendix CWriting up an inductive definition or proof
 1. Inductive definitions
 2. Inductive proofs
Appendix DThe FL propositional logic
Bibliography
Index