Logic and Proof

• 1. Introduction
  • 1.1. Mathematical Proof
  • 1.2. Symbolic Logic
  • 1.3. Interactive Theorem Proving
  • 1.4. The Semantic Point of View
  • 1.5. Goals Summarized
  • 1.6. About this Textbook
• 2. Propositional Logic
  • 2.1. A Puzzle
  • 2.2. A Solution
  • 2.3. Rules of Inference
  • 2.4. The Language of Propositional Logic
  • 2.5. Exercises
• 3. Natural Deduction for Propositional Logic
  • 3.1. Derivations in Natural Deduction
  • 3.2. Examples
  • 3.3. Forward and Backward Reasoning
  • 3.4. Reasoning by Cases
  • 3.5. Some Logical Identities
  • 3.6. Exercises
• 4. Propositional Logic in Lean
  • 4.1. Expressions for Propositions and Proofs
  • 4.2. More commands
  • 4.3. Building Natural Deduction Proofs
  • 4.4. Tactic Mode
  • 4.5. Forward Reasoning
  • 4.6. Definitions and Theorems
  • 4.7. Additional Syntax
  • 4.8. Exercises
• 5. Classical Reasoning
  • 5.1. Proof by Contradiction
  • 5.2. Some Classical Principles
  • 5.3. The contradiction Tactic
  • 5.4. Exercises
• 6. Semantics of Propositional Logic
  • 6.1. Truth Values and Assignments
  • 6.2. Truth Tables
  • 6.3. Soundness and Completeness
  • 6.4. Exercises
• 7. First Order Logic
  • 7.1. Functions, Predicates, and Relations
  • 7.2. The Universal Quantifier
  • 7.3. The Existential Quantifier
  • 7.4. Relativization and Sorts
  • 7.5. Equality
  • 7.6. Exercises
• 8. Natural Deduction for First Order Logic
  • 8.1. Rules of Inference
  • 8.2. The Universal Quantifier
  • 8.3. The Existential Quantifier
  • 8.4. Equality
  • 8.5. Counterexamples and Relativized Quantifiers
  • 8.6. Exercises
• 9. First Order Logic in Lean
  • 9.1. Functions, Predicates, and Relations
  • 9.2. Using the Universal Quantifier
  • 9.3. Using the Existential Quantifier
  • 9.4. Equality
  • 9.5. Tactic Mode
  • 9.6. Calculational Proofs
  • 9.7. Exercises
• 10. Semantics of First Order Logic
  • 10.1. Interpretations
  • 10.2. Truth in a Model
  • 10.3. Examples
  • 10.4. Validity and Logical Consequence
  • 10.5. Soundness and Completeness
  • 10.6. Exercises
• 11. Sets
  • 11.1. Elementary Set Theory
  • 11.2. Calculations with Sets
  • 11.3. Indexed Families of Sets
  • 11.4. Cartesian Product and Power Set
  • 11.5. Exercises
• 12. Sets in Lean
  • 12.1. Basics
  • 12.2. Some Identities
  • 12.3. Indexed Families
  • 12.4. Power Sets
  • 12.5. Exercises
• 13. Relations
  • 13.1. Order Relations
  • 13.2. More on Orderings
  • 13.3. Equivalence Relations and Equality
  • 13.4. Exercises
• 14. Relations in Lean
  • 14.1. Order Relations
  • 14.2. Orderings on Numbers
  • 14.3. Equivalence Relations
  • 14.4. Exercises
• 15. Functions
  • 15.1. The Function Concept
  • 15.2. Injective, Surjective, and Bijective Functions
  • 15.3. Functions and Subsets of the Domain
  • 15.4. Functions and Relations
  • 15.5. Exercises
• 16. Functions in Lean
  • 16.1. Functions and Symbolic Logic
  • 16.2. Second- and Higher-Order Logic
  • 16.3. Functions in Lean
  • 16.4. Defining the Inverse Classically
  • 16.5. Functions and Sets in Lean
  • 16.6. Exercises
• 17. The Natural Numbers and Induction
  • 17.1. The Principle of Induction
  • 17.2. Variants of Induction
  • 17.3. Recursive Definitions
  • 17.4. Defining Arithmetic Operations
  • 17.5. Arithmetic on the Natural Numbers
  • 17.6. The Integers
  • 17.7. Exercises
• 18. The Natural Numbers and Induction in Lean
  • 18.1. Induction and Recursion in Lean
  • 18.2. Defining the Arithmetic Operations in Lean
  • 18.3. Exercises
• 19. Elementary Number Theory
  • 19.1. The Quotient-Remainder Theorem
  • 19.2. Divisibility
  • 19.3. Prime Numbers
  • 19.4. Modular Arithmetic
  • 19.5. Properties of Squares
  • 19.6. Exercises
• 20. Combinatorics
  • 20.1. Finite Sets and Cardinality
  • 20.2. Counting Principles
  • 20.3. Ordered Selections
  • 20.4. Combinations and Binomial Coefficients
  • 20.5. The Inclusion-Exclusion Principle
  • 20.6. Exercises
• 21. The Real Numbers
  • 21.1. The Number Systems
  • 21.2. Quotient Constructions
  • 21.3. Constructing the Real Numbers
  • 21.4. The Completeness of the Real Numbers
  • 21.5. An Alternative Construction
  • 21.6. Exercises
• 22. The Infinite
  • 22.1. Equinumerosity
  • 22.2. Countably Infinite Sets
  • 22.3. Cantor’s Theorem
  • 22.4. An Alternative Definition of Finiteness
  • 22.5. The Cantor-Bernstein Theorem
  • 22.6. Exercises
• 23. Axiomatic Foundations
  • 23.1. Basic Axioms for Sets
  • 23.2. The Axiom of Infinity
  • 23.3. The Remaining Axioms
  • 23.4. Type Theory
  • 23.5. Exercises
• 24. Appendix: Natural Deduction Rules