An algebraic approach to the study of monadic substructural predicate logics over FLew

Monadic substructural predicate logic mFLew∀ that consists of the formulas with unary predicates and just one object variable, is the monadic fragment of substructural predicate logic FLew∀, which is indeed the predicate version of substructural logic FLew. The main aim of this paper is, based on the variety of monadic residuated lattices, to give an algebraic proof of the completeness theorem for monadic substructural predicate logic mFLew∀ and to obtain the subdirect representation of the variety of monadic semilinear residuated lattices. Firstly, using the equivalence between monadic substructural predicate logic mFLew∀ and S5-like substructural modal logic S5(FLew), we prove that the variety of monadic residuated lattices is actually the equivalent algebraic semantics of the logic mFLew∀, and give an algebraic proof of the completeness theorem for this logic via functional monadic residuated lattices. Subsequently taking the widest monadic semilinear residuated lattices, the monadic MTL-algebras as an example, we introduce the notion of sublinearly ordered monadic MTL-algebras and prove the subdirect representation theorem of the variety of monadic MTL-algebras, namely, the variety of monadic MTL-algebras is generated by its all sublinearly ordered members. Finally, by using the amalgamation property of the variety of MTL-algebras, we prove that the variety of MTL-algebras is generated by relatively functional sublinearly ordered monadic MTL-algebras from the view of pure algebraic point.