# Towards Fuzzy Constructive Type Theories

**Besik Dundua**

<figure><img src="image_1.png" /></figure>

School of Computer Science, Kutaisi International University, and Vekua Institute of Applied
Mathematics, Tbilisi State University, GEORGIA

**Furio Honsell**

<figure><img src="image_2.png" /></figure>

Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Udine University, ITALY

**Temur Kutsia**

<figure><img src="image_3.png" /></figure>

Research Institute for Symbolic Computation, Johannes Kepler University Linz, AUSTRIA

**Marina Lenisa**

<figure><img src="image_4.png" /></figure>

Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Udine University, ITALY

**Luigi Liquori**

<figure><img src="image_5.png" /></figure>

Centre Inria de l'Université Côte d'Azur, FRANCE

## Abstract

In this paper, we explore combinations of Fuzzy Logic and Constructive Higher Order Type Theory. Although Fuzzy Logic is more than 60 years old, and Fuzzy Type Theories have been studied in the classical case of Church's Theory of Types, there is yet no satisfactory understanding of how to deal with judgments of the shape $Γ ⊢ M :_e A$, where *e* is a fuzzy degree of confidence. Addressing this issue is important in view of the growing interest in quantitative and non-idempotent type theories. To this end, we introduce *fuzzy type assignment systems* in order to investigate how minimal fuzzy formulæ behave as types, according to some *fuzzy proposition-as-types* paradigm. Moreover, we study a fuzzy version of *intersection types*. In both systems assumptions are taken to be multisets and in $Γ ⊢ M :_e A$, *e* is either taken as a formula of minimal fuzzy logic or as its interpretation in the (residuated) lattice [0,1], endowed with a left-continuous T-norm. The first system sheds new light on how Fuzzy Logic relates to **BCK**-algebras. The latter, implicitly, keeps track of the number of times a given assumption is made. We prove the standard suite of metatheorems (inversion lemmata and subject-conversion) for the systems, and point to possible uses of the fuzzy minimal formula attached to the membership construct.

**2012 ACM Subject Classification** Theory of computation → Constructive mathematics; Theory of computation → Fuzzy logic

**Keywords and phrases** Fuzzy type theory, constructive type theory, lambda calculus, residuated lattices

**Funding** *Temur Kutsia:* Austrian Science Fund (FWF), Project P 35530

## 1 Introduction

Fuzzy Logic [14, 10, 12] is more than 60 years old. It is a form of many-valued logic in which the truth value of propositional variables may be any real number between 0 and 1, and it has been extensively used in control systems, in artificial intelligence, and recently in LifeTech. Significant work has already appeared on Fuzzy Type Theory in the classical setting of Church's Theory of Types [11], and as far as first order theories [6]. However, to the best of our knowledge, there is yet no complete and satisfactory understanding of how Fuzzy Logic combines with Higher Order *Constructive Type Theory*. We think that this issue needs to be addressed, since decorating a typing judgment with a fuzzy coefficient adds a new expressive dimension to the invariants, which types can capture, thus leading to *fuzzy constructive logic*. This should be particularly relevant in view of the growing interest, in the theoretical computer science community, in systems supporting quantitative and non-contractive reasoning, e.g. [8, 5, 4, 9].
In this paper, we introduce and investigate various notions of *fuzzy type assignment systems* for pure $\lambda$-calculus, and provide possible answers to the following questions.

- How do intuitionistic fragments of Fuzzy Logic behave as types in a possible *Fuzzy Proposition-as-Types* and *Proofs as $\lambda$-terms* paradigm?

- What is a fuzzy version of *Intersection Type Assignment Systems*?

Answering these two questions should pave the way for addressing more general questions such as the following: What are fuzzy twins of other type assignment systems à la Curry? What is the appropriate notion of Fuzzy Constructive Type Theory, for $\lambda$-terms à la Church? Moreover, since Fuzzy Logic has in general a non-idempotent semantics, how do fuzzy type assignment systems relate to quantitative and non-idempotent constructive type theories?

In particular, in the present paper we introduce three fuzzy type assignment systems. The first two systems $\mathcal{F}$ and $\mathcal{Q}$ provide an answer to the first question. In both systems, types are taken to be formulæ of Fuzzy Logic. They differ in that contexts are taken as sets of assumptions in $\mathcal{F}$, while in $\mathcal{Q}$ contexts are multisets of assumptions. Blurring the distinction between a fuzzy formula and its value in the standard semantics of Fuzzy Logic, namely the lattice [0,1] enriched with a left-continuous T-norm (see Definition 26), permits us to express properties of *inhabited fuzzy* formulæ by means of $\mathcal{F}$ and $\mathcal{Q}$. This approach highlights the connection with *affine $\lambda$-calculus*, thus recovering basic facts about minimal Fuzzy Logic, and its relation to **BCK-algebras** along a different route from the standard one as in e.g. [5]. Moreover, we show that taking contexts as multisets preserves the interpretation of fuzzy types under $\beta$-conversion.

Building on $\mathcal{Q}$, we introduce the *Fuzzy Intersection Type Assignment System $\mathcal{Q}^\cap$*, which is a “fuzzification” of the Intersection Type Assignment System [2, 3]. The system $\mathcal{Q}^\cap$ is a *quantitative*, hence *relevant*, system where fuzzy coefficients index the membership relation and contexts are *fuzzy multisets*, rather than sets. All the standard suite of results which hold in the *crisp* version, i.e. the original Intersection Types system, also hold for $\mathcal{Q}^\cap$. Namely, we have: inversion lemmata, subject expansion, and subject reduction. The benefit of this system, besides providing a theory of how the degree of confidence flows through applications and abstractions, permits keeping track of the number of occurrences of a variable in a term. We outline some applications. We chose to focus on Intersection Types because they generalize simple types and, moreover, can capture the class of strongly normalizing terms, as well as many other classes of $\lambda$-terms. We are confident that the same “fuzzification” can be similarly carried out for other types assignment systems for $\lambda$-terms à la Curry, such as higher order impredicative types.

For all notations and notions which are not explicitly spelled out in this paper, we refer to [3], for typed $\lambda$-calculi, and to e.g. [10, 12], for Fuzzy Logic.

