In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenberg-Moore algebras for some monad. We will also prove a completeness result: a formula is derivable from a given theory if and only if it is satisfied by all models of the theory. Finally, leveraging results by Milius and Urbat, we give HSP-like characterizations of subcategories of algebras which are categories of models of particular kinds of theories.
翻译:在这项工作中,我们提出一个正式的模糊代数推理系统。我们定义的序列计算基于两种主张,即获得平等和作为模糊集的成员存在术语。我们为这种计算提供了健全的语义学,并表明在这个系统中存在着一种自由模式的概念,允许我们(在有一定限制的情况下)为某些月经恢复作为艾伦堡-摩尔代数的模型。我们还将证明一个完整的结果:一个公式可以来自特定理论,如果它符合所有理论模型的要求的话。最后,Milius和Urbat的利用结果,我们给作为特定类型理论模型的代数子类的代数作了类似于HSP的描述。