Fuzzy Horn logic. I. Proof theory. (Q2580956)

Classically, the validity of a Horn formula \(\bigwedge_{i=1}^{n}(s_{1i}=s_{2i})\rightarrow{t_1=t_2}\) of equational logic means the validity of the entailment \(\bigcup_{i=1}^{n}\{s_{1i}=s_{2i}\}\models{t_1=t_2}\). Here the authors are interested to discuss, in the context of fuzzy logic with a graded notion of entailment and with a graded notion of equality, generalized entailments of the form \(X\models{t_1=t_2}\) for fuzzy sets \(X\) of equations. The membership degrees, and hence the truth degrees of the corresponding logic, are supposed to be choosen from a residuated lattice, in particular from a residuated lattice determined by a left-continuous t-norm. The paper offers a suitable notion of generalized equational implication with evaluated premisses together with a graded notion of proof, and has as main results Pavelka-style completeness theorems which state the coincidence of provability and entailment degrees under mildly restrictive assumptions.