THE OPEN LOGIC TEXT

THE OPEN LOGIC TEXT

Complete Build Open Logic Project

Revision: d4e99d0 (master) 2023-10-08

The Open Logic Text by the Open Logic Project is licensed under a Creative Commons Attribution 4.0 International License.

About the Open Logic Project

The Open Logic Text is an open-source, collaborative textbook of formal metalogic and formal methods, starting at an intermediate level (i.e., after an introductory formal logic course). Though aimed at a non-mathematical audience (in particular, students of philosophy and computer science), it is rigorous.

Coverage of some topics currently included may not yet be complete, and many sections still require substantial revision. We plan to expand the text to cover more topics in the future. We also plan to add features to the text, such as a glossary, a list of further reading, historical notes, pictures, better explanations, sections explaining the relevance of results to philosophy, computer science, and mathematics, and more problems and examples. If you find an error, or have a suggestion, please let the project team know.

The project operates in the spirit of open source. Not only is the text freely available, we provide the LaTeX source under the Creative Commons Attribution license, which gives anyone the right to download, use, modify, rearrange, convert, and re-distribute our work, as long as they give appropriate credit. Please see the Open Logic Project website at for additional information.

1

Contents

About the Open Logic Project

1

I Na?ive Set Theory

23

1 Sets

25

1.1 Extensionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

1.2 Subsets and Power Sets . . . . . . . . . . . . . . . . . . . . . . . 26

1.3 Some Important Sets . . . . . . . . . . . . . . . . . . . . . . . . . 28

1.4 Unions and Intersections . . . . . . . . . . . . . . . . . . . . . . 28

1.5 Pairs, Tuples, Cartesian Products . . . . . . . . . . . . . . . . . . 31

1.6 Russell's Paradox . . . . . . . . . . . . . . . . . . . . . . . . . . 33

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

2 Relations

35

2.1 Relations as Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

2.2 Philosophical Reflections . . . . . . . . . . . . . . . . . . . . . . 37

2.3 Special Properties of Relations . . . . . . . . . . . . . . . . . . . 38

2.4 Equivalence Relations . . . . . . . . . . . . . . . . . . . . . . . . 39

2.5 Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

2.6 Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

2.7 Operations on Relations . . . . . . . . . . . . . . . . . . . . . . . 43

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

3 Functions

45

3.1 Basics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

3.2 Kinds of Functions . . . . . . . . . . . . . . . . . . . . . . . . . . 47

3.3 Functions as Relations . . . . . . . . . . . . . . . . . . . . . . . . 49

3.4 Inverses of Functions . . . . . . . . . . . . . . . . . . . . . . . . 50

3.5 Composition of Functions . . . . . . . . . . . . . . . . . . . . . . 52

3.6 Partial Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

2

CONTENTS

4 The Size of Sets

55

4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

4.2 Enumerations and Enumerable Sets . . . . . . . . . . . . . . . . 55

4.3 Cantor's Zig-Zag Method . . . . . . . . . . . . . . . . . . . . . . 59

4.4 Pairing Functions and Codes . . . . . . . . . . . . . . . . . . . . 60

4.5 An Alternative Pairing Function . . . . . . . . . . . . . . . . . . 61

4.6 Non-enumerable Sets . . . . . . . . . . . . . . . . . . . . . . . . 63

4.7 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66

4.8 Equinumerosity . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

4.9 Sets of Different Sizes, and Cantor's Theorem . . . . . . . . . . 68

4.10 The Notion of Size, and Schro? der-Bernstein . . . . . . . . . . . 70

4.11 Enumerations and Enumerable Sets . . . . . . . . . . . . . . . . 71

4.12 Non-enumerable Sets . . . . . . . . . . . . . . . . . . . . . . . . 72

4.13 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

5 Arithmetization

79

5.1 From N to Z . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79

5.2 From Z to Q . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

5.3 The Real Line . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

5.4 From Q to R . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83

5.5 Some Philosophical Reflections . . . . . . . . . . . . . . . . . . . 85

5.6 Ordered Rings and Fields . . . . . . . . . . . . . . . . . . . . . . 87

5.7 Appendix: the Reals as Cauchy Sequences . . . . . . . . . . . . 90

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

6 Infinite Sets

94

6.1 Hilbert's Hotel . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

6.2 Dedekind Algebras . . . . . . . . . . . . . . . . . . . . . . . . . 95

