MacNeille completions of FL-algebras. (English) Zbl 1259.03086
The authors have been studying the completion problem of FL-algebras as part of algebraic proof theory, which is a research project to explore the connections between order algebra and proof theory. In their previous works, FL-algebraic equations were classified in a hierarchy called substructural, and those of some lowest levels were shown to be preserved by MacNeille completions of FLw-algebras, where some negative aspects in higher levels have also been pointed out. In this paper, they carry on the investigation for those of the next level P3 which include several interesting equations such as prelinearity, weak excluded middle, and so on. The main result is that all P3-equations are preserved by MacNeille completions of subdirectly irreducible FLew-algebras, from which then follows that any subvariety of FLew defined by such equations admits (not necessarily MacNeille) completions. The method, based on proof-theoretic ideas and techniques in substructural logics, is also applied to prove a similar result for FL-algebras in general, using the syntactic condition of acyclicity and modifying the definition of P3 suitably.
Reviewer: Osamu Sonobe (Follonica)
MSC:
| 03G25 | Other algebras related to logic |
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 06F05 | Ordered semigroups and monoids |
| 08B15 | Lattices of varieties |
| 03B55 | Intermediate logics |
| 06D20 | Heyting algebras (lattice-theoretic aspects) |
| 03F03 | Proof theory in general (including proof-theoretic semantics) |
Keywords:
residuated lattice; MacNeille completion; FL-algebra; Heyting algebra; substructural logic; superintuitionistic logic; substructural hierarchy; algebraic proof theoryReferences:
| [1] | Andreoli J.-M: Logic programming with focusing proofs in linear logic. J. Logic Comput 2(3), 297–347 (1992) · Zbl 0764.03020 · doi:10.1093/logcom/2.3.297 |
| [2] | Banaschewski B.: Hüllensysteme und Erweiterungen von Quasi-Ordnungen. Z. Math. Logik Grund. Math 2, 35–46 (1956) · Zbl 0073.26904 |
| [3] | Bezhanishvili G., Harding J.: MacNeille completions of Heyting algebras. Houston J. Math 30(4), 937–952 (2004) · Zbl 1066.06005 |
| [4] | Ciabattoni, A., Galatos N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: Proceedings of LICS’08, IEEE, 229–240 (2008) |
| [5] | Ciabattoni, A., Galatos N., Terui, K.: Algebraic proof theory for substructural logics: cut-elimination and completions. Annals of Pure and Applied Logic (to appear) www.kurims.kyoto-u.ac.jp/\(\sim\)terui/apt.pdf . · Zbl 1245.03026 |
| [6] | Galatos N.: Equational bases for joins of residuated-lattice varieties. Studia Logica 76(2), 227–240 (2004) · Zbl 1068.06007 · doi:10.1023/B:STUD.0000032086.42963.7c |
| [7] | Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: an algebraic glimpse at substructural logics, Studies in Logics and the Foundations of Mathematics, Elsevier (2007) · Zbl 1171.03001 |
| [8] | Galatos N., Ono H.: Algebraization, parameterized local deduction theorem and interpolation for substructural logics over FL. Studia Logica 83, 279–308 (2006) · Zbl 1105.03021 · doi:10.1007/s11225-006-8305-5 |
| [9] | Harding J.: A regular completion for the variety generated by the three-element Heyting algebra. Houston J. Math 34(3), 649–660 (2008) · Zbl 1229.06001 |
| [10] | Harding J.: Completions of ordered algebraic structures: a survey. In: Proceedings of the International Workshop on Interval/Probabilistic Uncertainty and Non-classical Logics. Advances in Soft Computing. Ono et al. Eds, Springer 46, 231–244 (2008) · Zbl 1151.06012 |
| [11] | Kowalski T., Litak T.: Completions of GBL algebras: negative results. Algebra Universalis 58, 373–384 (2008) · Zbl 1161.06010 · doi:10.1007/s00012-008-2056-2 |
| [12] | Ono H.: Logics without contraction rule and residuated lattices. Australas. J. Log 8(1), 1–32 (2010) |
| [13] | Schmidt J.: Zur Kennzeichnung der Dedekind-MacNeilleschen H”ulle einer geordneten Menge. Arch. Math. (Basel) 7, 241–249 (1956) · Zbl 0073.03801 · doi:10.1007/BF01900297 |
| [14] | Zakharyaschev M.: On intermediate logics. Soviet Math. Dokl 27(2), 274–277 (1983) · Zbl 0548.03009 |
| [15] | Zakharyaschev M.: Syntax and semantics of superintuitionistic logics. Algebra and Logic 28(4), 262–282 (1989) · Zbl 0708.03011 · doi:10.1007/BF01982017 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
