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.
Author(s): William M. Farmer
Series: Computer Science Foundations and Applied Logic
Edition: 1
Publisher: Springer Nature Switzerland
Year: 2023
Language: English
Pages: 295
Tags: Type Theory, Higher-Order Logic
Contents
Preface
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 Unde nedness?
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 Sequences
10.1 Systems of Natural Numbers
10.2 Notation for Sequences
10.3 Conclusions
10.4 Exercises
Chapter 11 Developments
11.1 Theory Developments
11.2 Development of Natural Number Arithmetic
11.2.1 Basic Definitions and Theorems
11.2.2 Commutative Semiring
11.2.3 Weak Total Order
11.2.4 Divides Lattice
11.3 Conclusions
11.4 Exercises
Chapter 12 Real Number Mathematics
12.1 Complete Ordered Fields
12.2 Alternatives to the Construction of COF
12.3 Development of Real Number Mathematics
12.3.1 Some Basic Definitions and Theorems
12.3.2 Naturals, Integers, and Rationals
12.3.3 Iterated Sum and Product Operators
12.3.4 Calculus
12.3.5 Euclidean Space
12.4 Skolem's Paradox
12.5 Conclusions
12.6 Exercises
Chapter 13 Morphisms
13.1 A Motivating Example
13.2 The Little Theories Method
13.3 Theory Morphisms
13.3.1 Theory Translations
13.3.2 Morphism Theorem
13.3.3 Examples of Theory Morphisms
13.3.4 Faithful Theory Morphisms
13.4 Development Morphisms
13.4.1 Development Translations
13.4.2 Transportations
13.5 Mathematics Libraries
13.5.1 Theory Graphs
13.5.2 Development Graphs
13.5.3 Realm Graphs
13.6 Theory Graph Combinators
13.7 Conclusions
13.8 Exercises
Chapter 14 Alonzo Variants
14.1 Alonzo with Indefinite Description
14.1.1 Introduction
14.1.2 Syntax
14.1.3 Semantics
14.1.4 Proof System
14.1.5 Theorems
14.2 Alonzo with Sorts
14.2.1 Introduction
14.2.2 Syntax
14.2.3 Semantics
14.2.4 Proof System
14.2.5 Theorems
14.3 Alonzo with Quotation and Evaluation
14.3.1 Introduction
14.3.2 Syntax
14.3.3 Semantics
14.3.4 Proof System
14.3.5 Theorems
14.4 Conclusions
Chapter 15 Software Support
15.1 Basis Support
15.2 Advanced Support
15.2.1 Organization
15.2.2 Inference
15.2.3 Computation
15.2.4 Concretization
15.2.5 Narration
15.3 Fully Integrated Support
15.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
List of Figures
List of Tables
List of Theorems, Examples, Remarks, and Modules
Index