6.3 Arithmetical Induction . . . . . . . . . . . . . . . . . . . . . . . 97

6.4 Dedekind's "Proof" . . . . . . . . . . . . . . . . . . . . . . . . . 98

6.5 Appendix: Proving Schro? der-Bernstein . . . . . . . . . . . . . . 100

II Propositional Logic

102

7 Syntax and Semantics

104

7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

7.2 Propositional Formulas . . . . . . . . . . . . . . . . . . . . . . . 105

7.3 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

7.4 Formation Sequences . . . . . . . . . . . . . . . . . . . . . . . . 108

7.5 Valuations and Satisfaction . . . . . . . . . . . . . . . . . . . . . 110

7.6 Semantic Notions . . . . . . . . . . . . . . . . . . . . . . . . . . 111

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112

Release : d4e99d0 (2023-10-08)

3

CONTENTS

8 Derivation Systems

114

8.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114

8.2 The Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . 116

8.3 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . 116

8.4 Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118

8.5 Axiomatic Derivations . . . . . . . . . . . . . . . . . . . . . . . . 119

9 The Sequent Calculus

121

9.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 121

9.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 122

9.3 Structural Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 123

9.4 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124

9.5 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 125

9.6 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 129

9.7 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 131

9.8 Derivability and the Propositional Connectives . . . . . . . . . 132

9.9 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137

10 Natural Deduction

139

10.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 139

10.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 140

10.3 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141

10.4 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 142

10.5 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 146

10.6 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 148

10.7 Derivability and the Propositional Connectives . . . . . . . . . 149

10.8 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

11 Tableaux

156

11.1 Rules and Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . 156

11.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 157

11.3 Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158

11.4 Examples of Tableaux . . . . . . . . . . . . . . . . . . . . . . . . 159

11.5 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 163

11.6 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 165

11.7 Derivability and the Propositional Connectives . . . . . . . . . 167

11.8 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172

12 Axiomatic Derivations

174

12.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 174

12.2 Axiom and Rules for the Propositional Connectives . . . . . . . 176

4

Release : d4e99d0 (2023-10-08)

CONTENTS

12.3 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 176 12.4 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 178 12.5 The Deduction Theorem . . . . . . . . . . . . . . . . . . . . . . . 179 12.6 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 181 12.7 Derivability and the Propositional Connectives . . . . . . . . . 182 12.8 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183 Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184

13 The Completeness Theorem

185

13.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185

13.2 Outline of the Proof . . . . . . . . . . . . . . . . . . . . . . . . . 186

13.3 Complete Consistent Sets of Sentences . . . . . . . . . . . . . . 187

13.4 Lindenbaum's Lemma . . . . . . . . . . . . . . . . . . . . . . . . 188

13.5 Construction of a Model . . . . . . . . . . . . . . . . . . . . . . . 189

13.6 The Completeness Theorem . . . . . . . . . . . . . . . . . . . . 190

13.7 The Compactness Theorem . . . . . . . . . . . . . . . . . . . . . 190

13.8 A Direct Proof of the Compactness Theorem . . . . . . . . . . . 191

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192

III First-order Logic

193

14 Introduction to First-Order Logic

195

14.1 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 195

14.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196

14.3 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197

14.4 Satisfaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198

14.5 Sentences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200

14.6 Semantic Notions . . . . . . . . . . . . . . . . . . . . . . . . . . 201

14.7 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

14.8 Models and Theories . . . . . . . . . . . . . . . . . . . . . . . . . 202

14.9 Soundness and Completeness . . . . . . . . . . . . . . . . . . . 203

15 Syntax of First-Order Logic

205

15.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205

15.2 First-Order Languages . . . . . . . . . . . . . . . . . . . . . . . . 205

15.3 Terms and Formulas . . . . . . . . . . . . . . . . . . . . . . . . . 207

15.4 Unique Readability . . . . . . . . . . . . . . . . . . . . . . . . . 210

15.5 Main operator of a Formula . . . . . . . . . . . . . . . . . . . . . 212

15.6 Subformulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213

15.7 Formation Sequences . . . . . . . . . . . . . . . . . . . . . . . . 215

15.8 Free Variables and Sentences . . . . . . . . . . . . . . . . . . . . 218

15.9 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 220

Release : d4e99d0 (2023-10-08)

5

CONTENTS

16 Semantics of First-Order Logic

222

16.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222

