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

Abstract Monadic substructural predicate logic $\mathbf{mFL_{ew}\forall }$ that consists of the formulas with unary predicates and just one object variable, is the monadic fragment of substructural predicate logic $\mathbf{FL_{ew}\forall }$, which is indeed the predicate version of substructural logic $\mathbf{FL_{ew}}$. 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 $\mathbf{mFL_{ew}\forall }$ and to obtain the subdirect representation of the variety of monadic semilinear residuated lattices. Firstly, using the equivalence between monadic substructural predicate logic $\mathbf{mFL_{ew}\forall }$ and S5-like substructural modal logic $\mathbf{S5(FL_{ew})}$, we prove that the variety of monadic residuated lattices is actually the equivalent algebraic semantics of the logic $\mathbf{mFL_{ew}\forall }$, 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.