**Synopsis.** In Section 2 we give basic definitions on Fuzzy Logic and Type Assignment Systems. In Section 3 we introduce the type assignment systems $\mathcal{F}$ and $\mathcal{Q}$ for assigning a fuzzy confidence degree to $\lambda$-terms and study their main properties. These systems amount to the case of *fuzzy membership* to a unique reflexive type $A \sim A \rightarrow A$ in Intersection Type Theory. Full Intersection Type Theory is considered in Section 4. Final remarks on Constructive Type Theories with a *fuzzy typing relation*, comparison with related work and directions for future work appear in Section 5. The Appendix A contains additional standard results and definitions in Fuzzy Logic.
# 2 Preliminaries

## 2.1 Fuzzy Logic

The language of minimal, i.e. negation-free, Fuzzy Logic is given by the following grammar:

$$d, e, f ::= X \mid d \land e \mid d \otimes e \mid d \Rightarrow e.$$

Its semantics is given by interpreting propositional variables X, as values in the interval [0,1] endowed with a left-continuous T-norm, thus making it a residuated lattice, see Appendix A. By abuse of notation, when clear from the context, we will use values in [0, 1] as constants in the language. The T-norm allows us to interpret the connectives, viz. ⊗ by the T-norm itself, ⇒ by its residuum, and ∧ by the minimum. We assume that ⊗ has higher priority than ⇒, the latter being right-associative, e.g. d ⇒ e ⇒ f ⊗ f' means d ⇒ (e ⇒ (f ⊗ f')). The three prominent examples of left-continuous T-norms on [0,1], namely Gödel's T-Norm, the product T-norm, and Łukasiewicz's T-norm, appear in Appendix A, together with some of the main properties of T-norms. We refer to [10, 12] for more details and basic definitions. A T-norm is said to be idempotent if d ⊗ d = d. Gödel's T-Norm is the only idempotent left-continuous T-norm.

## 2.2 Lambda terms and Intersection Type Assignment Systems

In this subsection, we introduce the untyped λ-calculus and the set of types that can be assigned to it. We focus on Intersection Type systems [2, 3].

### ► Definition 1 (λ-terms).

1. The set Λ of (untyped) λ-terms are defined as usual:

$$M, N ::= x \mid \lambda x.M \mid MN$$

where x is a variable, λx.M is an abstraction, and MN is a term application.

2. Affine λ-terms are λ-terms where each abstracted variable occurs at most once.

We refer to [1, 3] for standard notions and results concerning λ-calculus.

We briefly recall the basic definitions concerning intersection types, which are used Intersection Type Assignment Systems [3].

### ► Definition 2.

(i) Given a set of constants A and a distinguished constant U, the set T_A of intersection types over A are defined by the grammar:

$$A, B ::= c \mid U \mid A \to B \mid A \cap B$$

where c ∈ A;

(ii) A subtyping relation ≤ is a binary relation on T_A closed under the following axioms and rules:

$$A \leq A \ (\text{Refl})$$

$$A \cap B \leq A \ (\text{incL})$$

$$B \cap A \leq A \ (\text{incR})$$

$$B \to A \cap A' \leq (B \to A) \cap (B \to A') \ (\to \cap)$$

$$A \leq U \ (\text{Top})$$

$$U \leq A \to U \ (\to U)$$

$$\frac{A \leq B \quad A \leq B'}{A \leq B \cap B'} \ (\text{Glb})$$

$$\frac{A \leq B \quad B \leq B'}{A \leq B'} \ (\text{Trans})$$

$$\frac{A' \leq A \quad B \leq B'}{A \to B \leq A' \to B'} \ (\to)$$
(iii) An Intersection Type Theory is given by a set of rules on $\le$ which includes those in (ii).

We assume that $\cap$ has higher priority than $\to$, the latter being right-associative e.g. $A \to B \to C \cap C'$ means $A \to (B \to (C \cap C'))$. We write $A \sim B$ as short for $A \le B$ and $B \le A$. The above rules permit us to show that $\sim$ is a congruence w.r.t. to the signature of intersection types, given by the $\cap$ and $\to$ constructors, and that $\mathbb{T}/\sim$ is a meet semilattice.

### 3 Fuzzy Propositions-as-types

In this section we define type assignment systems for untyped $\lambda$-terms, where types are formulæ in minimal negation-free Fuzzy Logic as defined above, and hence $\lambda$-terms can be viewed as proofs for this fragment of Fuzzy Logic. This approach allows us to understand the systems with respect to two dual perspectives. On the one hand, evaluating the semantics of the types, using the residuated T-norm, these systems can be viewed as systems for assigning a confidence degree for a $\lambda$-term to belong to a universal type $A$ such that $A \sim A \to A$. This line of reasoning will be extended to the full system of intersection types, in Section 4. But, on the other hand, they can also be viewed as a means for characterizing sets of fuzzy formulæ, by way of the $\lambda$-terms which inhabit them as types, thereby providing an alternate route to basic results in minimal negation-free Fuzzy logic, see [12].

#### 3.1 Minimal Negation-free Fuzzy Logic - Qualitative Case

We introduce a fuzzy assignment system, i.e. a system for deriving judgments of the shape $\Gamma \vdash M : d$, where $\Gamma$ is a context, $M$ is a $\lambda$-term, and $d$ is a formula of minimal Fuzzy Logic.

**► Definition 3 (Fuzzy Assumptions, Fuzzy Qualitative Contexts).**

- A fuzzy assumption is a pair of the form $(x, d)$, usually written as $x : d$, where $x$ is a variable and $d$ is a fuzzy formula. The fuzzy assumption, $(x, d)$, means that the variable $x$ has membership or confidence degree $d$.

- A fuzzy qualitative context $\Gamma$ is a finite set of fuzzy assumptions with non-zero degrees. Note that $\Gamma$ may contain two or more different assumptions for the same variable, with possibly different confidence degrees.

Since we can interpret fuzzy formulæ as real numbers in $[0, 1]$, when convenient, we conflate $d$ with its value $[d] \in [0, 1]$, under a given interpretation of the propositional variables. Hence, in the following we write simply $(x, d)$.

**► Definition 4 (The type assignment system $\mathcal{F}$).** The qualitative Fuzzy Assignment System, $\mathcal{F}$, assigns fuzzy formulas to pure $\lambda$-terms according to the following rules:

$$ 
\begin{array}{l}
\overline{\Gamma, x : d \vdash_{\mathcal{F}} x : d} \quad (\text{Ax}) \\[1.5ex]
\frac{\Gamma, x : d_1, \dots, x : d_n \vdash_{\mathcal{F}} M : d \quad x \notin \Gamma}{\Gamma \vdash_{\mathcal{F}} \lambda x.M : d_1 \otimes \dots \otimes d_n \Rightarrow d} \quad (\Rightarrow I) \\[1.5ex]
\frac{\Gamma \vdash_{\mathcal{F}} M : d_1 \quad \Gamma \vdash_{\mathcal{F}} N : d_2 \quad d_1 \otimes d_2 > 0}{\Gamma \vdash_{\mathcal{F}} MN : d_1 \otimes d_2} \quad (\Rightarrow E)
\end{array}
$$

The following comments on the rules of the system $\mathcal{F}$ are in order.

- Rule ($\Rightarrow I$). We use the residuum, which corresponds to fuzzy implication. When dealing with multiple assumptions, we use the T-norm, i.e. weak conjunction, in the antecedent of $\Rightarrow$. Alternatively, we could have used the $\wedge$ operator corresponding to fuzzy strong
conjunction [12], namely the minimum. This choice, although reasonable, would make the quantitative system below, see Definition 10, more difficult to deal with.

- Rule (⇒E). The side condition $d_1 \otimes d_2 > 0$, can be dropped if we accept the rather trivial judgment $\Gamma \vdash_M M : 0$.

- Since when we interpret the Fuzzy Logic formulæ with a T-norm, we have that $x \otimes y \leq x$ but $x \leq y \Rightarrow x$, see Proposition 29, we see that (⇒E) decreases confidence, while (⇒I) increases confidence. Thus, this system complies with the explanation of the so-called *Sorites* Paradox [13] provided by Fuzzy Logic, namely that each application of *Modus Ponens* decreases the confidence degree.

- The following (≥) Rule, reminiscent of subtyping, naturally suggests itself,

$$ \frac{\Gamma \vdash_M M : d \quad d \geq e}{\Gamma \vdash_M M : e} (\geq). $$

We omit it for the sake of simplicity.

Notice that a given minimal fuzzy formula can have a derivation in $\mathcal{F}$ even if it is not valid w.r.t. to a T-norm. For instance, self-application can inhabit an invalid fuzzy formula, as shown in the following example.

### Example 5 (Self-application).

$$ \frac{x : d \vdash_M x : d \quad x : d \vdash_M x : d}{x : d \vdash_M xx : d \otimes d \quad \vdash_M \lambda x.xx : d \Rightarrow d \otimes d}. $$

In the following Theorem 6 and Proposition 7 we will characterize which proofs, i.e. $\lambda$-terms, yield valid fuzzy tautologies in system $\mathcal{F}$, when the predicates in the typing judgments are evaluated according to left-continuous T-norm.

### Theorem 6.

1. If $M$ is affine, i.e. variables occur at most once in the term, then for all left-continuous $T$-norms we have:

$$ x_1 : d_1, \dots, x_n : d_n \vdash_M M : d $$

implies

$$ \llbracket d_1 \Rightarrow \dots \Rightarrow d_n \Rightarrow d \rrbracket = 1. $$

2. If the $T$-norm is idempotent, then

$$ x_1 : d_1^1, \dots, x_1 : d_1^{m_1}, \dots, x_n : d_n^1, \dots, x_n : d_n^{m_n} \vdash_M M : d $$

implies

$$ \llbracket d_1^1 \otimes \dots \otimes d_1^{m_1} \Rightarrow \dots \Rightarrow d_n^1 \otimes \dots \otimes d_n^{m_n} \Rightarrow d \rrbracket = 1. $$

### Proof.

1. By induction on the derivation in $\mathcal{F}$, we can prove that if $M$ is affine and $\Gamma \vdash_M M : d$ then $\otimes \Gamma \leq d$, where $\otimes \Gamma$ is the tensor of the degrees in the assumptions of the variables which occur in $\Gamma$.

(Ax). Immediate, by Proposition 29.6 in Appendix A.

(⇒I). Immediate by induction hypothesis.

(⇒E). By monotonicity of the T-norm, see Definition 26.

Then, by Proposition 29.5 in Appendix A, we have $(\otimes \Gamma \Rightarrow d) = 1$.
2. By induction on the structure of the derivation in $\mathcal{F}$.

(Ax) and (⇒I). Immediate.

(⇒E). We use the fact that if $[[d_1 \Rightarrow d_2]] = 1$ and $[[e_1 \Rightarrow e_2]] = 1$ then we also have $[[d_1 \otimes e_1 \Rightarrow d_2]] = 1$ and $[[d_1 \otimes e_1 \Rightarrow e_2]] = 1$, and because of idempotency since $d_2 \otimes e_2 = \min\{d_2, e_2\}$, we have that $[[d_1 \otimes e_1 \Rightarrow d_2 \otimes e_2]] = 1$.

<figure><img src="image_6.png" /></figure>

We can also prove a form of converse to Theorem 6, namely that non-affine $\lambda$-terms do not inhabit tautologies, in general.

**Proposition 7.** Let $M$ be a closed $\lambda$-term where a variable, say $x$, occurs more than once in $M$, then we can derive a judgment $\Gamma \vdash_M M : d$ where, for some T-norm, $d$ does not evaluate to 1, that is, $d$ is not a fuzzy tautology.

**Proof.** We take the product T-norm, see Definition 28 in the Appendix. By induction on derivations, assume that variables that do not occur have confidence degree 1, and variables $x$ that occur have a value $p_x^{-1}$ for different primes $p_x$. We can prove by induction on derivations that if $\Gamma \vdash_M M : d$, then

$$d \leq \frac{\prod_{x_i \in \text{dom}(\Gamma)} p_{x_i}}{\prod_{x_i \in \text{dom}(\Gamma)} p_{x_i}^{\eta(x_i, M)}}$$

where $\eta(x_i, M)$ denotes the number of times the variable $x_i$ appears in $M$. Hence $d$ is smaller than 1 if a variable appears more than once.

<figure><img src="image_7.png" /></figure>

Theorem 6.1 has the form of a Deduction Theorem. From Proposition 7 and Theorem 6.1 one can easily see, by repeatedly applying Rule (⇒I) that only the types inhabited by an affine $\lambda$-term are formulæ whose value is 1 for all left-continuous T-norms. Recall that a type is inhabited when it is the type of a closed $\lambda$-term. It is folklore that these are the formulæ generated by applying the combinator $\mathbf{B} \equiv \lambda xyz.x(yz)$, $\mathbf{C} \equiv \lambda xyz.xzy$, and $\mathbf{K} \equiv \lambda xy.x$. Thus, we recover the connection with $\mathbf{BCK}$-algebras in Fuzzy Logic [12]. In particular, all formulæ inhabited by an affine $\lambda$-term in $\mathcal{F}$ hold in the Minimal T-norm Fuzzy Logic MTL [12], and hence in all its extensions, which include all left-continuous T-norm Fuzzy Logics.

From Theorem 6.2, we derive that all inhabited types are valid formulæ for the idempotent T-norm, namely Gödel T-norm, see Definition 28 in the Appendix. These are the purely implicational, i.e. minimal, intuitionistic tautologies, which are all valid in Gödel-Dummet Fuzzy Logic [10]. Clearly every minimal intuitionistic tautology is inhabited by a simply typed $\lambda$-term. Less obvious is that extending the inhabitants to all $\lambda$-terms does not increase the class of inhabited types.

We conclude this subsection with an example.

**Example 8.** Proposition 7 implies that $\vdash_M \mathbf{S} \equiv \lambda xyz.xz(yz) : d$, then it is not the case that $d = 1$ for every left-continuous T-norm. However, for a linear variant of $\mathbf{S}$, namely $\lambda xyzw.xz(yw)$ we have that if $\vdash_M \lambda xyzw.xz(yw) : d$, then the evaluation of $d$ in any left-continuous T-norm is 1.

## 3.2 Minimal Fuzzy Logic - Quantitative Case

In this subsection we modify system $\mathcal{F}$ taking contexts to be fuzzy multisets, namely we allow them to contain two or more equal or different assumptions for the same variable. We
will see that by doing so all inhabited fuzzy logic formulæ necessarily have value 1, in any left-continuous T-norm.

**Definition 9 (Fuzzy Quantitative Context).** A fuzzy quantitative context $\Gamma$ is a finite multiset of fuzzy assumptions with non-zero degrees.

**Definition 10 (Quantitative Fuzzy Assignment, $Q$).** The rules of the quantitative Fuzzy Assignment System, $Q$, are the following:

$$ \overline{x : d \vdash_Q x : d}^{(\Lambda x)} $$

$$ \frac{\Gamma, x : d_1, \dots, x : d_n \vdash_Q M : d \quad x \notin \Gamma \quad (\Rightarrow I)}{\Gamma \vdash_Q \lambda x.M : d_1 \otimes \dots \otimes d_n \Rightarrow d} $$

$$ \frac{\Gamma \vdash_Q M : d \quad x \notin \Gamma \quad (\Rightarrow 0)}{\Gamma \vdash_Q \lambda x.M : 1 \Rightarrow d} $$

$$ \frac{\Gamma_1 \vdash_Q M : d_1 \quad \Gamma_2 \vdash_Q N : d_2 \quad d_1 \otimes d_2 > 0 \quad (\Rightarrow E)}{\Gamma_1 :: \Gamma_2 \vdash_Q MN : d_1 \otimes d_2} $$

where $::$ denotes multiset union.

Notice that in $(Ax)$, above, there is no extra-context, to enforce the relevance of this quantitative system. Therefore, we need to add Rule $(\Rightarrow 0)$ to take care of weakening.

Theorem 12, below, shows that the inhabited fuzzy formulæ in $Q$ have confidence degree 1 for any T-norm. First, we need a lemma.

**Lemma 11 (Q-Invariance).** Let $\otimes \Gamma$ denote the tensor product of all confidence degrees assigned to variables in the context $\Gamma$, if $\Gamma \vdash_Q M : d$, then $\otimes \Gamma \le d$.

**Proof.**

By induction on the derivation in $Q$:
(Ax). Immediate, by Proposition 29.6 in Appendix A;
(⇒I) and (⇒0). Immediate by induction hypothesis;
(⇒E). By monotonicity of the T-norm, see Definition 26.

**Theorem 12.**

If the T-norm is left-continuous, then

$$ x_1 : d_1^1, \dots, x_1 : d_1^{m_1}, \dots, x_n : d_n^1, \dots, x_n : d_n^{m_n} \vdash_Q M : d $$

implies

$$ \llbracket d_1^1 \otimes \dots \otimes d_1^{m_1} \Rightarrow \dots \Rightarrow d_n^1 \otimes \dots \otimes d_n^{m_n} \Rightarrow d \rrbracket = 1. $$

**Proof.** By Lemma 11 we see that if $\Gamma \vdash_Q M : d$, then $\otimes \Gamma \le d$, hence using Proposition 29.5 in Appendix A we get the result.

It is natural now to ask the following question: what are the inhabited types in System $Q$? The simple answer is given in the following proposition.

**Proposition 13.** The class of inhabited types in $Q$ is the same as that of the types inhabited in $\mathcal{F}$ by affine terms.

**Proof.** Taking different variables for different uses of the rule (Ax), any derivation in $Q$ can be turned in a derivation in $\mathcal{F}$ for an affine term.
We end this subsection remarking that both in $\mathcal{F}$ and $\mathcal{Q}$ all $\lambda$-terms can receive infinitely many degrees of confidence depending on which (quantitative) fuzzy contexts we start from. For instance, using the trivial assignment, all terms can receive degree of confidence 1, even unsolvable terms, and hence also unsolvable terms can play the role of inhabitants. Fuzzy Intersection Type theories allow us to harness the class of derivations, as we will see in Section 4.

## 3.3 Subject-Reduction

As for all type assignment systems, it is natural to ask whether types are preserved under reduction/expansion of the term. Since both $\mathcal{F}$ and $\mathcal{Q}$ are sensitive to the number of times an assumption appears in the proof, albeit in different ways, the reduction of the subject and the expansion of the subject are not immediate. Actually, for $\mathcal{F}$ we have the following counterexamples.

**Counterexample 14 (Subject Expansion Fails in $\mathcal{F}$ for $\Delta I$).** We recall that $\Delta \equiv \lambda x.xx$ and $I \equiv \lambda x.x$. Consider the following derivation:

$$ \frac{x : d \vdash_{\mathcal{F}} x : d \qquad x : d \vdash_{\mathcal{F}} x : d}{x : d \vdash_{\mathcal{F}} xx : d \otimes d} \qquad \frac{x : d \vdash_{\mathcal{F}} x : d}{\emptyset \vdash_{\mathcal{F}} \lambda x.xx : d \Rightarrow d \otimes d} \qquad \frac{x : d \vdash_{\mathcal{F}} x : d}{\emptyset \vdash_{\mathcal{F}} \lambda x.x : d \Rightarrow d} \\ \hline \emptyset \vdash_{\mathcal{F}} (\lambda x.xx)(\lambda x.x) : (d \Rightarrow d \otimes d) \otimes 1 $$

now $(\lambda x.xx)(\lambda x.x) \to_{\beta} (\lambda x.x)(\lambda x.x)$, and, since for all T-norms $d \Rightarrow d = 1$, we have

$$ \frac{\emptyset \vdash_{\mathcal{F}} (\lambda x.x) : d \Rightarrow d \qquad \emptyset \vdash_{\mathcal{F}} (\lambda x.x) : d \Rightarrow d}{\emptyset \vdash_{\mathcal{F}} (\lambda x.x)(\lambda x.x) : 1 \otimes 1}, $$

but in the product T-norm $\llbracket (d \Rightarrow d \otimes d) \otimes 1 \rrbracket \leq \llbracket 1 \otimes 1 \rrbracket = 1$, in general. Hence in $\mathcal{F}$ the reduct can have a higher confidence degree than the redex.

**Counterexample 15 (Subject Reduction fails in $\mathcal{F}$ for (2 2)).** We recall that 2= $\lambda xy.x(xy)$ and 4= $\lambda xy.x(x(xy))$ are Church encodings of the natural numbers 2 and 4. Consider the following derivation:

$$ \frac{x : d, y : d \vdash_{\mathcal{F}} x(xy) : d \otimes d \otimes d}{\emptyset \vdash_{\mathcal{F}} \lambda xy.x(xy) : d \Rightarrow d \Rightarrow d \otimes d \otimes d} \qquad \frac{x : d, y : d \vdash_{\mathcal{F}} x(xy) : d \otimes d \otimes d}{\emptyset \vdash_{\mathcal{F}} \lambda xy.x(xy) : d \Rightarrow d \Rightarrow d \otimes d \otimes d} \\ \hline \emptyset \vdash_{\mathcal{F}} \mathbf{2} \mathbf{2} : (d \Rightarrow d \Rightarrow d \otimes d \otimes d) \otimes (d \Rightarrow d \Rightarrow d \otimes d \otimes d), $$

but $\mathbf{2} \mathbf{2} \to_{\beta} \mathbf{4}$. We have:

$$ \frac{x : d, y : d \vdash_{\mathcal{F}} x(x(xy)) : d \otimes d \otimes d \otimes d \otimes d}{\emptyset \vdash_{\mathcal{F}} \lambda xy.x(x(xy)) : d \Rightarrow d \Rightarrow d \otimes d \otimes d \otimes d \otimes d \otimes d}, $$

but in the product T-norm the value of the reduct is $d \otimes d \otimes d$, which is strictly smaller than the value of the redex, which is $d \otimes d$.

The counterexamples above show that the T-norm of the reduct can be strictly larger or strictly smaller than that of the redex. So we have the following proposition.

**Proposition 16.** Subject conversion holds in System $\mathcal{F}$ if and only if the norm is idempotent.
**Proof.** The “only if” part follows from Counterexamples 14 and 15. We have, in general, $d \otimes d \leq d$, but then $d \Rightarrow d \otimes d = \sup\{e \mid d \otimes e \leq d \otimes d\}$ since the norm is continuous. If this were 1, then we would have that $d = d \otimes d$, namely the T-norm would be idempotent. The “if” part follows from the fact that if the T-norm is idempotent by Theorem 6 we have that the value of the fully abstracted inhabited type is always 1. ◀

If we were to consider only affine terms in $\mathcal{F}$, $\beta$-conversion would hold. This can be expressed in the following proposition, which involves $\mathcal{Q}$.

**Proposition 17.** *Subject Reduction and Subject Expansion hold in System $\mathcal{Q}$.*

**Proof.** Immediate, since in the system $\mathcal{Q}$, the value of fully abstracted inhabited types is always 1. ◀

# 4 Fuzzy Intersection Types

We are now in the position of fruitfully studying the combination of intersection types, see Definition 2, with fuzzy type-membership. Namely, we introduce a *fuzzy type assignment* system assigning intersection types to pure $\lambda$-terms.

**Definition 18 (Typing assumption, typing context).**

1. A typing assumption is a triple of the form $(x, A, d)$, usually written as $x :_d A$, where $x$ is a variable, $A$ is a type and $d$ is a fuzzy formula, see Section 2.1, or, equivalently, a real number in $[0, 1]$ obtained by its evaluation w.r.t. a T-norm. Its intended meaning is that $x$ belongs to the type $A$ with degree of confidence $d$, in the context $\Gamma$.

2. A typing context $\Gamma$ is a finite multiset of typing assumptions with non-zero degrees.

Notice that a context $\Gamma$ may contain two or more assumptions for the same variable, possibly with the same type, and the same confidence degree. Thus, a typing context can be seen as a *fuzzy multiset*.

**Definition 19 (Quantitative Fuzzy Intersection Types $\mathcal{Q}^\cap$).** *The typing rules of the Fuzzy Intersection Types $\mathcal{Q}^\cap$ are the following:*

$$ \overline{x :_d A \vdash_{\mathcal{Q}^\cap} x :_d A} (Ax) \qquad \overline{\vdash_{\mathcal{Q}^\cap} M :_1 U} (U) $$

$$ \frac{\Gamma, x :_{d_1} A_1, \dots, x :_{d_n} A_n \vdash_{\mathcal{Q}^\cap} M :_d A \quad x \notin \text{dom}(\Gamma)}{\Gamma \vdash_{\mathcal{Q}^\cap} \lambda x.M :_{d_1 \otimes \dots \otimes d_n \Rightarrow d} A_1 \cap \dots \cap A_n \to A} \quad (\to I) $$

$$ \frac{\Gamma \vdash_{\mathcal{Q}^\cap} M :_d A \quad x \notin \text{dom}(\Gamma)}{\Gamma \vdash_{\mathcal{Q}^\cap} \lambda x.M :_{1 \Rightarrow d} B \to A} \quad (\to 0) $$

$$ \frac{\Gamma_1 \vdash_{\mathcal{Q}^\cap} M :_{d_1} A \to B \quad \Gamma_2 \vdash_{\mathcal{Q}^\cap} N :_{d_2} A \quad d_1 \otimes d_2 > 0}{\Gamma_1 :: \Gamma_2 \vdash_{\mathcal{Q}^\cap} MN :_{d_1 \otimes d_2} B} \quad (\to E) $$

$$ \frac{\Gamma_1 \vdash_{\mathcal{Q}^\cap} M :_{d_1} A \quad \Gamma_2 \vdash_{\mathcal{Q}^\cap} M :_{d_2} B}{\Gamma_1 :: \Gamma_2 \vdash_{\mathcal{Q}^\cap} M :_{d_1 \wedge d_2} A \cap B} (\cap I) \quad \frac{\Gamma \vdash_{\mathcal{Q}^\cap} M :_d A \quad A \leq B}{\Gamma \vdash_{\mathcal{Q}^\cap} M :_d B} (\leq) $$

where $\Gamma :: \Gamma'$ denotes multiset union, i.e. multiplicities of occurrences are not erased.

Some comments are in order.
■ How does the system $Q^\cap$ qualify with respect to contraction and idempotency? It is contraction free with respect to the fuzzy formula indexing the “:$d$” in the judgment $\Gamma \vdash_{Q^\cap} M :_d A$, but although contexts are multisets, the system is nonetheless idempotent as far as intersections are concerned, e.g. in rule $(\rightarrow I)$. However, not being idempotent w.r.t $\otimes$ in the degree of confidence, the judgment stores the information on the number of times an assumption is made, as if it were non-idempotent, only in a different format. Therefore, it has a quantitative nature.

■ The standard Intersection Type Assignment System [3], $T^\cap$, can be obtained from $\vdash_{Q^\cap}$ by erasing all fuzzy coefficients from the “:$d$” symbol, namely $(\Gamma \vdash_{Q^\cap} M :_d A)^\#$ yields $\Gamma' \vdash_{\cap} M : A$, where $\Gamma'$ is the set obtained from $\Gamma$ erasing multiple assumptions after having erased the confidence degree in each assumption; we denote by $(\Gamma)^\#$ the crisp context thus obtained.

■ We could introduce a fuzzy intersection type assignment system building on $\mathcal{F}$ rather than $Q$, but then the value of the fuzzy index would not be preserved by reduction or expansion, unless we focus on Gödel's T-norm, or affine $\lambda$-terms.

■ Notice, incidentally, that when reasoning with confidence degrees, $\Rightarrow$ behaves contravari-
antly on domains and covariantly on domains, as does $\rightarrow$ in intersection types theories.
That is, if $d \le d'$ and $e \le e'$, then $d' \Rightarrow e \le d \Rightarrow e'$.

- In rule $(\cap I)$ rather than $d_1 \wedge d_2$, which is interpreted by the minimum, we could have taken $\otimes$. Since $d_1 \otimes d_2 \le \min\{d_1, d_2\}$, our choice is more intuitive and does not affect the statement of the results.

- In Rule (≤) we could have allowed for a weakening of the degree of confidence in the conclusion, but this would break the preservation of the degree of confidence under conversion.

- As we did for the earlier systems, according to the needs of the argument, when clear from the context, we will consider the index in $:_d$ either as a formula of minimal negation-free Fuzzy Logic, or as its value w.r.t. to a given T-norm.

■ The confidence degree in Rule (U) appears to be the natural one.

We are now in the position of proving the main theorem.

► **Theorem 20.** If

$$
x_1 :_{d_{1,1}^1} A_1^1, \dots, x_1 :_{d_{1,k_1}^1} A_1^1, \dots, x_1 :_{d_{m_1,1}^1} A_{m_1}^1, \dots, x_1 :_{d_{m_1,k_{m_1}}^1} A_{m_1}^1, \dots
$$

...

$$
\dots, x_n :_{d_{1,1}^n} A_1^n, \dots, x_n :_{d_{1,k_1}^n} A_1^n, \dots, x_n :_{d_{m_n,1}^n} A_{m_n}^n, \dots, x_n :_{d_{m_n,k_{m_n}}^n} A_{m_n}^n \vdash_{Q^n} M :_d \sigma,
$$

then

$$
\llbracket d_{1,1}^1 \otimes \dots \otimes d_{1,k_1}^1 \Rightarrow \dots \Rightarrow d_{m_1,1}^1 \otimes \dots \otimes d_{m_1,k_{m_1}}^1 \Rightarrow \dots
$$

...

$$
\dots d_{1,1}^n \otimes \dots \otimes d_{1,k_1}^n \Rightarrow \dots \Rightarrow d_{m_n,1}^n \otimes \dots \otimes d_{m_n,k_{m_n}}^n \Rightarrow d \] = 1
$$

and

$$
\Gamma^{\#} \vdash_{\mathcal{T}} M : A
$$

in the standard intersection type theory.
**Proof.** (sketch) By induction on the structure of derivations we prove that the systems $Q^\cap$ and the standard intersection types assignment system $\mathcal{T}$ progress in parallel. Theorem 12 ensures that the interpretation of the fuzzy formula indexing the membership relation preserves the overall value 1. The only new case to consider is $\cap I$, but since $d_1 \otimes d_2$ gives smaller values, the overall value of $d_1 \wedge d_2$ is still 1. ◀

We can now also establish the standard suite of proof theoretical results on intersection types assignment systems.

► **Lemma 21 (Inversion Lemma).** 1. If $\Gamma \vdash_{Q^\cap} x :_d A$ and $A \not\cong U$, then $\Gamma(x) \le A$;

2. If $\Gamma \vdash_{Q^\cap} MN :_d A$ and $A \not\cong U$, then there exist $I, B_i, C_i$ for $i \in I$, such that $\bigcap_{i \in I} C_i \le A$ and $\Gamma \vdash_{Q^\cap} M :_{e_i} B_i \to C_i$ and $\Gamma \vdash_{Q^\cap} N :_{f_i} B_i$ for all $i \in I$, and $\otimes_{i \in I} e_i \otimes f_i$ is a subformula of $d$;

3. If $\Gamma \vdash_{Q^\cap} \lambda x.M :_d A$, then there exist $I$ and $B_i, C_i$ for $i \in I$ such that $\bigcap_{i \in I} (B_i \to C_i) \le A$ and $\Gamma, x :_{e_i} B_i \vdash_{Q^\cap} M :_{f_i} C_i$ for all $i \in I$, and $\otimes_{i \in I} e_i \Rightarrow f_i$ is a subformula of $d$.

**Proof.** By induction, paralleling the proof of the Inversion Lemma [3, Theorem 14.1.1]. ◀

► **Theorem 22 (Subject Expansion).** $M \to_\beta M'$ and $\Gamma \vdash_{Q^\cap} M' :_d A$ imply $\Gamma \vdash_{Q^\cap} M :_e A$.

**Proof.** Paralleling the proof of Subject Expansion [3, Corollary 14.2.5(ii)]. ◀

► **Theorem 23 (Subject Reduction).**

$$M \to M' \text{ and } \Gamma \vdash_{Q^\cap} M :_d A \text{ imply } \Gamma \vdash_{Q^\cap} M' :_e A'$$

**Proof.** Paralleling the proof of Subject Reduction [3, Proposition 14.2.1(ii)], using the fact that $\Gamma \vdash_{Q^\cap} \lambda x.N :_d A \to B$ implies $\Gamma, x :_{d_1} A \vdash_{Q^\cap} N :_{d_2} C$ for the appropriate shapes of the confidence indexes, according to the Inversion Lemma 21. ◀

In the above Theorems 22 and 23 one could give a sharper relation on the shapes of the formulæ occurring in the indexes $d$ and $e$. In the following Subsection 4.1 we elaborate on this issue.

► **Example 24 (Self-application Revisited).**

$$\frac{x :_d (A \to B) \cap A \vdash_{Q^\cap} x :_d (A \to B) \cap A}{x :_d (A \to B) \cap A \vdash_{Q^\cap} x :_d (A \to B)} \qquad \frac{x :_e (A \to B) \cap A \vdash_{Q^\cap} x :_e (A \to B) \cap A}{x :_e (A \to B) \cap A \vdash_{Q^\cap} x :_e A} \\ \frac{x :_d (A \to B) \cap A, x :_e (A \to B) \cap A \vdash_{Q^\cap} x x :_{d \otimes e} A}{\vdash_{Q^\cap} \lambda x.x x :_{d \otimes e \Rightarrow d \otimes e} B}$$

## 4.1 What sort of information can we extract from the fuzzy degree of a judgment?

If we evaluate the confidence degree of a provable judgment $\Gamma \vdash_{Q^\cap} M :_d A$, in $[0, 1]$, this gives us a measure on the membership of the term $M$ to the type $A$. But viewing the confidence degree $d$ as a formula of minimal fuzzy logic, we also have a “skeleton” of the derivation which established the inhabitation of the type $A$ by $M$. The confidence degree encodes a lot of information indeed. Here are some intriguing questions and conjectures.

- To what extent can the derivation be reconstructed from a provable judgment in $Q^\cap$? We conjecture that the inhabitation problem $\vdash_{Q^\cap} ? :_d A$ should be decidable. This conjecture is supported by the decidability of inhabitation for idempotent intersection types, see [3].

- The shape of the fuzzy formula should provide an estimate on the length of the longest $\beta$-reduction of $M$, if $M$ is typed without $U$, that is, if it is strongly normalizing.
5 Final remarks

In this paper, we have started an investigation of how Fuzzy Logic fares with Constructive Type Theory in view of the growing interest on quantitative systems in constructive Type Theory. We have proposed a number of fuzzy type assignment systems. These permit us to derive some results on Fuzzy Logic *per se*, through a fuzzy analogue of the formulæ-as-types paradigm, as well as provide a “fuzzification” of intersection type theories for pure λ-calculus. We plan to explore in the future λ-calculi à la Church, such as Constructive Type Theories where judgments have the shape $\Gamma \vdash_Q M :_d A$, but also have equality judgments.
$\Gamma \vdash_Q M_1 = M_2 :_d A$.

A related line of research, which we intend to explore, is how to derive a suitable fuzzy intersection type assignment system starting from a notion of *fuzzy similarity* between types. The natural understanding of fuzzy equality-types in Constructive Type Theory, given above, namely $\Gamma \vdash_Q M_1 =_d M_2 : A$, is a similarity relation, see Definition 30 in the Appendix. More precisely, given basic sets $D_i$'s, assume that a *similarity relation*, $S_{D_i}$, is given for each. Is there a natural way to extend the similarity to higher types, thereby deriving a fuzzy simple type-assignment system? Moreover, can we take $(D, \cdot)$ to be an applicative structure, and use as similarity the inverse of Hausdorff distance, *i.e.* $S_{P(D)}(A, B) = \min\{\inf_{x \in A} \sup_{y \in B} S_D(x, y), \inf_{x \in B} \sup_{y \in A} S_D(x, y)\}$, to inductively define similarity between logical relations within *D*? Appropriate conditions on the applicative behaviour of the points in *D* need to be enforced, however. This could provide a reading of the results in [9] on λ-quantitative theories, in terms of similarities, rather than of metrics.

**Related Work.** Some of our results can also be derived from the results on **BCK**-algebras in the theory of Fuzzy Propositional Logics, see e.g. [12], but our proofs follow a different route. Vilém Novák and his group have worked considerably on Fuzzy Type theory, but have mainly taken a classical approach [11]. Castelnuovo and Miculan [6] consider first order fuzzy theories in general, whereas we focus on higher order structures. A few authors have considered Fuzzy Type Theory specifically. G. Coraglia has done some preliminary work on Fuzzy Type Theory in the context of 2-categories (see https://etagreta.github.io/).

Since, as we already pointed out, Fuzzy Logic has a non-idempotent flavour, our work relates to non-idempotent intersection type theories [8, 7, 5, 4]. The information stored in the type in [5] is included in the information stored in the fuzzy formula that indexes the typing judgment in our system $Q^\frown$. More work needs to be done to compare the two approaches in depth.

We hope that the present paper will stimulate future discussions on the intriguing combination of Fuzzy Logic and Constructive Type Theory, as well as other formal systems for reasoning about concurrent processes.

References

1. Henk Barendregt. *The Lambda Calculus - its Syntax and Semantics*, volume 103 of *Studies in logic and the foundations of mathematics*. North-Holland, 1985. URL: https://api.pageplace.de/preview/DT0400.9780080933757_A23543814/preview-9780080933757_A23543814.pdf.

2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. *Journal of Symbolic Logic*, 48(4):931–940, 1983. doi:10.2307/2273659.

3. Henk Barendregt, Wil Dekkers, and Richard Statman. *Lambda Calculus with Types*. Cambridge University Press, 2013. doi:10.1017/CBO9781139032636.
4 Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. *Log. Methods Comput. Sci.*, 14(3), 2018. doi:10.23638/LMCS-14(3:7)2018.

5 Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. *Log. J. IGPL*, 25(4):431–464, 2017. doi:10.1093/JIGPAL/JZX018.

6 Davide Castelnovo and Marino Miculan. Fuzzy algebraic theories. In Florin Manea and Alex Simpson, editors, *30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)*, volume 216 of *LIPIcs*, pages 13:1–13:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.CSL.2022.13.

7 Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Mathematical Structures in Computer Science*, 28(7):1169–1203, 2018. doi:10.1017/S0960129516000396.

8 Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, *TACS*, volume 789 of *LNCS*, pages 555–574. Springer, 1994. doi:10.1007/3-540-57887-0_115.

9 Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On quantitative algebraic higher-order theories. In Amy P. Felty, editor, *7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel*, volume 228 of *LIPIcs*, pages 4:1–4:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.FSCD.2022.4.

10 George Metcalfe. Fundamentals of fuzzy logic. 2005. URL: https://api.semanticscholar.org/CorpusID17549644.

11 Vilém Novák. On fuzzy type theory. *Fuzzy Sets Syst.*, 149(2):235–273, 2005. doi:10.1016/J.FSS.2004.03.027.

12 Rostislav Horčík. Petr Cintula, Petr Hájek. Formal systems of fuzzy logic and their fragments. *Annals of Pure and Applied Logic*, 150:49–72, 2007. doi:10.1016/j.apal.2007.07.004.

13 Sorites paradox. https://plato.stanford.edu/entries/sorites-paradox/.

14 L.A. Zadeh. Fuzzy sets. *Information and Control*, 8(3):338–353, jun 1965. doi:10.1016/S0019-9958(65)90241-x.

A Notions in Fuzzy logic

► **Definition 25.** A fuzzy set is a pair $(S, \mu_S)$, where $S$ is a set and $\mu_S : S \to [0, 1]$ is a function. For all $x \in S$, $\mu_S(x)$ is called the degree of membership of $x$. We say that:

- $x$ is fully included in $(S, \mu_S)$, if $\mu_S = 1$;

- $x$ is not included in $(S, \mu_S)$, if $\mu_S(x) = 0$;

- $x$ is partially included in $(S, \mu_S)$, if $0 < \mu_S(x) < 1$.

If all $x \in S$ are fully included in $S$, the fuzzy set $S$ is said to be crisp.

► **Definition 26 (T-norm).** A T-norm, see [10], is a binary function $T : [0, 1] \times [0, 1] \to [0, 1]$ that satisfies the following properties:

- commutativity: $T(a, b) = T(b, a)$,

- associativity: $T(a, T(b, c)) = T(T(a, b), c)$,

- monotonicity: $T(a, b) \le T(c, d)$ if $a \le c$ and $b \le d$,

- the number 1 is the identity element: $T(a, 1) = a$.

Usually, T-norms are written in infix notation and the symbol $\otimes$ is used to denote them. In the paper, we consider only left-continuous t-norms.
**► Definition 27 (Residuum).** A binary function $\otimes: [0,1]^2 \to [0,1]$ is said to be residue if and only if there exists a binary function $\Rightarrow: [0,1]^2 \to [0,1]$ called the residuum of $\otimes$, such that $\otimes$ and $\Rightarrow$ form an adjoint pair, i.e.:

$$ \forall x, y, z \in [0, 1]. x \otimes y \leq z \Leftrightarrow x \leq y \Rightarrow z. $$

**► Definition 28.** Prominent examples of left-continuous T-norms are:

■ Gödel T-norm: $a \otimes b = \min(a, b)$, whose residuum is

$$ a \Rightarrow b = \begin{cases} b & \text{if } b \leq a \\ 1 & \text{otherwise;} \end{cases} $$

■ product T-norm: $a \otimes b = a * b$, whose residuum is

$$ a \Rightarrow b = \begin{cases} b/a & \text{if } b \leq a \\ 1 & \text{otherwise;} \end{cases} $$

■ Łukasiewicz T-norm: $a \otimes b = \max(0, a + b - 1)$, whose residuum is

$$ a \Rightarrow b = \begin{cases} 1 - a + b & \text{if } b \leq a \\ 1 & \text{otherwise.} \end{cases} $$

**► Proposition 29 (Norms with Residuum).** Given a left-continuous T-norm, $\otimes$, we have the following standard properties:

1. $\otimes$ uniquely determines a residuum defined as follows

$$ a \Rightarrow b := \sup\{c \mid a \otimes c \leq b\}. $$

2. $\Rightarrow$ is monotone in the second argument and anti-monotone in its first argument;

3. $x \Rightarrow 1 = 1, 1 \Rightarrow x = x$;

4. $y \leq x \Rightarrow y$;

5. $x \leq y$ implies $x \Rightarrow y = 1$;

6. $x \otimes y \leq x$, and hence $x \otimes y \leq \min\{x, y\}$;

7. $(x \otimes y) \Rightarrow z = x \Rightarrow (y \Rightarrow z)$;

8. $(x \otimes (x \Rightarrow y)) \leq y$;

9. $\min(d_1 \Rightarrow d, d_2 \Rightarrow d) = \max(d_1, d_2) \Rightarrow d$, and hence $x \otimes (x \Rightarrow y) \leq \min(x, y)$.

**Proof.** ■ Property (1) follows by definition the adjunction in Definition 27.

■ Properties (2)-(5) follow from item (1).

■ Property (6) follows from monotonicity of the T-norm and identity.

■ Property (7) follows from the adjunction of the T-norm.

■ Property (8) follows from the fact that, by adjunction we have $d \otimes (d \Rightarrow f) \leq f \Leftrightarrow (d \Rightarrow f) \leq (d \Rightarrow f)$, and hence $d \otimes (d \Rightarrow f) \leq f$ is always true.

■ Property (9) follows from the adjunction and previous results.

<figure><img src="image_8.png" /></figure>

**► Definition 30 (Similarity Relation).** A similarity relation, $S$, over a domain $D$, is a fuzzy subset of $D \times D$, which is reflexive, symmetric, and transitive.

Namely let $x, y, z \in D$ and let $\mu_S(x, y)$ denote the grade of membership of the ordered pair $(x, y) \in D \times D$. Then $S$ is a similarity relation in $D$ if and only if, for all $x, y, z \in D$,

■ $\mu_S(x, x) = 1$ (reflexivity),

■ $\mu_S(x, y) = 1$ implies $\mu_S(y, x) = 1$ (symmetry),

■ $\mu_S(x, z) \geq \mu_S(x, y) \otimes \mu_S(y, z)$ (transitivity).