Residuated Lattices: An Algebraic Glimpse at Substructural Logics

Cover......Page 1
Contents......Page 5
Detailed Contents......Page 9
List of Figures......Page 17
List of Tables......Page 19
Substructural logics and residuated lattices......Page 21
About the book and the intended audience......Page 22
Contents......Page 24
Topics not covered in the book......Page 26
A biased survey of algebraic logic......Page 27
Acknowledgements......Page 30
1.1. First-order languages and semantics......Page 33
1.1.2. Posets......Page 36
1.1.3. Lattices......Page 37
1.1.4. Heyting algebras and Boolean algebras......Page 41
1.1.5. Semigroups, monoids and other groupoids......Page 43
1.2.1. Homomorphisms, subalgebras, substructures, direct products......Page 44
1.2.2. Congruences......Page 47
1.2.3. Free algebras......Page 51
1.2.4. More on Heyting and Boolean algebras......Page 52
1.2.5. Mal’cev conditions......Page 53
1.2.6. Ultraproducts and Jónsson’s Lemma......Page 55
1.2.7. Equational logic......Page 57
1.3.1. Hilbert calculus for classical logic......Page 58
1.3.2. Gentzen’s sequent calculus for classical logic......Page 63
1.3.3. Calculi for intuitionistic logic......Page 67
1.3.4. Provability in Hilbert and Gentzen calculi......Page 69
1.4.1. Validity of formulas in algebras......Page 71
1.4.2. Lindenbaum-Tarski algebras......Page 72
1.4.3. Algebraization......Page 74
1.4.4. Superintuitionistic logics......Page 75
1.5.1. Cut elimination......Page 78
1.5.2. Decidability and subformula property......Page 81
1.6. Consequence relations and matrices......Page 82
1.6.2. Inference rules......Page 83
1.6.3. Proofs and theorems......Page 85
1.6.5. Examples......Page 86
1.6.6. First-order and (quasi)equational logic......Page 87
Exercises......Page 89
Notes......Page 92
2. Substructural logics and residuated lattices......Page 95
2.1.1. Structural rules......Page 96
2.1.2. Comma, fusion and implication......Page 99
2.1.3. Sequent calculus for the substructural logic FL......Page 104
2.1.4. Deducibility and substructural logics over FL......Page 107
2.2. Residuated lattices and FL-algebras......Page 111
2.3. Important subclasses of substructural logics......Page 117
2.3.1. Lambek calculus......Page 119
2.3.2. BCK logic and algebras......Page 121
2.3.3. Relevant logics......Page 124
2.3.4. Linear logic......Page 128
2.3.5. Łukasiewicz logic and MV-algebras......Page 129
2.3.6. Fuzzy logics and triangular norms......Page 133
2.3.7. Superintuitionistic logics and Heyting algebras......Page 135
2.3.8. Minimal logic and Brouwerian algebras......Page 136
2.3.9. Fregean logics and equivalential algebras......Page 137
2.4. Parametrized local deduction theorem......Page 139
2.5. Hilbert systems......Page 144
2.5.2. Derivable rules......Page 145
2.5.3. Equality of two consequence relations......Page 148
2.6.1. Algebraization......Page 150
2.6.2. Deductive filters......Page 154
Exercises......Page 155
Notes......Page 158
3. Residuation and structure theory......Page 161
3.1.1. Residuated pairs......Page 162
3.1.2. Galois connections......Page 165
3.1.3. Binary residuated maps......Page 168
3.2. Residuated structures......Page 169
3.3. Involutive residuated structures......Page 171
3.3.2. Involutive pogroupoids......Page 172
3.3.4. Term equivalences......Page 173
3.3.5. Constants......Page 174
3.3.6. Dual algebras......Page 175
3.4.1. Boolean algebras and generalized Boolean algebras......Page 176
3.4.2. Partially ordered and lattice ordered groups......Page 180
3.4.4. Cancellative residuated lattices......Page 182
3.4.5. MV-algebras and generalized MV-algebras......Page 185
3.4.6. BL-algebras and generalized BL-algebras......Page 189
3.4.7. Hoops......Page 190
3.4.8. Relation algebras......Page 191
3.4.10. Powerset of a monoid......Page 192
3.4.11. The nucleus image of a residuated lattice......Page 193
3.4.12. The Dedekind-MacNeille completion of a residuated lattice......Page 197
3.4.14. Quantales......Page 198
3.4.16. Conuclei and kernel contractions......Page 199
3.4.17. The dual of a residuated lattice with respect to an element......Page 200
3.4.18. Translations with respect to an invertible element......Page 201
3.5. Subvariety lattices......Page 202
3.5.2. Some subvarieties of FL_w......Page 205
3.5.3. Some subvarieties of RL......Page 206
3.6.1. Structure theory for special cases......Page 207
3.6.2. Convex normal subalgebras and submonoids, congruences and deductive filters......Page 210
3.6.3. Central negative idempotents......Page 218
3.6.4. Varieties with (equationally) definable principal congruences......Page 219
3.6.5. The congruence extension property......Page 220
3.6.6. Subdirectly irreducible algebras......Page 221
3.6.7. Constants......Page 223
Exercises......Page 224
Notes......Page 230
4.1. Syntactic proof of cut elimination......Page 231
4.1.1. Basic idea of cut elimination......Page 232
4.1.2. Contraction rule and mix rule......Page 234
4.2. Decidability as a consequence of cut elimination......Page 237
4.2.1. Decidability of basic substructural logics without contraction rule......Page 238
4.2.2. Decidability of intuitionistic logic—Gentzen's idea......Page 239
4.2.3. Decidability of basic substructural logics with the contraction rule......Page 242
4.3. Further results......Page 246
4.4.1. The quasiequational theory of residuated lattices......Page 250
4.4.2. The word problem......Page 251
4.4.3. Modular lattices......Page 252
4.4.4. Distributive residuated lattices......Page 255
Exercises......Page 260
Notes......Page 261
5.1.1. Disjunction property......Page 265
5.1.2. Craig interpolation property......Page 266
5.1.3. Maehara’s method......Page 267
5.1.4. Variable sharing property of logics without the weakening rules......Page 273
5.2. Maksimova’s variable separation property......Page 274
5.3.1. Disjunction property......Page 277
5.3.2. Halldén Completeness......Page 280
5.4. Maksimova’s property and well-connected pairs......Page 285
5.5.1. Strong deductive interpolation property......Page 291
5.5.2. Robinson property......Page 292
5.5.3. Amalgamation property and Robinson property......Page 295
5.5.4. Algebraic characterization of the deductive interpolation property......Page 297
5.6. Craig interpolation property......Page 299
5.6.1. Extensions of Craig interpolation property......Page 300
5.6.2. Super-amalgamation property and strong Robinson property......Page 302
5.6.3. Algebraic characterization of Craig interpolation property......Page 303
5.6.4. Joint embedding property......Page 305
5.6.5. Interpolation property and pseudo-relevance property......Page 306
Notes......Page 307
6.1. Completions of posets......Page 309
6.1.1. Some properties of canonical extensions......Page 313
6.1.2. Canonical extensions of maps......Page 315
6.1.3. Operators and preservation of identities......Page 317
6.2. Canonical extensions of residuated groupoids......Page 318
6.2.1. Canonicity......Page 320
6.2.2. A counterexample for canonical extensions......Page 322
6.3. Nuclear completions of residuated groupoids......Page 323
6.3.1. Canonical extensions as nuclear completions......Page 325
6.4. Negative results for completions......Page 326
6.4.1. MV-algebras......Page 328
6.4.3. Product algebras......Page 329
6.5. Finite embeddability property......Page 330
6.5.1. An embedding construction......Page 332
6.5.2. FEP for some subvarieties of FL......Page 335
6.5.3. Counterexamples for FEP......Page 338
Exercises......Page 339
Notes......Page 341
7. Algebraic aspects of cut elimination......Page 343
7.1. Gentzen matrices for the sequent calculus FL......Page 344
7.2. Quasi-completions and cut elimination......Page 347
7.3.1. Involutive substructural logics......Page 352
7.3.3. Completeness of tableau systems......Page 357
7.4. Finite model property......Page 359
Notes......Page 362
8.1. Overview......Page 365
8.2. Glivenko equivalence......Page 368
8.3. Glivenko properties......Page 372
8.3.1. The Glivenko property......Page 373
8.3.2. The deductive Glivenko property......Page 374
8.3.3. The equational Glivenko property......Page 375
8.3.4. An axiomatization for the Glivenko variety of an involutive variety......Page 378
8.4.1. The deductive equational Glivenko property......Page 380
8.4.2. An alternative characterization for the equational Glivenko property......Page 382
8.5.1. The cyclic case......Page 384
8.5.2. The classical case......Page 387
8.5.3. The basic logic case......Page 390
8.6. Generalized Kolmogorov translation......Page 392
Notes......Page 395
9. Lattices of logics and varieties......Page 397
9.1. General facts about atoms......Page 398
9.2. Minimal subvarieties of RL......Page 400
9.2.1. Commutative, representable atoms......Page 401
9.2.3. Bounded, 3-potent, representable atoms......Page 404
9.2.4. Idempotent, commutative atoms......Page 405
9.2.5. Idempotent, representable atoms......Page 406
9.3. Minimal subvarieties of FL......Page 411
9.3.1. Minimal subvarieties of FL_o and FL_i......Page 412
9.3.2. Minimal subvarieties of representable FL_ec and FL_ei......Page 414
9.3.3. Minimal subvarieties of FL_e with term-definable bounds......Page 417
9.3.4. Minimal subvarieties of FL_eco......Page 420
9.4. Almost minimal subvarieties of FL_ew......Page 421
9.4.1. General facts about almost minimal varieties......Page 422
9.4.2. Almost minimal subvarieties of InFL_ew......Page 425
9.4.3. Almost minimal subvarieties of representable FL_ew......Page 430
9.4.4. Almost minimal subvarieties of 2-potent DFL_ew......Page 434
9.5. Almost minimal varieties of BL-algebras......Page 435
9.6. Translations of subvariety lattices......Page 437
9.6.1. Generalized ordinal sums......Page 438
9.7.1. Varieties of residuated lattices generated by positive universal classes......Page 442
9.7.2. Equational basis for joins of varieties......Page 446
9.7.3. Direct product decompositions......Page 449
9.8. The subvariety lattices of LG and LG⁻......Page 451
9.8.1. From subvarieties of LG⁻ to subvarieties of LG......Page 452
9.8.2. From subvarieties of LG to subvarieties of LG⁻......Page 454
Exercises......Page 456
Notes......Page 457
10.1. Splittings in general......Page 459
10.2. Splittings in varieties of algebras......Page 460
10.3. Algebras describing themselves......Page 461
10.3.1. Jankov terms......Page 462
10.3.2. Example of Jankov term and diagram......Page 463
10.3.3. Generalized Jankov terms......Page 465
10.4. Construction that excludes splittings......Page 466
10.4.1. An introductory example......Page 467
10.4.2. Expansions......Page 468
10.4.3. Iterated expansions......Page 474
10.4.4. Twisted products......Page 476
Exercises......Page 479
Notes......Page 480
11.1. Semisimplicity, discriminator, EDPC......Page 483
11.1.1. Some connections to logics......Page 484
11.3. A characterization of semisimple FL_ew-algebras......Page 485
11.4. Sequent calculi for FL_ew......Page 486
11.5. Semisimplicity of free FL_ew-algebras......Page 490
11.6. Inside FL_ew semisimplicity implies discriminator: outline......Page 491
11.7.1. Finding subdirectly irreducibles......Page 492
11.7.2. A necessary condition for semisimplicity......Page 493
11.8. Semisimplicity forces discriminator......Page 494
11.8.1. An ultraproduct construction......Page 495
11.8.2. Semisimplicity forces n-potency......Page 496
Exercises......Page 497
Notes......Page 498
B......Page 499
C......Page 501
D......Page 502
F......Page 503
G......Page 504
H......Page 505
J......Page 506
K......Page 507
L......Page 508
M......Page 509
O......Page 510
P......Page 511
S......Page 512
U......Page 513
W......Page 514
Z......Page 515
Index......Page 517