Logic and Proof - Lean

Logic and Proof

Release 3.18.4 Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn

Dec 04, 2021

CONTENTS

1 Introduction

1

1.1 Mathematical Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.2 Symbolic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.3 Interactive Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

1.4 The Semantic Point of View . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.5 Goals Summarized . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

1.6 About this Textbook . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 Propositional Logic

7

2.1 A Puzzle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.2 A Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.3 Rules of Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2.4 The Language of Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

2.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3 Natural Deduction for Propositional Logic

17

3.1 Derivations in Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3.3 Forward and Backward Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

3.4 Reasoning by Cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

3.5 Some Logical Identities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

3.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

4 Propositional Logic in Lean

25

4.1 Expressions for Propositions and Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

4.2 More commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

4.3 Building Natural Deduction Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

4.4 Forward Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

4.5 Definitions and Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

4.6 Additional Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

4.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

5 Classical Reasoning

41

5.1 Proof by Contradiction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

5.2 Some Classical Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

5.3 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

6 Semantics of Propositional Logic

47

6.1 Truth Values and Assignments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

6.2 Truth Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

6.3 Soundness and Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

i

6.4 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

7 First Order Logic

55

7.1 Functions, Predicates, and Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

7.2 The Universal Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

7.3 The Existential Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

7.4 Relativization and Sorts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60

7.5 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

7.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

8 Natural Deduction for First Order Logic

65

8.1 Rules of Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

8.2 The Universal Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

8.3 The Existential Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

8.4 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

8.5 Counterexamples and Relativized Quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69

8.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

9 First Order Logic in Lean

73

9.1 Functions, Predicates, and Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

9.2 Using the Universal Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

9.3 Using the Existential Quantifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

9.4 Equality and calculational proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

9.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

10 Semantics of First Order Logic

89

10.1 Interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

10.2 Truth in a Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

10.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

10.4 Validity and Logical Consequence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

10.5 Soundness and Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

10.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

11 Sets

97

11.1 Elementary Set Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

11.2 Calculations with Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

11.3 Indexed Families of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

11.4 Cartesian Product and Power Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105

11.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

12 Sets in Lean

109

12.1 Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109

12.2 Some Identities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113

12.3 Indexed Families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114

12.4 Power Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118

12.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118

13 Relations

121

13.1 Order Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121

13.2 More on Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123

13.3 Equivalence Relations and Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124

13.4 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125

14 Relations in Lean

127

14.1 Order Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127

ii

14.2 Orderings on Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 14.3 Equivalence Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131 14.4 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133

15 Functions

135

15.1 The Function Concept . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135

15.2 Injective, Surjective, and Bijective Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137

15.3 Functions and Subsets of the Domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139

15.4 Functions and Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140

15.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141

16 Functions in Lean

143

16.1 Functions and Symbolic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143

16.2 Second- and Higher-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144

16.3 Functions in Lean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145

16.4 Defining the Inverse Classically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148

16.5 Functions and Sets in Lean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

16.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151

17 The Natural Numbers and Induction

155

17.1 The Principle of Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155

17.2 Variants of Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157

17.3 Recursive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160

17.4 Defining Arithmetic Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162

17.5 Arithmetic on the Natural Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164

17.6 The Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166

17.7 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167

18 The Natural Numbers and Induction in Lean

169

18.1 Induction and Recursion in Lean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169

18.2 Defining the Arithmetic Operations in Lean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172

18.3 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173

19 Elementary Number Theory

175

19.1 The Quotient-Remainder Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175

19.2 Divisibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176

19.3 Prime Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179

19.4 Modular Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180

19.5 Properties of Squares . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182

19.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183

20 Combinatorics

185

20.1 Finite Sets and Cardinality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185

20.2 Counting Principles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186

20.3 Ordered Selections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188

20.4 Combinations and Binomial Coefficients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189

20.5 The Inclusion-Exclusion Principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191

20.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192

21 The Real Numbers

195

21.1 The Number Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195

21.2 Quotient Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196

21.3 Constructing the Real Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198

21.4 The Completeness of the Real Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199

21.5 An Alternative Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200

iii

21.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

22 The Infinite

203

22.1 Equinumerosity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203

22.2 Countably Infinite Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204

22.3 Cantor's Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207

22.4 An Alternative Definition of Finiteness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208

22.5 The Cantor-Bernstein Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209

22.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209

23 Axiomatic Foundations

211

23.1 Basic Axioms for Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211

23.2 The Axiom of Infinity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213

23.3 The Remaining Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215

23.4 Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217

23.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219

24 Appendix: Natural Deduction Rules

221

iv

CHAPTER

ONE

INTRODUCTION

