Residuated Lattices: An Algebraic Glimpse at Substructural Logics (eBook)
532 Seiten
Elsevier Science (Verlag)
978-0-08-048964-3 (ISBN)
As the book progresses the first objective gains predominance over the second. Although the precise point of equilibrium would be difficult to specify, it is safe to say that we enter the technical part with the discussion of various completions of residuated structures. These include Dedekind-McNeille completions and canonical extensions. Completions are used later in investigating several finiteness properties such as the finite model property, generation of varieties by their finite members, and finite embeddability. The algebraic analysis of cut elimination that follows, also takes recourse to completions. Decidability of logics, equational and quasi-equational theories comes next, where we show how proof theoretical methods like cut elimination are preferable for small logics/theories, but semantic tools like Rabin's theorem work better for big ones. Then we turn to Glivenko's theorem, which says that a formula is an intuitionistic tautology if and only if its double negation is a classical one. We generalise it to the substructural setting, identifying for each substructural logic its Glivenko equivalence class with smallest and largest element. This is also where we begin investigating lattices of logics and varieties, rather than particular examples. We continue in this vein by presenting a number of results concerning minimal varieties/maximal logics. A typical theorem there says that for some given well-known variety its subvariety lattice has precisely such-and-such number of minimal members (where values for such-and-such include, but are not limited to, continuum, countably many and two). In the last two chapters we focus on the lattice of varieties corresponding to logics without contraction. In one we prove a negative result: that there are no nontrivial splittings in that variety. In the other, we prove a positive one: that semisimple varieties coincide with discriminator ones.
Within the second, more technical part of the book another transition process may be traced. Namely, we begin with logically inclined technicalities and end with algebraically inclined ones. Here, perhaps, algebraic rendering of Glivenko theorems marks the equilibrium point, at least in the sense that finiteness properties, decidability and Glivenko theorems are of clear interest to logicians, whereas semisimplicity and discriminator varieties are universal algebra par exellence. It is for the reader to judge whether we succeeded in weaving these threads into a seamless fabric.
- Considers both the algebraic and logical perspective within a common framework.
- Written by experts in the area.
- Easily accessible to graduate students and researchers from other fields.
- Results summarized in tables and diagrams to provide an overview of the area.
- Useful as a textbook for a course in algebraic logic, with exercises and suggested research directions.
- Provides a concise introduction to the subject and leads directly to research topics.
- The ideas from algebra and logic are developed hand-in-hand and the connections are shown in every level.
The book is meant to serve two purposes. The first and more obvious one is to present state of the art results in algebraic research into residuated structures related to substructural logics. The second, less obvious but equally important, is to provide a reasonably gentle introduction to algebraic logic. At the beginning, the second objective is predominant. Thus, in the first few chapters the reader will find a primer of universal algebra for logicians, a crash course in nonclassical logics for algebraists, an introduction to residuated structures, an outline of Gentzen-style calculi as well as some titbits of proof theory - the celebrated Hauptsatz, or cut elimination theorem, among them. These lead naturally to a discussion of interconnections between logic and algebra, where we try to demonstrate how they form two sides of the same coin. We envisage that the initial chapters could be used as a textbook for a graduate course, perhaps entitled Algebra and Substructural Logics. As the book progresses the first objective gains predominance over the second. Although the precise point of equilibrium would be difficult to specify, it is safe to say that we enter the technical part with the discussion of various completions of residuated structures. These include Dedekind-McNeille completions and canonical extensions. Completions are used later in investigating several finiteness properties such as the finite model property, generation of varieties by their finite members, and finite embeddability. The algebraic analysis of cut elimination that follows, also takes recourse to completions. Decidability of logics, equational and quasi-equational theories comes next, where we show how proof theoretical methods like cut elimination are preferable for small logics/theories, but semantic tools like Rabin's theorem work better for big ones. Then we turn to Glivenko's theorem, which says that a formula is an intuitionistic tautology if and only if its double negation is a classical one. We generalise it to the substructural setting, identifying for each substructural logic its Glivenko equivalence class with smallest and largest element. This is also where we begin investigating lattices of logics and varieties, rather than particular examples. We continue in this vein by presenting a number of results concerning minimal varieties/maximal logics. A typical theorem there says that for some given well-known variety its subvariety lattice has precisely such-and-such number of minimal members (where values for such-and-such include, but are not limited to, continuum, countably many and two). In the last two chapters we focus on the lattice of varieties corresponding to logics without contraction. In one we prove a negative result: that there are no nontrivial splittings in that variety. In the other, we prove a positive one: that semisimple varieties coincide with discriminator ones. Within the second, more technical part of the book another transition process may be traced. Namely, we begin with logically inclined technicalities and end with algebraically inclined ones. Here, perhaps, algebraic rendering of Glivenko theorems marks the equilibrium point, at least in the sense that finiteness properties, decidability and Glivenko theorems are of clear interest to logicians, whereas semisimplicity and discriminator varieties are universal algebra par exellence. It is for the reader to judge whether we succeeded in weaving these threads into a seamless fabric.
Cover 1
Copyright Page 5
Table of Contents 8
Detailed Contents 12
List of Figures 20
List of Tables 22
Introduction 24
Chapter 1. Getting started 36
1.1. First-order languages and semantics 36
1.1.1. Preorders 39
1.1.2. Posets 39
1.1.3. Lattices 40
1.1.4. Heyting algebras and Boolean algebras 44
1.1.5. Semigroups, monoids and other groupoids 46
1.2. Concepts from universal algebra 47
1.2.1. Homomorphisms, subalgebras, substructures, direct products 47
1.2.2. Congruences 50
1.2.3. Free algebras 54
1.2.4. More on Heyting and Boolean algebras 55
1.2.5. Mal’cev conditions 56
1.2.6. Ultraproducts and Jónsson’s Lemma 58
1.2.7. Equational logic 60
1.2.8. Quasivarieties 61
1.3. Logic 61
1.3.1. Hilbert calculus for classical logic 61
1.3.2. Gentzen’s sequent calculus for classical logic 66
1.3.3. Calculi for intuitionistic logic 70
1.3.4. Provability in Hilbert and Gentzen calculi 72
1.4. Logic and algebra 74
1.4.1. Validity of formulas in algebras 74
1.4.2. Lindenbaum-Tarski algebras 75
1.4.3. Algebraization 77
1.4.4. Superintuitionistic logics 78
1.5. Cut elimination in sequent calculi 81
1.5.1. Cut elimination 81
1.5.2. Decidability and subformula property 84
1.6. Consequence relations and matrices 85
1.6.1. Consequence relations 86
1.6.2. Inference rules 86
1.6.3. Proofs and theorems 88
1.6.4. Matrices 89
1.6.5. Examples 89
1.6.6. First-order and (quasi)equational logic 90
Exercises 92
Notes 95
Chapter 2. Substructural logics and residuated lattices 98
2.1. Sequent calculi and substructural logics 99
2.1.1. Structural rules 99
2.1.2. Comma, fusion and implication 102
2.1.3. Sequent calculus for the substructural logic FL 107
2.1.4. Deducibility and substructural logics over FL 110
2.2. Residuated lattices and FL-algebras 114
2.3. Important subclasses of substructural logics 120
2.3.1. Lambek calculus 122
2.3.2. BCK logic and algebras 124
2.3.3. Relevant logics 127
2.3.4. Linear logic 131
2.3.5. •ukasiewicz logic and MV-algebras 132
2.3.6. Fuzzy logics and triangular norms 136
2.3.7. Superintuitionistic logics and Heyting algebras 138
2.3.8. Minimal logic and Brouwerian algebras 139
2.3.9. Fregean logics and equivalential algebras 140
2.3.10. Overview of logics over FL 142
2.4. Parametrized local deduction theorem 142
2.5. Hilbert systems 147
2.5.1. The systems HFLe and HFL 148
2.5.2. Derivable rules 148
2.5.3. Equality of two consequence relations 151
2.6. Algebraization and deductive filters 153
2.6.1. Algebraization 153
2.6.2. Deductive filters 157
Exercises 158
Notes 161
Chapter 3. Residuation and structure theory 164
3.1. Residuation theory and Galois connections 165
3.1.1. Residuated pairs 165
3.1.2. Galois connections 168
3.1.3. Binary residuated maps 171
3.2. Residuated structures 172
3.3. Involutive residuated structures 174
3.3.1. Involutive posets 175
3.3.2. Involutive pogroupoids 175
3.3.3. Involutive division posets 176
3.3.4. Term equivalences 176
3.3.5. Constants 177
3.3.6. Dual algebras 178
3.4. Further examples of residuated structures 179
3.4.1. Boolean algebras and generalized Boolean algebras 179
3.4.2. Partially ordered and lattice ordered groups 183
3.4.3. The negative cone of a residuated lattice 185
3.4.4. Cancellative residuated lattices 185
3.4.5. MV-algebras and generalized MV-algebras 188
3.4.6. BL-algebras and generalized BL-algebras 192
3.4.7. Hoops 193
3.4.8. Relation algebras 194
3.4.9. Ideals of a ring 195
3.4.10. Powerset of a monoid 195
3.4.11. The nucleus image of a residuated lattice 196
3.4.12. The Dedekind-MacNeille completion of a residuated lattice 200
3.4.13. Order ideals of a partially ordered monoid 201
3.4.14. Quantales 201
3.4.15. Retraction to an interval 202
3.4.16. Conuclei and kernel contractions 202
3.4.17. The dual of a residuated lattice with respect to an element 203
3.4.18. Translations with respect to an invertible element 204
3.5. Subvariety lattices 205
3.5.1. Some subvarieties of FL 208
3.5.2. Some subvarieties of FLw 208
3.5.3. Some subvarieties of RL 209
3.6. Structure theory 210
3.6.1. Structure theory for special cases 210
3.6.2. Convex normal subalgebras and submonoids, congruences and deductive filters 213
3.6.3. Central negative idempotents 221
3.6.4. Varieties with (equationally) definable principal congruences 222
3.6.5. The congruence extension property 223
3.6.6. Subdirectly irreducible algebras 224
3.6.7. Constants 226
Exercises 227
Notes 233
Chapter 4. Decidability 234
4.1. Syntactic proof of cut elimination 234
4.1.1. Basic idea of cut elimination 235
4.1.2. Contraction rule and mix rule 237
4.2. Decidability as a consequence of cut elimination 240
4.2.1. Decidability of basic substructural logics without contraction rule 241
4.2.2. Decidability of intuitionistic logic „ Gentzens idea 242
4.2.3. Decidability of basic substructural logics with the contraction rule 245
4.3. Further results 249
4.4. Undecidability 253
4.4.1. The quasiequational theory of residuated lattices 253
4.4.2. The word problem 254
4.4.3. Modular lattices 255
4.4.4. Distributive residuated lattices 258
Exercises 263
Notes 264
Chapter 5. Logical and algebraic properties 268
5.1. Syntactic approach to logical properties 268
5.1.1. Disjunction property 268
5.1.2. Craig interpolation property 269
5.1.3. Maehara’s method 270
5.1.4. Variable sharing property of logics without the weakening rules 276
5.2. Maksimova’s variable separation property 277
5.3. Algebraic characterizations 280
5.3.1. Disjunction property 280
5.3.2. Halldén Completeness 283
5.4. Maksimova’s property and well-connected pairs 288
5.5. Deductive interpolation properties 294
5.5.1. Strong deductive interpolation property 294
5.5.2. Robinson property 295
5.5.3. Amalgamation property and Robinson property 298
5.5.4. Algebraic characterization of the deductive interpolation property 300
5.6. Craig interpolation property 302
5.6.1. Extensions of Craig interpolation property 303
5.6.2. Super-amalgamation property and strong Robinson property 305
5.6.3. Algebraic characterization of Craig interpolation property 306
5.6.4. Joint embedding property 308
5.6.5. Interpolation property and pseudo-relevance property 309
Exercises 310
Notes 310
Chapter 6. Completions and finite embeddability 312
6.1. Completions of posets 312
6.1.1. Some properties of canonical extensions 316
6.1.2. Canonical extensions of maps 318
6.1.3. Operators and preservation of identities 320
6.2. Canonical extensions of residuated groupoids 321
6.2.1. Canonicity 323
6.2.2. A counterexample for canonical extensions 325
6.3. Nuclear completions of residuated groupoids 326
6.3.1. Canonical extensions as nuclear completions 328
6.4. Negative results for completions 329
6.4.1. MV-algebras 331
6.4.2. Lattice-ordered groups 332
6.4.3. Product algebras 332
6.5. Finite embeddability property 333
6.5.1. An embedding construction 335
6.5.2. FEP for some subvarieties of FL 338
6.5.3. Counterexamples for FEP 341
Exercises 342
Notes 344
Chapter 7. Algebraic aspects of cut elimination 346
7.1. Gentzen matrices for the sequent calculus FL 347
7.2. Quasi-completions and cut elimination 350
7.3. Cut elimination for other systems 355
7.3.1. Involutive substructural logics 355
7.3.2. Cyclic substructural modal logics 360
7.3.3. Completeness of tableau systems 360
7.4. Finite model property 362
Exercises 365
Notes 365
Chapter 8. Glivenko theorems 368
8.1. Overview 368
8.2. Glivenko equivalence 371
8.3. Glivenko properties 375
8.3.1. The Glivenko property 376
8.3.2. The deductive Glivenko property 377
8.3.3. The equational Glivenko property 378
8.3.4. An axiomatization for the Glivenko variety of an involutive variety 381
8.4. More on the equational Glivenko property 383
8.4.1. The deductive equational Glivenko property 383
8.4.2. An alternative characterization for the equational Glivenko property 385
8.5. Special cases 387
8.5.1. The cyclic case 387
8.5.2. The classical case 390
8.5.3. The basic logic case 393
8.6. Generalized Kolmogorov translation 395
Exercises 398
Notes 398
Chapter 9. Lattices of logics and varieties 400
9.1. General facts about atoms 401
9.2. Minimal subvarieties of RL 403
9.2.1. Commutative, representable atoms 404
9.2.2. Cancellative atoms 407
9.2.3. Bounded, 3-potent, representable atoms 407
9.2.4. Idempotent, commutative atoms 408
9.2.5. Idempotent, representable atoms 409
9.3. Minimal subvarieties of FL 414
9.3.1. Minimal subvarieties of FLo and FLi 415
9.3.2. Minimal subvarieties of representable FLec and FLei 417
9.3.3. Minimal subvarieties of FLe with term-definable bounds 420
9.3.4. Minimal subvarieties of FLeco 423
9.4. Almost minimal subvarieties of FLew 424
9.4.1. General facts about almost minimal varieties 425
9.4.2. Almost minimal subvarieties of InFLew 428
9.4.3. Almost minimal subvarieties of representable FLew 433
9.4.4. Almost minimal subvarieties of 2-potent DFLew 437
9.5. Almost minimal varieties of BL-algebras 438
9.6. Translations of subvariety lattices 440
9.6.1. Generalized ordinal sums 441
9.7. Axiomatizations for joins of varieties and meets of logics 445
9.7.1. Varieties of residuated lattices generated by positive universal classes 445
9.7.2. Equational basis for joins of varieties 449
9.7.3. Direct product decompositions 452
9.8. The subvariety lattices of LG and LG– 454
9.8.1. From subvarieties of LG– to subvarieties of LG 455
9.8.2. From subvarieties of LG to subvarieties of LG– 457
9.8.3. Categorical equivalence and the functor L -> L–
Exercises 459
Notes 460
Chapter 10. Splittings 462
10.1. Splittings in general 462
10.2. Splittings in varieties of algebras 463
10.3. Algebras describing themselves 464
10.3.1. Jankov terms 465
10.3.2. Example of Jankov term and diagram 466
10.3.3. Generalized Jankov terms 468
10.4. Construction that excludes splittings 469
10.4.1. An introductory example 470
10.4.2. Expansions 471
10.4.3. Iterated expansions 477
10.4.4. Twisted products 479
10.5. Only one splitting 482
Exercises 482
Notes 483
Chapter 11. Semisimplicity 486
11.1. Semisimplicity, discriminator, EDPC 486
11.1.1. Some connections to logics 487
11.2. Free FLew-algebras are semisimple: outline 488
11.3. A characterization of semisimple FLew-algebras 488
11.4. Sequent calculi for FLew 489
11.5. Semisimplicity of free FLew-algebras 493
11.6. Inside FLew semisimplicity implies discriminator: outline 494
11.7. A characterization of semisimple subvarieties of FLew 495
11.7.1. Finding subdirectly irreducibles 495
11.7.2. A necessary condition for semisimplicity 496
11.8. Semisimplicity forces discriminator 497
11.8.1. An ultraproduct construction 498
11.8.2. Semisimplicity forces n-potency 499
Exercises 500
Notes 501
Bibliography 502
Index 520
| Erscheint lt. Verlag | 25.4.2007 |
|---|---|
| Sprache | englisch |
| Themenwelt | Sachbuch/Ratgeber |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Mathematik / Informatik ► Mathematik ► Algebra | |
| Mathematik / Informatik ► Mathematik ► Angewandte Mathematik | |
| Mathematik / Informatik ► Mathematik ► Arithmetik / Zahlentheorie | |
| Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre | |
| Technik | |
| ISBN-10 | 0-08-048964-8 / 0080489648 |
| ISBN-13 | 978-0-08-048964-3 / 9780080489643 |
| Haben Sie eine Frage zum Produkt? |
PDF (Adobe DRM)Kopierschutz: Adobe-DRM
Adobe-DRM ist ein Kopierschutz, der das eBook vor Mißbrauch schützen soll. Dabei wird das eBook bereits beim Download auf Ihre persönliche Adobe-ID autorisiert. Lesen können Sie das eBook dann nur auf den Geräten, welche ebenfalls auf Ihre Adobe-ID registriert sind.
Details zum Adobe-DRM
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen eine
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen eine
Geräteliste und zusätzliche Hinweise
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich
