MacNeille completions of FL-algebras (Q652517)

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.