The Quest for the Basic Fuzzy Logic

Abstract

The quest for basic fuzzy logic was initiated by Petr Hájek when he proposed his basic fuzzy logic BL, complete with respect to the semantics given by all continuous t-norms. Later weaker systems, such as MTL, UL or $\mathrm{psMTL}^r$, complete with respect to broader (but still meaningful for fuzzy logics) semantics, have been introduced and disputed the throne of the basic fuzzy logic. We contribute to the quest with our own proposal of a basic fuzzy logic. Indeed, we put forth a very weak logic called $\mathrm {SL}^\ell$, introduced and studied in earlier works of the authors, and propose it as a base of a new framework which allows to work in a uniform way with both propositional and first-order fuzzy logics.

2000 Mathematics Subject Classification: 03G10, 03G25, 03G27, 06B99, 06F99

1 Introduction

The present work intends to be both a survey and a position paper, conceived as a homage to Petr Hájek and his absolutely crucial contributions to Mathematical Fuzzy Logic (MFL). Our aim is to present some of the main developments in the area, starting with Hájek’s seminal works and continuing with the contributions of many others, and we want to do it by taking the search of the basic fuzzy logic as the leitmotif. Indeed, as it will be apparent in the short historical account given later in this introduction, this search has been one of the main reasons for the development of new weaker systems of fuzzy logics and the necessary mathematical apparatus to deal with them. Hájek started the quest when he proposed his basic fuzzy logic $\mathrm {BL}$, complete with respect to the semantics given by all continuous t-norms. Later weaker systems, such as $\mathrm {MTL}$, $\mathrm {UL}$ or ${\mathrm {ps}}\mathrm {MTL}^r$, complete with respect to broader (but still meaningful for fuzzy logics) semantics, have been introduced and disputed the throne of the basic fuzzy logic. We survey the development of these systems with a stress on how they have yielded systematical approaches to MFL. The chapter is also a position paper because we contribute to the quest with our own proposal of a basic fuzzy logic. Indeed, we put forth a very weak logic called $\mathrm {SL}^\ell$, introduced and studied by Cintula and Noguera (2011), Cintula et al. (2013), and propose it as a base of a new framework which allows to work in a uniform way with both propositional and first-order fuzzy logics. We present a wealth of results to illustrate the power and usefulness of this framework, which support our thesis that, from a well-defined point of view, $\mathrm {SL}^\ell$ can indeed be seen as the basic fuzzy logic.¹

1.1 T-Norm Based Fuzzy Logics

Mathematical Fuzzy Logic (MFL) started as the study of logics based on particular continuous t-norms,² most prominently Łukasiewicz logic $\L$, Gödel–Dummett logic $\mathrm {G}$ and Product logic $\Pi$. These logics are rendered in a language with the truth-constant $\overline{0}$ (falsum) and binary connectives $\rightarrow$ (implication) and & (fusion, residuated/strong conjunction). They are complete with respect to the standard semantics, which has the real-unit interval $[0,1]$ as the set of truth degrees and interprets falsum $\bot$ by $0$, fusion $\mathbin { \& }$ by the corresponding t-norm, and the implication $\rightarrow$ by its residuum,³ which always exists for continuous t-norms. On the other hand, these systems are also complete with respect to an algebraic semantics ($\mathrm {MV}$-algebras, Gödel algebras, and product algebras, respectively) and with respect to the subclass of their linearly ordered members, also known as ($\mathrm {MV}$-/Gödel/product) chains. These three algebraic semantics are mutually incomparable superclasses of Boolean algebras, which amounts to say that $\L$, $\mathrm {G}$ and $\Pi$ are mutually incomparable subclassical logics. In fact, classical logic can be retrieved as axiomatic extension of any of these three systems obtained by adding the excluded middle axiom.

In this context, Petr Hájek introduced a natural question: is it possible to see $\L$, $\mathrm {G}$ and $\Pi$ (and, in general, any fuzzy logic with a continuous t-norm-based semantics) as extensions of the same fuzzy logic? In other words: is there a basic fuzzy logic underlying all (by then) known fuzzy logic systems? As an answer to this question, he introduced in his monograph (Hájek 1998b) a system, weaker than $\L$, $\mathrm {G}$ and $\Pi$, which he named $\mathrm {BL}$ (for basic logic). This logic was given by means of a Hilbert-style calculus in the language ${\fancyscript{L}} = \{\mathbin { \& }, \rightarrow , \overline{0}\}$ of type $\langle 2, 2, 0 \rangle$, with the deduction rule of modus ponens $\mathrm {(MP)}$—from $\varphi$ and $\varphi \rightarrow \psi$ infer $\psi$—and the following axioms (taking $\rightarrow$ as the least binding connective):  

(A1):

$(\varphi \rightarrow \psi ) \rightarrow ((\psi \rightarrow \chi ) \rightarrow (\varphi \rightarrow \chi ))$

(A2):

$\varphi \mathbin { \& }\psi \rightarrow \varphi$

(A3):

$\varphi \mathbin { \& }\psi \rightarrow \psi \mathbin { \& }\varphi$

(A4):

$\varphi \mathbin { \& }(\varphi \rightarrow \psi ) \rightarrow \psi \mathbin { \& }(\psi \rightarrow \varphi )$

(A5a):

$(\varphi \rightarrow (\psi \rightarrow \chi )) \rightarrow (\varphi \mathbin { \& }\psi \rightarrow \chi )$

(A5b):

$(\varphi \mathbin { \& }\psi \rightarrow \chi ) \rightarrow (\varphi \rightarrow (\psi \rightarrow \chi ))$

(A6):

$((\varphi \rightarrow \psi ) \rightarrow \chi ) \rightarrow (((\psi \rightarrow \varphi )\rightarrow \chi )\rightarrow \chi )$

(A7):

$\overline{0} \rightarrow \varphi$

  Other connectives are introduced as follows:

$$ \begin{aligned} \begin{array}{llrll} \varphi \wedge \psi &{}= \varphi \mathbin { \& }(\varphi \rightarrow \psi )&{}&{}\qquad \qquad \lnot \varphi &{}= \varphi \rightarrow \overline{0}\\ \varphi \vee \psi &{}= ((\varphi \rightarrow \psi ) \rightarrow \psi ) \wedge ((\psi \rightarrow \varphi )\rightarrow \varphi )&{}&{}\qquad \qquad \overline{1} &{}= \lnot \overline{0}\\ \varphi \leftrightarrow \psi &{}= (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi ) &{}&{}&{}\\ \end{array} \end{aligned}$$

Petr Hájek also introduced the corresponding algebraic semantics for his logic. A $\mathrm {BL}$ -algebra is an algebra ${\varvec{A}}=\langle {A,\wedge ,\vee ,\cdot ,\rightarrow ,0,1}\rangle$ such that

• $\langle {A,\wedge ,\vee ,0,1}\rangle$ is a bounded lattice

• $\langle {A,\cdot ,1}\rangle$ is a commutative monoid

• for each $a,b,c\in A$ we have

  $$\begin{aligned} \begin{array}{*{20}l} a\cdot b\leqslant c \quad \mathrm{iff} \quad b\leqslant a \rightarrow c &{} \qquad (\text {residuation})\\ (a \rightarrow b) \vee (b \rightarrow a) = 1 &{}\qquad (\text {prelinearity})\\ a \cdot (a\rightarrow b) = b \cdot (b\rightarrow a) &{}\qquad (\text {divisibility}) \end{array} \end{aligned}$$

We say that a $\mathrm {BL}$-algebra is:

• Linearly ordered (or $\mathrm {BL}$-chain) if its lattice order is total.

• Standard if its lattice reduct is the real unit interval [0, 1] ordered in the usual way.

Note that in a standard $\mathrm {BL}$-algebra $\mathbin { \& }$ is interpreted by a continuous t-norm and $\rightarrow$ by its residuum; and vice versa: each continuous t-norm fully determines its corresponding standard $\mathrm {BL}$-algebra.

Hájek proved completeness of $\mathrm {BL}$ with respect to $\mathrm {BL}$-algebras and $\mathrm {BL}$-chains and conjectured that $\mathrm {BL}$ should be also complete with respect to the standard $\mathrm {BL}$-algebras (i.e., the semantics given by all continuous t-norms). The conjecture was later proved true: Hájek himself showed the completeness by adding two additional axioms (Hájek 1998a) which later were shown to be derivable in $\mathrm {BL}$ (Cignoli et al. 2000). Therefore, $\mathrm {BL}$ could really be seen, at that time, as a basic fuzzy logic. Indeed, it was a genuine fuzzy logic because it retained what was then seen as the defining property of fuzzy logics: completeness with respect to a semantics based on continuous t-norms. And it was also basic in the following two senses:

• 1. it could not be made weaker without losing essential properties and

• 2. it provided a base for the study of all fuzzy logics.

The first item followed from the completeness of $\mathrm {BL}$ w.r.t. the semantics given by all continuous t-norms; thus, in a context of continuous t-norm based logics one could not possibly take a weaker system. The second meaning relied on the fact that the three main fuzzy logics ($\L$, $\mathrm {G}$, and $\Pi$) are all axiomatic extensions of $\mathrm {BL}$ and, in fact, the methods used by Hájek to introduce, algebraize, and study $\mathrm {BL}$ could be utilized for any other logic based on continuous t-norms. Actually, already  Hájek (1998b) developed a uniform mathematical theory for MFL. He considered all axiomatic extensions of $\mathrm {BL}$ (not just the three prominent ones) as fuzzy logics (he called them schematic extensions) and systematically studied their first-order extensions (inspired by  Rasiowa (1974)), extensions with modalities, complexity issues, etc.

Moreover, mainly thanks to the availability of good mathematical characterizations for continuous t-norms and $\mathrm {BL}$-chains, $\mathrm {BL}$ has turned out to be a crucial logical system giving rise to an intense research with lots of nice results obtained by many authors (for an up-to-date survey see Busaniche and Montagna (2011)). For these reasons, we want to take on the occasion of the present tribute volume to Petr Hájek to propose that both $\mathrm {BL}$ logic and $\mathrm {BL}$-algebras should rightfully be renamed after their creator as Hájek logic and Hájek algebras ($\mathrm {HL}$ and $\mathrm {HL}$-algebras, for short).

Another strong reason supporting abandoning the name ‘Basic Logic’ is that the development of MFL has shown that $\mathrm {HL}$ was actually not basic enough. That is, $\mathrm {HL}$ was indeed a good basic logic for the initial framework in which it was formulated, but the active research area that Hájek helped creating with his monograph and his weakest logical system soon expanded its horizons to broader frameworks which demanded a revision of the basic logic. Therefore, Hájek had not settled but only initiated the quest for the basic fuzzy logic.

The first step towards a broader point of view was taken by Esteva and Godo, who noticed that the necessary and sufficient condition for a t-norm to have a residuum is not continuity, but left-continuity. Inspired by this fact they introduced by Esteva and Godo (2001) the logic $\mathrm {MTL}$ (shorthand for Monoidal t-norm based Logic) as an attempt to axiomatize the standard semantics given by all residuated t-norms. It was introduced by means of a Hilbert-style calculus in the language ${\fancyscript{L}} = \{\mathbin { \& }, \rightarrow , \wedge , \overline{0}\}$ of type $\langle 2, 2, 2, 0 \rangle$, ($\wedge$ is no longer a derived connective and has to be considered as primitive). This calculus is the same as the one for $\mathrm {HL}$ only axiom (A4) is replaced by the following three axioms:  

(A4a):

$\varphi \wedge \psi \rightarrow \varphi$

(A4b):

$\varphi \wedge \psi \rightarrow \psi \wedge \varphi$

(A4c):

$\varphi \mathbin { \& }(\varphi \rightarrow \psi ) \rightarrow \varphi \wedge \psi$

 

Similarly to the previous cases, Esteva and Godo introduced a broader class of algebraic structures, $\mathrm {MTL}$-algebras (defined analogously to $\mathrm {HL}$-algebras but without requiring the fulfilment of the divisibility condition) and proved that $\mathrm {MTL}$ is complete both w.r.t. the semantics given by all $\mathrm {MTL}$-algebras and w.r.t. $\mathrm {MTL}$-chains. Moreover,  Jenei and Montagna (2002) indeed proved $\mathrm {MTL}$ to be complete with respect to the semantics given by all left-continuous (i.e. residuated) t-norms. Thus it was a better candidate than $\mathrm {HL}$ for a basic fuzzy logic, which could be retrieved as the axiomatic extension of $\mathrm {MTL}$ by axiom (A4).

1.2 Core Fuzzy Logics

In the broader framework for MFL promoted by Esteva and Godo, i.e. that of logics based on residuated t-norms, the system $\mathrm {MTL}$ indeed fulfilled our requirements for a basic fuzzy logic, as expressed in the previous subsection. It was a genuine fuzzy logic enjoying a standard completeness theorem w.r.t. a semantics based on left-continuous t-norms, it could not be made weaker without losing this property and all known fuzzy logics could be obtained as extensions of $\mathrm {MTL}$, thus providing a good base for a new systematical study of MFL. In fact, Petr Hájek saluted $\mathrm {MTL}$ as the new basic fuzzy logic and defined (Hájek and Cintula 2006) a precise general framework taking $\mathrm {MTL}$ as the basic system and not restricting to its axiomatic extensions (i.e. logics in the same language as $\mathrm {MTL}$) but rather to its axiomatic expansions (by allowing new additional connectives). In particular they introduced two classes of logics which, though not very broad from the general perspective of the whole logical landscape, are still large enough to cover the most studied fuzzy logics. These two classes have provided a useful framework for a general study of these logics and have been utilized in particular in the study of completeness of (propositional and first-order) fuzzy logics w.r.t. distinguished semantics  (Cintula et al. 2009) and the arithmetical complexity of first-order fuzzy logics  (Montagna and Noguera 2010). The rough idea was to capture, by simple syntactic means, a class of logics which share many desirable properties with $\mathrm {MTL}$.

Definition 12.1

A logic $\mathrm {L}$ in a language $\fancyscript{L}$ is a core fuzzy logic if:

• 1. $\mathrm {L}$ expands $\mathrm {MTL}$.

• 2. For all $\fancyscript{L}$-formulae $\varphi ,\psi ,\chi$ the following holds:⁴

  $$\begin{aligned} \varphi \leftrightarrow \psi \vdash _{\mathrm {L}}\chi \leftrightarrow \chi ', \end{aligned}$$

  (Cong)

  where $\chi '$ is a formula resulting from $\chi$ by replacing some occurrences of its subformula $\varphi$ by the formula $\psi$.

• 3. $\mathrm {L}$ has an axiomatic system with modus ponens as the only deduction rule.

Table 12.1 Some axiomatic extensions of $\mathrm {MTL}$ obtained by adding the corresponding additional axiom schemata

Table 12.2 Some usual axiom schemata in fuzzy logics

Therefore, core fuzzy logics are essentially well-behaved axiomatic expansions of $\mathrm {MTL}$.⁵ Observe, that since $\mathrm {MTL}$ is a finitary logic⁶ and we are only considering adding axioms, not rules, all core fuzzy logics remain finitary. Table 12.1 collects prominent members of the family of core fuzzy logics together with the axioms one needs to add to $\mathrm {MTL}$ to obtain them (see the definition of axioms in Table 12.2). An important logic, which does not fall under the scope of the previous definition, is the expansion of $\mathrm {MTL}$ with the Monteiro–Baaz projection connective $\triangle$ (Baaz 1996; Monteiro 1980). This logic, denoted as ${\mathrm {MTL}}_\triangle$, is obtained by adding the unary connective $\triangle$ to the language, the rule of $\triangle$ -Necessitation $({\mathrm {Nec}}_{\!\triangle })$—from $\varphi$ infer $\triangle \varphi$—and the following axioms:  

$(\triangle 1)$ :

$\triangle \varphi \vee \lnot \triangle \varphi$

$(\triangle 2)$ :

$\triangle (\varphi \vee \psi )\rightarrow \triangle \varphi \vee \triangle \psi$

$(\triangle 3)$ :

$\triangle \varphi \rightarrow \varphi$

$(\triangle 4)$ :

$\triangle \varphi \rightarrow \triangle \triangle \varphi$

$(\triangle 5)$ :

$\triangle (\varphi \rightarrow \psi )\rightarrow (\triangle \varphi \rightarrow \triangle \psi )$

 

Taking ${\mathrm {MTL}}_\triangle$ as an alternative basic logic, Hájek and Cintula defined another class of fuzzy logics, now with the $\triangle$ connective:

Definition 12.2

A logic $\mathrm {L}$ in a language $\fancyscript{L}$ is a $\triangle$ -core fuzzy logic if:

• 1. $\mathrm {L}$ expands ${\mathrm {MTL}}_\triangle$.

• 2. For all $\fancyscript{L}$-formulae $\varphi ,\psi ,\chi$ the following holds:

  $$\begin{aligned} \varphi \leftrightarrow \psi \vdash _{\mathrm {L}}\chi \leftrightarrow \chi ', \end{aligned}$$

  (Cong)

  where $\chi '$ is a formula resulting from $\chi$ by replacing some occurrences of its subformula $\varphi$ by the formula $\psi$.

• 3. $\mathrm {L}$ has an axiomatic system with modus ponens and $(\textit{Nec}_\triangle )$ as the only deduction rules.

Expansions of fuzzy logics with $\triangle$ were already systematically studied by Petr Hájek already in his seminal monograph (Hájek 1998b) and have since then been considered for most fuzzy logics, making the class of $\triangle$-core fuzzy logics another largely populated useful class.

Other well-known fuzzy logics in expanded languages fall under the scope of the two classes we have introduced, such as logics with truth-constants for intermediate truth-values (a Petr Hájek’s variant of the Pavelka’s extension of Łukasiewicz logic (Hájek 1998b; Pavelka 1979; Novák 1990) later studied in many works by other authors (Savický et al. 2006; Esteva et al. 2009;  (Esteva et al. 2011, Sect. 2))), logics $\mathrm {L}_{{\sim }}$ expanded with an extra involutive negation (again initiated by Petr Hájek and followed by others (Esteva et al. 2000; Cintula et al. 2006; Esteva et al. 2000; Flaminio and Marchioni 2006; Haniková and Savický 2008; (Esteva et al. 2011, Sect. 4))), or logics combining conjunctions and implications corresponding to different t-norms (Cintula 2003; Horčík and Cintula 2004; Montagna and Panti 2001; Esteva et al. 2001; (Esteva et al. 2011, Sect. 5)). On the other hand there are logics expanding $\mathrm {MTL}$ studied in the literature which are neither core nor $\triangle$-core because they need some additional deduction rules, the prominent examples being the logic ${\mathrm {PL}}$ $'$ (the extension of Łukasiewicz logic with an additional product-like conjunction which has no zero-divisors  (Horčík and Cintula 2004)) or logics with truth-hedges (Esteva et al. 2013).

Core and $\triangle$-core fuzzy logics are all finitary and well-behaved from several points of view. In particular, for every such logic $\mathrm {L}$ one can define in a natural way a corresponding class of algebraic structures, $\mathrm {L}$-algebras, which provide a complete semantics as in the case of $\mathrm {MTL}$ or the previously mentioned logics and, more importantly, the completeness theorem is preserved if we restrict ourselves to linearly ordered $\mathrm {L}$-algebras. Moreover, these classes of algebras are always varieties, i.e. they can be presented in terms of equations or, equivalently, are closed under formation of homomorphic images, subalgebras and direct products.

Another interesting property shared by the logics in these classes is the deduction theorem. Petr Hájek (1998b) already proved deduction theorems for several fuzzy logics, including his basic logic, and also for his expansions with $\triangle$. One can analogously obtain deduction theorems for all the logics in the classes just defined (in a local form for core fuzzy logics, global for $\triangle$-core):⁷

Theorem 12.1

• 1. Let $\mathrm {L}$ be a core fuzzy logic in a language $\fancyscript{L}$. For every $\varGamma \cup \{\varphi ,\psi \} \subseteq { Fm _{\fancyscript{L}}}$, $\varGamma ,\varphi \vdash _\mathrm {L} \psi$ iff there is $n \geqslant 0$ such that $\varGamma \vdash _\mathrm {L} \varphi ^n \rightarrow \psi$.

• 2. Let $\mathrm {L}$ be a core $\triangle$-fuzzy logic in a language $\fancyscript{L}$. For every $\varGamma \cup \{\varphi ,\psi \} \subseteq { Fm _{\fancyscript{L}}}$, $\varGamma ,\varphi \vdash _\mathrm {L} \psi$ iff $\varGamma \vdash _\mathrm {L} \triangle \varphi \rightarrow \psi$.

We will give more precise details both about algebraization of logics and about deduction theorems in Sect. 12.2.

1.3 Substructural Logics as a Framework for Fuzzy Logics

The quest for the basic fuzzy logic did not end with $\mathrm {MTL}$ (or ${\mathrm {MTL}}_\triangle$). Indeed, $\mathrm {MTL}$ has been further weakened in two different directions beyond the framework of core fuzzy logics:

• by dropping commutativity of conjunction Hájek (2003b) obtained the logic ${\mathrm {ps}}\mathrm {MTL}^r$ which Jenei and Montagna (2003) proved to be complete with respect to the semantics on non-commutative residuated t-norms,

• by removing integrality (i.e. not requiring the neutral element of conjunction to be maximum of the order) Metcalfe and Montagna (2007) proposed the logic $\mathrm {UL}$ which is, in turn, complete with respect to left-continuous uninorms.

Petr Hájek liked to describe this process of successive weakening of fuzzy logics by telling the joke of the crazy scientist that studied fleas by removing their legs one by one and checking whether they could still jump (Hájek 2005b).⁸ Namely, if $\mathrm {HL}$ was the original flea, it lost the ‘divisibility leg’ when it was substituted by $\mathrm {MTL}$, and then ${\mathrm {ps}}\mathrm {MTL}^r$ and $\mathrm {UL}$ respectively lost the ‘commutativity and the integrality leg’ while retaining the ability to ‘jump’ (i.e., the completeness w.r.t. intended semantics based on reals).

These weaker fuzzy logics (and even $\mathrm {MTL}$ itself (Esteva et al. 2003)) can be fruitfully studied in the context of substructural logics. Recall the bounded full Lambek logic ${\mathrm {FL}}$,⁹ a basic substructural logic which does not satisfy any of the usual three structural rules: exchange, weakening, and contraction. Although firstly presented by means of a Gentzen calculus, it can be given a Hilbert-style presentation and shown to be an algebraizable logic in the sense of Blok and Pigozzi (1989) whose equivalent algebraic semantics is the variety of bounded pointed lattice-ordered residuated monoids (usually referred to as bounded pointed residuated lattices or ${\mathrm {FL}}$ -algebras). Intuitionistic logic together with logics ${{\mathrm {FL}}}_{{\mathrm {e}}}$, ${{\mathrm {FL}}}_{\mathrm {w}},$ and ${{\mathrm {FL}}}_{{\mathrm {ew}}}$ are among the most prominent extensions of ${\mathrm {FL}}$. These logics are obtained by adding some of the structural rules and correspond to subvarieties of residuated lattices satisfying corresponding extra algebraic properties (Galatos et al. 2007). Actually, many fuzzy logics have been shown to be axiomatic extensions of some of these prominent substructural logics by adding some axioms that enforce completeness with respect to some class of linearly ordered residuated lattices (or chains). For instance, Gödel–Dummett logic is the logic of linearly ordered Heyting algebras (${{\mathrm {FL}}}_{{\mathrm {ewc}}}$-chains), $\mathrm {MTL}$ is the logic ${{\mathrm {FL}}}^\ell _{{\mathrm {e}}\mathrm {w}}$ of ${}{\mathrm {FL}_{\mathrm {ew}}^{}}$-chains,¹⁰ $\mathrm {UL}$ is the logic ${{\mathrm {FL}}}^\ell _{{\mathrm {e}}}$ of ${}{\mathrm {FL}_{\mathrm {e}}^{}}$-chains, and ${\mathrm {ps}}\mathrm {MTL}^r$ is the logic ${{\mathrm {FL}}}^\ell _{\mathrm {w}}$ of ${}{\mathrm {FL}_{\mathrm {w}}^{}}$-chains.

This common feature, completeness with respect to their corresponding linearly ordered algebraic structures, has motivated the methodological paper (Běhounek and Cintula 2006) where the authors postulate that fuzzy logics are the logics of chains, in the sense that they are logics complete with respect to a semantics of chains. However, all the fuzzy logics mentioned so far do enjoy a stronger property: the standard completeness theorem, i.e. completeness with respect to a semantics of algebras defined on the real unit interval $[0,1]$ which Petr Hájek and many others have considered to be the intended semantics for fuzzy logics. Following Hájek’s flea joke, we could say that those fleas are fuzzy logics that jump well provided that they satisfy standard completeness. Actually, many authors implicitly (and sometimes even explicitly, e.g. Metcalfe and Montagna (2007)) regard standard completeness as an essential requirement for fuzzy logics. It is, thus, reasonable to expect any candidate for the basic fuzzy logic to satisfy this stronger requirement. But, although they fulfill that, neither ${{{\mathrm {FL}}}}^\ell _{{\mathrm {e}}}$ nor ${{\mathrm {FL}}}^\ell _{\mathrm {w}}$ can be taken as basic because they are not comparable and hence do not satisfy our second meaning of basic. A reasonable candidate could be the logic ${\mathrm {{{\mathrm {FL}}}}^\ell }$ of ${\mathrm {FL}}$-chains (a common generalization of ${{\mathrm {FL}}}^\ell _{{\mathrm {e}}}$ and ${{\mathrm {FL}}}^\ell _{\mathrm {w}}$). But, interestingly enough, this logic does not enjoy the standard completeness (as proved by Wang and Zhao (2009)) and, therefore, we must discard it. Moreover, one can also argue that ${\mathrm {{{\mathrm {FL}}}}^\ell }$ is still not basic enough (in the first meaning) because it satisfies a remaining structural rule: associativity. Hence, in the context of substructural logics, it could still be made weaker by removing associativity.

There have actually been several studies on non-associative substructural logics, starting with the original Lambek non-associative calculus (Lambek 1961) (without lattice connectives), and followed (in the full language) e.g. by  Buszkowski and Farulewski (2009). Recently, a general algebraic framework to study fuzzy logics considered as a subfamily of (not necessarily associative) substructural logics has been developed by Cintula and Noguera (2011). It is based on the logic $\mathrm {SL}$, a non-associative version of the bounded Full Lambek calculus, introduced by Galatos and Ono (2010).¹¹ $\mathrm {SL}$ is formulated in the language ${\mathrm {\fancyscript{L}_{\mathrm SL}}}= \{\wedge ,\vee ,\mathbin { \& },\rightarrow ,\rightsquigarrow ,\overline{0},\overline{1},\bot \}$ (we also make use of the defined connectives $\varphi \leftrightarrow \psi = (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi )$ and $\top = \bot \rightarrow \bot$)¹² and axiomatized by means of the Hilbert-style calculus (Galatos and Ono 2010, Fig. 5) presented in Table 12.3.

Table 12.3 Axiomatic system of $\mathrm {SL}$

Moreover, Galatos and Ono proved that ${\mathrm {SL}}$ is an algebraizable logic whose equivalent algebraic semantics is the variety of bounded lattice-ordered residuated unital groupoids, where the monoidal structure of the previous logics has become just a groupoid on account of the lack of associativity (we will see more details in Sect. 12.2). Therefore, if we are looking for a logic complete with respect to standard chains in the non-associative context, it makes sense to consider, in a similar fashion as with ${\mathrm {FL}}$ and its extensions, the logic ${\mathrm {{\mathrm {SL}}}^\ell }$ as the logic of bounded linearly ordered residuated unital groupoids.

1.4 Goals and Outline of the Chapter

The main goal of this chapter is to propose $\mathrm {SL}^\ell$ as a new basic fuzzy logic. The current stage of development in MFL requires a broader framework than that provided by core and $\triangle$-core fuzzy logics. This is witnessed by several works (some already mentioned) dealing with fuzzy logics which either need some additional deduction rule or are weaker than $\mathrm {MTL}$, e.g. Botur (2011), Esteva et al. (2013), Gabbay and Metcalfe (2007), Hájek (2003a, b, c), Hájek and Ševčík (2004), Horčík and Cintula (2004), Jenei and Montagna (2003), Marchioni and Montagna (2008), Metcalfe and Montagna (2007), Wang and Zhao (2009). For this reason fuzzy logics have started being systematically studied in the context of (not necessarily associative) substructural logics by Cintula and Noguera (2011). However, this work did not offer a basic fuzzy logic in its framework.

On the other hand, $\mathrm {SL}^\ell$ has been introduced and studied as an axiomatic extension of $\mathrm {SL}$ in the recent paper (Cintula et al. 2013) where, among others, it has been shown to enjoy standard completeness. Based on these results we will defend here the thesis that $\mathrm {SL}^\ell$ can serve as a basic fuzzy logic, good enough for the current needs of MFL. We will argue that is genuinely fuzzy and basic in both senses mentioned earlier in this introduction. To this end, we introduce a new class of logics containing core and $\triangle$-core fuzzy logics and much more: core semilinear logics. The adjective ‘semilinear’ in the name of this class refers to a notion introduced by Cintula and Noguera (2010) in order to capture the idea of fuzzy logics as logics of chains proposed by Běhounek and Cintula (2006). The idea is the following: if a logic has a reasonable implication $\rightarrow$ (which is the case of $\mathrm {SL}$ and many of its expansions like core and $\triangle$-core fuzzy logics) then its corresponding algebraic structures can be ordered in terms of the implication ($a \leqslant b$ iff $a \rightarrow b \geqslant 1$); the logic is said to be semilinear iff it is complete w.r.t. the class of algebras where the order just defined is total. Moreover, the class of core semilinear logics contains both core and $\triangle$-core fuzzy logics and is defined in formally analogous way. Actually, the class of core semilinear logics provides a convenient intermediate level of generality, between that of core and $\triangle$-core fuzzy logics and that of weakly implicative semilinear logics of Cintula and Noguera (2011), by fixing ${\mathrm {SL}^\ell }$ (and, therefore, its language) as a common base and allowing for non-axiomatic extensions.

Outline of the chapter After this introduction that has presented the topic (historically and conceptually), the main logical systems, the classes of ($\triangle$-)core fuzzy logics, and the motivation for the forthcoming class of core semilinear logics,¹³ Section 12.2 presents, in mathematical details, the necessary logical and algebraic framework for our approach, which mainly restricts to substructural logics understood as well-behaved expansions of the non-associative logic $\mathrm {SL}$. Section 12.2.1 gives the basic notions, Sect. 12.2.2 presents the useful syntactical notion of almost $\mathrm {(MP)}$-based logics, and Sect. 12.2.3 is devoted to generation of filters, algebraization, and completeness w.r.t. (finitely) subdirectly irreducible algebras. Section 12.3, as the central part of the chapter, focuses on propositional core semilinear logics. After defining them, Sect. 12.3.1 shows several useful characterizations of semilinear logics and their axiomatizations, including a presentation of $\mathrm {SL}^\ell$ as axiomatic extension of $\mathrm {SL}$; Section 12.3.2 is a survey on completeness properties of core semilinear logics w.r.t. significant algebraic semantics, in particular we stress the standard completeness of $\mathrm {SL}^\ell$. Finally, Sect. 12.4 is devoted to first-order predicate counterparts of core semilinear logics, including ${\mathrm {{{{\mathrm {SL}^\ell }}\forall ^{}}}}$, the first-order extension of $\mathrm {SL}^\ell$. Section 12.4.1 shows the axiomatization of these logics, Sect. 12.4.2 presents their semantics based on general and witnessed models, and Sect. 12.4.3 focuses again on distinguished semantics, in particular stressing that ${\mathrm {{{{\mathrm {SL}^\ell }}\forall ^{}}}}$ enjoys standard completeness too.

2 Logical Framework

In order to deal with the classes of logics mentioned above, we need some flexibility as regards both propositional languages and logics. Therefore, for the sake of reference and in order to fix terminology in a convenient way for this chapter, we shall start with some standard general definitions and conventions.¹⁴

2.1 Basic Syntax and Semantics

In this chapter we consider logics as given by finitary Hilbert-style proof systems expanding that of $\mathrm {SL}$ (see Table 12.3 in the introduction). Following Hájek’s methodology, we restrict to finitary systems as he did when proposing schematic extensions of $\mathrm {HL}$ as a systematical approach to MFL. This does not undermine the suitability of our proposed basic logic $\mathrm {SL}^\ell$ (or its first-order counterpart) because the infinitary systems of fuzzy logic can still be retrieved as its extensions; we disregard them here for simplicity of presentation only.

A propositional language $\fancyscript{L}$ is a countable type, i.e. a function $ar:C_\fancyscript{L} \rightarrow \mathsf {N}$, where $C_\fancyscript{L}$ is a countable set of symbols called connectives, giving for each one its arity. Nullary connectives are also called truth-constants. We write $\langle {c,n}\rangle \in \fancyscript{L}$ whenever $c\in C_\fancyscript{L}$ and $ar(c) = n$. The basic language in this chapter is ${\mathrm {\fancyscript{L}_{\mathrm SL}}}$ with binary connectives $\wedge ,\vee ,\mathbin { \& },\rightarrow ,\rightsquigarrow$ and truth-constants $\overline{0},\overline{1},\bot$ (we also make use of the defined connectives $\top = \bot \rightarrow \bot$ and $\varphi \leftrightarrow \psi = (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi )$). Let ${Var}$ be a fixed infinite countable set of symbols called variables. The set ${ Fm _{\fancyscript{L}}}$ of formulae in a propositional language $\fancyscript{L}$ is the least set containing ${Var}$ and closed under connectives of $\fancyscript{L}$, i.e. for each $\langle {c,n}\rangle \in \fancyscript{L}$ and every $\varphi _1,\ldots ,\varphi _n \in { Fm _{\fancyscript{L}}}$, $c(\varphi _1,\ldots ,\varphi _n)$ is a formula. ${ Fm _{\fancyscript{L}}}$ can be seen as the domain of the absolutely free algebra ${ Fm _{\fancyscript{L}}}$ of type $\fancyscript{L}$ and generators ${Var}$. An $\fancyscript{L}$ -substitution is an endomorphism on the algebra ${ Fm _{\fancyscript{L}}}$, i.e. a mapping $\sigma :{ Fm _{\fancyscript{L}}}\rightarrow { Fm _{\fancyscript{L}}}$, such that $\sigma (c(\varphi _1,\ldots ,\varphi _n)) = c(\sigma (\varphi _1),\dots , \sigma (\varphi _n))$ holds for each $\langle {c,n}\rangle \in \fancyscript{L}$ and every $\varphi _1,\ldots ,\varphi _n \in { Fm _{\fancyscript{L}}}$. Since an $\fancyscript{L}$-substitution is a mapping whose domain is a free $\fancyscript{L}$-algebra, it is fully determined by its values on the generators (propositional variables).

An axiomatic system ${\fancyscript{A}}\!{\fancyscript{S}}$ in a propositional language ${\fancyscript{L}}$ is a pair $\langle {Ax,R}\rangle$ where $Ax$ is set of formulae (the axioms) and $R$ is a set of pairs $\langle {\varGamma ,\varphi }\rangle$ (the rules) where $\varGamma$ is a finite non-empty set of formulae and $\varphi$ is a formula.¹⁵ Moreover, both $Ax$ and $R$ are closed under arbitrary substitutions. Given $\varGamma \cup \{\varphi \} \subseteq { Fm _{\fancyscript{L}}}$, we say that $\varphi$ is provable from $\varGamma$ in ${\fancyscript{A}}\!{\fancyscript{S}}$, in symbols $\varGamma \vdash _{\!{\fancyscript{A}}\!{\fancyscript{S}}} \varphi$, if there exists a finite sequence of formulae $\langle {\varphi _0, \ldots , \varphi _n}\rangle$ (a proof) such that:

• $\varphi _ n = \varphi$, and

• for every $i \leqslant n$, either $\varphi _i \in \varGamma \cup Ax$ or there is some rule $\langle {\Delta ,\varphi _i}\rangle \in R$ such that $\Delta \subseteq \{\varphi _0, \ldots , \varphi _{i-1}\}$.

Observe that the provability relation $\vdash _{\!{\fancyscript{A}}\!{\fancyscript{S}}}$ is finitary, i.e., if $\varGamma \vdash _{\!{\fancyscript{A}}\!{\fancyscript{S}}}\varphi$, then there is a finite $\varGamma '\subseteq \varGamma$ such that $\varGamma '\vdash _{\!{\fancyscript{A}}\!{\fancyscript{S}}}\varphi$.

Let $\fancyscript{L}_1 \subseteq \fancyscript{L}_2$ be propositional languages and ${\fancyscript{A}}\!{\fancyscript{S}}_{\!i}$ an axiomatic system in $\fancyscript{L}_i$. We say that ${\fancyscript{A}}\!{\fancyscript{S}}_{\!2}$ is an expansion of ${\fancyscript{A}}\!{\fancyscript{S}}_{\!1}$ by axioms $Ax$ and rules $R$ if all its axioms (rules) are $\fancyscript{L}_2$-substitutional instances of axioms (rules) of ${\fancyscript{A}}\!{\fancyscript{S}}_{\!1}$ or formulae from $Ax$ (rules from $R$).

Now we are ready to give our formal convention restricting logics to finitary expansions of $\mathrm {SL}$ with well-behaved connectives.

Convention 12.2

A logic $\mathrm {L}$ in a language $\fancyscript{L} \supseteq {\mathrm {\fancyscript{L}_{\mathrm SL}}}$ is the provability relation given by an axiomatic system ${\fancyscript{A}}\!{\fancyscript{S}}$ in $\fancyscript{L}$ which is an expansion of that of $\mathrm {SL}$ (see Table 12.3) and for all $\fancyscript{L}$-formulae $\varphi ,\psi ,\chi$ the following holds:

$$\begin{aligned} \varphi \leftrightarrow \psi \vdash _{{\fancyscript{A}}\!{\fancyscript{S}}}\chi \leftrightarrow \chi ', \end{aligned}$$

(Cong)

where $\chi '$ is a formula resulting from $\chi$ by replacing some occurrences of its subformula $\varphi$ by a formula $\psi$. In this case we say that ${\fancyscript{A}}\!{\fancyscript{S}}$ is a presentation of $\mathrm {L}$ (or that $\mathrm {L}$ is axiomatized by ${\fancyscript{A}}\!{\fancyscript{S}}$) and write $\varGamma \vdash _\mathrm {L} \varphi$ instead of $\varGamma \vdash _{{\fancyscript{A}}\!{\fancyscript{S}}} \varphi$.

Remark 12.1

One can equivalently replace the condition $({\mathrm {Cong}})$ by the following:

$$\begin{aligned} \varphi \leftrightarrow \psi \vdash _{{\fancyscript{A}}\!{\fancyscript{S}}} c(\chi _1,\dots ,\chi _{i}, \varphi ,\dots ,\chi _n)\leftrightarrow c(\chi _1,\dots ,\chi _{i}, \psi ,\dots ,\chi _n) \qquad (\text {Cong}^{i}_{c}) \end{aligned}$$

for each $\langle c,n\rangle \in \fancyscript{L}$ and each $0 \leqslant i < n$. Therefore, since this condition is already satisfied in $\mathrm {SL}$ for all its connectives, in order to check whether a particular expansion of $\mathrm {SL}$ is a logic in the sense just defined, it is enough to check $({\mathrm {Cong}}^i_c)$ for all new connectives (this statement remains true if we replace $\mathrm {SL}$ by any other logic).

The notion of expansion can naturally be formulated for logics. Let $\fancyscript{L}_1 \subseteq \fancyscript{L}_2$ be propositional languages and $\mathrm {L_i}$ a logic in $\fancyscript{L}_i$. We say that

• $\mathrm {L_2}$ is the expansion of $\mathrm {L_1}$ by axioms $Ax$ and rules $R$ if it is axiomatized by expanding some presentation of $\mathrm {L}_1$ with axioms $Ax$ and rules $R$.

• $\mathrm {L_2}$ is an (axiomatic) expansion of $\mathrm {L_1}$ if it is the expansion of $\mathrm {L_1}$ by some axioms and rules (or just axioms respectively).

If $\fancyscript{L}_1=\fancyscript{L}_2$, we use the term ‘extension’ instead of ‘expansion’. Let ${\fancyscript{S}}$ be a collection of extensions of a given logic $\mathrm {L}$. We define the following two axiomatic systems and two logics:

$$ \begin{array}{ll} \bigcap {\fancyscript{S}} = \{ \langle {\varGamma ,\varphi }\rangle \mid \varGamma \vdash _\mathrm {L}\varphi \text { for each } \mathrm {L}\in {\fancyscript{S}}\} &{} \qquad \qquad \bigwedge {\fancyscript{S}} = {\vdash _{\bigcap {}{\fancyscript{S}}}} \\ \bigcup {\fancyscript{S}} = \{ \langle {\varGamma ,\varphi }\rangle \mid \varGamma \vdash _\mathrm {L}\varphi \text { for some } \mathrm {L}\in {\fancyscript{S}}\} &{} \qquad \qquad \bigvee {\fancyscript{S}} = {\vdash _{\bigcup {}{\fancyscript{S}}}} \end{array} $$

It is clear that $\bigwedge {}{\fancyscript{S}}$ and $\bigvee {}{\fancyscript{S}}$ are respectively the infimum and the supremum of ${\fancyscript{S}}$ in the set of extensions of $\mathrm {L}$ ordered by inclusion. Therefore, the set of extensions of a given logic $\mathrm {L}$ always forms a complete lattice. Note that $\bigvee {}{\fancyscript{S}}$ can be axiomatized by taking the union of arbitrary axiomatic systems for the logics in ${\fancyscript{S}}$. Thus, in particular, if all logics in ${\fancyscript{S}}$ are axiomatic extensions of $\mathrm {L}$, then so is $\bigvee {}{\fancyscript{S}}$. Therefore, the class of axiomatic extensions of $\mathrm {L}$ is a sub-join-semilattice of the lattice of all extensions of $\mathrm {L}$. The axiomatization of meets is not so straightforward; at the end of Sect. 12.3.1 we will see how to deal with this problem in the restricted setting of core semilinear logics.

Some important axiomatic extensions of $\mathrm {SL}$ are obtained by adding the axioms $\mathrm {a}_1,\mathrm {a}_2,{\mathrm {e}},\mathrm {c},\mathrm {i}, \mathrm {o}$ corresponding to structural rules (see Table 12.4).

Table 12.4 Axioms for structural rules

Given any $S\subseteq \{\mathrm {\mathrm {a}_1,\mathrm {a}_2,{\mathrm {e}},\mathrm {c},\mathrm {i},\mathrm {o}\}}$, by ${\mathrm {SL}}_S$ we denote the axiomatic extension of $\mathrm {SL}$ by $S$. If $\{\mathrm {a}_1,\mathrm {a}_2\} \subseteq S$, then instead of them we write the symbol ‘$\mathrm {a}$’. Analogously if $\{\mathrm {i},\mathrm {o}\} \subseteq S$, instead of them we write the symbol ‘$\mathrm {w}$’. Equivalent ways to formulate these axioms are known (Cintula and Noguera 2011, Theorem 2.5.7.). ${\mathrm {SL}}_\mathrm {a}$ is, in fact, the bounded full Lambek logic. Next, we introduce the basic algebraic notions that will allow to provide a semantics for our logics.

Definition 12.3

A bounded pointed lattice-ordered residuated unital groupoid, or shortly just $\mathrm {SL}$ -algebra, is an algebra ${\varvec{A}}=\langle {A,\wedge ,\vee ,\cdot ,\backslash ,/,0,1,\bot ,\top }\rangle$ such that

• $\langle {A,\wedge ,\vee ,\bot ,\top }\rangle$ is a bounded lattice

• $1$ is the unit of $\cdot$

• for each $a,b,c\in A$ we have

  $$ a\cdot b\leqslant c\quad {\mathrm {iff}}\quad b\leqslant a\backslash c\quad {\mathrm {iff}}\quad a\leqslant c/b\,. $$

The class of all $\mathrm {SL}$-algebras is a variety and it is denoted as $\mathbb {SL}$. Observe that the residuation condition together with the fact that $1$ is a neutral element implies that for every $\mathrm {SL}$-algebra ${\varvec{A}}$ and each $a,b \in A$ we have

$$ a\leqslant b\quad {\mathrm {iff}}\quad 1\leqslant a\backslash b\quad {\mathrm {iff}}\quad 1\leqslant b/a\,. $$

Given an $\mathrm {SL}$-algebra ${\varvec{A}}=\langle {A,\wedge ,\vee ,\cdot ,\backslash ,/,0,1,\bot ,\top }\rangle$, an ${\varvec{A}}$ -evaluation is a homomorphism from the algebra of formulae to ${\varvec{A}}$ such that the connectives $\wedge ,\vee ,\mathbin { \& },\rightarrow , \rightsquigarrow , \overline{0},\overline{1},\bot ,\top$ are respectively interpreted by the functions $\wedge ,\vee ,\cdot ,\backslash ,/,0,1,\bot ,\top$, i.e., a mapping from ${ Fm _{\fancyscript{L}}}$ to $A$ such that $e(*) = *$ for ${*}\in \{0,1,\bot ,\top \}$ and $e(\varphi \mathbin {\circ } \psi ) = e(\varphi ) \mathbin {{\circ }'} e(\psi )$, where ${\circ }\in \{\wedge ,\vee ,\mathbin { \& },\rightarrow ,\rightsquigarrow \}$ and ${\circ }'$ is the corresponding operation from $\{\wedge ,\vee ,\cdot ,\backslash ,/\}$.¹⁶ By means of this notion, we can give, more generally, the following definition for the algebraic counterpart of any logic.

Definition 12.4

Let $\mathrm {L}$ be a logic in language $\fancyscript{L}$ which is the expansion of $\mathrm {SL}$ by axioms $Ax$ and rules $R$. An $\fancyscript{L}$-algebra ${\varvec{A}}$ is an $\mathrm {L}$-algebra if

• its reduct ${\varvec{A}}_{\mathrm {SL}}=\langle {A,\wedge ,\vee ,\cdot ,\backslash ,/,0,1,\bot ,\top }\rangle$ is an $\mathrm {SL}$-algebra,

• for every $\varphi \in Ax$ and every ${\varvec{A}}$-evaluation $e$, $e(\varphi ) \geqslant 1$,

• for each $\langle {\varGamma ,\varphi }\rangle \in R$ and each ${\varvec{A}}$-evaluation $e$, if $e(\psi ) \geqslant 1$ for all $\psi \in \varGamma$, then $e(\varphi ) \geqslant 1$.

${\varvec{A}}$ is a linearly ordered (or $\mathrm {L}$ -chain) if its lattice order is total. The class of all (linearly ordered) $\mathrm {L}$-algebras is denoted by $\mathbb {L}$ (or ${{\mathbb {L}}_ lin }$ respectively).

Table 12.5 Equations defining important classes of $\mathrm {SL}$-algebras

Table 12.5 shows what equations have to be added to SL-algebras, to obtain, for arbitrary $S\subseteq$ $\{$a$_1$, a$_2$, e, c, i, o$\}$, the class of SL$_S$-algebras.

The following completeness theorem follows from more general results (see Sect. 12.2.3 where we show more on the connection between logics and algebras) but can also be directly proved by means of the usual Lindenbaum–Tarski process. It shows how $\mathrm {L}$-algebras really give an algebraic semantics for $\mathrm {SL}$ and its expansions.

Theorem 12.3

Let $\mathrm {L}$ be a logic. Then for every set of formulae $\varGamma$ and every formula $\varphi$ the following are equivalent:

• 1. $\varGamma \vdash _\mathrm {L} \varphi$,

• 2. for every ${\varvec{A}} \in \mathbb {L}$ and every ${\varvec{A}}$-evaluation $e$, if $e(\psi ) \geqslant 1$ for every $\psi \in \varGamma$, then $e(\varphi ) \geqslant 1$.

2.2 Almost $\mathrm {(MP)}$-Based Logics and Deduction Theorems

In the introduction we have formulated the usual deduction theorems for core and $\triangle$-core fuzzy logics (Theorem 12.1). In this section we show how this can be generalized to all logics in the present framework (expansions of $\mathrm {SL}$) provided that the additional rules they satisfy are of a suitable form. Technically, this corresponds to the notion of almost $\mathrm {(MP)}$-based logic that, as shown by Cintula et al. (2013), essentially allows to repeat Hájek’s original proof of deduction theorem now in this wide context. To this end, we introduce a few more syntactical notions. Let $\star$ be a new propositional variable not occurring in $Var$, which acts as placeholder for a special kind of substitutions. The notions of formula and substitution are augmented by the prefix $\star$- whenever they are construed over the set of variables ${Var} \cup \{\star \}$ and are left as they are if construed in the original set of variables ${Var}$. If $\varphi$ and $\delta$ are $\star$-formulae, by $\delta (\varphi )$ we denote the formula obtained from $\delta$ when one replaces the occurrences of $\star$ by $\varphi$; note that if $\varphi$ is a formula, then so is $\delta (\varphi )$ (i.e., $\star$ does not occur in $\delta (\varphi )$).

Definition 12.5

Given a set of $\star$-formulae $\varGamma$, we define the sets $\varGamma ^*$ and $\Pi (\varGamma )$ of $\star$-formulae:

• $\varGamma ^*$ is the smallest set containing $\star$ and $\delta (\gamma )\in \varGamma ^*$ for each $\delta \in \varGamma$ and each $\gamma \in \varGamma ^*$.

• $\Pi (\varGamma )$ is the smallest set of $\star$-formulae containing $\varGamma \cup \{\overline{1}\}$ and closed under $\mathbin { \& }$.

We are now ready to give the formal definition of almost $\mathrm {(MP)}$-based logic.

Definition 12.6

Let ${\mathrm {bDT}}$ be a set of $\star$-formulae closed under all $\star$-substitutions $\sigma$ such that $\sigma (\star ) =\star$. A logic $\mathrm {L}$ is almost $\mathrm {(MP)}$ -based w.r.t. the set of basic deduction terms ${\mathrm {bDT}}$ if:

• $\mathrm {L}$ has a presentation where the only deduction rules are modus ponens and those of the form $\langle {\varphi , \gamma (\varphi )}\rangle$ for $\gamma \in {\mathrm {bDT}}$, and

• for each $\beta \in {\mathrm {bDT}}$ and each formulae $\varphi ,\psi$, there exist $\beta _1,\beta _2\in {\mathrm {bDT}}^*$ such that:¹⁷

  $$ \vdash _{\mathrm {L}} \beta _1(\varphi \mathbin \rightarrow \psi ) \mathbin \rightarrow (\beta _2(\varphi ) \mathbin \rightarrow \beta (\psi )). $$

$\mathrm {L}$ is called $\mathrm {(MP)}$ -based if it admits the empty set as a set of basic deduction terms.

Table 12.6 New axiomatic system for $\mathrm {SL}$

$\mathrm {SL}$ can be shown to be indeed an almost $\mathrm {(MP)}$-based logic. For this, of course, one needs to endow it with a convenient alternative presentation. Consider the axiomatic system from Table 12.6 and let us introduce a convenient notation for the terms appearing on the right-hand side of the rules $(\alpha )$, $(\alpha ')$, $(\beta )$, and $(\beta ')$. Given arbitrary formulae $\delta ,\varepsilon$, we define the following $\star$-formulae:

$$ \begin{aligned} \alpha _{\delta ,\varepsilon }&= \delta \mathbin { \& }\varepsilon \rightarrow \delta \mathbin { \& }(\varepsilon \mathbin { \& }\star )&\beta _{\delta ,\varepsilon }&= \delta \rightarrow (\varepsilon \rightarrow (\varepsilon \mathbin { \& }\delta ) \mathbin { \& }\star )\\ \alpha '_{\delta ,\varepsilon }&= \delta \mathbin { \& }\varepsilon \rightarrow (\delta \mathbin { \& }\star ) \mathbin { \& }\varepsilon&\beta '_{\delta ,\varepsilon }&= \delta \rightarrow (\varepsilon \rightsquigarrow (\delta \mathbin { \& }\varepsilon ) \mathbin { \& }\star ) \end{aligned}$$

Note that the terms in the second line generalize the well-known notions of left and right conjugates used in associative logics:¹⁸

$$ \lambda _{\varepsilon } = \varepsilon \rightarrow \star \mathbin { \& }\varepsilon \qquad \qquad \rho _{\varepsilon } = \varepsilon \rightsquigarrow \varepsilon \mathbin { \& }\star $$

Cintula et al. (2013) proved that the axiomatic system from Table 12.6 is indeed a presentation of $\mathrm {SL}$, therefore we can obtain the following result for $\mathrm {SL}$ and some of its notable axiomatic extension (it also shows how the sets of basic deduction terms, and so posteriorly the axioms systems, of these extensions can be simplified).

Theorem 12.4

((Cintula et al. 2013, Sect. 3.1)) Let $S\subseteq \{\mathrm {\mathrm {a},{\mathrm {e}},\mathrm {w}\}}$. Then any axiomatic extension of the logic ${\mathrm {SL}}_S$ is almost $\mathrm {(MP)}$-based with respect to the corresponding set of basic deduction terms listed in Table 12.7.

Table 12.7 ${\mathrm {bDT}}$s of prominent substructural logics

Theorem 12.5

(Local deduction theorem ((Cintula et al. 2013, Corollary 3.12))) Let $\mathrm {L}$ be an almost $\mathrm {(MP)}$-based logic with a set of basic deduction terms ${\mathrm {bDT}}$. Then for each set $\varGamma$ of formulae and each formulae $\varphi$ and $\psi$ the following holds:

$$ \varGamma ,\varphi \vdash _\mathrm {L} \psi \qquad \text{ iff }\qquad \varGamma \vdash _{\mathrm {L}} \gamma (\varphi ) \mathbin \rightarrow \psi \text{ for } \text{ some } \gamma \in \Pi ({\mathrm {bDT}}^*). $$

Therefore, we obtain a (parameterized or non-parameterized, depending on the presence of variables other than $\star$ in the set ${\mathrm {bDT}}$) local deduction theorem for $\mathrm {SL}$ and its axiomatic extensions (sometimes with a simplified set ${\mathrm {bDT}}$; see Table 12.7).

2.3 Consequences of Algebraization

Given a logic $\mathrm {L}$ in a language $\fancyscript{L}$ and an $\fancyscript{L}$-algebra ${\varvec{A}}$, a set $F \subseteq A$ is an $\mathrm {L}$ -filter if for every set of formulae $\varGamma \cup \{\varphi \}$ such that $\varGamma \vdash _\mathrm {L} \varphi$ and every ${\varvec{A}}$-evaluation $e$ it holds: if $e[\varGamma ] \subseteq F$, then $e(\varphi ) \in F$. By $\fancyscript{F}i_{\mathrm {L}}({\varvec{A}})$ we denote the set of all $\mathrm {L}$-filters over ${\varvec{A}}$. Since $\fancyscript{F}i_{\mathrm {L}}({\varvec{A}})$ is a closure system (it clearly contains $A$ and is closed under arbitrary intersections), one can define a notion of generated filter. Given $X \subseteq A$, the $\mathrm {L}$-filter generated by $X$, denoted as ${\mathrm {Fi}}^{\varvec{A}}_\mathrm {L}(X)$ is the least $\mathrm {L}$-filter containing $X$ (we omit the indexes when clear from the context). With this terminology one can also prove a semantical (or transferred) version of (parameterized) local deduction theorem; Theorem 12.5 is the particular case in which ${\varvec{A}}$ is the algebra of formulae (observe that in this case $\varphi \in {\mathrm {Fi}}(\varGamma )$ iff $\varGamma \vdash _\mathrm {L}\varphi$). First we introduce two technical notions:

Definition 12.7

Given a set of $\star$-formulae $\varGamma$, an $\mathrm {SL}$-algebra ${\varvec{A}}$, and a set $X\subseteq A$, we define

• $\varGamma ^{\varvec{A}}$ as the set of unary polynomials built using terms from $\varGamma$ with coefficients from $A$ and variable $\star$, i.e., $\{\delta (\star ,a_1,\dots , a_n) \mid \delta (\star ,p_1,\dots , p_n)\in \varGamma \text { and } a_1,\dots , a_n \in ~A\}$.

• $\varGamma ^{\varvec{A}}(X)$ as the set $\{\delta ^{\varvec{A}}(x) \mid \delta (\star )\in \varGamma ^{\varvec{A}} \text { and } x\in X\}$.

Theorem 12.6

(Cintula et al. 2013, Theorem 3.11) Let $\mathrm {L}$ be an almost $\mathrm {(MP)}$-based logic in a language $\fancyscript{L}$ with a set of basic deduction terms ${\mathrm {bDT}}$. Let ${\varvec{A}}$ be an $\fancyscript{L}$-algebra and $X \cup \{x\} \subseteq A$. Then

$$y \in {\mathrm {Fi}}^{\varvec{A}}_\mathrm {L}(X,x) \qquad \text{ iff }\qquad \gamma ^{\varvec{A}}(x) \backslash y \in {\mathrm {Fi}}^{\varvec{A}}_\mathrm {L}(X) \text{ for } \text{ some } \gamma \in (\Pi ({\mathrm {bDT}}^*))^{\varvec{A}}.$$

On the other hand, Theorem 12.6 can be used to obtain a general form of the usual algebraic description of the filter generated by a set.

Corollary 12.1

(Cintula et al. 2013, Corollary 3.13) Let $\mathrm {L}$ be an almost $\mathrm {(MP)}$-based logic with a set of basic deduction terms ${\mathrm {bDT}}$. Let ${\varvec{A}}$ be an $\mathrm {L}$-algebra and $X \subseteq A$. Then

$$ {\mathrm {Fi}}^{\varvec{A}}_\mathrm {L}(X) = \{a \in A \mid a \geqslant x\ \text {for some}\ x \in (\Pi ({\mathrm {bDT}}^{*}))^{\varvec{A}}(X)\}\,. $$

The algebraic completeness result we have seen above (Theorem 12.3) can be strengthened obtaining that $\mathrm {SL}$ is actually an algebraizable logic in the sense of Blok and Pigozzi (1989) and $\mathbb {SL}$ is its equivalent algebraic semantics with translations $\rho (p \approx q) = p\leftrightarrow q$ and $\tau (p) = p \wedge \overline{1} \approx \overline{1}$. Indeed, if we consider formal equations in the language ${\mathrm {\fancyscript{L}_{\mathrm SL}}}$ as expressions of the form $\varphi \approx \psi$ where $\varphi ,\psi \in Fm_{\mathrm {\fancyscript{L}_{\mathrm SL}}}$ and if $\vDash _\mathbb {SL}$ denotes the equational consequence with respect to the class $\mathbb {SL}$, it is easy to prove that:

• 1. $\Pi \vDash _\mathbb {SL} \varphi \approx \psi$ iff $\rho [\Pi ] \vdash _{\mathrm {SL}}\rho (\varphi \approx \psi )$

• 2. $p \vdash _{\mathrm {SL}}\rho [\tau (p)]$ and $\rho [\tau (p)]\vdash _{\mathrm {SL}}p$

Actually, this result can be extended to every logic $\mathrm {L}$ and its corresponding class of algebras $\mathbb {L}$. If $\mathrm {L}$ is a logic in a language $\fancyscript{L}$ which is the expansion of $\mathrm {SL}$ by axioms $Ax$ and rules $R$, then $\mathrm {L}$-algebras can also be described as the expansions of $\mathrm {SL}$-algebras satisfying:

• the equation $\tau (\varphi )$ for each $\varphi \in Ax$

• the quasiequation $\tau (\varphi _1)\ \mathsf {and}\ \ldots \ \mathsf {and}\ \tau (\varphi _n) \Rightarrow \tau (\varphi )$ for each $\langle {\{\varphi _1, \ldots , \varphi _n\}, \varphi }\rangle$ from $R$.

Therefore, the class $\mathbb {L}$ is always a quasivariety and it is a variety if $R = \emptyset$, i.e. if $\mathrm {L}$ is an axiomatic expansion of $\mathrm {SL}$ (note that this condition is not necessary as demonstrated e.g. by the logic $\mathrm {MTL}$ $_\triangle$). Conversely, given a quasivariety $\mathbb {L}$ of $\fancyscript{L}$-algebras, one can always find a quasiequational base obtained by adding a set of equations $E$ and a set of quasiequations $Q$ to an equational base of $\mathbb {SL}$. Then $\mathbb {L}$ is the equivalent algebraic semantics of the logic obtained as the expansion of ${\mathrm {SL}}$ by

• the axiom $\rho (\varphi ,\psi )$ for each equation $\varphi \approx \psi \in E$

• the rule $\langle {\{\rho (\varphi _1,\psi _1), \ldots , \rho (\varphi _n,\psi _n)\}, \rho (\varphi ,\psi )}\rangle$ for each quasiequation $(\varphi _1 \approx \psi _1)\, \mathsf {and}\, \ldots \, \mathsf {and}\ (\varphi _n \approx \psi _n) \Rightarrow {\varphi \mathbin {\approx } \psi } \in Q$.

Moreover, if we fix a language $\fancyscript{L} \supseteq {\mathrm {\fancyscript{L}_{\mathrm SL}}}$ and a logic $\mathrm {L}$ in $\fancyscript{L}$, the translations $\tau$ and $\rho$ between formulae and equations give a bijective correspondence between extensions of $\mathrm {L}$ and quasivarieties of $\mathrm {L}$-algebras, and a bijective correspondence (its restriction) between axiomatic extensions of $\mathrm {L}$ and varieties of $\mathrm {L}$-algebras. These bijections are, actually, dual lattice isomorphisms.

A logic is called strongly algebraizable if its corresponding quasivariety is actually a variety. Obviously, strongly algebraizable logics in ${\mathrm {\fancyscript{L}_{\mathrm SL}}}$ coincide with axiomatic extensions of $\mathrm {SL}$.

Algebraizability also gives a strong correspondence between filters and (relative) congruences in $\mathrm {L}$-algebras, which can be made explicit using the particular forms of the translations. Let ${\varvec{{Con}}}_{\mathbb {L}}({\varvec{A}})$ denote the lattice of congruences of ${\varvec{A}}$ relative to $\mathbb {L}$, i.e. those giving a quotient in $\mathbb {L}$. If $\mathbb {L}$ is a variety, then ${\varvec{{Con}}}_{\mathbb {L}}({\varvec{A}})$ is precisely the lattice of all congruences of ${\varvec{A}}$. The Leibniz operator $\varOmega _{\varvec{A}}$ is defined, for any $F \in \fancyscript{F}i_{\mathrm {L}}({\varvec{A}})$, as $\varOmega _{\varvec{A}}(F) = \{\langle {a,b}\rangle \in A^2 \mid a \backslash b \in F \text { and } b \backslash a \in F \}$. Now we can state a specific variant of a well-known theorem of abstract algebraic logic (Czelakowski 2001), narrowed down to our setting.

Proposition 12.1

Let $\mathrm {L}$ be a logic and ${\varvec{A}}$ an $\mathrm {L}$-algebra. The Leibniz operator $\varOmega _{\varvec{A}}$ is a lattice isomorphism from $\fancyscript{F}i_{\mathrm {L}}({\varvec{A}})$ to ${\varvec{{Con}}}_{\mathbb {L}}({\varvec{A}})$. Its inverse is the function that maps any $\theta \in {\varvec{{Con}}}_{\mathbb {L}}({\varvec{A}})$ to the filter $\{a \in A \mid \langle {a \wedge 1, 1}\rangle \in \theta \}$.

Observe that the minimum filter is the one generated by the emptyset, ${\mathrm {Fi}}(\emptyset )$, and it must correspond to the identity congruence $Id_{\varvec{A}}$. Therefore, using the previous proposition, we obtain that, on any $\mathrm {L}$-algebra ${\varvec{A}}$, ${\mathrm {Fi}}(\emptyset ) = \{a \in A \mid a \geqslant 1\}$. This set is, of course, contained in any other filter. It is also worth noting that Proposition 12.1 and Corollary 12.1 give a description of the relative principal congruence generated by a pair of elements of a given algebra of an almost $\mathrm {(MP)}$-based logic.

Finally, we focus on a restriction of the completeness theorem (Theorem 12.3) to a couple of subclasses of algebraic models that will play an important rôle when characterizing semilinearity in the next section: relatively (finitely) subdirectly irreducible algebras. Given a class of algebras $\mathbb {K}$ an algebra ${\varvec{A}}$ is (finitely) subdirectly irreducible relative to $\mathbb {K}$ if for every (finite non-empty) subdirect representation $\alpha$ of ${\varvec{A}}$ with a family $\{{\varvec{A}}_i \mid i \in I\} \subseteq \mathbb {K}$ there is $i \in I$ such that $\pi _i \circ \alpha$ is an isomorphism. The class of all (finitely) subdirectly irreducible algebras relative to $\mathbb {K}$ is denoted as $\mathbb {K}_{\mathrm {R(F)SI}}$. Of course $\mathbb {K}_\mathrm {RSI}\subseteq \mathbb {K}_\mathrm {RFSI}$. Observe that the trivial algebra is by definition in $\mathbb {K}_\mathrm {RFSI}$ but not in $\mathbb {K}_\mathrm {RSI}$. Again, the next theorem is a specific variant of a well-known fact of abstract algebraic logic.

Theorem 12.7

Let $\mathrm {L}$ be a logic. Then for every set of formulae $\varGamma$ and every formula $\varphi$ the following are equivalent:

• 1. $\varGamma \vdash _\mathrm {L} \varphi$,

• 2. for every countable ${\varvec{A}} \in \mathbb {L}_\mathrm {RSI}$ and every ${\varvec{A}}$-evaluation $e$, if $e(\psi ) \geqslant 1$ for every $\psi \in \varGamma$, then $e(\varphi ) \geqslant 1$.

3 Core Semilinear Logics

Let us start by recalling two notions mentioned in the introduction: first we give a formal semantical definition of the logic $\mathrm {SL}^\ell$ (later in Theorem 12.12 we present some of its natural axiomatizations).

Definition 12.8

The logic ${\mathrm {SL}^\ell }$ is defined as follows for every set $\varGamma$ of formulae and every formula $\varphi$:

• 1. $\varGamma \vdash _{\mathrm {SL}^\ell }\varphi$ if and only if

• 2. $e(\varphi ) \geqslant 1$ for each ${\mathrm {SL}}$ -chain ${\varvec{A}}$ and each ${\varvec{A}}$-evaluation $e$ such that $e(\psi )\geqslant 1$ for all $\psi \in \varGamma$.

Remark 12.2

Clearly ${\mathrm {SL}^\ell }$ extends $\mathrm {SL}$ and so ((Cintula and Noguera 2011, Propositions 3.1.15 and 3.1.16)) it follows that ${\mathrm {SL}^\ell }$ is a logic in the sense of Convention 12.2 and that the classes of ${\mathrm {SL}^\ell }$-chains and ${\mathrm {SL}}$-chains coincide.

The second notion is that of core fuzzy logics formally defined in Definition 12.1. Let us reformulate this definition using the terminology introduced in the previous section (especially Convention 12.2 which stipulates that all the logics considered in this chapter satisfy the condition $({\mathrm {Cong}})$):

Definition 12.9

A logic $\mathrm {L}$ is a core fuzzy logic if it expands $\mathrm {MTL}$ by some set of axioms $Ax$.

Let us now generalize this class in two aspects: first, we replace $\mathrm {MTL}$ by the (much) weaker logic $\mathrm {SL}^\ell$ and, second, we include logics axiomatized by using extra rules provided that they satisfy a certain stability condition involving disjunction. As we shall soon see (in Theorem 12.8), these conditions are sufficient and necessary for an expansion of ${\mathrm {SL}^\ell }$ to remain complete w.r.t. chains.

Definition 12.10

A logic $\mathrm {L}$ is a core semilinear logic if it expands $\mathrm {SL}^\ell$ by some sets of axioms $Ax$ and rules $R$ such that for each $\langle {\varGamma ,\varphi }\rangle \in R$ and every formula $\psi$ we have:

$$ \varGamma \vee \psi \vdash _\mathrm {L} \varphi \vee \psi , $$

where by $\varGamma \vee \psi$ we denote the set $\{\chi \vee \psi \mid \chi \in \varGamma \}$.

Observe that if $\mathrm {L}$ is an expansion of a core semilinear logic by axioms $Ax$ and rules ${R}$, then $\mathrm {L}$ is itself a core semilinear logic iff for each $\langle {\varGamma ,\varphi }\rangle \in {R}$ we have $\varGamma \vee \psi \vdash _\mathrm {L} \varphi \vee \psi .$ Thus in particular:

• Any axiomatic expansion of a core semilinear logic is a core semilinear logic.

• Any axiomatic expansion of $\mathrm {SL}$ is a core semilinear logic iff it expands $\mathrm {SL}^\ell$.

The first item justifies why Hájek considered all axiomatic extensions (schematic extensions) of $\mathrm {HL}$ in his framework for fuzzy logics, since they were all complete with respect to chains. Moreover, one can check that $\mathrm {MTL}$ is an extension of $\mathrm {SL}^\ell$; therefore $\mathrm {MTL}$ and all core fuzzy logics are core semilinear logics. Similarly, it is easy to show that $\triangle$-core fuzzy logics are core semilinear (note that we are adding only one rule $\langle {\varphi ,\triangle \varphi }\rangle$ and we can easily prove that $\varphi \vee \psi \vdash _\mathrm {L} \triangle \varphi \vee \psi$ using axioms of ${\mathrm {MTL}}_\triangle$).

By restricting and re-elaborating results from the general theory presented by Cintula and Noguera (2011) (and by using some new results by Cintula et al. (2013) and by Cintula and Noguera (2013)), in this section we present several characterizations of core semilinear logics, some general methods to obtain their Hilbert-style axiomatizations, and a survey of their completeness results.

3.1 Characterizations and Properties of Core Semilinear Logics

The first characterization justifies the usage of the adjective ‘semilinear’. This terminology comes from the theory of residuated lattices (Olson and Raftery 2007) where it denotes classes of algebras such that in all (relatively) subdirectly irreducible members the lattice order is linear.¹⁹ Such property characterizes core semilinear logics as shown by conditions 3 and 4 of the following theorem. Moreover, as stated in condition 2, this is also equivalent with what we consider the main property of our logics: completeness with respect to the semantics given by chains.

Theorem 12.8

(Semilinearity) Let $\mathrm {L}$ be a logic. Then the following are equivalent:

• 1. $\mathrm {L}$ is a core semilinear logic.

• 2. $\mathrm {L}$ is complete w.r.t. $\mathrm {L}$-chains, i.e. the following are equivalent for any set of formulae $\varGamma \cup \{\varphi \}$:

  • a. $\varGamma \vdash _\mathrm {L} \varphi$

  • b. $e(\varphi ) \geqslant 1$ for each $\mathrm {L}$ -chain ${\varvec{A}}$ and each ${\varvec{A}}$-evaluation $e$ such that $e(\psi )\geqslant 1$ for all $\psi \in \varGamma$.

• 3. ${\mathbb {L}}_{\mathrm {RFSI}} = {{\mathbb {L}}_ lin }$.

• 4. ${\mathbb {L}}_{\mathrm {RSI}} \subseteq {{\mathbb {L}}_ lin }$.

Proof

Logics satisfying condition 2 are, in particular, weakly implicative semilinear logics in the sense of Cintula and Noguera (2011); thus we can use a result by (Cintula and Noguera (2011), Corollary 3.2.14.) to prove the equivalence of the first two properties (for $\mathrm {L_1}$ being $\mathrm {SL}^\ell$ and $\mathrm {L_2}$ being $\mathrm {L}$; we need to check the validity of three premises of that corollary: (a) ${\mathrm {SL}^\ell }$ is a weakly implicative semilinear logic: directly from Definition 12.8 and its following remark, (b) $\vee$ is a protodisjunction: trivially satisfied, and (c) $\mathrm {L}$ proves $({\mathrm {MP}}_\vee )$: established by Cintula and Noguera (2011), Proposition 3.2.2.

The equivalence of the latter three claims was established by (Cintula and Noguera (2011), Theorem 3.1.8). $\square$

Thus, as established in the proof of the theorem above, core semilinear logic are weakly implicative semilinear logics in the sense of Cintula and Noguera (2010, 2011). In fact, in the terminology of those papers, they are exactly algebraically implicative semilinear finitary expansions of $\mathrm {SL}^\ell$.

In order to formulate the syntactic characterization theorem for core semilinear logics (in terms of syntactic properties) we need to make use of special kinds of theories. Recall that a theory is a deductively closed set of formulae, i.e., $T\vdash \varphi$ implies that $\varphi \in T$). We say that a theory $T$ is

• maximally consistent w.r.t. a formula $\varphi$ if $\varphi \notin T$ and for every $\psi \notin T$ we have $T,\psi \vdash \varphi$

• saturated if it is maximally consistent w.r.t. some formula $\varphi$

• linear ²⁰ if for each formulae $\varphi$ and $\psi$ we have $\varphi \rightarrow \psi \in T$ or $\psi \rightarrow \varphi \in T$

• prime if for each formulae $\varphi$ and $\psi$ we have $\varphi \in T$ or $\psi \in T$ whenever $\varphi \vee \psi \in T$.

We also need a special formula $(\varphi \rightarrow \psi )\vee (\psi \rightarrow \varphi )$, called prelinearity and usually denoted by $\mathrm {(P_\vee )}$, which could be equivalently replaced in the formulation of the syntactic characterization theorem by any of the following two theorems of $\mathrm {SL}^\ell$ (as shown by (Cintula and Noguera (2011), Lemma 3.2.8)):  

$({\mathrm {lin}}_\wedge )$ :

$(\varphi \wedge \psi \mathbin \rightarrow \chi )\mathbin \rightarrow (\varphi \mathbin \rightarrow \chi )\vee (\psi \mathbin \rightarrow \chi )$

$({\mathrm {lin}}_\vee )$ :

$(\chi \mathbin \rightarrow \varphi \vee \psi )\mathbin \rightarrow (\chi \mathbin \rightarrow \varphi )\vee (\chi \mathbin \rightarrow \psi )$.

 

Theorem 12.9

(Syntactic characterization theorem) Let $\mathrm {L}$ be a logic. Then the following are equivalent:

• 1. $\mathrm {L}$ is a core semilinear logic.

• 2. $\mathrm {L}$ has the Semilinearity Property, $\mathrm {SLP}$, i.e. for every set of formulae $\varGamma \cup \{\varphi ,\psi ,\chi \}$ the following rule holds

  $$ \frac{\varGamma ,\varphi \mathbin \rightarrow \psi \vdash _\mathrm {L}\chi \qquad \varGamma ,\psi \mathbin \rightarrow \varphi \vdash _\mathrm {L}\chi }{\varGamma \vdash _\mathrm {L}\chi }\,. $$

• 3. $\mathrm {L}$ has the Linear Extension Property, $\mathrm {LEP}$, i.e. for every theory $T$ and a formula $\varphi$ such that $\varphi \notin T$, there is a linear theory $T' \supseteq T$ such that $\varphi \notin T'$.

• 4. Saturated theories are linear.

• 5. $\mathrm {L}$ proves $\mathrm {(P_\vee )}$ and has the Proof by Cases Property, $\mathrm {PCP}$, i.e. for every set of formulae $\varGamma \cup \{\varphi ,\psi ,\chi \}$ holds

  $$ \frac{\varGamma ,\varphi \vdash _\mathrm {L}\chi \qquad \varGamma ,\psi \vdash _\mathrm {L}\chi }{\varGamma ,\varphi \vee \psi \vdash _\mathrm {L}\chi }\,. $$

• 6. $\mathrm {L}$ proves $\mathrm {(P_\vee )}$ and has an axiomatic system $\langle {{Ax},{R}}\rangle$ such that for each $\langle {\varGamma ,\varphi }\rangle \in {R}$ we have:

  $$ \varGamma \vee \psi \vdash _\mathrm {L} \varphi \vee \psi . $$

• 7. $\mathrm {L}$ proves $\mathrm {(P_\vee )}$ and has the Prime Extension Property, $\mathrm {PEP}$, i.e. for every theory $T$ and a formula $\varphi$ such that $\varphi \notin T$, there is a prime theory $T' \supseteq T$ such that $\varphi \notin T'$.

• 8. $\mathrm {L}$ proves $\mathrm {(P_\vee )}$ and its saturated theories are prime.

Proof

The equivalence of the first three claims was proved by (Cintula and Noguera (2011), Theorem 3.1.8). To prove 1 implies 4 observe that saturated theories are finitely $\cap$-irreducible (ibid., Proposition 2.3.7) and so they are linear (ibid., Theorem 3.1.8). Conversely, if saturated theories are linear, then the Abstract Lindenbaum Lemma (ibid., Lemma 2.3.8) clearly implies $\mathrm {LEP}$ (i.e. claim 3).

The equivalence of 1 and 5 is also established using results by Cintula and Noguera (2011) (use Theorem 3.2.4 after observing that any $\mathrm {L}$ proves $({\mathrm {MP}}_\vee )$ as established in Proposition 3.2.2); the equivalence of 5 and 6 follows from Theorem 2.7.15. We use Theorem 2.7.23 to directly prove that 5 is equivalent with 7 and 7 implies 8. Finally, by using a similar reasoning as in the proof of 4 implies 3, we complete the whole proof by showing that 8 implies 7. $\square$

Remark 12.3

Most of these characterizations are inspired by the original ideas behind the proof of completeness of $\mathrm {HL}$ and its schematic extensions by Hájek (1998b): actually in Lemma 2.3.15. he gives a direct proof of transferred $\mathrm {PEP}$ (the third line of the following theorem) and in Lemma 2.4.2 he proves $\mathrm {LEP}$ by proving $\mathrm {SLP}$ first (without giving names to any of these properties).

Observe that while claim 6 is a just minor reformulation of Definition 12.10 of core semilinear logics, it provides an easy way to check whether a logic is core semilinear without having to prove that it extends $\mathrm {SL}^\ell$.

Note that theories are exactly the filters on the term algebra ${ Fm _{\fancyscript{L}}}$. Thus it makes sense to generalize the classes of theories we introduced above to filters with ‘$\varGamma \vdash \varphi$’ replaced by ‘$x\in {\mathrm {Fi}}(X)$’, e.g. a filter $F$ in an $\mathrm {L}$-algebra ${\varvec{A}}$ is maximally consistent (algebraist would say ‘maximal non-trivial’) w.r.t. an element $a\in A$ if $a \notin F$ and for every $b\notin F$ we have $a \in {\mathrm {Fi}}(F\cup \{b\})$. This allows us not only to see the conditions appearing in the syntactic characterization theorem as claims about filters on the term algebra ${ Fm _{\fancyscript{L}}}$, but mainly to formulate their transferred variants which speak about all $\mathrm {L}$-algebras. We collect these results in the next theorem together with some other useful algebraic properties $\mathrm {L}$-algebras.

Theorem 12.10

Let $\mathrm {L}$ be a core semilinear logic and ${\varvec{A}}$ an $\mathrm {L}$-algebra. Then:

• 1. For each set $X\cup \{a,b\}\subseteq A$ the following holds:

  $${\mathrm {Fi}}(X,a)\,\cap \,{\mathrm {Fi}}(X,b) = {\mathrm {Fi}}(X,a\vee b) \quad \quad {\mathrm {Fi}}(X,a\rightarrow b)\, \cap \,{\mathrm {Fi}}(X,b\rightarrow a) = {\mathrm {Fi}}(X). $$

• 2. Linear and prime filters coincide and contain the set of saturated filters.

• 3. For each filter $F\in \fancyscript{F}i_{\mathrm {L}}({\varvec{A}})$ and each $a\in A$ such that $a\not \in F$, there is a linear/prime filter $F' \supseteq F$ such that $a \notin F'$.

• 4. The lattice of $\mathrm {L}$-filters is distributive.

• 5. The lattice of relative ${\mathbb {L}}$-congruences is distributive.

• 6. The $\{\vee ,\wedge \}$-reduct of ${\varvec{A}}$ is a distributive lattice.

Proof

We will freely use all equivalent characterizations of core semilinear logics established before.

• 1. ((Cintula and Noguera 2011, Theorems 2.7.18 and 3.1.8)).

• 2. (ibid., Theorems 2.7.23, Theorem 3.1.8, and Proposition 2.3.7).

• 3. (ibid., Theorem 2.7.23) and claim 2.

• 4. (ibid., Theorem 2.7.20).

• 5. Claim 4 and Proposition 12.1.

• 6. (ibid., Theorem 3.2.12).

The following proposition is, among others, important to establish the soundness of the upcoming crucial definition of ${\mathrm {L}^\ell }$.

Proposition 12.2

The intersection of a family of core semilinear logics in the same language is a core semilinear logic.

Proof

First we need to observe that the intersection is a logic in the sense of Convention 12.2. This is established by (Cintula and Noguera (2011), Proposition 3.1.16). Then, the fact that it is core semilinear is a simple corollary of the syntactic characterization theorem (e.g. of the Semilinearity Property). $\square$

Definition 12.11

For a logic $\mathrm {L}$ we define the logic ${\mathrm {L}^\ell }$ as the least core semilinear logic extending $\mathrm {L}$.

The following two theorems give useful, semantical and syntactical, descriptions of ${\mathrm {L}^\ell }$. The first one is very general and, besides providing a semantical characterization of ${\mathrm {L}^\ell }$ as the logic of $\mathrm {L}$-chains, it shows how to extend any axiomatization of $\mathrm {L}$ into an axiomatization of ${\mathrm {L}^\ell }$. Roughly speaking, it adds prelinearity and the $\vee$-form of all rules (cf. the syntactic characterization theorem 12.9). Note that Petr Hájek also obtained some logics in these ways: e.g. he showed that $\mathrm {G}$ was in fact the logic of linearly ordered Heyting algebras or defined ${\mathrm {ps}}\mathrm {MTL}^r$ as the logic ${\mathrm {ps}}\mathrm {MTL}$-chains.

Theorem 12.11

Let $\mathrm {L}$ be a logic. Then:

• ${\mathrm {L}^\ell }$-chains coincide with $\mathrm {L}$-chains and the class $\mathbb {L}^\ell$ of ${\mathrm {L}^\ell }$-algebras is exactly the quasivariety generated by ${{\mathbb {L}}_ lin }$.

• If $\mathrm {L}$ is axiomatized by axioms $Ax$ and rules $R$, then ${\mathrm {L}^\ell }$ is the extension of $\mathrm {L}$ by the axiom ${\mathrm {(P_\vee )}}$ and the set of rules $\{\langle {\varGamma \vee \psi , \varphi \vee \psi }\rangle \mid \langle {\varGamma ,\varphi }\rangle \in R\}$.

• If $\mathrm {L}$ is obtained as the expansion of some core semilinear logic by axioms $Ax$ and rules $R$, then ${\mathrm {L}^\ell }$ is the extension of $\mathrm {L}$ by the rules $\{\langle {\varGamma \vee \psi , \varphi \vee \psi }\rangle \mid \langle {\varGamma ,\varphi }\rangle \in R\}$.

Proof

Again we use results by Cintula and Noguera (2011). The first claim follows from Proposition 3.1.15; the second follows from Proposition 3.2.9 and Theorem 2.7.27. The third one is an obvious corollary of already established facts. $\square$

The problem of the axiomatizations provided by this theorem is that they require additional new rules. We show that if $\mathrm {L}$ is almost $\mathrm {(MP)}$-based we can do better: ${\mathrm {L}^\ell }$ is then actually an axiomatic extension of $\mathrm {L}$ by variations of the prelinearity axiom. We present two variants, $B$ and $C$, of this axiomatization because they generalize two different usual formulations appearing in the literature; for comparison we also add a presentation $A$ resulting from the direct application of the previous theorem. Note that this theorem can be used to axiomatize the two logics mentioned above and studied by Petr Hájek: $\mathrm {G}$ and ${\mathrm {ps}}\mathrm {MTL}^r$.

Theorem 12.12

Let $\mathrm {L}$ be an almost $\mathrm {(MP)}$-based logic with a set ${\mathrm {bDT}}$ of basic deductive terms. Then ${\mathrm {L}^\ell }$ is axiomatized by adding to $\mathrm {L}$ any of the following:  

$A$ :

$(\varphi \rightarrow \psi ) \vee (\psi \rightarrow \varphi )$

$(\varphi \rightarrow \psi ) \vee \chi , \varphi \vee \chi \vdash \psi \vee \chi$

$\varphi \vee \psi \vdash \gamma (\varphi ) \vee \psi$, for every $\gamma \in {\mathrm {bDT}}$

$B$ :

$((\varphi \rightarrow \psi )\wedge \overline{1}) \vee \gamma ((\psi \rightarrow \varphi )\wedge \overline{1})$, for every $\gamma \in {\mathrm {bDT}}\cup \{\star \}$

$C$ :

$(\varphi \vee \psi \rightarrow \psi ) \vee \gamma (\varphi \vee \psi \rightarrow \varphi )$, for every $\gamma \in {\mathrm {bDT}}\cup \{\star \wedge \overline{1}\}$.

 

Proof

A weaker claim, for extensions of $\mathrm {SL}^\ell$, is proved by (Cintula et al. (2013), Theorem 4.29). One can easily see, by inspecting the proof, that the theorem remains valid in our framework of expansions of $\mathrm {SL}^\ell$. $\square$

Table 12.8 collects axiomatizations of important semilinear substructural logics obtained as axiomatization $B$ from Theorem 12.2. We present them in the form of axiom schemata, sometimes altered a little (in an equivalent way) for simplicity or to obtain some form known from the literature (Cintula et al. 2013).

Table 12.8 Axiomatization of ${\mathrm {L}^\ell }$ for prominent substructural logics

As mentioned in Sect. 12.2.2, finding nice Hilbert-style presentations for meets in the lattice of extensions of a given logic (in particular, showing that the meet of axiomatic extensions is itself an axiomatic extension of the base logic) is not straightforward. The following theorem gives a presentation for meets of extensions of a given core semilinear logic by capitalizing on the fact that $\vee$ enjoys $\mathrm {PCP}$ in all core semilinear logics.

Theorem 12.13

Let $\mathrm {L}_1$ and $\mathrm {L}_2$ be semilinear extensions of a core semilinear logic $\mathrm {L}$ defined by the sets of axioms $Ax_i$ and rules $R_i$. Then $\mathrm {L}_1 \cap \mathrm {L}_2$ is the extension of $\mathrm {L}$ obtained by adding

• the set of axioms $\{\varphi \vee \psi \mid \varphi \in Ax_1 \text { and } \psi \in Ax_2\}$ and

• the union of the following three sets of rules:

  • $\langle {\varGamma \vee \chi , \varphi \vee \psi \vee \chi }\rangle \mid \langle {\varGamma , \varphi }\rangle \in R_1,\, \psi \in Ax_2, \text { and } \chi \text { a formula}\}$

  • $\langle {\varGamma \vee \chi , \varphi \vee \psi \vee \chi }\rangle \mid \langle {\varGamma , \varphi }\rangle \in R_2,\, \psi \in {Ax}_1, \text { and } \chi \text { a formula}\}$

  • $\langle {(\varGamma _1\cup \varGamma _2)\vee \chi , \varphi _1\vee \varphi _2\vee \chi }\rangle \,{\mid }\, \langle {\varGamma _1, \varphi _1}\rangle \, {\in }\, R_1,\, \langle {\varGamma _2, \varphi _2}\rangle \, {\in }\, R_2, \text { and } \chi \text { a formula}\}$

Proof

Established by (Cintula and Noguera (2013), Theorem 5.10). $\square$

To close the subsection we clarify the position of core semilinear (axiomatic) extensions of given logic in the lattice of all its (axiomatic) extensions.

Corollary 12.2

Let $\mathrm {L}$ be a logic. Then the class of core semilinear extensions of $\mathrm {L}$ is a sublattice of the lattice of extensions of ${\mathrm {L}^\ell }$. Furthermore, the class of core semilinear axiomatic extensions of $\mathrm {L}$ is a principal filter in the lattice of axiomatic extensions of ${\mathrm {L}^\ell }$.

3.2 Completeness Results

We devote this subsection to completeness theorems for core semilinear logics. As discussed in the introduction, a crucial guideline for Petr Hájek and others when studying new fuzzy logics was to find logical systems complete with respect to a semantics of algebras defined on the real unit interval $[0,1]$. This kind of completeness results have been known as standard completeness theorems, although this terminology is not univocally defined. Indeed, by standard semantics one means the semantics that, due to some design choices, is considered to be the intended one for the logic. In some cases it consists of all algebras defined over $[0,1]$ (e.g. for $\mathrm {HL}$, ${\mathrm {SHL}}$, $\mathrm {MTL}$, ${\mathrm {SMTL}}$, or $\mathrm {IMTL}$); in other cases it consists of algebras with a fixed interpretation using particular operations (e.g. for $\L$, $\mathrm {G}$ or $\Pi$ where one interprets $\mathbin { \& }$ as the corresponding t-norm (Hájek 1998b), or for logics with an additional involutive negation ${\sim }$ where one interprets it as $1-x$ (Esteva et al. 2000). In all the examples taken from ($\triangle$-)core fuzzy logics, the standard semantics is based on left-continuous t-norms and their residua. Later on, the introduction of weaker systems brought forth an analogous relaxation for the corresponding algebraic structures on $[0,1]$, such as residuated uninorms (for $\mathrm {UL}$) or residuated non-commutative t-norms (for ${\mathrm {ps}}\mathrm {MTL}^r$). Recently, when considering a standard semantics for ${\mathrm {SL}}^\ell$ (Cintula et al. 2013), even associativity has been dropped giving rise to residuated unital groupoids on $[0,1]$.

Some other works have however focused on other kinds of semantics for fuzzy logics, besides the real-valued one. It is the case of rational-chain semantics, hyperreal-chain semantics or finite-chain semantics (e.g. Cintula et al. 2009; Esteva et al. 2010; Flaminio 2008; Montagna and Noguera 2010) where instead of  [0, 1] one respectively takes the rational unit interval, any hyperreal interval or any finite linearly ordered set as the domain for the intended models. A systematical study of the corresponding completeness properties is better presented in the following general formulation.

Definition 12.12

Let $\mathrm {L}$ be a core semilinear logic and $\mathbb {K}\subseteq {{\mathbb {L}}_ lin }$. We say that $\mathrm {L}$ has the Strong $\mathbb {K}$ -Completeness, ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ for short, when the following are equivalent for every set of formulae $\varGamma \cup \{\varphi \}$:

• 1. $\varGamma \vdash _\mathrm {L} \varphi$,

• 2. for every ${\varvec{A}} \in \mathbb {K}$ and every ${\varvec{A}}$-evaluation $e$, if $e(\psi ) \geqslant 1$ for every $\psi \in \varGamma$, then $e(\varphi ) \geqslant 1$.

If the equivalence above holds for finite $\varGamma$ (or only for $\varGamma =\emptyset$) we speak about Finite Strong $\mathbb {K}$ -Completeness (or just $\mathbb {K}$ -Completeness, respectively). The Finite Strong $\mathbb {K}$-Completeness is denoted by ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ whereas the $\mathbb {K}$-Completeness is denoted by $\mathbb {K}{\mathrm {C}}$.

It is easy to show that the failure of completeness properties is inherited by conservative expansions (recall that a logic $\mathrm {L_2}$ in a language $\fancyscript{L}_2$ is a conservative expansion of a logic $\mathrm {L_1}$ in a language $\fancyscript{L}_1$ if $\fancyscript{L}_1 \subseteq \fancyscript{L}_2$ and for each set of $\fancyscript{L}_1$-formulae $\varGamma \cup \{\varphi \}$ we have that $\varGamma \vdash _{\mathrm {L_2}}\varphi$ iff $\varGamma \vdash _{\mathrm {L_1}}\varphi$).

Proposition 12.3

((Cintula and Noguera 2011, Proposition 3.4.14)) Let $\mathrm {L}'$ be a conservative expansion of $\mathrm {L}$, $\mathbb {K}'$ a class of $\mathrm {L}'$-chains and $\mathbb {K}$ the class of their $\mathrm {L}$-reducts. If $\mathrm {L'}$ enjoys the $\mathbb {K}'\mathrm {C}$, then $\mathrm {L}$ enjoys the $\mathbb {K}{\mathrm {C}}$. The analogous claim holds for $\mathrm {FS}\mathbb {K}'\mathrm {C}$ and $\mathrm {S}\mathbb {K}'\mathrm {C}$.

We recall now several algebraic characterizations of completeness properties by Cintula et al. (2009) and Cintula and Noguera (2011). In what follows we will use the following operators on classes of algebras of the same type:

• ${\mathbf {S}}(\mathbb {K})$ is the class of subalgebras of members in $\mathbb {K}$,

• ${\mathbf {I}}(\mathbb {K})$ is the class of algebras isomorphic to a member in $\mathbb {K}$,

• ${\mathbf {H}}(\mathbb {K})$ is the class of homomorphic images of members in $\mathbb {K}$,

• ${\mathbf {P}}(\mathbb {K})$ is the class of direct products of members in $\mathbb {K}$,

• ${\mathbf {P}}_{fin}(\mathbb {K})$ is the class of finite direct products of members in $\mathbb {K}$,

• ${\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ is the class of ultraproducts of members in $\mathbb {K}$,

• ${\mathbf {P}}_{\sigma \text {-}f}(\mathbb {K})$ is the class of reduced products of members in $\mathbb {K}$ over countably complete filters (i.e. filters closed under countable intersections),

• ${\mathbf {V}}(\mathbb {K})$ is the variety generated by $\mathbb {K}$, i.e., ${\mathbf {V}}(\mathbb {K})={\mathbf {HSP}}(\mathbb {K})$,

• ${\mathbf {Q}}(\mathbb {K})$ is the quasivariety generated by $\mathbb {K}$, i.e., ${\mathbf {Q}}(\mathbb {K})={\mathbf {ISP}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$.

Let us fix a core semilinear logic $\mathrm {L}$ and a class of $\mathrm {L}$-chains $\mathbb {K}$. We present several characterizations of the general completeness properties. The first one relates them respectively with generation of the class of algebras as a variety, a quasivariety and a generalized quasivariety, respectively.

Theorem 12.14

((Cintula and Noguera 2011, Theorem 3.4.3))

• 1. $\mathrm {L}$ has the $\mathbb {K}{\mathrm {C}}$ if, and only if, ${\mathbf {H}}({\mathbb {L}})={\mathbf {V}}(\mathbb {K})$.

• 2. $\mathrm {L}$ has the ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ if, and only if, ${\mathbb {L}}={\mathbf {Q}}(\mathbb {K})$.

• 3. $\mathrm {L}$ has the ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ if, and only if, ${\mathbb {L}}={\mathbf {I}}{\mathbf {S}}{\mathbf {P}}_{\sigma \text {-}f}(\mathbb {K})$.

The completeness properties of $\mathrm {L}$ can be also characterized in terms of (finitely) subdirectly irreducible algebras relative to ${\mathbb {L}}$. Recall that, by Theorem 12.8, finitely subdirectly irreducible $\mathrm {L}$-algebras relative to ${\mathbb {L}}$ coincide with the class of $\mathrm {L}$-chains, i.e., we have $\mathbb {L}_{\mathrm {RSI}}\subseteq \mathbb {L}_{\mathrm {RFSI}}={{\mathbb {L}}_ lin }$. Given a class of algebras $\mathbb {M}$, the class of its nontrivial members is denoted $\mathbb {M}^{+}$. Similarly, $\mathbb {M}^{\sigma }$ stands for the class of countable members of $\mathbb {M}$.

Theorem 12.15

We have the following chains of equivalences:

• 1. $\mathrm {L}$ has the $\mathbb {K}{\mathrm {C}}$ iff  ${{\mathbb {L}}_ lin }\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ iff  $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$.

• 2. $\mathrm {L}$ has the ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ iff  $\mathbb {L}^{+}_{lin}\subseteq {\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ iff  $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$.

• 3. $\mathrm {L}$ has the ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ iff  $\mathbb {L}^{\sigma +}_{lin}\subseteq {\mathbf {IS}}(\mathbb {K})$ iff  $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {IS}}(\mathbb {K})$.

Proof

To prove the first claim we use a result by Dziobiak (1989) showing that for any congruence distributive quasivariety $\mathbb {Q}$ and any subclass of algebras $\mathbb {M}\subseteq \mathbb {Q}$ we have ${\mathbf {V}}(\mathbb {M})\cap \mathbb {Q}_{\mathrm {RFSI}}\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {M})$. Indeed from Theorem 12.10 we know that the quasivariety $\mathbb {L}$ is congruence distributive and thus by setting $\mathbb {Q}=\mathbb {L}$ and $\mathbb {M}=\mathbb {K}$ we obtain

$$ {\mathbf {V}}(\mathbb {K})\cap {{\mathbb {L}}_ lin }={\mathbf {V}}(\mathbb {K})\cap \mathbb {L}_{\mathrm {RFSI}}\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K}). $$

Now assume that $\mathrm {L}$ has the $\mathbb {K}{\mathrm {C}}$. Then by Theorem 12.14 we have ${\mathbf {H}}(\mathbb {L})={\mathbf {V}}(\mathbb {K})$. Consequently, ${{\mathbb {L}}_ lin }\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ because ${{\mathbb {L}}_ lin }\subseteq {\mathbf {H}}(\mathbb {L})$. Further, it is obvious that ${{\mathbb {L}}_ lin }\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ implies $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ since $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {{\mathbb {L}}_ lin }$. Finally, suppose that $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {HS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$. By Theorem 12.14 it is sufficient to show that ${\mathbf {H}}(\mathbb {L})={\mathbf {V}}(\mathbb {K})$. Since ${\mathbf {V}}(\mathbb {L})={\mathbf {H}}(\mathbb {L})$ and $\mathbb {K}\subseteq \mathbb {L}$, we always have ${\mathbf {V}}(\mathbb {K})\subseteq {\mathbf {H}}(\mathbb {L})$. Conversely, $\mathrm {L}$ is strongly complete w.r.t. $\mathbb {L}_{\mathrm {RSI}}^{\sigma }$ by Theorem 12.7. Thus by Theorem 12.14 we have ${\mathbf {H}}(\mathbb {L})={\mathbf {V}}(\mathbb {L}_{\mathrm {RSI}}^{\sigma })$. Consequently, by our assumption we obtain ${\mathbf {H}}(\mathbb {L})\subseteq {\mathbf {V}}(\mathbb {K})$.

The first equivalence of the second claim is proved by (Cintula and Noguera (2011), Theorem 3.4.11). In order to prove the remaining one, one can argue similarly as above. Indeed, since $\mathbb {L}_{\mathrm {RSI}}^{\sigma }\subseteq \mathbb {L}^{+}_{lin}$, $\mathbb {L}^{+}_{lin}\subseteq {\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$ implies $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$. Conversely, assume that $\mathbb {L}^{\sigma }_{\mathrm {RSI}}\subseteq {\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K})$. Again using Theorems 12.7 and 12.14, we obtain

$$ \mathbb {L}={\mathbf {Q}}(\mathbb {L}^{\sigma }_{\mathrm {RSI}})\subseteq {\mathbf {Q}}({\mathbf {IS}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K}))= {\mathbf {Q}}(\mathbb {K})\subseteq \mathbb {L}\,. $$

Thus $\mathrm {L}$ enjoys ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ by Theorem 12.14.

The last claim is proved by (Cintula and Noguera (2011), Theorem 3.4.6). $\square$

Corollary 12.3

If $\mathrm {L}$ enjoys ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$, then it enjoys the ${\mathrm {S}}{\mathbf {P}}_{\mathrm {U}}(\mathbb {K}){\mathrm {C}}$ as well.

Alternatively, for logics with finitely many propositional connectives, an algebraic property equivalent to finite strong $\mathbb {K}$-completeness is expressed in terms of partial embeddings. This was, in fact, the property used by Hájek and others to prove standard completeness of $\mathrm {HL}$.

Definition 12.13

Given two algebras ${\varvec{A}}$ and ${\varvec{B}}$ of the same language $\fancyscript{L}$, we say that a finite subset $X$ of ${\varvec{A}}$ is partially embeddable into ${\varvec{B}}$ if there is a one-to-one mapping $f:X\rightarrow B$ such that for each $\langle {c,n}\rangle \in \fancyscript{L}$ and each $a_1, \dots , a_n\in X$ satisfying $c^{\varvec{A}}(a_1, \dots , a_n) \in X$, $f(c^{\varvec{A}}(a_1, \dots , a_n)) = c^{\varvec{B}}(f(a_1), \dots , f(a_n))$.

A class $\mathbb {K}$ of algebras is partially embeddable into a class $\mathbb {K}'$ if every finite subset of every member of $\mathbb {K}$ is partially embeddable into a member of $\mathbb {K}'$.

Theorem 12.16

If the language of $\mathrm {L}$ is finite, then the following are equivalent:

• 1. $\mathrm {L}$ has the ${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$.

• 2. The class $\mathbb {L}^{\sigma }_{\mathrm {RSI}}$ is partially embeddable into $\mathbb {K}$.

• 3. The class $\mathbb {L}^{+}_{lin}$ is partially embeddable into $\mathbb {K}$.

• 4. $\mathbb {L}$ is partially embeddable into ${\mathbf {P}}_{\textit{fin}}(\mathbb {K})$.

Proof

The equivalence of the first three claims is proved by (Cintula and Noguera (2011), Theorem 3.4.8).

(3)$\Rightarrow$(4): Let ${\varvec{A}}\in \mathbb {L}$ and $X\subseteq A$ a finite subset. By a well-known fact from universal algebra, every algebra ${\varvec{C}}$ in a quasivariety $\mathbb {Q}$ is a subdirect product of subdirectly irreducible algebras relative to $\mathbb {Q}$. Since $\mathbb {L}$ is a quasivariety, it follows that ${\varvec{A}}$ can be viewed as a subdirect product of a family $\{{\varvec{A}}_{i}\in \mathbb {L}_{\mathrm {RSI}}\mid i\in I\}$. Since $X$ is finite, it suffices to consider only finitely many ${\varvec{A}}_{i}$’s in order to separate elements of $X$. Thus $X$ is partially embeddable into a finite direct product of some subdirectly irreducible algebras relative to $\mathbb {L}$. Since $\mathbb {L}_{\mathrm {RSI}}\subseteq {{\mathbb {L}}_ lin }$ by Theorem 12.8, $X$ is partially embeddable into ${\mathbf {P}}_{\textit{fin}}(\mathbb {K})$ by (3).

(4)$\Rightarrow$(1): Assume that $\varGamma \not \vdash _{\mathrm {L}}\varphi$ for a finite set $\varGamma$ of formulae. By Theorem 12.7 there is a counter-model ${\varvec{A}}\in \mathbb {L}_{\mathrm {RSI}}$. By (4) we have also a counter-model ${\varvec{B}}\in {\mathbf {P}}_{\textit{fin}}(\mathbb {K})$. Since ${\varvec{B}}$ is a direct product of members from $\mathbb {K}$, one of them actually has to be a counter-model as well. $\square$

Remark 12.4

Notice that the implications from $2$, $3$, or $4$ to $1$ hold also for infinite languages, whereas the converse ones do not (as shown by (Cintula et al. (2009), Example 3.10)).

Let us now deal with particular notable semantics. We consider first the class of all finite $\mathrm {L}$-chains, denoted by $\fancyscript{F}$.

Theorem 12.17

((Cintula and Noguera 2011, Theorem 3.4.16.)) The following are equivalent:

• 1. $\mathrm {L}$ enjoys the ${{\mathrm {S}}\fancyscript{F}{\mathrm {C}}}$.

• 2. All $\mathrm {L}$-chains are finite.

• 3. There exists $n \in \mathsf {N}$ such each $\mathrm {L}$-chain has at most $n$ elements.

• 4. There exists $n \in \mathsf {N}$ such that    $\vdash _\mathrm {L} \bigvee _{i < n} (x_i \rightarrow x_{i+1})$.

Corollary 12.4

For any core semilinear logic $\mathrm {L}$ and a natural number $n$, the axiomatic extension $\mathrm {L_{{\leqslant }n}}$ obtained by adding the schema $\bigvee _{i < n} (x_i \rightarrow x_{i+1})$ is a semilinear logic which is strongly complete with respect the $\mathrm {L}$-chains of length less than or equal to $n$.

Next we show that the properties of ${\mathrm {FS}}\fancyscript{F}{\mathrm {C}}$ and $\fancyscript{F}{\mathrm {C}}$ have purely algebraic characterizations in terms of basic notions studied in universal algebra. We say that a class of algebras $\mathbb {M}$ has:

• the finite embeddability property (${\mathrm {FEP}}$) if $\mathbb {M}$ is partially embeddable into the class of its finite members,

• the (strong) finite model property ((S)FMP) if every (quasi-)identity that fails to hold in $\mathbb {M}$ can be refuted in a finite member of $\mathbb {M}$.

The next theorem follows from Theorem 12.16 but can be also seen as an instance of a purely universal-algebraic result by Blok and van Alten (2002) (after replacing the first claim by an equivalent algebraic formulation using Theorem 12.14).

Theorem 12.18

The following are equivalent:

• 1. $\mathrm {L}$ enjoys the ${{\mathrm {FS}}\fancyscript{F}{\mathrm {C}}}$.

• 2. $\mathbb {L}$ enjoys the SFMP.

• 3. $\mathbb {L}$ enjoys the ${{\mathrm {FEP}}}$.

Finally, the algebraic characterization of $\fancyscript{F}{\mathrm {C}}$ is not much of use because it involves free algebras whose structure is usually quite complex, but we include it for the sake of completeness.

Theorem 12.19

The following are equivalent:

• 1. $\mathrm {L}$ enjoys the ${\fancyscript{F}{\mathrm {C}}}$.

• 2. $\mathbb {L}$ enjoys the FMP.

• 3. The class of finitely generated ${\mathbb {L}}$-free algebras is partially embeddable into the class of finite members of ${\mathbb {L}}$.

Proof

(1)$\Rightarrow$(2): Since $\mathrm {L}$ is algebraizable, the first claim implies the second one.

(2)$\Rightarrow$(3): Assume that $\mathbb {L}$ has the FMP. Let ${\varvec{F}}$ be a finitely generated ${\mathbb {L}}$-free algebra and $X\subseteq F$ a finite subset. We will construct a partial embedding

$$ f:X\rightarrow \!\!\!\prod _{\begin{array}{c} x,y\in X\\ x\ne y\end{array}}A_{x,y}, $$

where ${\varvec{A}}_{x,y}$ are going to be finite members of ${\mathbb {L}}$. Let $x,y\in X$ such that $x\ne y$. Since ${\varvec{F}}$ is free, $x,y$ can be viewed as equivalence classes of terms. Consider any term $t_{x}$ belonging to $x$ and similarly any term $t_{y}$ from $y$. Then the identity $t_{x}\approx t_{y}$ does not hold in ${\mathbb {L}}$ because $x\ne y$. By FMP there is a finite algebra ${\varvec{A}}_{x,y}\in {\mathbb {L}}$ where $t_{x}\approx t_{y}$ can be refuted. Since ${\varvec{F}}$ is free, we have a surjective homomorphism $f_{x,y}:F\rightarrow A_{x,y}$ such that $f_{x,y}(x)\ne f_{x,y}(y)$. The collection of homomorphisms $f_{x,y}$ induces a homomorphism

$$ g:F\rightarrow \!\!\! \prod _{\begin{array}{c} x,y\in X\\ x\ne y\end{array}}A_{x,y} $$

defined by $g(z)=\langle {f_{x,y}(z)}\rangle _{x,y\in X, x\ne y}$ whose restriction to $X$ gives the desired partial embedding $f$.

(3)$\Rightarrow$(1): Let $\varphi$ be a formula which is not a theorem of $\mathrm {L}$, i.e., $\not \vdash _{\mathrm {L}}\varphi$. By algebraizability the identity $\overline{1}\approx \overline{1}\wedge \varphi$ does not hold in ${\mathbb {L}}$. Consequently, $\overline{1}\approx \overline{1}\wedge \varphi$ does not hold in a finitely generated ${\mathbb {L}}$-free algebra ${\varvec{F}}$. Since ${\varvec{F}}$ is partially embeddable into a finite member ${\varvec{A}}\in {\mathbb {L}}$, $\overline{1}\approx \overline{1}\wedge \varphi$ does not hold in ${\varvec{A}}$. By a well-known fact from universal algebra, every algebra ${\varvec{C}}$ in a quasivariety $\mathbb {Q}$ is a subdirect product of subdirectly irreducible algebras relative to $\mathbb {Q}$ which are homomorphic images of ${\varvec{C}}$. Since $\mathbb {L}_{\mathrm {RSI}}\subseteq {{\mathbb {L}}_ lin }$, ${\varvec{A}}$ is a subdirect product of chains ${\varvec{B}}_{i}$, $i\in I$, which are homomorphic images of ${\varvec{A}}$. Thus ${\varvec{B}}_{i}$’s have to be finite as well. Consequently, $\overline{1}\approx \overline{1}\wedge \varphi$ does not hold in $\prod _{i\in I}{\varvec{B}}_{i}$ and therefore $\overline{1}\approx \overline{1}\wedge \varphi$ can be refuted in one of the ${\varvec{B}}_{i}$’s. $\square$

The completeness properties w.r.t. the class $\fancyscript{F}$ of finite $\mathrm {L}$-chains are usually used in order to show decidability of theorems and finite consequence of $\mathrm {L}$. More precisely, if $\mathrm {L}$ is finitely axiomatizable then $\fancyscript{F}{\mathrm {C}}$ implies decidability of the set $\{\varphi \mid {}\vdash _{\mathrm {L}}\varphi \}$ and ${\mathrm {FS}}\fancyscript{F}{\mathrm {C}}$ implies decidability of $\{\langle {\varGamma ,\varphi }\rangle \mid \varGamma \vdash _{\mathrm {L}}\varphi ,\,\varGamma \ {\mathrm {finite}}\}$. Table 12.9 lists several known results on completeness properties w.r.t. $\fancyscript{F}$ (see Horčík (2011), Wang (2013) and references thereof).

Table 12.9 Finite strong completeness w.r.t. $\fancyscript{F}$ for some core semilinear logics

We now consider the semantics given by chains defined over the rational and the real unit interval. We present both notions together because their completeness properties are much related.²¹

Definition 12.14

The class $\fancyscript{R}\subseteq {{\mathbb {L}}_ lin }$ is defined as: ${\varvec{A}} \in \fancyscript{R}$ if the domain of ${\varvec{A}}$ is the real unit interval $[0,1]$ and $\leqslant _{\varvec{A}}$ is the usual order on reals. The class $\fancyscript{Q}\subseteq {{\mathbb {L}}_ lin }$ is analogously defined requiring the rational unit interval as domain.

Theorem 12.20

((Cintula and Noguera 2011, Theorem 3.4.19))

• 1. $\mathrm {L}$ has the ${\mathrm {FS}}\fancyscript{Q}{\mathrm {C}}$ iff it has the $\mathrm {S}\fancyscript{Q}\mathrm {C}$.

• 2. If $\mathrm {L}$ has the $\fancyscript{R}\mathrm {C}$, then it has the $\fancyscript{Q}\mathrm {C}$.

• 3. If $\mathrm {L}$ has the ${\mathrm {FS}}\fancyscript{R}\mathrm {C}$, then it has the $\mathrm {S}\fancyscript{Q}\mathrm {C}$.

Observe that the completeness properties with respect to $\fancyscript{Q}$ are, in fact, equivalent to completeness properties with respect to the whole class of densely ordered chains. Indeed, when we have an evaluation over a densely ordered linear model providing a counterexample to some derivation, we can apply the downward Löwenheim–Skolem Theorem to the (countable) subalgebra generated by the image of all formulae by the evaluation and obtain a rational countermodel.

Strong rational completeness also admits a proof-theoretic characterization in terms of the Density Property:²²

Theorem 12.21

The following are equivalent:

• 1. $\mathrm {L}$ has the $\mathrm {S}\fancyscript{Q}\mathrm {C}$.

• 2. $\mathrm {L}$ has the Density Property $\mathrm {DP}$, i.e. if for any set of formulae $\varGamma \cup \{\varphi ,\psi ,\chi \}$ and any variable $p$ not occurring in $\varGamma \cup \{\varphi ,\psi ,\chi \}$ the following meta-rule holds:

  $$ \frac{\varGamma \vdash _\mathrm {L}(\varphi \mathbin \rightarrow p)\vee (p\mathbin \rightarrow \psi ) \vee \chi }{ \varGamma \vdash _\mathrm {L}(\varphi \mathbin \rightarrow \psi )\vee \chi }. $$

• 3. $\mathrm {L}$ is the intersection of all its extensions satisfying the $\mathrm {DP}$.

Proof

Again we use results by Cintula and Noguera (2011). The equivalence of 1 and 2 follows Theorem 3.3.8. The equivalence with 3 follows from Theorem 3.3.13. $\square$

The last claim gives some insight into an approach used in the fuzzy logic literature to prove completeness w.r.t. the semantics of densely ordered chains (e.g. by Metcalfe and Montagna (2007) for the logic $\mathrm {UL}$). Indeed, in this approach one starts from a suitable proof-theoretic description of a logic $\mathrm {L}$, which then is extended into a proof-system for the intersection of all extensions of $\mathrm {L}$ satisfying the $\mathrm {DP}$ just by adding $\mathrm {DP}$ as a rule (in the proof-theoretic sense, not as we understand rules here). This rule is then shown to be eliminable (using analogs of the well-known cut-elimination techniques), i.e., the condition 3 is met and hence the original logic is complete w.r.t. its densely ordered chains (of course, our general theory is not helpful in this last step, because here one needs to use specific properties of the logic in question).

Many works in the literature of MFL focus on the study of these completeness properties. Besides the historical papers devoted to particular logical systems, there are more systematic approaches dealing with the study of these properties by Cintula et al. (2009) and Horčík (2011). Table 12.10 collects the results for some prominent core semilinear logics. Unlike ${\mathrm {{{\mathrm {FL}}}}^\ell }$, the weakest core semilinear logic $\mathrm {SL}^\ell$ does enjoy all these completeness properties, as proved by Cintula et al. (2013). In particular, if one considers residuated groupoids defined over $[0,1]$ as its intended semantics, then $\mathrm {SL}^\ell$ enjoys standard completeness in the strong version, and hence, can be regarded as a genuine fuzzy logic as much as $\mathrm {HL}$, $\mathrm {MTL}$ or $\mathrm {UL}$. On the other hand, it can arguably be seen as a basic logic in the meanings described in the introduction. Indeed, the class of core semilinear logics is based in this logic and provides a useful framework covering virtually all the work done nowadays in MFL; moreover in the context of substructural logics complete w.r.t. chains could not be made weaker. We have therefore defended the role of $\mathrm {SL}^\ell$ as basic fuzzy logic in the framework of propositional logics. In the last part of the chapter we argue that this is also the case at the first-order level.

Table 12.10 Real and rational completeness for some core semilinear logics

4 First-Order Core Semilinear Logics

In this section we present the theory of first-order core semilinear logics. The presentation, definitions, and results of the first two subsections closely follow the work of (Cintula and Noguera (2011), Sect. 5) simplified to our setting of core semilinear logics. The third subsection generalizes results of Cintula et al. (2009) (proved there for core fuzzy logics) and shortly surveys the undecidability results treated in detail by Hájek et al. (2011).

4.1 Syntax

In the following let $\mathrm {L}$ be a fixed core semilinear logic in a propositional language $\fancyscript{L}$. The language of a first-order extension of $\mathrm {L}$ is defined in the same way as in classical first-order logic. In order to fix the notation and terminology we give an explicit definition:

Definition 12.15

A predicate language ${{{\fancyscript{P}}}}$ is a triple $\langle Pred _{\fancyscript{P}}, Func _{\fancyscript{P}}, Ar _{\fancyscript{P}}\rangle$, where $Pred _{\fancyscript{P}}$ is a non-empty set of predicate symbols, $Func _{\fancyscript{P}}$ is a set (disjoint with $Pred _{\fancyscript{P}}$) of function symbols, and $Ar _{\fancyscript{P}}$ is the arity function, assigning to each predicate or function symbol a natural number called the arity of the symbol. The function symbols $F$ with $Ar _{\fancyscript{P}}(F)=0$ are called object or individual constants. The predicates symbols $P$ for which $Ar _{\fancyscript{P}}(P)=0$ are called truth constants. ²³

${\fancyscript{P}}$-terms and (atomic) ${\fancyscript{P}}$-formulae of a given predicate language are defined as in classical logic (note that the notion of formula also depends on propositional connectives in $\fancyscript{L}$). A ${\fancyscript{P}}$-theory is a set of ${\fancyscript{P}}$-formulae. The notions of free occurrence of a variable, substitutability, open formula, and closed formula (or, synonymously, sentence) are defined in the same way as in classical logic. Unlike in classical logic, in fuzzy logics without involutive negation the quantifiers $\forall$ and $\exists$ are not mutually definable, so the primitive language of ${\mathrm {{{{L}}\forall ^{}}}}$ has to contain both of them.

There are several variants of the first-order extension of a propositional fuzzy logic $\mathrm {L}$ that can be defined. Following Hájek’s original approach and his developments (Hájek 1998b, 2007a, b, 2010), here we restrict ourselves to logics of models over linearly ordered algebras (see Sect. 12.4.2) and introduce the first-order logics ${\mathrm {{{L}\forall ^{}}}}$ and ${\mathrm {{{{L}}\forall ^{w}}}}$ (respectively, complete w.r.t. all models or w.r.t. witnessed models). The axiomatic systems of the logics ${\mathrm {{{L}\forall ^{}}}}$ and ${\mathrm {{{{L}}\forall ^{w}}}}$ are defined as follows:

Definition 12.16

Let $\fancyscript{P}$ be a predicate language. The logic ${\mathrm {{{L}\forall ^{}}}}$ in language $\fancyscript{P}$ has the following axioms:²⁴  

$\mathrm{(P)}$ :

The axioms of ${\mathrm {L}}$

$(\forall 1)$ :

$(\forall {x})$ $\varphi$(x)$\mathrel {\rightarrow }$ $\varphi$($t$),   where the ${\fancyscript{P}}$-term $t$ is substitutable for $x$ in $\varphi$

$(\exists 1)$ :

$\varphi$($t$)$\mathrel {\rightarrow }$ $(\exists {x})$ $\varphi$($x$),   where the ${\fancyscript{P}}$-term $t$ is substitutable for $x$ in $\varphi$

$(\forall 2)$ :

$(\forall {x})$($\chi$ $\mathrel {\rightarrow }$ $\varphi$)$\mathrel {\rightarrow }$($\chi$ $\mathrel {\rightarrow }$ $(\forall {x})$ $\varphi$),   where $x$ is not free in $\chi$

$(\exists 2)$ :

$(\forall {x})$($\varphi$ $\mathrel {\rightarrow }$ $\chi$)$\mathrel {\rightarrow }$($(\exists {x})$ $\varphi$ $\mathrel {\rightarrow }$ $\chi$),   where $x$ is not free in $\chi$

$(\forall 3)$ :

$(\forall {x})$($\chi$ $\mathbin {\vee }$ $\varphi$)$\mathrel {\rightarrow }$ $\chi$ $\mathbin {\vee }$ $(\forall {x})$ $\varphi$,   where $x$ is not free in $\chi$.

  The deduction rules of ${\mathrm {{{L}\forall ^{}}}}$ are those of $\mathrm {L}$ plus the rule of generalization:  

${\mathrm {(Gen)}}$ :

$\langle {\varphi , (\forall {x})\varphi }\rangle$.

  The logic ${\mathrm {{{L}\forall ^{w}}}}$ is the extension of ${\mathrm {{{L}\forall ^{}}}}$ by the axioms:  

$({\mathrm {C}}\forall )$ :

$(\exists {x})$($\varphi$($x$)$\mathrel {\rightarrow }$ $(\forall {y})$ $\varphi$($y$))

$({\mathrm {C}}\exists )$ :

$(\exists {x})$($(\exists {y})$ $\varphi$($y$)$\mathrel {\rightarrow }$ $\varphi$($x$)).

 

The notions of proof and provability are defined for first-order core semilinear logics in the same way as in first-order classical logic. The fact that the formula $\varphi$ is provable in ${\mathrm {{{L}\forall ^{}}}}$ from a theory $T$ will be denoted by $T\vdash _{{\mathrm {{{L}\forall ^{}}}}}\varphi$, and analogously for ${\mathrm {{{L}\forall ^{w}}}}$; in a fixed context we can write just $T\vdash \varphi$.

Helena Rasiowa (1974) gave a first general theory of first-order non-classical logics based on her notion of propositional implicative logic. The presentation of her first-order logics, which we denote ${\mathrm {{{L}\forall ^{m}}}}$, omitted the axiom $(\forall 3)$.²⁵ The superscript ‘$\mathrm {m}$’ stands for ‘minimal’, because ${\mathrm {{{L}\forall ^{m}}}}$ is, in a sense, the weakest first-order extension of $\mathrm {L}$. Indeed, ${\mathrm {{{L}\forall ^{m}}}}$ is sound and complete w.r.t. first-order models built over arbitrary $\mathrm {L}$-algebras. However, the axioms of ${\mathrm {{{L}\forall ^{m}}}}$ are not strong enough to ensure the completeness w.r.t. first-order models (see the next subsection for technical details) over linearly ordered $\mathrm {L}$-algebras—i.e., the usual chain completeness theorem, which we have presented as an essential common trait of all core semilinear logics. That is the reason why Hájek needed to add the axiom $(\forall 3)$ in his presentation of first-order fuzzy logics. This axiom is valid in all models over $\mathrm {L}$-chains (though not generally in models over arbitrary $\mathrm {L}$-algebras) and ensures the chain completeness theorem for the resulting logic ${\mathrm {{{{L}}\forall ^{}}}}$.²⁶ This makes ${\mathrm {{{L}\forall ^{}}}}$ a natural choice for the first-order extension of a given core semilinear logic $\mathrm {L}$. Consequently, we denote this first-order logic as ${\mathrm {{{L}\forall ^{}}}}$ with no superscript (though in some works the more systematic denotation ${\mathrm {{{L}\forall ^{\ell }}}}$ is used). Finally let us note that in the context of MFL, the logics ${\mathrm {{{L}\forall ^{m}}}}$ were rediscovered by Petr Hájek (2000), where he denoted them by ${\mathrm {{{L}\forall ^{}}}}^-$.

Let us list some important theorems that are provable in all logics ${\mathrm {{{L}\forall ^{}}}}$. Their proofs in MTL or HL are given e.g. by Esteva and Godo (2001) or Hájek (1998b); proofs in a weaker setting are given by Cintula and Noguera (2011).

Theorem 12.22

((Cintula and Noguera 2011, Propositions 4.2.5 and 4.3.2)) Let ${\fancyscript{P}}$ be a predicate language, $\varphi$, $\psi$, $\chi$ ${\fancyscript{P}}$-formulae, $x$ a variable not free in $\chi$, and $x'$ a variable not occurring in $\varphi$. The following ${\fancyscript{P}}$-formulae are theorems of ${\mathrm {{{L}\forall ^{}}}}$:

(${\mathrm {T}}\forall 1$)	$\chi \mathrel {\leftrightarrow }(\forall {x})\chi$	(${\mathrm {T}}\forall 11$)	$(\exists {x})(\chi \mathrel {\rightarrow }\varphi ) \mathrel {\rightarrow }(\chi \mathrel {\rightarrow }(\exists {x})\varphi )$
(${\mathrm {T}}\forall 2$)	$(\exists {x})\chi \mathrel {\leftrightarrow }\chi$	(${\mathrm {T}}\forall 12$)	$(\exists {x})(\varphi \mathrel {\rightarrow }\chi ) \mathrel {\rightarrow }((\forall {x})\varphi \mathrel {\rightarrow }\chi )$
(${\mathrm {T}}\forall 3$)	$(\forall {x})\varphi (x)\mathrel {\leftrightarrow }(\forall {x'})\varphi (x')$	(${\mathrm {T}}\forall 13$)	$(\forall {x})(\varphi \wedge \psi ) \mathrel {\leftrightarrow }(\forall {x})\varphi \wedge (\forall {x})\psi$
(${\mathrm {T}}\forall 4$)	$(\exists {x})\varphi (x)\mathrel {\leftrightarrow }(\exists {x'})\varphi (x')$	(${\mathrm {T}}\forall 14$)	$(\exists {x})(\varphi \vee \psi ) \mathrel {\leftrightarrow }(\exists {x})\varphi \vee (\exists {x})\psi$
(${\mathrm {T}}\forall 5$)	$(\forall {x})(\forall {y})\varphi \mathrel {\leftrightarrow }(\forall {y})(\forall {x})\varphi$	(${\mathrm {T}}\forall 15$)	$(\forall {x})(\varphi \vee \chi )\mathrel {\leftrightarrow }(\forall {x})\varphi \vee \chi$
(${\mathrm {T}}\forall 6$)	$(\exists {x})(\exists {y})\varphi \mathrel {\leftrightarrow }(\exists {y})(\exists {x})\varphi$	(${\mathrm {T}}\forall 16$)	$(\exists {x})(\varphi \wedge \chi ) \mathrel {\leftrightarrow }(\exists {x})\varphi \wedge \chi$
(${\mathrm {T}}\forall 7$)	$(\forall {x})(\varphi \mathrel {\rightarrow }\psi ) \mathrel {\rightarrow }((\forall {x})\varphi \mathrel {\rightarrow }(\forall {x})\psi )$	(${\mathrm {T}}\forall 17$)	$(\exists {x})(\varphi \mathbin { \& }\chi )\mathrel {\leftrightarrow }(\exists {x})\varphi \mathbin { \& }\chi$
(${\mathrm {T}}\forall 8$)	$(\forall {x})(\varphi \mathrel {\rightarrow }\psi ) \mathrel {\rightarrow }((\exists {x})\varphi \mathrel {\rightarrow }(\exists {x})\psi )$	(${\mathrm {T}}\forall 18$)	$(\exists {x})(\varphi ^n)\mathrel {\leftrightarrow }((\exists {x})\varphi )^n$
(${\mathrm {T}}\forall 9$)	$(\chi \mathrel {\rightarrow }(\forall {x})\varphi ) \mathrel {\leftrightarrow }(\forall {x})(\chi \mathrel {\rightarrow }\varphi )$	(${\mathrm {T}}\forall 19$)	$(\exists {x})\varphi \mathrel {\rightarrow }{\lnot }(\forall {x}){\lnot }\varphi$
(${\mathrm {T}}\forall 10$)	$((\exists {x})\varphi \mathrel {\rightarrow }\chi ) \mathrel {\leftrightarrow }(\forall {x})(\varphi \mathrel {\rightarrow }\chi )$	(${\mathrm {T}}\forall 20$)	${\lnot }(\exists {x})\varphi \mathrel {\leftrightarrow }(\forall {x}){\lnot }\varphi$

Remark 12.5

The converse implication of $(\mathrm{{T}}\forall 19)$ is provable in ${\mathrm {{{{{\L }}}\forall ^{}}}}$, ${\mathrm {{{\mathrm {IMTL}}\forall ^{}}}}$, or ${\mathrm {{{{{\mathrm {NM}}}}\forall ^{}}}}$, i.e., in logics where $\lnot$ is involutive (i.e. proves $\lnot \lnot \varphi \rightarrow \varphi )$. Thus in such logics the existential quantifier is definable and the axioms $(\exists 1)$ and $(\exists 2)$ become redundant. Actually, for this claim to hold, the presence of an arbitrary unary connective ${\sim }$ such that $\varphi \mathrel {\rightarrow }\psi \vdash _\mathrm {L}{\sim }\psi \mathrel {\rightarrow }{\sim }\varphi$ and $\vdash _\mathrm {L}\varphi \mathrel {\leftrightarrow }{\sim }{\sim }\varphi$ is sufficient (which could be either the ‘natural’ logical negation given by implication, or a new primitive connective added in logics $\mathrm {L}_{\sim }$).

The provability of the converse implications of $(\mathrm{{T}}\forall 11)$ or $(\mathrm{{T}}\forall 12)$ is equivalent to provability of $({\mathrm {C}}\exists )$ or $({\mathrm {C}}\forall )$ resp., i.e., if ${\mathrm {{{L}\forall ^{}}}}$ proves them, then ${\mathrm {{{L}\forall ^{}}}} = {\mathrm {{{L}\forall ^{w}}}}$. This is the case of Łukasiewicz logic; product logic proves $({\mathrm {C}}\exists )$ (and so the converse of $(\mathrm{{T}}\forall 11)$) but not $({\mathrm {C}}\forall )$, and Gödel logic proves neither. Finally it is worth noting that the axiom $(\forall 3)$ is redundant in the axiomatization of ${\mathrm {{{{\L }}\forall ^{}}}}$ and thus ${\mathrm {{{{\L }}\forall ^{m}}}} = {\mathrm {{{{\L }}\forall ^{}}}} = {\mathrm {{{{\L }}\forall ^{w}}}}$.

Some syntactic metatheorems valid in propositional core semilinear logics hold analogously for their first-order logics:

Theorem 12.23

((Cintula and Noguera 2011, Theorems 4.2.6, 4.2.8, and 4.3.9 and Corollary 4.2.11)) Let $\mathrm {L}$ be a core semilinear logic, ${\vdash }$ be either $\vdash _{\mathrm {{{L}\forall ^{}}}}$ or ${\vdash _{\mathrm {{{L}\forall ^{w}}}}}$, and ${\fancyscript{P}}$ be a predicate language. Then the following holds for each ${\fancyscript{P}}$-theory $T$, ${\fancyscript{P}}$-sentences $\varphi ,\psi ,$ and ${\fancyscript{P}}$-formula $\chi$:

• 1. The intersubstitutability:

  $$ \varphi \mathrel {\leftrightarrow }\psi \vdash \chi \mathrel {\leftrightarrow }\chi ', $$

  where $\chi '$ is obtained from $\chi$ by replacing some occurrences of $\varphi$ by $\psi$.

• 2. The constants theorem:

  $$ T\vdash \chi (c) \qquad \text { iff } \qquad T\vdash \chi (x),$$

  for any constant $c$ not occurring in $T\cup \{\chi \}$.

• 3. The proof by cases property:

  $$ \frac{T,\varphi \vdash \chi \qquad \qquad T,\psi \vdash \chi }{T,\varphi \mathbin {\vee }\psi \vdash \chi } $$

• 4. The semilinearity property:

  $$ \frac{T,\varphi \mathrel {\rightarrow }\psi \vdash \chi \qquad \qquad T,\psi \mathrel {\rightarrow }\varphi \vdash \chi }{T\vdash \chi } $$

  If, furthermore, $\mathrm {L}$ is almost $\mathrm {(MP)}$-based with a set of basic deductive terms ${\mathrm {bDT}}$, we can add:

• 5. The local deduction theorem:

  $$\begin{aligned} T,\varphi \vdash \chi \qquad \text{ iff }\qquad T\vdash \delta (\varphi ) \mathbin \rightarrow \chi \quad \text{ for } \text{ some } \delta \in \Pi ({\mathrm {bDT}}^*)_{\fancyscript{P}}, \end{aligned}$$

  where by $\Pi ({\mathrm {bDT}}^*)_{\fancyscript{P}}$ we denote the set of formulae resulting from any $\star$-formula from $\Pi ({\mathrm {bDT}}^*)$ by replacing all its propositional variables other than $\star$ by arbitrary ${{{\fancyscript{P}}}}$-sentences.

Petr  Hájek (1998b) (or later Hájek and Cintula 2006) used the local deduction theorems for schematic extensions of $\mathrm {HL}$ (for ($\triangle$-)core fuzzy logics resp.) to show the semilinearity property (even though only in the latter it is formulated explicitly), which in turn is a crucial prerequisite for proving the completeness theorem.

4.2 General and Witnessed Semantics

In this subsection we shall introduce the (witnessed) semantics of predicate fuzzy logics, corresponding to the axiomatic systems ${\mathrm {{{{L}}\forall ^{}}}}$ and ${\mathrm {{{{L}}\forall ^{w}}}}$ respectively. To simplify the formulation of upcoming definitions let us fix: a core semilinear logic $\mathrm {L}$ in a propositional language $\fancyscript{L}$, a predicate language ${\fancyscript{P}}=\langle { Pred , Func , Ar }\rangle$, and an $\mathrm {L}$-chain ${\varvec{B}}$.

Definition 12.17

A ${\varvec{B}}$ -structure $\mathbf M$ for the predicate language ${\fancyscript{P}}$ has the form: $\langle {M,(P_\mathbf M)_{P\in Pred }, (F_\mathbf M)_{F\in Func }}\rangle$, where $M$ is a non-empty domain; for each $n$-ary predicate symbol $P\in Pred ,$ $P_\mathbf M$ is an $n$-ary fuzzy relation on $M$, i.e., a function $M^n\rightarrow B$ (identified with an element of $B$ if $n=0$); for each $n$-ary function symbol $F\in Func$, $F_\mathbf M$ is a function $M^n\rightarrow M$ (identified with an element of $M$ if $n=0$).

Let $\mathbf M$ be a ${\varvec{B}}$-structure for ${\fancyscript{P}}$. An $\mathbf M$ -evaluation of the object variables is a mapping $\mathrm {v}$ which assigns an element from $M$ to each object variable. Let $\mathrm {v}$ be an $\mathbf M$-evaluation, $x$ a variable, and $a\in M$. Then by $\mathrm {v}[x{\mapsto }a]$ we denote the $\mathbf M$-evaluation such that $\mathrm {v}[x{\mapsto }a](x) = a$ and $\mathrm {v}[x{\mapsto }a](y) = \mathrm {v}(y)$ for each object variable $y$ different from $x$.

Let $\mathbf M$ be a ${\varvec{B}}$-structure for ${\fancyscript{P}}$ and $\mathrm {v}$ an $\mathbf M$-evaluation. We define the values of terms and the truth values of formulae in $\mathbf M$ for an evaluation $\mathrm {v}$ recursively as follows noting that in the last two clauses, if the infimum or supremum does not exist, then the corresponding value is taken to be undefined, and in all clauses, if one of the arguments is undefined, then the result is undefined:

$$\begin{aligned} \left\| {x}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= \mathrm {v}(x)\\ \left\| {F(t_1,\dots ,t_n)}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= F_\mathbf M(\left\| {t_1}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}},\dots ,\left\| {t_n}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}) \quad \text {for }F\in Func \\ \left\| {P(t_{1},\dots ,t_{n})}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= P_\mathbf M(\left\| {t_{1}}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}},\dots ,\left\| {t_{n}}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}) \quad \text {for }P\in Pred \\ \left\| {c(\varphi _{1},\dots ,\varphi _{n})}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= c_{\varvec{B}}(\left\| {\varphi _{1}}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}},\dots ,\left\| {\varphi _{n}}\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}) \quad \text {for } c \in \fancyscript{L}\\ \left\| {(\forall {x})\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= \inf \{ \left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}[x{\mapsto }a]} \mid a\in M \}\\ \left\| {(\exists {x})\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= \sup \{ \left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}[x{\mapsto }a]} \mid a\in M \}. \end{aligned}$$

We say that the $\varvec{B}$-structure $\mathbf M$ is

• safe if $\left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}$ is defined for each ${\fancyscript{P}}$-formula $\varphi$ and each $\mathbf M$-evaluation $\mathrm {v}$,

• witnessed if for each ${\fancyscript{P}}$-formula $\varphi$ we have:

  $$\begin{aligned} \left\| {(\forall {x})\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= \min \{ \left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}[x{\mapsto }a]} \mid a\in M \}\\ \left\| {(\exists {x})\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}}&= \max \{ \left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}[x{\mapsto }a]} \mid a\in M \}. \end{aligned}$$

Note that each witnessed structure is safe. To simplify the upcoming definitions and theorems we write $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ if $\left\| {\varphi }\right\| ^{{\varvec{B}}}_{\mathbf M,\mathrm {v}} \geqslant _{\varvec{B}} 1$ for each $\mathbf M$-evaluation $\mathrm {v}$.

Definition 12.18

Let $\mathbf M$ be a ${\varvec{B}}$-structure for ${\fancyscript{P}}$ and $T$ a ${\fancyscript{P}}$-theory. Then $\mathbf M$ is called a ${\varvec{B}}$ -model of $T$ if it is safe and $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ for each $\varphi \in T$.

Observe that models are safe structures by definition. Since, obviously, each safe ${\varvec{B}}$-structure is a ${\varvec{B}}$-model of the empty theory, we shall use the term model for both models and safe structures in the rest of the text.²⁷ By a slight abuse of language we use the term model also for the pair $\langle {{\varvec{B}},\mathbf M}\rangle$.

The following completeness theorems show that the syntactic presentations introduced above succeed in capturing the intended general chain-semantics for first-order fuzzy logics.²⁸

Theorem 12.24

((Cintula and Noguera 2011, Theorems 4.3.5 and 4.4.10)) Let $\mathrm {L}$ be a core semilinear logic, ${\fancyscript{P}}$ a predicate language, $T$ a ${\fancyscript{P}}$-theory, and $\varphi$ a ${\fancyscript{P}}$-formula. Then the following are equivalent:

• $T\vdash _{{\mathrm {{{{L}}\forall ^{}}}}}\varphi$.

• $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ for each $\mathrm {L}$-chain ${\varvec{B}}$ and each model $\langle {{\varvec{B}},\mathbf M}\rangle$ of the theory $T$.

Theorem 12.25

((Cintula and Noguera 2011, Theorem 4.5.12 and Example 4.5.3)) Let $\mathrm {L}$ be an axiomatic expansion of $\mathrm {SL}$ $^\ell _{\mathrm {ae}}$, ${\fancyscript{P}}$ a predicate language, $T$ a ${\fancyscript{P}}$-theory, and $\varphi$ a ${\fancyscript{P}}$-formula. Then the following are equivalent:

• $T\vdash _{{\mathrm {{{{L}}\forall ^{w}}}}}\varphi$.

• $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ for each $\mathrm {L}$-chain ${\varvec{B}}$ and each witnessed model $\langle {{\varvec{B}},\mathbf M}\rangle$ of the theory $T$.

4.3 Standard Semantics

Already in the pioneering works of Petr Hájek, as in the case of propositional fuzzy logics, the general chain completeness we have just seen was not considered sufficient and, in fact, a crucial item in his agenda was again the search for standard completeness theorems with respect to distinguished classes of models. In order to survey the corresponding results in our framework, in this section we restrict ourselves to countable predicate languages. We shall say that $\langle {{\varvec{B}},\mathbf M}\rangle$ is a $\mathbb {K}$ -model (of $T$) for some $\mathbb {K}\subseteq {{\mathbb {L}}_ lin }$ if $\langle {{\varvec{B}},\mathbf M}\rangle$ is a model (of $T$) and ${\varvec{B}}\in \mathbb {K}$.

Definition 12.19

Let $\mathrm {L}$ be a core semilinear logic and $\mathbb {K}\subseteq {{\mathbb {L}}_ lin }$. We say that ${\mathrm {{{L}\forall ^{}}}}$ enjoys enjoys (finite) strong $\mathbb {K}$ -completeness ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ (${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ resp.) if for each countable predicate language ${{{\fancyscript{P}}}}$, ${{{\fancyscript{P}}}}$-formula $\varphi$, and (finite) ${{{\fancyscript{P}}}}$-theory $T$ holds:

$$ T\vdash _{\mathrm {{{L}\forall ^{}}}} \varphi \quad \text {iff}\quad \langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi \text { for each } \mathbb {K}\text {-model } \langle {{\varvec{B}},\mathbf M}\rangle \text { of the theory }T $$

We say that ${\mathrm {{{L}\forall ^{}}}}$ enjoys $\mathbb {K}$ -completeness $\mathbb {K}{\mathrm {C}}$ if the equivalence holds for $T=\emptyset$.

All these properties are stronger than their corresponding ones for propositional logics:

Theorem 12.26

Let ${\mathrm {L}}$ be a core semilinear logic and $\mathbb {K}$ a class of $\mathrm {L}$-chains. If  ${\mathrm {{{L}\forall ^{}}}}$ has the ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ (${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ or $\mathbb {K}{\mathrm {C}}$ respectively), then $\mathrm {L}$ has the ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$ (${\mathrm {FS}}\mathbb {K}{\mathrm {C}}$ or $\mathbb {K}{\mathrm {C}}$ respectively).

As in the propositional case (Theorem 12.15), strong $\mathbb {K}$-completeness is related to an embedding property, although it is a stronger one requiring preservation of existing suprema and infima:

Definition 12.20

Let ${\varvec{A}}$ and ${\varvec{B}}$ be two algebras of the same type with (defined) lattice operations. We say that an embedding $f:{\varvec{A}}\rightarrow {\varvec{B}}$ is a $\sigma$ -embedding if $f(\sup C) = \sup f[C]$ (whenever $\sup C$ exists) and $f(\inf D) = \inf f[D]$ (whenever $\inf D$ exists) for each countable $C,D\subseteq A$.

Theorem 12.27

Let $\mathrm {L}$ be a core semilinear logic. If every countable $\mathrm {L}$-chain ${\varvec{A}}$ can be $\sigma$-embedded into some $\mathrm {L}$-chain ${\varvec{B}}\in \mathbb {K}$, then ${\mathrm {{{L}\forall ^{}}}}$ enjoys ${\mathrm {S}}\mathbb {K}{\mathrm {C}}$.

The proof of this theorem is almost straightforward. Unlike in the propositional case, the existence of $\sigma$-embeddings is not a necessary condition, as shown by (Cintula et al. (2009), Theorem 5.38), but nevertheless it is the usual method for proving these results. It also has an interesting corollary for completeness w.r.t. finite chains (recall the characterizations of ${\mathrm {S}}\fancyscript{F}{\mathrm {C}}$ in Theorem 12.17).

Corollary 12.5

Let $\mathrm {L}$ be a core semilinear logic. Then $\mathrm {L}$ enjoys the ${\mathrm {S}}\fancyscript{F}{\mathrm {C}}$ iff ${\mathrm {{{L}\forall ^{}}}}$ enjoys the ${\mathrm {S}}\fancyscript{F}{\mathrm {C}}$.

It is obvious that every ${\varvec{B}}$-structure over a finite $\mathrm {L}$-chain is necessarily witnessed. Thus we have the following proposition which can be used in order to disprove the $\fancyscript{F}{\mathrm {C}}$ for many logics.

Proposition 12.4

Let $\mathrm {L}$ be a core semilinear logic such that ${\mathrm {{{L}\forall ^{}}}}$ enjoys $\fancyscript{F}{\mathrm {C}}$. Then ${\mathrm {{{L}\forall ^{}}}} = {\mathrm {{{L}\forall ^{w}}}}$.

For instance, the examples by (Hájek (1998b), Lemma 5.3.6) can be used to show that $({\mathrm {C}}\exists )$ is unprovable in G$\forall$ and $({\mathrm {C}}\forall )$ is unprovable both in G$\forall$ and in $\Pi \forall$. We can also easily show that $\not \vdash _{\mathrm{NM}\forall } ({\mathrm {C}}\forall )$. Thus these logics do not enjoy $\fancyscript{F}{\mathrm {C}}$.

Table 12.11 Completeness properties for some first-order core semilinear logics

Table 12.11 collects results on real, rational and finite-chain completeness of prominent core semilinear logics. Their proofs are scattered in the literature (e.g. Hájek (1998b); Esteva and Godo (2001)). Cintula et al. (2009) give more information and detailed references. For logics weaker than ${\mathrm {{{\mathrm {MTL}}\forall ^{}}}}$ the negative results are derived from the corresponding failure of completeness at the propositional level, while the positive ones are justified by observing that the embeddings built to prove completeness for the underlying propositional logic are actually $\sigma$-embeddings. Observe that the family of logics in the first row of the table include ${\mathrm {{{{\mathrm {SL}^\ell }}\forall ^{}}}}$, which enjoys both strong rational and real (i.e. standard) completeness. This fact was not stated before in the literature because the only paper dealing with ${\mathrm {SL}^\ell }$ (Cintula et al. 2013) concentrated only on propositional logics, but it is not difficult to check that for $\mathrm {SL}^\ell$ the obtained embedding is also actually a $\sigma$-embedding, i.e., we obtain:

Theorem 12.28

Let ${\mathrm {S}}\subseteq \{{\mathrm {e}},{\mathrm {c}},{\mathrm {i}},{\mathrm {o}}\}$. Then for each countable predicate language ${{{\fancyscript{P}}}}$, ${{{\fancyscript{P}}}}$-formula $\varphi$, and ${{{\fancyscript{P}}}}$-theory $T$ holds:

$$ T\vdash _{\mathrm {{{{}{\mathrm {SL}_{\mathrm {S}}^{\ell }}}\forall ^{}}}} \varphi \quad \text {iff}\quad \langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi \text { for each }\fancyscript{R}\text {-model}\, \langle {{\varvec{B}},\mathbf M}\rangle \text { of the theory }T. $$

It is worth adding that for all core fuzzy logics appearing in the table the same results hold for their expansions with $\triangle$; moreover ${\mathrm {G}}_{\sim }$ behaves like $\mathrm {G}$, while ${{\mathrm {SHL}}}_{{\sim }}$ and $\L \Pi$ behave like $\mathrm {HL}$. Observe the rather surprising behavior of continuous t-norm based logics regarding the rational-chain semantics: while ${\mathrm {{{\L }\forall ^{}}}}$, ${\mathrm {{{\Pi }\forall ^{}}}}$, and ${\mathrm {{{{\mathrm {G}}}\forall ^{}}}}$ enjoy the $\mathrm {S}\fancyscript{Q}\mathrm {C}$, the logics ${\mathrm {{{{\mathrm {HL}}}\forall ^{}}}}$ and ${\mathrm {{{{{\mathrm {SHL}}}}\forall ^{}}}}$ do not even have $\fancyscript{Q}\mathrm {C}$ (Cintula et al. 2009). Petr Hájek (1998b) already gave an important hint towards the failure of rational completeness in ${\mathrm {{{{\mathrm {HL}}}\forall ^{}}}}$ and ${\mathrm {{{{{\mathrm {SHL}}}}\forall ^{}}}}$: he found a first-order formula,$(\forall x)(\chi \mathbin { \& }\varphi ) \rightarrow (\chi \mathbin { \& }(\forall x)\varphi )$, which holds in every model on a densely ordered $\mathrm {HL}$-chain but, as shown later by Esteva and Godo (2001), it is not a tautology of any of those two logics; therefore it makes sense to extend them with this axiom and, by doing so, one obtains new first-order logics complete with respect to all models over rational $\mathrm {HL}$-chains or, respectively, ${\mathrm {SHL}}$-chains (Cintula et al. 2009).

Finding particular examples of formulae witnessing failure of $\fancyscript{R}\mathrm {C}$ of a given logic is not an easy task. Even though some examples were found by Petr Hájek (2004b) for some particular cases, a usual method of proving this is to show that the set of standard tautologies (see next definition) is not recursively enumerable, and therefore it cannot coincide with the set of its theorems. Determining the position in the arithmetical hierarchy (e.g. Rogers 1967) of prominent sets of formulae (such as the tautologies of a given logic) is an important field of study in mathematical logic with major contributions done by Petr Hájek. Here we just briefly mention a few results related to fuzzy logics: a full treatment of the arithmetical complexity of first-order ($\triangle$-)fuzzy logics was presented by Hájek et al. (2011). Other references on the topic are Hájek (2001, 2004a, 2005a), Montagna (2001, 2005), Montagna and Noguera (2010).

First let us introduce some prominent sets of first-order formulae given by a core semilinear logic $\mathrm {L}$:

Definition 12.21

We say that a sentence $\varphi$ is

• A general (resp., standard) tautology of ${\mathrm {{{L}\forall ^{}}}}$ if $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ for each ($\fancyscript{R}$-)model $\langle {{\varvec{B}},\mathbf M}\rangle$.

• Generally (resp., standardly) satisfiable in ${\mathrm {{{L}\forall ^{}}}}$ if $\langle {{\varvec{B}},\mathbf M}\rangle \vDash \varphi$ for some ($\fancyscript{R}$-)model $\langle {{\varvec{B}},\mathbf M}\rangle$.

The sets of general and standard tautologies and generally and standardly satisfiable sentences are denoted, respectively, by ${\mathrm {genTAUT}}$, ${\mathrm {stTAUT}}$, ${\mathrm {genSAT}}$, and ${\mathrm {stSAT}}$.

For illustration, let us state the results for four predicate logics: ${\mathrm {{{{{\mathrm {HL}}}}\forall ^{}}}}$, ${\mathrm {{{{{\L }}}\forall ^{}}}}$, ${\mathrm {{{{G}}\forall ^{}}}}$, and ${\mathrm {{{{\Pi }}\forall ^{}}}}$. For each of them, the set of general tautologies is ${{\varvec{\Sigma }_1}}$-complete (thus they are recursively axiomatizable, but undecidable) and the set of generally satisfiable formulae is ${{\varvec{\Pi }_1}}$-complete. For the arithmetical complexity of their standard semantics see Table 12.12 (where “-c” stands for “-complete” and “${{\varvec{NA}}}$” for “non-arithmetical”). It can be seen that as far as standard semantics is concerned, the four logics differ drastically with respect to their degree of undecidability.

Table 12.12 Arithmetical complexity of standard semantics

5 Conclusions

In this chapter we have presented a general approach to fuzzy logics based on the logic $\mathrm {SL}^\ell$. We have introduced a broad class of, both propositional and predicate, core semilinear logics and shown their axiomatizations and completeness with respect to models over chains. Moreover, we have surveyed their completeness results with respect to distinguished semantics and obtained, in particular, that the weakest predicate fuzzy logic of our framework, ${\mathrm {{{{\mathrm {SL}^\ell }}\forall ^{}}}}$, enjoys the standard completeness theorem. Therefore, our flea still jumps (and jumps very well, even in the first-order case!) and we can arguably say that the quest for the basic fuzzy logic initiated by Petr Hájek so far seems to culminate with $\mathrm {SL}^\ell$. Indeed, both for propositional and first-order predicate logics, $\mathrm {SL}^\ell$ provides a good ground level to build broad families of logics containing all the important particular systems of fuzzy logic: propositional fuzzy logics are captured inside the class of core semilinear logics, while first-order fuzzy logics are obtained as extensions of the logic ${\mathrm {{{L}\forall ^{}}}}$ built over a core semilinear logic $\mathrm {L}$. Moreover, ${\mathrm {SL}^\ell }$ is the weakest possible logic one could take in the context of substructural logics in a language with lattice connectives, a conjunction which is not required to satisfy any property corresponding to the usual structural rules and its left and right residua. We do not know whether Mathematical Fuzzy Logic will require an even weaker system to serve as the basic fuzzy logic in the future. Only time will tell. What we can say is that, at the moment, we do not see any remaining legs to be pulled.