Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas

Description

This unique textbook, in contrast to a standard logic text, provides the reader with a logic that 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. For this second edition, more than 400 additions, corrections, and improvements have been made, including a new chapter on inductive sets and types. 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 - Includes a module system for building libraries of mathematical knowledge - Employs two semantics, one for mathematics and one for logic - Emphasizes the model-theoretic view of predicate logic - Presents several important topics, such as definite description and theory morphisms, not usually found in standard logic textbooks Aimed at students of mathematics and computing at the graduate or upper-undergraduate level, this book is well suited for mathematicians, computing professionals, engineers, and scientists who need a practical logic for expressing and reasoning about mathematical ideas. Contents Preface List of Figures List of Tables List of Theorems, Examples, Remarks, and Modules About the Author Chapter 1 Introduction Summary of the Contents Chapter 2 Answers to Readers' Questions 2.1 Why Logic? 2.2 Why a Practical Logic? 2.3 Why Simple Type Theory? 2.4 Why not First-Order Logic? 2.5 Why not Set Theory? 2.6 Why not Dependent Type Theory? 2.7 Why Undefinedness? 2.8 Why Model Theory instead of Proof Theory? Chapter 3 Preliminary Concepts 3.1 What is Mathematics? 3.2 Mathematical Values 3.2.1 Sets 3.2.2 Sequences 3.2.3 Relations 3.2.4 Functions 3.2.5 Boolean Values and Predicates 3.3 Binders 3.4 Undefinedness 3.5 Mathematical Structures 3.6 Examples of Mathematical Structures 3.7 Conclusions 3.8 Exercises Chapter 4 Syntax 4.1 Notation 4.2 Symbols 4.3 Types 4.4 Expressions 4.5 Bound and Free Variables 4.6 Substitution 4.7 Languages 4.8 Conclusions 4.9 Exercises Chapter 5 Semantics 5.1 Interpretations 5.2 General Models 5.3 Finite General Models 5.4 Standard Models 5.5 Satisfiability, Validity, and Semantic Consequence 5.6 Isomorphic General Models 5.7 Expansion of a General Model 5.8 Standard vs. General Semantics 5.9 Examples of Standard Models 5.10 Conclusions 5.11 Exercises Chapter 6 Additional Notation 6.1 Boolean Operators 6.2 Binary Operators 6.3 Quantifiers 6.4 Definedness 6.5 Sets 6.6 Tuples 6.7 Functions 6.8 Miscellaneous Notation 6.9 Quasitypes and Dependent Quasitypes 6.10 Conclusions 6.11 Exercises Chapter 7 Beta-Reduction and Substitution 7.1 Beta-Reduction 7.2 Universal Instantiation 7.3 Invalid Beta-Reduction 7.4 Alpha-Conversion 7.5 Conclusions 7.6 Exercises Chapter 8 Proof Systems 8.1 Background 8.2 A Proof System for Alonzo 8.2.1 Axioms 8.2.2 Rules of Inference 8.2.3 Proofs 8.3 Soundness 8.4 Frugal General Models 8.5 Completeness 8.6 Conclusions 8.7 Exercises Chapter 9 Theories 9.1 Axiomatic Theories 9.2 Theory Extensions 9.3 Conservative Theory Extensions 9.4 Categorical Theories 9.5 Complete Theories 9.6 Fundamental Form of a Mathematical Problem 9.7 Model Theory 9.8 Conclusions 9.9 Exercises Chapter 10 Inductive Sets and Types 10.1 Inductive Sets 10.2 Inductive Types 10.3 Inductive Type Theory Extensions 10.4 Conclusions 10.5 Exercises Chapter 11 Sequences 11.1 Systems of Natural Numbers 11.2 Notation for Sequences 11.3 Conclusions 11.4 Exercises Chapter 12 Developments 12.1 Theory Developments 12.2 Development of Natural Number Arithmetic 12.2.1 Some Basic Definitions and Theorems 12.2.2 Commutative Semiring 12.2.3 Weak Total Order 12.2.4 Divides Lattice 12.3 Conclusions 12.4 Exercises Chapter 13 Real Number Mathematics 13.1 Complete Ordered Fields 13.2 Alternatives to the Construction of COF 13.3 Development of Real Number Mathematics 13.3.1 Some Basic Definitions and Theorems 13.3.2 Naturals, Integers, and Rationals 13.3.3 Iterated Sum and Product Operators 13.3.4 Calculus 13.3.5 Euclidean Space 13.4 Skolem's Paradox 13.5 Conclusions 13.6 Exercises Chapter 14 Morphisms 14.1 A Motivating Example 14.2 The Little Theories Method 14.3 Theory Morphisms 14.3.1 Theory Translations 14.3.2 Morphism Theorem 14.3.3 Examples of Theory Morphisms 14.3.4 Translation Presentation Convention 14.3.5 Faithful Theory Morphisms 14.4 Development Morphisms 14.4.1 Development Translations 14.4.2 Transportations 14.4.3 Inclusion Transportation Convention 14.5 Mathematics Libraries 14.5.1 Theory Graphs 14.5.2 Development Graphs 14.5.3 Realm Graphs 14.6 Theory Graph Combinators 14.7 Conclusions 14.8 Exercises Chapter 15 Alonzo Variants 15.1 Alonzo with Indefinite Description 15.1.1 Introduction 15.1.2 Syntax 15.1.3 Semantics 15.1.4 Proof System 15.1.5 Theorems 15.2 Alonzo with Sorts 15.2.1 Introduction 15.2.2 Syntax 15.2.3 Semantics 15.2.4 Proof System 15.2.5 Theorems 15.3 Alonzo with Quotation and Evaluation 15.3.1 Introduction 15.3.2 Syntax 15.3.3 Semantics 15.3.4 Proof System 15.3.5 Theorems 15.4 Conclusions Chapter 16 Software Support 16.1 Basis Support 16.2 Advanced Support 16.2.1 Organization 16.2.2 Inference 16.2.3 Computation 16.2.4 Concretization 16.2.5 Narration 16.3 Fully Integrated Support 16.4 Conclusions Appendix A Metatheorems of A A.1 Universal Instantiation A.2 Alpha-Conversion A.3 Substitution Rule A.4 Tautology Theorems A.5 Deduction Theorem A.6 Miscellaneous Metatheorems Appendix B Soundness of A Appendix C Henkin's Theorem for A Bibliography Index