1.1 Mathematical Proof

Although there is written evidence of mathematical activity in Egypt as early as 3000 BC, many scholars locate the birth of mathematics proper in ancient Greece around the sixth century BC, when deductive proof was first introduced. Aristotle credited Thales of Miletus with recognizing the importance of not just what we know but how we know it, and finding grounds for knowledge in the deductive method. Around 300 BC, Euclid codified a deductive approach to geometry in his treatise, the Elements. Through the centuries, Euclid's axiomatic style was held as a paradigm of rigorous argumentation, not just in mathematics, but in philosophy and the sciences as well. Here is an example of an ordinary proof, in contemporary mathematical language. It establishes a fact that was known to the Pythagoreans.

Theorem. 2 is irrational, which is to say, it cannot be expressed as a fraction a/b, where a and b are integers.

Proof. Suppose 2 = a/b for some pair of integers a and b. By removing any common factors, we can assume a/b is in lowest terms, so that a and b have no factor in common. Then we have a = 2b, and squaring both sides, we have a2 = 2b2. The last equation implies that a2 is even, and since the square of an odd number is odd, a itself must be even as well. We therefore have a = 2c for some integer c. Substituting this into the equation a2 = 2b2, we have 4c2 = 2b2, and hence 2c2 = b2. This means that b2 is even, and so b is even as well. The fact that a and b are both even contradicts the fact that a and b have no common factor. So the original assumption that 2 = a/b is false.

In the next example, we focus on the natural numbers, N = {0, 1, 2, . . .}.

A natural number n greater than or equal to 2 is said to be composite if it can be written as a product n = m ? k where neither m nor k is equal to 1, and prime otherwise. Notice that if n = m ? k witnesses the fact that n is composite, then m and k are both smaller than n. Notice also that, by convention, 0 and 1 are considered neither prime nor composite.

Theorem. Every natural number greater than or equal to 2 can be written as a product of primes. Proof. We proceed by induction on n. Let n be any natural number greater than 2. If n is prime, we are done; we can consider n itself as a product with one term. Otherwise, n is composite, and we can write n = m ? k where m and k are

1

Logic and Proof, Release 3.18.4

smaller than n and greater than 1. By the inductive hypothesis, each of m and k can be written as a product of primes, say m = p1 ? p2 ? . . . ? pu and k = q1 ? q2 ? . . . ? qv. But then we have

n = m ? k = p1 ? p2 ? . . . ? pu ? q1 ? q2 ? . . . ? qv,

a product of primes, as required.

Later, we will see that more is true: every natural number greater than 2 can be written as a product of primes in a unique way, a fact known as the fundamental theorem of arithmetic. The first goal of this course is to teach you to write clear, readable mathematical proofs. We will do this by considering a number of examples, but also by taking a reflective point of view: we will carefully study the components of mathematical language and the structure of mathematical proofs, in order to gain a better understanding of how they work.

1.2 Symbolic Logic

Toward understanding how proofs work, it will be helpful to study a subject known as "symbolic logic," which provides an idealized model of mathematical language and proof. In the Prior Analytics, the ancient Greek philosopher set out to analyze patterns of reasoning, and developed the theory of the syllogism. Here is one instance of a syllogism:

Every man is an animal. Every animal is mortal. Therefore every man is mortal.

Aristotle observed that the correctness of this inference has nothing to do with the truth or falsity of the individual statements, but, rather, the general pattern:

Every A is B. Every B is C. Therefore every A is C.

We can substitute various properties for A, B, and C; try substituting the properties of being a fish, being a unicorn, being a swimming creature, being a mythical creature, etc. The various statements that result may come out true or false, but all the instantiations will have the following crucial feature: if the two hypotheses come out true, then the conclusion comes out true as well. We express this by saying that the inference is valid.

Although the patterns of language addressed by Aristotle's theory of reasoning are limited, we have him to thank for a crucial insight: we can classify valid patterns of inference by their logical form, while abstracting away specific content. It is this fundamental observation that underlies the entire field of symbolic logic.

In the seventeenth century, Leibniz proposed the design of a characteristica universalis, a universal symbolic language in which one would express any assertion in a precise way, and a calculus ratiocinatur, a "calculus of thought" which would express the precise rules of reasoning. Leibniz himself took some steps to develop such a language and calculus, but much greater strides were made in the nineteenth century, through the work of Boole, Frege, Peirce, Schroeder, and others. Early in the twentieth century, these efforts blossomed into the field of mathematical logic.

2

Chapter 1. Introduction

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download