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.
To fulfill the demand for quickly locating and searching documents.
It is intelligent file search solution for home and business.