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. - 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.
Author(s): Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, Hiroakira Ono
Series: Studies in Logic and the Foundations of Mathematics 151
Edition: 1
Publisher: Elsevier
Year: 2007
Language: English
Commentary: TOC missing and other frontmatter
Pages: 509
Cover ......Page 1
List of Figures ......Page 2
List of Tables ......Page 4
Substructural logics and residuated lattices ......Page 6
About the book and the intended audience ......Page 7
Contents ......Page 9
Topics not covered in the book ......Page 11
A biased survey of algebraic logic ......Page 12
Acknowledgements ......Page 15
1.1. First-order languages and semantics ......Page 16
1.1.2. Posets ......Page 19
1.1.3. Lattices ......Page 20
1.1.4. Heyting algebras and Boolean algebras ......Page 24
1.1.5. Semigroups, monoids and other groupoids ......Page 26
1.2.1. Homomorphisms, subalgebras, substructures, direct products ......Page 27
1.2.2. Congruences ......Page 30
1.2.3. Free algebras ......Page 34
1.2.4. More on Heyting and Boolean algebras ......Page 35
1.2.5. Malcev conditions ......Page 36
1.2.6. Ultraproducts and Jónssons Lemma ......Page 38
1.2.7. Equational logic ......Page 40
1.3.1. Hilbert calculus for classical logic ......Page 41
1.3.2. Gentzens sequent calculus for classical logic ......Page 46
1.3.3. Calculi for intuitionistic logic ......Page 50
1.3.4. Provability in Hilbert and Gentzen calculi ......Page 52
1.4.1. Validity of formulas in algebras ......Page 54
1.4.2. Lindenbaum-Tarski algebras ......Page 55
1.4.3. Algebraization ......Page 57
1.4.4. Superintuitionistic logics ......Page 58
1.5.1. Cut elimination ......Page 61
1.5.2. Decidability and subformula property ......Page 64
1.6. Consequence relations and matrices ......Page 65
1.6.2. Inference rules ......Page 66
1.6.3. Proofs and theorems ......Page 68
1.6.5. Examples ......Page 69
1.6.6. First-order and (quasi)equational logic ......Page 70
Exercises ......Page 72
Notes ......Page 75
2. Substructural logics and residuated lattices ......Page 77
2.1.1. Structural rules ......Page 78
2.1.2. Comma, fusion and implication ......Page 81
2.1.3. Sequent calculus for the substructural logic FL ......Page 86
2.1.4. Deducibility and substructural logics over FL ......Page 89
2.2. Residuated lattices and FL-algebras ......Page 93
2.3. Important subclasses of substructural logics ......Page 99
2.3.1. Lambek calculus ......Page 101
2.3.2. BCK logic and algebras ......Page 103
2.3.3. Relevant logics ......Page 106
2.3.4. Linear logic ......Page 110
2.3.5. ukasiewicz logic and MV-algebras ......Page 111
2.3.6. Fuzzy logics and triangular norms ......Page 115
2.3.7. Superintuitionistic logics and Heyting algebras ......Page 117
2.3.8. Minimal logic and Brouwerian algebras ......Page 118
2.3.9. Fregean logics and equivalential algebras ......Page 119
2.4. Parametrized local deduction theorem ......Page 121
2.5. Hilbert systems ......Page 126
2.5.2. Derivable rules ......Page 127
2.5.3. Equality of two consequence relations ......Page 130
2.6.1. Algebraization ......Page 132
2.6.2. Deductive filters ......Page 136
Exercises ......Page 137
Notes ......Page 140
3. Residuation and structure theory ......Page 142
3.1.1. Residuated pairs ......Page 143
3.1.2. Galois connections ......Page 146
3.1.3. Binary residuated maps ......Page 149
3.2. Residuated structures ......Page 150
3.3. Involutive residuated structures ......Page 152
3.3.2. Involutive pogroupoids ......Page 153
3.3.4. Term equivalences ......Page 154
3.3.5. Constants ......Page 155
3.3.6. Dual algebras ......Page 156
3.4.1. Boolean algebras and generalized Boolean algebras ......Page 157
3.4.2. Partially ordered and lattice ordered groups ......Page 161
3.4.4. Cancellative residuated lattices ......Page 163
3.4.5. MV-algebras and generalized MV-algebras ......Page 166
3.4.6. BL-algebras and generalized BL-algebras ......Page 170
3.4.7. Hoops ......Page 171
3.4.8. Relation algebras ......Page 172
3.4.10. Powerset of a monoid ......Page 173
3.4.11. The nucleus image of a residuated lattice ......Page 174
3.4.12. The Dedekind-MacNeille completion of a residuated lattice ......Page 178
3.4.14. Quantales ......Page 179
3.4.16. Conuclei and kernel contractions ......Page 180
3.4.17. The dual of a residuated lattice with respect to an element ......Page 181
3.4.18. Translations with respect to an invertible element ......Page 182
3.5. Subvariety lattices ......Page 183
3.5.2. Some subvarieties of FL_w ......Page 186
3.5.3. Some subvarieties of RL ......Page 187
3.6.1. Structure theory for special cases ......Page 188
3.6.2. Convex normal subalgebras and submonoids, congruences and deductive filters ......Page 191
3.6.3. Central negative idempotents ......Page 199
3.6.4. Varieties with (equationally) definable principal congruences ......Page 200
3.6.5. The congruence extension property ......Page 201
3.6.6. Subdirectly irreducible algebras ......Page 202
3.6.7. Constants ......Page 204
Exercises ......Page 205
Notes ......Page 211
4.1. Syntactic proof of cut elimination ......Page 212
4.1.1. Basic idea of cut elimination ......Page 213
4.1.2. Contraction rule and mix rule ......Page 215
4.2. Decidability as a consequence of cut elimination ......Page 218
4.2.1. Decidability of basic substructural logics without contraction rule ......Page 219
4.2.2. Decidability of intuitionistic logicGentzen's idea ......Page 220
4.2.3. Decidability of basic substructural logics with the contraction rule ......Page 223
4.3. Further results ......Page 227
4.4.1. The quasiequational theory of residuated lattices ......Page 231
4.4.2. The word problem ......Page 232
4.4.3. Modular lattices ......Page 233
4.4.4. Distributive residuated lattices ......Page 236
Exercises ......Page 241
Notes ......Page 242
5.1.1. Disjunction property ......Page 245
5.1.2. Craig interpolation property ......Page 246
5.1.3. Maeharas method ......Page 247
5.1.4. Variable sharing property of logics without the weakening rules ......Page 253
5.2. Maksimovas variable separation property ......Page 254
5.3.1. Disjunction property ......Page 257
5.3.2. Halldén Completeness ......Page 260
5.4. Maksimovas property and well-connected pairs ......Page 265
5.5.1. Strong deductive interpolation property ......Page 271
5.5.2. Robinson property ......Page 272
5.5.3. Amalgamation property and Robinson property ......Page 275
5.5.4. Algebraic characterization of the deductive interpolation property ......Page 277
5.6. Craig interpolation property ......Page 279
5.6.1. Extensions of Craig interpolation property ......Page 280
5.6.2. Super-amalgamation property and strong Robinson property ......Page 282
5.6.3. Algebraic characterization of Craig interpolation property ......Page 283
5.6.4. Joint embedding property ......Page 285
5.6.5. Interpolation property and pseudo-relevance property ......Page 286
Notes ......Page 287
6.1. Completions of posets ......Page 289
6.1.1. Some properties of canonical extensions ......Page 293
6.1.2. Canonical extensions of maps ......Page 295
6.1.3. Operators and preservation of identities ......Page 297
6.2. Canonical extensions of residuated groupoids ......Page 298
6.2.1. Canonicity ......Page 300
6.2.2. A counterexample for canonical extensions ......Page 302
6.3. Nuclear completions of residuated groupoids ......Page 303
6.3.1. Canonical extensions as nuclear completions ......Page 305
6.4. Negative results for completions ......Page 306
6.4.1. MV-algebras ......Page 308
6.4.3. Product algebras ......Page 309
6.5. Finite embeddability property ......Page 310
6.5.1. An embedding construction ......Page 312
6.5.2. FEP for some subvarieties of FL ......Page 315
6.5.3. Counterexamples for FEP ......Page 318
Exercises ......Page 319
Notes ......Page 321
7. Algebraic aspects of cut elimination ......Page 322
7.1. Gentzen matrices for the sequent calculus FL ......Page 323
7.2. Quasi-completions and cut elimination ......Page 326
7.3.1. Involutive substructural logics ......Page 331
7.3.3. Completeness of tableau systems ......Page 336
7.4. Finite model property ......Page 338
Notes ......Page 341
8.1. Overview ......Page 343
8.2. Glivenko equivalence ......Page 346
8.3. Glivenko properties ......Page 350
8.3.1. The Glivenko property ......Page 351
8.3.2. The deductive Glivenko property ......Page 352
8.3.3. The equational Glivenko property ......Page 353
8.3.4. An axiomatization for the Glivenko variety of an involutive variety ......Page 356
8.4.1. The deductive equational Glivenko property ......Page 358
8.4.2. An alternative characterization for the equational Glivenko property ......Page 360
8.5.1. The cyclic case ......Page 362
8.5.2. The classical case ......Page 365
8.5.3. The basic logic case ......Page 368
8.6. Generalized Kolmogorov translation ......Page 370
Notes ......Page 373
9. Lattices of logics and varieties ......Page 374
9.1. General facts about atoms ......Page 375
9.2. Minimal subvarieties of RL ......Page 377
9.2.1. Commutative, representable atoms ......Page 378
9.2.3. Bounded, 3-potent, representable atoms ......Page 381
9.2.4. Idempotent, commutative atoms ......Page 382
9.2.5. Idempotent, representable atoms ......Page 383
9.3. Minimal subvarieties of FL ......Page 388
9.3.1. Minimal subvarieties of FL_o and FL_i ......Page 389
9.3.2. Minimal subvarieties of representable FL_ec and FL_ei ......Page 391
9.3.3. Minimal subvarieties of FL_e with term-definable bounds ......Page 394
9.3.4. Minimal subvarieties of FL_eco ......Page 397
9.4. Almost minimal subvarieties of FL_ew ......Page 398
9.4.1. General facts about almost minimal varieties ......Page 399
9.4.2. Almost minimal subvarieties of InFL_ew ......Page 402
9.4.3. Almost minimal subvarieties of representable FL_ew ......Page 407
9.4.4. Almost minimal subvarieties of 2-potent DFL_ew ......Page 411
9.5. Almost minimal varieties of BL-algebras ......Page 412
9.6. Translations of subvariety lattices ......Page 414
9.6.1. Generalized ordinal sums ......Page 415
9.7.1. Varieties of residuated lattices generated by positive universal classes ......Page 419
9.7.2. Equational basis for joins of varieties ......Page 423
9.7.3. Direct product decompositions ......Page 426
9.8. The subvariety lattices of LG and LG⁻ ......Page 428
9.8.1. From subvarieties of LG⁻ to subvarieties of LG ......Page 429
9.8.2. From subvarieties of LG to subvarieties of LG⁻ ......Page 431
Exercises ......Page 433
Notes ......Page 434
10.1. Splittings in general ......Page 436
10.2. Splittings in varieties of algebras ......Page 437
10.3. Algebras describing themselves ......Page 438
10.3.1. Jankov terms ......Page 439
10.3.2. Example of Jankov term and diagram ......Page 440
10.3.3. Generalized Jankov terms ......Page 442
10.4. Construction that excludes splittings ......Page 443
10.4.1. An introductory example ......Page 444
10.4.2. Expansions ......Page 445
10.4.3. Iterated expansions ......Page 451
10.4.4. Twisted products ......Page 453
Exercises ......Page 456
Notes ......Page 457
11.1. Semisimplicity, discriminator, EDPC ......Page 459
11.1.1. Some connections to logics ......Page 460
11.3. A characterization of semisimple FL_ew-algebras ......Page 461
11.4. Sequent calculi for FL_ew ......Page 462
11.5. Semisimplicity of free FL_ew-algebras ......Page 466
11.6. Inside FL_ew semisimplicity implies discriminator: outline ......Page 467
11.7.1. Finding subdirectly irreducibles ......Page 468
11.7.2. A necessary condition for semisimplicity ......Page 469
11.8. Semisimplicity forces discriminator ......Page 470
11.8.1. An ultraproduct construction ......Page 471
11.8.2. Semisimplicity forces n-potency ......Page 472
Exercises ......Page 473
Notes ......Page 474
B ......Page 475
C ......Page 477
D ......Page 478
F ......Page 479
G ......Page 480
H ......Page 481
J ......Page 482
K ......Page 483
L ......Page 484
M ......Page 485
O ......Page 486
P ......Page 487
S ......Page 488
U ......Page 489
W ......Page 490
Z ......Page 491
Index ......Page 492