16.2 Structures for First-order Languages . . . . . . . . . . . . . . . 223

16.3 Covered Structures for First-order Languages . . . . . . . . . . 224

16.4 Satisfaction of a Formula in a Structure . . . . . . . . . . . . . . 225

16.5 Variable Assignments . . . . . . . . . . . . . . . . . . . . . . . . 230

16.6 Extensionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232

16.7 Semantic Notions . . . . . . . . . . . . . . . . . . . . . . . . . . 234

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235

17 Theories and Their Models

238

17.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 238

17.2 Expressing Properties of Structures . . . . . . . . . . . . . . . . 240

17.3 Examples of First-Order Theories . . . . . . . . . . . . . . . . . 240

17.4 Expressing Relations in a Structure . . . . . . . . . . . . . . . . 243

17.5 The Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . 244

17.6 Expressing the Size of Structures . . . . . . . . . . . . . . . . . . 246

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247

18 Derivation Systems

249

18.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249

18.2 The Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . 251

18.3 Natural Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . 251

18.4 Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253

18.5 Axiomatic Derivations . . . . . . . . . . . . . . . . . . . . . . . . 254

19 The Sequent Calculus

256

19.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 256

19.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 257

19.3 Quantifier Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 258

19.4 Structural Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 259

19.5 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 260

19.6 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 261

19.7 Derivations with Quantifiers . . . . . . . . . . . . . . . . . . . . 265

19.8 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 266

19.9 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 268

19.10 Derivability and the Propositional Connectives . . . . . . . . . 269

19.11 Derivability and the Quantifiers . . . . . . . . . . . . . . . . . . 271

19.12 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271

19.13 Derivations with Identity predicate . . . . . . . . . . . . . . . . 276

19.14 Soundness with Identity predicate . . . . . . . . . . . . . . . . . 277

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277

20 Natural Deduction

280

6

Release : d4e99d0 (2023-10-08)

CONTENTS

20.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 280 20.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 281 20.3 Quantifier Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 282 20.4 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283 20.5 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 285 20.6 Derivations with Quantifiers . . . . . . . . . . . . . . . . . . . . 288 20.7 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 292 20.8 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 294 20.9 Derivability and the Propositional Connectives . . . . . . . . . 295 20.10 Derivability and the Quantifiers . . . . . . . . . . . . . . . . . . 296 20.11 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 297 20.12 Derivations with Identity predicate . . . . . . . . . . . . . . . . 301 20.13 Soundness with Identity predicate . . . . . . . . . . . . . . . . . 303 Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303

21 Tableaux

306

21.1 Rules and Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . 306

21.2 Propositional Rules . . . . . . . . . . . . . . . . . . . . . . . . . 307

21.3 Quantifier Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 308

21.4 Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309

21.5 Examples of Tableaux . . . . . . . . . . . . . . . . . . . . . . . . 310

21.6 Tableaux with Quantifiers . . . . . . . . . . . . . . . . . . . . . . 314

21.7 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 318

21.8 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 320

21.9 Derivability and the Propositional Connectives . . . . . . . . . 321

21.10 Derivability and the Quantifiers . . . . . . . . . . . . . . . . . . 324

21.11 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 325

21.12 Tableaux with Identity predicate . . . . . . . . . . . . . . . . . . 328

21.13 Soundness with Identity predicate . . . . . . . . . . . . . . . . . 329

Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 329

22 Axiomatic Derivations

332

22.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 332

22.2 Axiom and Rules for the Propositional Connectives . . . . . . . 334

22.3 Axioms and Rules for Quantifiers . . . . . . . . . . . . . . . . . 334

22.4 Examples of Derivations . . . . . . . . . . . . . . . . . . . . . . 335

22.5 Derivations with Quantifiers . . . . . . . . . . . . . . . . . . . . 336

22.6 Proof-Theoretic Notions . . . . . . . . . . . . . . . . . . . . . . . 337

22.7 The Deduction Theorem . . . . . . . . . . . . . . . . . . . . . . . 338

22.8 The Deduction Theorem with Quantifiers . . . . . . . . . . . . 340

22.9 Derivability and Consistency . . . . . . . . . . . . . . . . . . . . 341

22.10 Derivability and the Propositional Connectives . . . . . . . . . 342

22.11 Derivability and the Quantifiers . . . . . . . . . . . . . . . . . . 343

22.12 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343

Release : d4e99d0 (2023-10-08)

7

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

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

Google Online Preview   Download