Set Theory and Arithmetic in Fuzzy Logic

Abstract

This chapter offers a review of Petr Hájek’s contributions to first-order axiomatic theories in fuzzy logic (in particular, ZF-style fuzzy set theories, arithmetic with a fuzzy truth predicate, and fuzzy set theory with unrestricted comprehension schema). Generalizations of Hájek’s results in these areas to MTL as the background logic are presented and discussed.

2010 Mathematics Subject Classification: 03E72, 03H15

1 Introduction

One of Petr Hájek’s great endeavours in logic was the development of first-order fuzzy logic ${{\mathrm {BL}\forall }}$ (1998): this work unified some earlier conceptions of many-valued semantics and their calculi, but it also technically prepared the ground for a natural next step, that being an attempt at employing ${{\mathrm {BL}\forall }}$ or its extensions as background logics for non-classical axiomatic theories of fuzzy mathematics. Hájek initiated this study in the late nineties, in parallel with a continued investigation of the properties of ${{\mathrm {BL}\forall }}$ itself. Considering his previous engagements in set theory and arithmetic, and also the key rôles these disciplines play in logic, it seems natural that he focused primarily on these theories, from both mathematical and metamathematical points of view. With time passing, other authors have contributed to the area; other parts of axiomatic fuzzy mathematics based on fuzzy logic have been explored; and the work of several predecessors turned out to be important. Nevertheless, Hájek’s (and his co-authors’) elegant results stand out as fundamental contributions to the aforementioned axiomatic theories of fuzzy mathematics, and for a large part coincide with the state of the art in these fields of research.

In this chapter we survey Hájek’s contributions to arithmetic and set theory over fuzzy logic, in some cases slightly generalizing the results. Our generalizations always concern the underlying fuzzy logic: Hájek, as the designer of the logic ${{\mathrm {BL}\forall }}$, naturally worked in this logic or in one of its three prominent extensions— Łukasiewicz, Gödel, or product logic. However, Esteva and Godo’s similar, but weaker fuzzy logic $\mathrm {MTL}$ of left-continuous t-norms can be, from many points of view, seen as an even more fundamental fuzzy logic; therefore, where meaningful and easy enough, we discuss or present the generalization of Hájek’s results to $\mathrm {MTL}$.

The chapter is organized as follows: after the necessary preliminaries given in Sect. 4.2, we address three areas of axiomatic fuzzy mathematics—a ZF-style fuzzy set theory (Sect. 4.3), arithmetic with a fuzzy truth predicate (Sect. 4.4), and naïve Cantor-style fuzzy set theory (Sect. 4.5). The motivation and historical background are presented at the beginning of each section. Owing to the survey character of this chapter, for details and proofs (except for those which are new) we refer the readers to the original works indicated within the text.

2 Preliminaries

This chapter deals with some formal theories axiomatized in several first-order fuzzy logics: $\mathrm {MTL}$ $\forall$, $\mathrm {BL}$ $\forall$, and its three salient extensions— Łukasiewicz logic ($\mathrm {{\L }\forall }$), Gödel logic ($\mathrm {G\forall }$), and product fuzzy logic ($\mathrm {\Pi \forall }$), with or without the connective $\triangle$. We assume the reader’s familiarity with the basic apparatus of these fuzzy logics; all standard definitions can be found in the introductory chapter by Běhounek, Cintula, and Hájek (2011), which is freely available online. In this section we only focus on the definitions and theorems needed further on which cannot be found in the chapter.

Of the first-order variants of a fuzzy logic $\mathrm {L}$ (see (Běhounek et al. 2011, Def. 5.1.2)), throughout the chapter we employ exclusively that first-order variant ${\mathrm {L}\forall }$ which includes the axiom $(\forall {x})(\chi \mathbin {\vee }\varphi )\mathrel {\rightarrow }\chi \mathbin {\vee }(\forall {x})\varphi$ (for $x$ not free in $\chi$) ensuring strong completeness with respect to (safe) models over linearly ordered $\mathrm {L}$-algebras.

Convention 4.1

Let us fix the following notational conventions:

• The conjunction $\varphi \mathbin { \& }\dots \mathbin { \& }\varphi$ of $n$ identical conjuncts $\varphi$ will be denoted by $\varphi ^n$.

• The exponents $\varphi ^n$ take the highest precedence in formulae, followed by prefix unary connectives. The connectives $\mathrel {\rightarrow }$ and $\mathrel {\leftrightarrow }$ take the lowest precedence.

• The chain of implications $\varphi _1\mathrel {\rightarrow }\varphi _2,{\varphi _2\mathrel {\rightarrow }\varphi _3},\dots ,\varphi _{n-1}\mathrel {\rightarrow }\varphi _n$ can be written as $\varphi _1\longrightarrow \varphi _2\longrightarrow \dots \longrightarrow \varphi _n$, and similarly for $\longleftrightarrow$.

• We use the abbreviations $(\forall {xPt})\varphi$ and $(\exists {xPt})\varphi$, respectively, for $(\forall {x})(xPt\mathrel {\rightarrow }\varphi )$ and $(\exists {x})(xPt\mathrel { \& }\varphi )$, for any infix binary predicate $P$, term $t$, formula $\varphi$, and variable $x$.

• Negation of an atomic formula can alternatively be expressed by crossing its (usually infix) predicate: $x\notin y=_{\mathrm {df}}{\lnot }(x \in y)$, and similarly for $\ne$, $\not \subseteq$, $\not \approx$, etc.

As usual, by an extension of a logic $\mathrm {L}$ we mean a logic which is at least as strong as $\mathrm {L}$ and has the same logical symbols as $\mathrm {L}$. (Thus, e.g., $\mathrm {BL}$ is an extension of $\mathrm {MTL}$, but $\mathrm {BL_\triangle }$ is not.)

Definition 4.1

Let $\mathrm {L}$ be a logic extending ${{\mathrm {MTL}\forall }}$ or ${{{\mathrm {MTL}\forall }_\triangle }}$. Let $T$ be a theory over $\mathrm {L}$, $M$ a model of $T$, and $\varphi$ a formula in the language of $T$.

We say that $\varphi$ is crisp in M if $M\models \varphi \mathbin {\vee }{\lnot }\varphi$, and that $\varphi$ is crisp in T if it is crisp in all models of $T$.

Taking into account the semantics of $\mathrm {L}$, one can observe that $\varphi$ is crisp in $M$ iff it only takes the values $0$ and $1$ in $M$; the linear completeness theorem for $\mathrm {L}$ yields that $\varphi$ is crisp in $T$ iff $T\vdash _{\mathrm {L}}\varphi \mathbin {\vee }{\lnot }\varphi$. By convention we will also say that an $n$-ary predicate $P$ is crisp in $M$ or $T$ if the formula $P(x_1,\ldots ,x_n)$ is crisp in $M$ or $T$.

Definition 4.2

Let $\mathrm {L}$ extend ${\mathrm {MTL}\forall }$ or ${{\mathrm {MTL}\forall }_\triangle }$. By $\mathrm {L}_=$ we shall denote the logic $\mathrm {L}$ with the identity predicate $=$ that satisfies the reflexivity axiom $x=x$ and the intersubstitutivity schema ${x=y}\mathrel {\rightarrow }(\varphi (x)\mathrel {\leftrightarrow }\varphi (y))$.

Remark 4.1

It can be observed that the identity predicate $=$ is symmetric and transitive, using suitable intersubstitutivity axioms. The crispness of $=$ can be enforced by the additional axiom ${x=y}\mathrel {\vee }{x\ne y}$. However, the latter axiom is superfluous in all extensions of ${{{\mathrm {MTL}\forall }_\triangle }{}_=}$, and also in those extensions of ${{\mathrm {MTL}\forall }{}_=}$ that validate the schema $(\varphi \mathrel {\rightarrow }\varphi ^2)\mathrel {\rightarrow }(\varphi \mathbin {\vee }{\lnot }\varphi )$, e.g., in ${{\mathrm {{\L }}\forall }{}_=}$and ${{\mathrm {\Pi }\forall }{}_=}$, since over all these logics the predicate $=$ comes out crisp anyway (the proof is analogous to that due to (Hájek 2005, Cor. 1)).

Later on we will need the following lemmata, formulated here just for the variants of $\mathrm {MTL}$, but valid as well for any stronger logic (as they only assert some provability claims).

Lemma 4.1

The following are theorems of propositional $\mathrm {MTL}$:

• 1. $(\varphi \mathrel {\rightarrow }\varphi \mathbin { \& }\varphi )\mathbin { \& }(\varphi \mathrel {\rightarrow }\psi )\mathrel {\rightarrow }(\varphi \mathbin {\wedge }\psi \mathrel {\rightarrow }\varphi \mathbin { \& }\psi )$

• 2. $(\varphi \mathrel {\rightarrow }\varphi \mathbin { \& }\varphi )\mathbin { \& }(\psi \mathrel {\rightarrow }\psi \mathbin { \& }\psi )\mathrel {\rightarrow }(\varphi \mathbin {\wedge }\psi \mathrel {\rightarrow }\varphi \mathbin { \& }\psi )$

Proof

1. $\varphi \mathbin {\wedge }\psi \longrightarrow \varphi \longrightarrow \varphi \mathbin { \& }\varphi \longrightarrow \varphi \mathbin { \& }\psi$ (the antecedents of the theorem are used in the second and third implication).

2. By prelinearity, we can take the cases $\varphi \mathrel {\rightarrow }\psi$ and $\psi \mathrel {\rightarrow }\varphi$. The former case follows by weakening from Lemma 4.1(1); the latter is proved analogously: $\varphi \mathbin {\wedge }\psi \longrightarrow \psi \longrightarrow \psi \mathbin { \& }\psi \longrightarrow \varphi \mathbin { \& }\psi$. $\square$

Lemma 4.2

(cf. Haniková 2004) ${{\mathrm {MTL}\forall }_\triangle }$ proves:

• 1. $(\exists {x})\triangle \varphi \rightarrow \triangle (\exists {x})\varphi$

• 2. $(\forall {x})\triangle \varphi \mathrel {\leftrightarrow }\triangle (\forall {x})\varphi$

• 3. $(\forall {x})\triangle (\varphi \mathbin { \& }\psi )\rightarrow (\forall {x})\triangle \varphi \mathbin { \& }(\forall {x})\triangle \psi$

• 4. $\triangle (\varphi \vee \lnot \varphi )\mathrel {\leftrightarrow }\triangle (\varphi \rightarrow \triangle \varphi )$

Proof

By inspection of the ${{\mathrm {BL}\forall }_\triangle }$-proofs (Haniková 2004) we can observe that the theorems are valid in ${{\mathrm {MTL}\forall }_\triangle }$, too. $\square$

Lemma 4.3

Let $\varphi (x,y,\dots )$ be a formula of ${\mathrm {MTL}\forall }$ and $\psi (x,\dots )$ a formula of ${{\mathrm {MTL}\forall }{}_=}$, and $t$ be a term substitutable for both $x$ and $y$ in $\varphi$ and for $x$ in $\psi$. Then:

• 1. ${\mathrm {MTL}\forall }$ proves: $\varphi (t,t)\mathrel {\rightarrow }(\exists {x})\varphi (x,t)$

• 2. ${{\mathrm {MTL}\forall }{}_=}$ proves: $(\forall {x=t})(\psi (x))\mathrel {\leftrightarrow }\psi (t)$

• 3. ${{\mathrm {MTL}\forall }{}_=}$ proves: $(\exists {x=t})(\psi (x))\mathrel {\leftrightarrow }\psi (t)$

Proof

1. Immediate by the $\mathrm {MTL}$ $\forall$-axiom of dual specification.

2. Left to right: $(\forall {x})(x=t\mathrel {\rightarrow }\psi (x))\longrightarrow (t=t\mathrel {\rightarrow }\psi (t))\longleftrightarrow \psi (t)$, by specification and the reflexivity of $=$. Right to left: $\psi (t)\mathrel {\rightarrow }(x=t\mathrel {\rightarrow }\psi (x))$ by the intersubstitutivity of equals; generalize on $x$ and shift the quantifier to the consequent.

3. Left to right: $x=t\mathrel { \& }\psi (x)\mathrel {\rightarrow }\psi (t)$ by the intersubstitutivity of equals; generalize on $x$ and shift the quantifier (as $\exists$) to the antecedent. Right to left: $\psi (t)\longrightarrow (t=t\mathrel { \& }\psi (t))\longrightarrow (\exists {x})(x=t\mathrel { \& }\psi (t))$, by the reflexivity of $=$, dual specification, and Lemma 4.3(1). $\square$

Lemma 4.4

In ${{\mathrm {MTL}\forall }{}_=}$, any formula is equivalent to a formula in which function symbols are applied only to variables and occur only in atomic subformulae of the form $y=F(x_1,\ldots ,x_k)$.

Proof

Using Lemma 4.3, we can inductively decompose nested terms $s(t)$ by $\varphi (s(t))\mathrel {\leftrightarrow }(\exists {x=t})\varphi (s(x))$ and finally by

$$ \varphi (F(x_1,\dots ,x_k))\mathrel {\leftrightarrow }(\exists {y=F(x_1,\ldots ,x_k)})\varphi (y) $$

for all function symbols $F$. $\square$

We now give a few results on the conservativity of introducing predicate and function symbols.

Definition 4.3

For $\mathrm {L}$ a logic, $T_1$ a theory in a language $\varGamma _1$ and $T_2\supseteq T_1$ a theory in a language $\varGamma _2\supseteq \varGamma _1$, we say that $T_2$ is a conservative extension of $T_1$ if $T_2\vdash _\mathrm {L}\varphi$ implies $T_1\vdash _\mathrm {L}\varphi$ for each $\varGamma _1$-formula $\varphi$.

The proofs of the following theorems are easy adaptations of the proofs due to Hájek (2000). Note that Theorem 4.3 covers introducing constants, too, for $n=0$ (in which case the congruence axiom becomes trivially provable and need not be explicitly added to the theory).

Theorem 4.2

(Adding predicate symbols; cf. Hájek 2000) Let $\mathrm {L}$ extend ${{\mathrm {MTL}\forall }}$ or ${{\mathrm {MTL}\forall }_\triangle }$ and $T$ be a theory over $\mathrm {L}$ in a language $\varGamma$. Let $P\not \in \varGamma$ be an $n$-ary predicate symbol and $\varphi (x_1,\dots , x_n)$ a $\varGamma$-formula. If $T'$ results from $T$ by adding $P$ and the axiom

$$ P(x_1,\dots ,x_n)\mathrel {\leftrightarrow }\varphi (x_1,\dots ,x_n) $$

then $T'$ is a conservative extension of $T$.

Theorem 4.3

(Adding function symbols; cf. Hájek 2000) Let $\mathrm {L}$ extend ${{\mathrm {MTL}\forall }{}_=}$ or ${{{\mathrm {MTL}\forall }_\triangle }{}_=}$ and $T$ be a theory over $\mathrm {L}$ in a language $\varGamma$. Let $F\notin \varGamma$ be an $n$-ary function symbol and $\varphi$ a $\varGamma$-formula with $n+1$ free variables. Let $T'$ result from $T$ by adding the axiom $\varphi (x_1,\dots ,x_n,F(x_1,\dots ,x_n))$ and the congruence axiom $x_1=z_1\mathrel { \& }\dots \mathrel { \& }x_n=z_n\rightarrow F(x_1,\dots ,x_n)=F(z_1,\dots ,z_n)$.

• 1. If $\mathrm {L}$ extends ${{\mathrm {MTL}\forall }{}_=}$ and $T\vdash _\mathrm {L}(\exists {y})\varphi (x_1,\dots ,x_n,y)$, then $T'$ is a conservative extension of $T$.

• 2. If $\mathrm {L}$ extends ${{{\mathrm {MTL}\forall }_\triangle }{}_=}$ and $T\vdash _\mathrm {L}(\exists {y})\triangle \varphi (x_1,\dots ,x_n,y)$, then $T'$ is a conservative extension of $T$.

If, in addition, $T\vdash _{\mathrm {L}}(\exists {y})(\varphi (x_1,\ldots ,x_n,y)\mathbin { \& }(\forall {y'})(\varphi (x_1,\ldots ,x_n,y')\mathrel {\rightarrow }y=y'))$, then each $T'$-formula is $T'$-equivalent to a $T$-formula.

3 ZF-Style Set Theories in Fuzzy Logic

This section intends to give an overview of results on axiomatic set theory developed in fuzzy logic in the style of classical Zermelo–Fraenkel set theory. It draws primarily on Hájek and Haniková’s paper (2003), where a ZF-like set theory is developed over ${{{\mathrm {BL}\forall }_\triangle }}$. The theory introduced by Hájek and Haniková was called ‘fuzzy set theory’ for simplicity, and the acronym $\mathrm {FST}$ was used; this was not meant to suggest that FST was the set theory in fuzzy logic, since clearly there are many possible ways to develop a set theory in fuzzy logic. It was shown that FST theory admitted many-valued models, and that at the same time it faithfully interpreted classical Zermelo–Fraenkel set theory $\mathrm {ZF}$. Moreover, some of its mathematics was developed.

Here, for the sake of precision, we shall use ${\mathrm {FST}_{\mathrm {BL}}}$ for the above theory of Hájek and Haniková (2003) over ${{{\mathrm {BL}\forall }_\triangle }}$, and alongside, we shall consider a theory ${\mathrm {FST}_{\mathrm {MTL}}}$ developed over ${{{\mathrm {MTL}\forall }_\triangle }}$. The focus will be on the theory ${\mathrm {FST}_{\mathrm {BL}}}$.

We start with a short overview of related $\mathrm {ZF}$-style set theories in non-classical logics. A more comprehensive treatment of the history of the subject can be found in Gottwald’s survey (2006); see also Haniková (2004); these take into account also the interesting story of the full comprehension schema (discussed in Sect. 4.5).

An early attempt is presented in the works of Klaua (1965, 1966, 1967), who does not develop axiomatic theory but constructs cumulative hierarchies of sets, defining many-valued truth functions of $=$, $\subseteq$, and $\in$ over a set of truth values that is an MV-algebra. Interestingly, Klaua (1967) constructs a cumulative universe similar to ours in definition of its elements and the value of the membership function, but with a non-crisp equality; his universe then validates extensionality and comprehension, but fails to validate the congruence axioms. Klaua’s works have been continued and made more accessible in the works of Gottwald (1976a, b, 1977).

It is instructive to study a selection of chapters on $\mathrm {ZF}$-style set theory in the intuitionistic logic. Powell (1975) defines a $\mathrm {ZF}$-like theory with an additional axiom of double complement (similar in effect to our support), develops some technical means, such as ordinals and ranks, and defines a class of stabilized sets, which it proves to be an inner model of classical $\mathrm {ZF}$. Grayson (1979) omits double complement but uses collection instead of replacement, and constructs, within the theory, a Heyting-valued universe over a complete Heyting algebra. Using a particular Boolean algebra which it constructs, it shows relative consistency with respect to $\mathrm {ZF}$. This paper also offers examples of how (variants of) axioms of classical $\mathrm {ZF}$ can strengthen the underlying logic to the classical one. For example, the axiom of foundation, together with a very weak fragment of $\mathrm {ZF}$, implies the law of the excluded middle, which yields the full classical logic (both in intuitionistic logic and in the logics we use here), and thus the theory becomes classical. It also shows—by using $\in$-induction instead of foundation—that some classically equivalent principles are no longer equivalent in a weaker logical setting.

Inspired by the intuitionistic set theory results, Takeuti and Titani (1984) wrote a paper on $\mathrm {ZF}$-style set theory over Gödel logic, giving an axiomatization and presenting some nice mathematics. Later (1992), the authors enhanced their approach to a logical system that combines Łukasiewicz connectives with the product conjunction, the strict negation and a constant denoting $\frac{1}{2}$ on $[0,1]$ (thus defining the well-known logic of Takeuti and Titani, a predecessor of the logics Ł$\mathrm {\Pi }$ and Ł$\mathrm {\Pi }\frac{1}{2}$—see (Hájek 1998, Sect. 9.1)). This logic contains Gödel logic, and it is Gödel logic that is used in the set-theoretic axioms. Equality in this system is many-valued. Within their set-theoretic universe, Takeuti and Titani are then able to reconstruct the algebra of truth values determining the logic, and they also prove a completeness theorem. In her paper (1999), Titani gives analogous constructions, including completeness, for a set theory in lattice-valued logic. This theory was interpreted in ${\mathrm {FST}_{\mathrm {BL}}}$ by Hájek and Haniková (2013).

We will now start developing our theories ${\mathrm {FST}_{\mathrm {BL}}}$ and ${\mathrm {FST}_{\mathrm {MTL}}}$. We will not give proofs for statements that were proved elsewhere, for ${\mathrm {FST}_{\mathrm {BL}}}$; as for a possible generalization for ${\mathrm {FST}_{\mathrm {MTL}}}$, proofs can be obtained by inspection of the ${\mathrm {FST}_{\mathrm {BL}}}$ case. For both theories, we assume the logic contains a (crisp) equality. The only non-logical symbol in the language is a binary predicate symbol $\in$.

Definition 4.4

In both ${\mathrm {FST}_{\mathrm {BL}}}$ and ${\mathrm {FST}_{\mathrm {MTL}}}$ we define:

• Crispness: $\mathrm {Cr}(x)\equiv _{\mathrm {df}}(\forall {u})\triangle (u\in x \vee u\notin x)$

• Inclusion: $x\subseteq y\equiv _{\mathrm {df}}(\forall {z\in x})(z\in y)$

Semantically, crisp sets only take the classical membership values. Using Lemma 4.2 one gets:

$$\begin{aligned} \mathrm {Cr}(x)\longleftrightarrow {}&(\forall {u})\triangle ({u\in x}\rightarrow \triangle ({u\in x}))\longleftrightarrow \\&\triangle (\forall {u})({u\in x}\rightarrow \triangle ({u\in x}))\longleftrightarrow \triangle \triangle (\forall {u}) ({u\in x}\rightarrow \triangle ({u\in x})), \end{aligned}$$

so crispness itself is a crisp property: one has $\vdash _{{{\mathrm {MTL}\forall }_\triangle }}\mathrm {Cr}(x)\mathrel {\leftrightarrow }\triangle \mathrm {Cr}(x)$. Thus also $\mathrm {Cr}(x)\longleftrightarrow \triangle \mathrm {Cr}(x)\longleftrightarrow (\triangle \mathrm {Cr}(x))^2\longleftrightarrow (\mathrm {Cr}(x))^2$.

Definition 4.5

${\mathrm {FST}_{\mathrm {BL}}}$ is a theory over ${{{\mathrm {\mathrm {BL}}\forall }_\triangle }{}_=}$, with a basic predicate symbol $\in$. (${\mathrm {FST}_{\mathrm {MTL}}}$ is defined analogously over ${{{\mathrm {MTL}\forall }_\triangle }{}_=}$.) The axioms of the theory are as follows:

• 1. Extensionality: $x=y\mathrel {\leftrightarrow }\triangle (x\subseteq y)\mathbin { \& }\triangle (y\subseteq x)$; the condition on the right is ${{{\mathrm {MTL}\forall }_\triangle }}$-equivalent to $(\forall {z})\triangle (z\in x\mathrel {\leftrightarrow }z\in y)$

• 2. Empty set: $(\exists {x})\triangle (\forall {y})(y\notin x)$; we introduce¹ a new constant $\emptyset$

• 3. Pair: $(\exists {z})\triangle (\forall {u})(u\in z\mathrel {\leftrightarrow }(u=x\vee u=y))$; we introduce the pairing $\{x,y\}$ and singleton $\{x\}$ function symbols

• 4. Union: $(\exists {z})\triangle (\forall {u})(u\in z\mathrel {\leftrightarrow }(\exists {y})(u\in y\mathrel { \& }y\in x))$; we introduce a unary function symbol $\bigcup x$, and we use $x\cup y$ for $\bigcup \{x,y\}$

• 5. Weak power: $(\exists {z})\triangle (\forall {u})(u\in z\mathrel {\leftrightarrow }\triangle (u\subseteq x))$; we introduce a unary function symbol $\mathrm {WP}(x)$

• 6. Infinity: $(\exists {z})\triangle (\emptyset \in z\mathrel { \& }(\forall {x \in z})(x\cup \{x\}\in z))$

• 7. Separation: $(\exists {z})\triangle (\forall {u})(u\in z\mathrel {\leftrightarrow }(u\in x\mathrel { \& }\varphi (u,x)))$, if $z$ is not free in $\varphi$; we introduce a function symbol $\{ u\in z \mid \varphi (u,x) \}$, and we use $x\cap y$ for $\{ u\in x \mid u\in y \}$

• 8. Collection: $(\exists {z})\triangle ((\forall {u\in x})(\exists {v})\varphi (u,v)\rightarrow (\forall {u\in x})(\exists {v\in z})\varphi (u,v))$, if $z$ is not free in $\varphi$

• 9. $\in$-Induction: $\triangle (\forall {x})(\triangle (\forall {y\in x})\varphi (y)\rightarrow \varphi (x))\rightarrow \triangle (\forall {x})\varphi (x)$

• 10. Support: $(\exists {z})(\mathrm {Cr}(z)\mathbin { \& }\triangle (x\subseteq z))$

Let us remark that making $=$ a crisp predicate is not an altogether arbitrary decision. Indeed, in particular logics, such as Łukasiewicz logic or product logic,² even much weaker assumptions on equality than those of Definition 4.2 entail its crispness; this was pointed out by Petr Hájek in an unpublished note. This, together with the fact that a crisp equality is much easier to handle (while it does not prevent a development of a very rich fuzzy set theory), makes the crispness of $=$ a universal choice in our theory.

We consistently use $\triangle$ after existential quantifiers³ in axioms in order to be able to define some of the standard set-theoretic operations like the empty set, a pair, a union, the set $\omega$, etc., as the Skolem functions of these axioms (i.e., by Theorem 4.3). Notice that if ${\mathrm {FST}_{\mathrm {BL}}}$ and ${\mathrm {FST}_{\mathrm {MTL}}}$ were defined with the function symbols for these set-theoretic operations in the primitive language, the corresponding Skolem axioms (i.e., ${y\notin \emptyset }$, ${u\in \{ x,y \}}\mathrel {\leftrightarrow }{u=x}\mathrel {\vee }{u=y}$, etc.) would not contain these $\triangle$’s.

In the weak power set axiom, the second $\triangle$ weakens the statement.

Further, similarly as in set theory over the intuitionistic logic (Grayson 1979), the axiom of foundation in a very weak setting implies the law of excluded middle for all formulae. Therefore, $\in$-induction is used instead. For a reader familiar with Hájek and Haniková’s paper (2003), we point out that here we employ a different spelling of the $\in$-induction schema: originally, the schema read $\triangle (\forall {x})((\forall {{y\in x}})\varphi (y)\rightarrow \varphi (x))\rightarrow \triangle (\forall {x})\varphi (x)$. The current form of induction axiom was inspired by Titani’s paper (1999). As pointed out by Hájek and Haniková (2013), it is an open problem whether the original $\in$-induction implies the current one (the converse is obviously the case).

Given the above sample of possible problems, the first thing one might like to vouchsafe is that the presented theory really is fuzzy, i.e., that it admits many-valued models. Hájek and Haniková (2003) showed this for ${\mathrm {FST}_{\mathrm {BL}}}$, in the following manner.

Take a complete ${{{\mathrm {BL}\forall }_\triangle }}$-chain ${\varvec{A}}=\langle A, *^{ {\varvec{A}}}, \rightarrow ^{ {\varvec{A}}}, \wedge ^{ {\varvec{A}}},\vee ^{ {\varvec{A}}},0^{ {\varvec{A}}},1^{ {\varvec{A}}},\triangle ^{ {\varvec{A}}}\rangle$ and define a universe $V^ {\varvec{A}}$ by transfinite induction. Take $\mathrm {Fnc}(x)$ for a unary predicate stating that $x$ is a function, and $\mathrm {Dom}(x)$ and $\mathrm {Rng}(x)$ for unary functions assigning to $x$ its domain and range, respectively. Set:

$$ \begin{aligned} V^ {\varvec{A}}_0&= \{\emptyset \}\\ V^ {\varvec{A}}_{\alpha +1}&= \{f:\mathrm {Fnc}(f) \mathbin { \& }\mathrm {Dom}(f)= V^ {\varvec{A}}_\alpha \mathbin { \& }\mathrm {Rng}(f)\subseteq A\}\,\text {for any ordinal }\alpha \\ V^ {\varvec{A}}_\lambda&= \bigcup _{\alpha <\lambda }V^ {\varvec{A}}_\alpha \text {for a limit ordinal }\lambda \\ V^ {\varvec{A}}&= \bigcup _{\alpha \in {\mathrm {Ord}}}V^ {\varvec{A}}_\alpha \end{aligned}$$

Observe that $\alpha \le \beta \in \mathrm {Ord}$ implies $V^ {\varvec{A}}_\alpha \subseteq V^ {\varvec{A}}_\beta$. Define two binary functions from $V^ {\varvec{A}}$ into $A$, assigning to any $u,v\in V^ {\varvec{A}}$ the values $\Vert u\in v\Vert$ and $\Vert u=v\Vert$ in $A$:

$$\begin{aligned} \Vert u\in v\Vert&= v(u)\text { if }u\in \mathrm {Dom}(v),\text { otherwise }0^ {\varvec{A}}\\ \Vert u=v\Vert&= 1^ {\varvec{A}}\text { if }u=v,\text { otherwise }0^ {\varvec{A}} \end{aligned}$$

and use induction on the complexity of formulae to define for any formula $\varphi (x_1,\dots ,x_n)$ a corresponding $n$-ary function from $(V^ {\varvec{A}})^n$ into $A$, assigning to an $n$-tuple $u_1,\dots ,u_n$ the value $\Vert \varphi (u_1,\dots ,u_n)\Vert$:

$$ \begin{aligned} \Vert 0\Vert&= 0^ {\varvec{A}}\\ \Vert \psi \mathbin { \& }\chi \Vert&= \Vert \psi \Vert *^ {\varvec{A}}\Vert \chi \Vert ,\text { and similarly for } \mathrel {\rightarrow }, \mathbin {\wedge }\ \text {and}\ \mathbin {\vee }\\ \Vert \triangle \psi \Vert&= \triangle ^ {\varvec{A}}\Vert \psi \Vert \\ \Vert (\forall {x})\psi \Vert&= \textstyle \bigwedge _{u\in V^ {\varvec{A}}}\Vert \psi (x/u)\Vert \\ \Vert (\exists {x})\psi \Vert&= \textstyle \bigvee _{u\in V^ {\varvec{A}}}\Vert \psi (x/u)\Vert \end{aligned}$$

For a sentence $\varphi$, one says that $\varphi$ is valid in $V^ {\varvec{A}}$ iff $\Vert \varphi \Vert =1^ {\varvec{A}}$ is provable in $\mathrm {ZF}$. We are able to demonstrate the following soundness result:

Theorem 4.4

Let $\varphi$ be a closed formula provable in ${\mathrm {FST}_{\mathrm {BL}}}$. Let ${\varvec{A}}$ be a complete ${{{\mathrm {BL}\forall }_\triangle }}$-chain. Then $\varphi$ is valid in $V^ {\varvec{A}}$.

We remark that an analogous construction of an ${\varvec{A}}$-valued universe can be performed for a complete ${{{\mathrm {MTL}\forall }_\triangle }}$-algebra; based on that, the above result can be stated for ${\mathrm {FST}_{\mathrm {MTL}}}$ w.r.t. the universe defined over such algebra. In either case, the given construction provides an interpretation of the fuzzy set theory in classical $\mathrm {ZF}$. Currently, there is no completeness theorem available.

Within ${\mathrm {FST}_{\mathrm {BL}}}$, one can define a class of hereditarily crisp sets and prove it to be an inner model of $\mathrm {ZF}$ in ${\mathrm {FST}_{\mathrm {BL}}}$.

Definition 4.6

In ${\mathrm {FST}_{\mathrm {BL}}}$ we define the following predicates:

• $\mathrm {HCT}(x) \equiv _{\mathrm {df}}\mathrm {Cr}(x)\mathbin { \& }(\forall {u\in x})(\mathrm {Cr}(u)\mathrel { \& }u\subseteq x)$; we write $x \in \mathrm {HCT}$ for $\mathrm {HCT}(x)$

• $\mathrm {H}(x) \equiv _{\mathrm {df}}\mathrm {Cr}(x)\mathbin { \& }(\exists {x'\in \mathrm {HCT}})(x\subseteq x')$; we write $x \in \mathrm {H}$ for $\mathrm {H}(x)$

Lemma 4.5

${\mathrm {FST}_{\mathrm {BL}}}$ proves that $\mathrm {HCT}$ and $\mathrm {H}$ are crisp classes, and moreover, that $\mathrm {H}$ is transitive.

It was further shown (Hájek and Haniková 2003) that ${\mathrm {FST}_{\mathrm {BL}}}$ proves $\mathrm {H}$ to be an inner model of $\mathrm {ZF}$. In more detail, for $\varphi$ a formula in the language of $\mathrm {ZF}$ (where the language of classical logic is considered with connectives $\mathbin { \& }$, $\rightarrow$, $0$, and the universal quantifier $\forall$) one defines a translation $\varphi ^\mathrm {H}$ inductively as follows:

$$ \begin{aligned} \varphi ^\mathrm {H}&= \varphi \text { for } \varphi \text { atomic}\\ 0^\mathrm {H}&= 0 \\ (\psi \mathbin { \& }\chi )^\mathrm {H}&= \psi ^\mathrm {H}\mathbin { \& }\chi ^\mathrm {H}\\ (\psi \mathrel {\rightarrow }\chi )^\mathrm {H}&= \psi ^\mathrm {H}\mathrel {\rightarrow }\chi ^\mathrm {H}\\ ((\forall {x})\psi )^\mathrm {H}&= (\forall {x \in \mathrm {H}})(\psi ^\mathrm {H}) \end{aligned}$$

(Then also $(\lnot \psi )^\mathrm {H}=\lnot (\psi ^\mathrm {H})$, $(\psi \vee \chi )^\mathrm {H}=\psi ^\mathrm {H}\vee \chi ^\mathrm {H}$, and $((\exists {x})\psi )^\mathrm {H}=(\exists {x \in \mathrm {H}})(\psi ^\mathrm {H})$).

One can show that the law of the excluded middle holds in $\mathrm {H}$:

Lemma 4.6

Let $\varphi (x_1,\dots ,x_n)$ be a ZF-formula whose free variables are among $x_1,\dots ,x_n$. Then ${\mathrm {FST}_{\mathrm {BL}}}$ proves

$$(\forall {x_1\in \mathrm {H}})\dots (\forall {x_n\in \mathrm {H}})(\varphi ^\mathrm {H}(x_1,\dots ,x_n)\vee \lnot \varphi ^\mathrm {H}(x_1,\dots ,x_n)) .$$

Considering classical ZF with the axioms of empty set, pair, union, power set, infinity, separation, collection, extensionality, and $\in$-induction, one can prove their translations in ${\mathrm {FST}_{\mathrm {BL}}}$:

Lemma 4.7

For $\varphi$ being the universal closure of any of the abovementioned axioms of $\mathrm {ZF}$, ${\mathrm {FST}_{\mathrm {BL}}}$ proves $\varphi ^\mathrm {H}$.

This provides an interpretation of $\mathrm {ZF}$ in ${\mathrm {FST}_{\mathrm {BL}}}$ (in particular, $\mathrm {H}$ is an inner model of $\mathrm {ZF}$ in ${\mathrm {FST}_{\mathrm {BL}}}$):

Theorem 4.5

Let a closed formula $\varphi$ be a theorem of $\mathrm {ZF}$. Then ${\mathrm {FST}_{\mathrm {BL}}}\vdash \varphi ^\mathrm {H}$.

Moreover, the interpretation is faithful: if ${\mathrm {FST}_{\mathrm {BL}}}\vdash \varphi ^\mathrm {H}$, then $\mathrm {ZF}\vdash \varphi ^\mathrm {H}$ (since it is formally stronger), but then $\mathrm {ZF}\vdash \varphi$.

Again, by inspection of the proof, one arrives at the conclusion that exactly the same result can be obtained for ${\mathrm {FST}_{\mathrm {MTL}}}$. This poses the question of a formal difference between ${\mathrm {FST}_{\mathrm {BL}}}$ and ${\mathrm {FST}_{\mathrm {MTL}}}$: it would be interesting to determine to what degree the two theories, built in one fashion over two distinct logics, differ.

We now discuss ordinal numbers in ${\mathrm {FST}_{\mathrm {BL}}}$ (Hájek and Haniková 2013). In order to obtain a suitable definition of ordinal numbers in ${\mathrm {FST}_{\mathrm {BL}}}$, we rely on Theorem 4.5. Recall the classical definition of an ordinal number by a predicate symbol $\mathrm {Ord}_0$:

$$ \begin{aligned} \mathrm {Ord}_0(x) \equiv _{\mathrm {df}}{}&(\forall {y\in x})(y\subseteq x)\mathrel { \& }\\&(\forall {y,z\in x})(y\in z\vee y=z\vee z\in y)\mathrel { \& }\\&(\forall {q\subseteq x})(q\ne \emptyset \rightarrow (\exists {y\in q})(y\cap q=\emptyset )) \end{aligned}$$

If $x \in \mathrm {H}$, then $\mathrm {Ord}_0(x)\mathrel {\leftrightarrow }\mathrm {Ord}_0^\mathrm {H}(x)$, and $\mathrm {Ord}_0(x)$ is crisp. We define ordinal numbers to be those sets in $\mathrm {H}$ for which $\mathrm {Ord}_0^\mathrm {H}$ is satisfied:

Definition 4.7

In ${\mathrm {FST}_{\mathrm {BL}}}$ we define: $\mathrm {Ord}(x)\equiv _{\mathrm {df}}x \in \mathrm {H}\mathbin { \& }\mathrm {Ord}_0(x)$.

Furthermore, we define in ${\mathrm {FST}_{\mathrm {BL}}}$:

$$ \begin{aligned} \mathrm{CrispFn}(f) \equiv _{\mathrm {df}}\mathrm{Rel}(f) \mathbin { \& }\mathrm {Cr}(f) \mathbin { \& }(\forall {x \in \mathrm{Dom}(f)})(\langle x,y\rangle \in f \mathrel { \& }\langle x,z \rangle \in f\mathrel {\rightarrow }y=z) \end{aligned}$$

where the property of being a relation, and the operations of ordered pair, domain, and range are defined as in classical $\mathrm {ZF}$.

The iterated weak power property is as follows:

$$ \begin{aligned} \mathrm{ItWP}(f)\equiv _{\mathrm {df}}&~ \mathrm{CrispFn}(f)\mathrel { \& }\mathrm{Dom}(f)\in \mathrm{Ord}\mathrel { \& }f(\emptyset )=\emptyset \mathrel { \& }\\&\quad (\forall {\alpha \in \mathrm{Ord}})(\alpha \ne \emptyset \mathrel { \& }\alpha \in \mathrm{Dom}(f)\mathrel {\rightarrow }f(\alpha )=\bigcup _{\beta \in \alpha }\mathrm {WP}(f(\beta ))) \end{aligned}$$

The notion is crisp: $\mathrm{ItWP}(f)\mathrel {\leftrightarrow }\triangle \mathrm{ItWP}(f).$ Moreover, $\mathrm{ItWP}(f)\mathrel { \& }\mathrm{ItWP}(g)\mathrel { \& }\mathrm{Dom}(f)\le \mathrm{Dom}(g)\mathrel {\rightarrow }\triangle (f\subseteq g)$.

Lemma 4.8

${\mathrm {FST}_{\mathrm {BL}}}$ proves: $(\forall {\alpha \in \mathrm{Ord}})(\exists {f})(\mathrm{ItWP}(f)\mathrel { \& }\mathrm{Dom}(f)=\alpha ).$

Definition 4.8

For each $\alpha \in \mathrm{Ord}$, let $\hat{V}_\alpha$ be the unique (crisp) set $z$ such that:

$$ (\exists {f}) (\mathrm{ItWP}(f) \mathrel { \& }\alpha \in \mathrm{Dom}(f) \mathrel { \& }f(\alpha )=z) $$

Then one can show some classical results about ordinal induction and ranks, as:

Theorem 4.6

${\mathrm {FST}_{\mathrm {BL}}}$ proves: $(\forall {x})(\exists {\alpha \in \mathrm{Ord}})(x \in \hat{V}_\alpha )$.

4 Arithmetic and the Truth Predicate

In this section we focus on theories of arithmetic over fuzzy logic. We recall the results obtained by Hájek, Paris, and Shepherdson (2000), taking into account also Restall’s results (1995); these papers muse on the degree to which considering a logical system formally weaker than the classical one eradicates the paradoxes one obtains when adding a truth predicate to a theory of arithmetic. Then we briefly visit the method which Petr Hájek used in order to show that the first-order satisfiability problem in a standard product algebra is non-arithmetical (Hájek 2001). Interestingly, in all these works, the theory of arithmetic is a crisp one—enriched, in the respective cases, by new language elements that admit a many-valued interpretation.

4.1 Classical Arithmetic and the Truth Predicate

We start with a tiny review of theories of arithmetic in classical first-order logic. The language of arithmetic has a unary function symbol $s$ for successors, binary function symbols $+$ for addition and $\cdot$ for multiplication, an object constant $0$, and its predicate symbols are $=$ for equality and $\le$ for ordering.⁴ An arithmetical formula (sentence) is a formula (sentence) in this language.

We assume $=$ is a logical symbol and the usual axioms for it are implicitly present. Robinson arithmetic $\mathrm {Q}$ has the following axioms:

$$\begin{aligned} \begin{array}{ll} {(\mathrm Q1) }&{}\quad s(x)=s(y)\mathrel {\rightarrow }x=y \\ {(\mathrm Q2) }&{}\quad s(x)\ne 0 \\ {(\mathrm Q3) }&{}\quad x\ne 0 \mathrel {\rightarrow }(\exists {y})(x=s(y)) \\ {(\mathrm Q4) }&{}\quad x+0=x \\ {(\mathrm Q5) }&{}\quad x+s(y) = s(x+y) \\ {(\mathrm Q6) }&{}\quad x\cdot 0 = 0 \\ {(\mathrm Q7) }&{}\quad x\cdot s(y) = x\cdot y +x \\ {(\mathrm Q8) }&{}\quad x\le y \mathrel {\leftrightarrow }(\exists {z}) (z+x = y) \end{array} \end{aligned}$$

Peano arithmetic $\mathrm {PA}$ adds induction, usually as an axiom schema. Here we will need a (classically equivalent) rule: for each arithmetical formula $\varphi$, from $\varphi (0)$ and $(\forall {x})( \varphi (x) \mathrel {\rightarrow }\varphi (s(x)) )$ derive $(\forall {x}) \varphi (x)$.

The standard model of arithmetic is the structure $\fancyscript{N}= \langle N, 0, s, +, \cdot , \le \rangle$, where $N$ is the set of natural numbers and $0$, $s$, $+$, $\cdot$, $\le$ are the familiar operations and ordering of natural numbers (by an abuse that is quite common, the same notation is maintained for the symbols of the language and for their interpretations on $N$).

An arithmetization of syntax, first introduced by Gödel, is feasible in theories of arithmetic such as $\mathrm {Q}$ or $\mathrm {PA}$; thereby, in particular, each arithmetical formula $\varphi$ is assigned a Gödel number, denoted $\overline{\varphi }$. Then one obtains a classical diagonal result: for $T$ a theory containing $\mathrm {PA}$,⁵ and for each formula $\psi$ in the language of $T$ with exactly one free variable, there is a sentence $\varphi$ in the language of $T$ such that $T\vdash \varphi \mathrel {\leftrightarrow }\psi (\overline{\varphi })$.

A theory $T$ such as above (i.e., with a Gödel encoding of formulae), has a truth predicate iff its language contains a unary predicate symbol $\mathrm {Tr}$ such that $T\vdash \varphi \mathrel {\leftrightarrow }\mathrm {Tr}(\overline{\varphi })$ for each sentence $\varphi$ of the language. This is what Petr Hájek likes to call the (full) dequotation scheme, with the following example for its import: the sentence ‘It’s snowing’ is true if and only if it’s snowing. Hence another term in usage ‘It’s snowing–“It’s snowing” lemma’. On the margin, we remark that a per-partes dequotation is native to $\mathrm {PA}$ (or indeed, ${\mathrm {I}\Sigma _1}$): one can define partial truth predicates for fixed levels of the arithmetical hierarchy and fixed number of free variables (Hájek and Pudlák 1993). However, here it is required of $\mathrm {Tr}$ that it do the same job uniformly for all formulae.

The juxtaposition of the diagonal result with the requirements posed on a truth predicate reveals that consistent arithmetical theories (over classical logic) cannot define their own truth (a result due to Tarski): taking $\lnot \mathrm {Tr}(x)$ for $\psi (x)$, diagonalization yields a sentence $\varphi$ such that $T\vdash \varphi \mathrel {\leftrightarrow }{\lnot }\mathrm {Tr}(\overline{\varphi })$, so $T\vdash \varphi \mathrel {\leftrightarrow }\lnot \varphi$, a contradiction.

4.2 Arithmetic with a Fuzzy Truth Predicate

Hájek et al. (2000) noted that a (crisp) Peano arithmetic might be combined with a (many-valued) truth predicate over Łukasiewicz logic (where the existence of a $\varphi$ such that $\varphi \mathrel {\leftrightarrow }\lnot \varphi$ is not contradictory); it then proceeds to develop the theory. We shall reproduce its main results, in combination with those by Restall (1995).

Definition 4.9

$\mathrm {PA}\L$ stands for a Peano arithmetic in Łukasiewicz logic, i.e., a theory with the axioms and rules of first-order Łukasiewicz logic ${\mathrm {\L }\forall }$, the congruence axioms of equality w.r.t. the primitive symbols of the language of arithmetic, the above axioms (Q1)–(Q8), and the induction rule.

Making $\mathrm {PA}\L$ crisp is easy: one postulates a crispness axiom for the predicate symbol $=$ as the only basic predicate symbol of the theory ($\le$ is definable). In other words, ${x=y}\vee {x\ne y}$ is adopted as a new axiom. Then one can prove crispness for all arithmetical formulae, propagating it over connectives and quantifiers.

However, Restall (1995, actually earlier than Hájek et al. 2000) shows that $\mathrm {PA}\L$ is provably crisp even without a crispness axiom.⁶ The proof is a neat example of weakening operating hand in hand with the induction rule, showing that:

• 1. $\mathrm {PA}\L \vdash x=0 \mathrel {\vee }x\ne 0$

• 2. If $\mathrm {PA}\L \vdash \varphi (0,y)$ and $\mathrm {PA}\L \vdash \varphi (x,0)$ and $\mathrm {PA}\L \vdash \varphi (x,y)\mathrel {\rightarrow }\varphi (s(x),s(y))$, then $\mathrm {PA}\L \vdash \varphi (x,y)$.

• 3. $\mathrm {PA}\L \vdash (\exists {x})(x=0 \mathrel {\leftrightarrow }y=z)$

• 4. $\mathrm {PA}\L \vdash y=z \mathrel {\vee }y\ne z$

and consequently:

Theorem 4.7

(Restall 1995) Let $\varphi (x_1,\dots , x_n)$ be an arithmetical formula. Then

$$ \mathrm {PA}\L \vdash \varphi (x_1,\dots ,x_n)\vee \lnot \varphi (x_1,\dots ,x_n). $$

Crispness pertaining to $\mathrm {PA}\L$ as the theory of numbers, as Restall goes on to remark, need not concern additional concepts that one may wish to add to it, such as the truth predicate; these may be governed by the laws of Łukasiewicz logic ${\mathrm {\L }\forall }$.

Definition 4.10

(Hájek et al. 2000) $\mathrm {PA}\L \mathrm {Tr}$ is the theory obtained from $\mathrm {PA}\L$ by expanding its language with a new unary predicate symbol $\mathrm {Tr}$ (extending the congruence axioms of $=$ to include $\mathrm {Tr}$, while only arithmetical formulae are considered in the induction rule) and adding the axiom schema $\varphi \mathrel {\leftrightarrow }\mathrm {Tr}(\overline{\varphi })$ for each formula $\varphi$ of the expanded language.

Theorem 4.8

(Hájek et al. 2000) $\mathrm {PA}\L \mathrm {Tr}$ is consistent.⁷

Hence any theory obtained by replacing ${\mathrm {\L }\forall }$ with a weaker logic is consistent too. In choosing a weaker logic, one might want to retain weakening in order to be able to prove crispness of the arithmetical part.

The paper then proceeds to show that one cannot go further and demand that $\mathrm {Tr}$ as formalized truth commute with the connectives: such a theory is contradictory.

Theorem 4.9

(Hájek et al. 2000) The standard model $\fancyscript{N}$ cannot be expanded to a model of $\mathrm {PA}\L \mathrm {Tr}$. Thus $\mathrm {PA}\L \mathrm {Tr}$ has no standard model.

Actually, Restall (1995) shows that $\mathrm {PA}\L$ as such is $\omega$-inconsistent over the standard MV-algebra $[0,1]_{\L }$. It is yet to be investigated whether Peano arithmetic with a truth predicate developed in a suitable weaker logic than ${\mathrm {\L }\forall }$ might have standard models.

4.3 Non-arithmeticity of Product Logic

Now we turn to a different topic, though with the same arithmetic flavour. We recall a result of Hájek (2001), where a particular expansion of a crisp, finitely axiomatizable arithmetic over first-order product logic ${\mathrm {\Pi }\forall }$ is considered, in order to show that first-order satisfiability in standard product algebra $[0,1]_{\mathrm {\Pi }}$ is non-arithmetical.

Definition 4.11

(Hájek 2001)

• 1. ${\mathrm {Q}}\mathrm {\Pi }$ stands for a crisp theory extending Robinson arithmetic in product logic with finitely many axioms (such as the theory $\mathrm {PA}^-$ of Kaye 1991).

• 2. ${\mathrm {Q}}\mathrm {\Pi }{\mathrm {U}}$ expands ${\mathrm {Q}}\mathrm {\Pi }$ with a new unary predicate $U$ and adds the following axioms:

  $$\begin{aligned}&\lnot (\forall {x}) Ux \\&\lnot (\exists {x}) \lnot Ux \\&y=s(x) \mathrel {\rightarrow }(Uy\mathrel {\leftrightarrow }(Ux)^2) \\&x\le y \mathrel {\rightarrow }(Uy\mathrel {\rightarrow }Ux) \end{aligned}$$

Informally speaking, the axioms enforce the truth value of $Ux$ to decrease monotonically (and exponentially) towards $0$, but never reaching it, as $x$ is iteratively incremented by the successor function $s$. Hájek has shown that, among all (classical) structures for the language of arithmetic, exactly those that are isomorphic to the standard model of arithmetic ($\fancyscript{N}$) can be expanded to a $[0,1]_\Pi$ -model of ${\mathrm {Q}}\mathrm {\Pi }{\mathrm {U}}$. Hence, one can decide truth in the standard model of arithmetic in the manner indicated in the next theorem. Take $\bigwedge {\mathrm {Q}}\mathrm {\Pi }{\mathrm {U}}$ to be the $\wedge$-conjunction of all axioms of ${\mathrm {Q}}\mathrm {\Pi }{\mathrm {U}}$.

Theorem 4.10

(Hájek 2001) An arithmetical sentence $\varphi$ is true in $\fancyscript{N}$ iff the formula

$$ \bigwedge {\mathrm {Q}}\mathrm {\Pi }{\mathrm {U}}\wedge \varphi $$

is satisfiable in $[0,1]_{\mathrm {\Pi }}$.

Hence, first-order satisfiability in $[0,1]_{\mathrm {\Pi }}$ is a non-arithmetical decision problem. This technique inspired Franco Montagna to prove that also first-order tautologousness in the standard product algebra $[0,1]_{\mathrm {\Pi }}$, as well as in all standard BL-algebras, are non-arithmetical; these results are to be found in Montagna’s paper (2001), actually in the volume containing also Hájek’s paper (2001).

5 Cantor–Łukasiewicz Set Theory

Another first-order mathematical theory to which Hájek has significantly contributed is naïve set theory over Łukasiewicz logic. As is well known, the rule of contraction (or equivalently the validity of $\varphi \mathrel {\rightarrow }\varphi \mathbin { \& }\varphi$ in sufficiently strong logics) is needed to obtain a contradiction from the existence of Russell’s set by the usual proof. Indeed, the consistency of the unrestricted comprehension schema has been established over several contraction-free logics, including the logic BCK (Petersen 2000) and variants of linear logic (Grishin 1982; Terui 2004). Łukasiewicz logic, which is closely related to the latter logics and like them disvalidates the contraction rule, is thus a natural candidate for the investigation of whether or not it can support a consistent and viable naïve set theory.

The consistency of the unrestricted comprehension schema over Łukasiewicz logic was first conjectured by Skolem (1957). In the 1960s, Skolem (1960), Chang (1963), and Fenstad (1964) obtained various partial consistency results for the comprehension schema restricted to certain syntactic classes of formulae. A proof of the full consistency theorem was eventually published by White (1979). Unlike its predecessors, White’s proof was based strictly on proof-theoretical methods and did not attempt at constructing a model for the theory.

White’s proof of the consistency of unrestricted comprehension over Łukasiewicz logic prompted Hájek to elaborate the theory, for which he coined the name Cantor–Łukasiewicz set theory. With the consistency of Cantor–Łukasiewicz set theory supposedly established, its non-triviality was questioned: i.e., whether the theory is strong enough to reconstruct reasonably large parts of mathematics (as conjectured already by Skolem). Hájek’s contributions (2005, 2013a, b), dealing mainly with arithmetic and decidability in Cantor–Łukasiewicz set theory, gave a partially negative answer to this question. Naïve comprehension over (standard) Łukasiewicz logic has also been developed by Restall (1995), some of whose earlier results Hájek independently rediscovered (2005), and by Yatabe (2007, 2009) who extended some of Hájek’s results. We survey the results on Cantor–Łukasiewicz set theory in Sects. 4.5.1–4.5.2.

In 2010 Terui (pers. comm.) found what appears to be a serious gap in White’s consistency proof. Consequently, the consistency status of Cantor–Łukasiewicz set theory remains unknown. It is therefore worth asking which of Hájek’s and Yatabe’s results survive in weaker fuzzy logics, such as IMTL or MTL.⁸ This problem is addressed in Sect. 4.5.3 below, giving some initial positive results and indicating the main problems that such enterprize has to face.

5.1 Basic Notions of Cantor–Łukasiewicz Set Theory

Definition 4.12

(Hájek 2005) Cantor–Łukasiewicz set theory, denoted here by $\mathrm {C_{{\L }}}$,⁹ is a theory in first-order Łukasiewicz logic. The language of $\mathrm {C_{{\L }}}$ is the smallest language $\fancyscript{L}$ such that it contains the binary membership predicate $\in$ and for each formula $\varphi$ of $\fancyscript{L}$ and each variable $x$ contains the comprehension term $\{ x \mid \varphi \}$. (Thus, comprehension terms in $\mathrm {C_{{\L }}}$ can be nested.) The theory $\mathrm {C_{{\L }}}$ is axiomatized by the unrestricted comprehension schema:

$$ y\in \{ x \mid \varphi (x) \}\mathrel {\leftrightarrow }\varphi (y), $$

for each formula $\varphi$ of $\mathrm {C_{{\L }}}$ and any variables $x,y$.

Remark 4.2

An alternative way of axiomatizing naïve set theory is to use the comprehension schema of the form:

$$\begin{aligned}&(\exists {z})(\forall {x})(x \in z\mathrel {\leftrightarrow }\varphi ) \end{aligned}$$

(4.1)

for any formula $\varphi$ in the language containing just the binary membership predicate $\in$ and not containing free occurrences of the variable $z$. The latter restriction is partly alleviated by the fixed-point theorem (see Theorem 4.13), which makes it possible to introduce sets by self-referential formulae (though not uniquely). The comprehension terms of Definition 4.12 are then the Skolem functions of the comprehension axioms (4.1), conservatively introduceable, eliminable, and nestable by Theorems 4.11 and 4.3 and Lemma 4.4.

Remark 4.3

Clearly, no bivalent or even finitely-valued propositional operator can be admitted in the propositional language of naïve set theories over fuzzy logics on pain of contradiction, as Russell’s paradox could easily be reconstructed by means of such an operator. Unrestricted comprehension is thus inconsistent in any fuzzy logic with $\triangle$ (incl. ${\L }_\triangle$) as well as in any fuzzy logic with strict negation (e.g., Gödel logic, product logic, and the logics $\mathrm {SBL}$ and $\mathrm {SMTL}$). For further restrictions on the fuzzy logic underlying naïve comprehension see Corollary 4.4.

Cantor–Łukasiewicz set theory is in many respects similar to other naïve set theories over various logics, esp. substructural. In particular, the shared features include the distinction between intensional and extensional equality, the fixed-point theorem, the existence of the universal and Russell’s set, non-well-foundedness of the universe, etc. The reason for these resemblances is the fact that the proofs of these theorems are mainly based on instances of the comprehension schema and involve just a few logical steps, all of which are available in most usual non-classical logics. Moreover, the comprehension schema ensures the availability of the constructions provided by the axioms of ZF-style set theories, such as pairing, unions, power sets, and infinity. We shall give a brief account of these features of $\mathrm {C_{{\L }}}$. Unless a reference is given, the proofs are easy or can be found in papers by Hájek (2005) and Cantini (2003).

First observe that by the comprehension schema, the usual elementary fuzzy set operations are available in $\mathrm {C_{{\L }}}$:

Definition 4.13

In $\mathrm {C_{{\L }}}$, we define:¹⁰

$$ \begin{aligned} \emptyset&=_{\mathrm {df}}\{ q \mid \bot \}&\backslash x&=_{\mathrm {df}}\{ q \mid q\notin x \} \\ x\cap y&=_{\mathrm {df}}\{ q \mid q\in x\mathrel { \& }q\in y \}&x\cup y&=_{\mathrm {df}}\{ q \mid q\in x\oplus q\in y \} \\ x\sqcap y&=_{\mathrm {df}}\{ q \mid q\in x\mathrel {\wedge }q\in y \}&x\sqcup y&=_{\mathrm {df}}\{ q \mid q\in x\mathrel {\vee }q\in y \} \end{aligned}$$

The usual properties of these fuzzy set operations are provable in $\mathrm {C_{{\L }}}$.¹¹ Notice, however, that the notions of kernel and support of a fuzzy set are undefinable in $\mathrm {C_{{\L }}}$, as they would make the connective $\triangle$ definable (by setting $\triangle \varphi (y)\equiv y\in \mathop {\mathrm {Ker}}\nolimits \{ x \mid \varphi (x) \}$). Thus unlike ZF-style fuzzy set theories (such as $\mathrm {FST}$ of Sect. 4.3), naïve fuzzy set theories can hardly serve as axiomatizations of Zadeh’s fuzzy sets, as some of the basic concepts of fuzzy set theory cannot be defined in theories with unrestricted comprehension.¹²

Definition 4.14

In $\mathrm {C_{{\L }}}$, we define the following binary predicates:

• Inclusion: $x\subseteq y\equiv _{\mathrm {df}}(\forall {u})(u\in x\mathrel {\rightarrow }u\in y)$.

• Extensional equality (or co-extensionality):¹³ $x\approx y\equiv _{\mathrm {df}}(\forall {u})(u\in x\mathrel {\leftrightarrow }u\in y)$.

• Leibniz equality: $x=y\equiv _{\mathrm {df}}(\forall {u})(x \in u\mathrel {\leftrightarrow }y\in u)$.

We will use $x\ne y$, $x\not \approx y$, $x\notin y$, etc., respectively for ${\lnot }(x=y)$, ${\lnot }(x\approx y)$, ${\lnot }(x \in y)$, etc.

As there is a direct correspondence between sets and properties in $\mathrm {C_{{\L }}}$, the definition of Leibniz equality effectively says that the sets which have the same properties (expressible in the language of $\mathrm {C_{{\L }}}$) are equal (cf. Leibniz’s principle of identity of indiscernibles). Since moreover a concept’s intension is often identified with the set of its properties, Leibniz equality can also be understood as co-intensionality, or intensional equality. Unlike in first-order fuzzy logics with identity (see Sect. 4.2), the predicates $=$ and $\approx$ are defined predicates of $\mathrm {C_{{\L }}}$. It turns out that the properties required of the identity predicate (in particular, the intersubstitutivity of identicals) are satisfied by Leibniz equality, but not by extensional equality. Since moreover Leibniz equality turns out to be crisp in $\mathrm {C_{{\L }}}$, it can be understood as the crisp identity of the objects of $\mathrm {C_{{\L }}}$ (i.e., each model of $\mathrm {C_{{\L }}}$ can be factorized by $=$ salva veritate of all formulae).

The following theorem lists basic provable properties of both equalities.

Theorem 4.11

$\mathrm {C_{{\L }}}$ proves:

• 1. Both $=$ and $\approx$ are fuzzy equivalence relations; i.e.:

  $$ {x=x},\quad {x=y}\mathrel {\rightarrow }{y=x},\quad {x=y}\mathrel { \& }{y=z}\mathrel {\rightarrow }{x=z}, $$

  and analogously for $\approx$. Moreover, $\subseteq$ is a fuzzy preorder whose min-symmetrization is $\approx$:

  $$ x\subseteq x,\quad x\subseteq y\mathrel { \& }y\subseteq z\mathrel {\rightarrow }x\subseteq z,\quad x\approx y\mathrel {\leftrightarrow }x\subseteq y\mathrel {\wedge }y\subseteq x. $$

• 2. Leibniz equality is crisp, i.e., $x=y\mathrel {\vee }x\ne y$.

• 3. Leibniz equality ensures intersubstitutivity: $x=y\mathrel {\rightarrow }(\varphi (x)\mathrel {\leftrightarrow }\varphi (y))$, for any $\mathrm {C_{{\L }}}$-formula $\varphi$.

• 4. Leibniz equality implies co-extensionality: $x=y\mathrel {\rightarrow }x\approx y$. The converse (i.e., the extensionality of $\mathrm {C_{{\L }}}$-sets), however, is inconsistent with $\mathrm {C_{{\L }}}$ (Hájek 2005).¹⁴

By means of the crisp identity, (crisp) singletons, pairs, and ordered pairs can be defined in $\mathrm {C_{{\L }}}$:

Definition 4.15

In $\mathrm {C_{{\L }}}$, we define (for all $k\ge 1$):

$$\begin{aligned} \{ x \}&=_{\mathrm {df}}\{ q \mid q=x \}&\{ x,y \}&=_{\mathrm {df}}\{ q \mid q=x\mathrel {\vee }q=y \} \\ \langle {x,y}\rangle&=_{\mathrm {df}}\{ \{ x \},\{ x,y \} \}&\langle {x_1,\ldots ,x_k,x_{k+1}}\rangle&=_{\mathrm {df}}\langle {\langle {x_1,\ldots ,x_k}\rangle ,x_{k+1}}\rangle \end{aligned}$$

The behavior of these crisp sets is as expected (cf. Theorem 4.20 below). In particular, $\mathrm {C_{{\L }}}$ proves $\langle {x,y}\rangle =\langle {u,v}\rangle \mathrel {\leftrightarrow }{x=u}\mathrel {\wedge }{y=v}$. This makes it possible to employ the following notation:

Convention 4.12

By $\{ \langle {x,y}\rangle \mid \varphi \}$ we abbreviate the comprehension term $\{ q \mid (\exists {x})(\exists {y})(q=\langle {x,y}\rangle \mathrel {\wedge }\varphi ) \}$, and similarly for tuples of higher arities.

Like many other naïve set theories, $\mathrm {C_{{\L }}}$ enjoys the fixed-point theorem that makes self-referential definitions possible:

Theorem 4.13

(The Fixed-Point Theorem) For each formula $\varphi (x,\dots ,z)$ of $\mathrm {C_{{\L }}}$ there is a comprehension term $\zeta _{\varphi }$ such that $\mathrm {C_{{\L }}}$ proves $\zeta _{\varphi }\approx \{ x \mid \varphi (x,\dots ,\zeta _{\varphi }) \}$.

Hájek’s proof of the Fixed Point Theorem (2005) is just a reformulation of Cantini’s proof (2003), which works well in $\mathrm {C_{{\L }}}$. The proof is constructive, i.e., yields effectively and explicitly a particular fixed-point comprehension term $\zeta _{\varphi }$ for each formula $\varphi$.

Convention 4.14

Let us denote the particular fixed-point comprehension term $\zeta$ constructed in the proof of Theorem 4.13 by $\mathop {\mathrm {FP}}\nolimits _{{\!}z}\{ x \mid \varphi (x,\dots ,z) \}$. In definitions using the fixed-point theorem, instead of $u=_{\mathrm {df}}\mathop {\mathrm {FP}}\nolimits _{{\!}z}\{ x \mid \varphi (x,\dots ,z) \}$ we shall write just $u\approx _{\mathrm {df}}\{ x \mid \varphi (x,\dots ,u) \}$.

Thus if we define a fixed point $u\approx _{\mathrm {df}}\{ x \mid \varphi (x,\dots ,u) \}$, then by Theorem 4.13, $\mathrm {C_{{\L }}}$ proves $q\in u\mathrel {\leftrightarrow }\varphi (q,\dots ,u)$. The fixed-point theorem thus ensures that the “equation” $\mathrm {C_{{\L }}}\vdash q\in z\mathrel {\leftrightarrow }\varphi (q,\dots ,z)$ has a solution in $z$ for any formula $\varphi (q,\dots ,z)$. Consequently, as usual in non-classical naïve set theories enjoying the fixed-point theorem, $\mathrm {C_{{\L }}}$ proves the (non-unique) existence of a “Quine atom” $u\approx \{ u \}$, a set comprised of its own properties $u\approx \{ p \mid {u\in p} \}$, etc.

5.2 Arithmetic in Cantor–Łukasiewicz Set Theory

In naïve set theories that enjoy the fixed-point theorem, the set $\omega$ of natural numbers can be defined in a more elegant way than in $\mathrm {ZF}$-like set theories, straightforwardly applying the idea that a natural number is either $0$ or the successor of another natural number. Identifying $0$ with the empty set $\emptyset$ and the successor $s(x)$ of $x$ with $\{ x \}$, we define by the fixed-point theorem:

$$\begin{aligned} \omega \approx _{\mathrm {df}}\{ n \mid n=0\mathrel {\vee }(\exists {m\in \omega })(n=s(m)) \}. \end{aligned}$$

(4.2)

The definition is not unique w.r.t. Leibniz identity: Hájek (2013a) showed that there are infinitely many terms $\omega _i$ such that $\omega \approx \omega _i$ (so $\omega _i$ satisfies the co-extensionality (4.2) as well), but $\omega _i\ne \omega _j$, for each (metamathematical) natural numbers $i,j\in \mathbb N$.¹⁵

$\mathrm {C_{{\L }}}$ expanded by the constant $\omega$ satisfying (4.2) proves some basic arithmetical properties of $\omega$ (cf. Sect. 4.4.1), e.g.:

Theorem 4.15

(Hájek 2005) $\mathrm {C_{{\L }}}$ proves:

• 1. $s(x)\ne 0$

• 2. $s(x)=s(y)\mathrel {\rightarrow }x=y$

• 3. $x \in \omega \mathrel {\leftrightarrow }s(x)\in \omega$

With suitable definitions of addition and multiplication (as given in Hájek (2013a), namely as ternary predicates, adapting the usual inductive definitions to Łukasiewicz logic by means of min-conjunction $\mathbin {\wedge }$), further arithmetical properties, amounting in effect to a $\mathrm {C_{{\L }}}$-analogue of Grzegorczyk’s weakening $\mathrm {Q}^-$ of Robinson arithmetic, can be proved. The proof of essential undecidability of the latter weak classical arithmetic can then be adapted for $\mathrm {C_{{\L }}}$, yielding its essential undecidability and incompleteness. The proof proceeds along the usual lines of Gödel numbering and self-reference (Hájek 2013a).

Theorem 4.16

(Hájek 2013a) The theory $\mathrm {C_{{\L }}}$ is essentially undecidable and essentially incomplete; i.e., each consistent recursively axiomatizable extension of $\mathrm {C_{{\L }}}$ is undecidable and incomplete.

Recall, though, that a theory $T$ over first-order Łukasiewicz logic is considered complete if for each pair $\varphi ,\psi$ of sentences in the language of $T$, either $\varphi \mathrel {\rightarrow }\psi$ or $\psi \mathrel {\rightarrow }\varphi$ is provable in $T$ (Hájek 1998); such theories are also called linear (e.g., Hájek and Cintula 2006). Incompleteness thus means that for some pair $\varphi ,\psi$ of sentences, neither $\varphi \mathrel {\rightarrow }\psi$ nor $\psi \mathrel {\rightarrow }\varphi$ is provable in $T$. The self-referential lemma thus refers to pairs of formulae as well:

Lemma 4.9

(Hájek 2013a) For each pair $\psi _1(x_1,x_2),\psi _2(x_1,x_2)$ of $\mathrm {C_{{\L }}}$-formulae there is a pair $\varphi _1,\varphi _2$ of $\mathrm {C_{{\L }}}$-sentences such that $\mathrm {C_{{\L }}}$ proves $\varphi _1\mathrel {\leftrightarrow }\psi _1(\overline{\varphi }_1,\overline{\varphi }_2)$ and $\varphi _2\mathrel {\leftrightarrow }\psi _2(\overline{\varphi }_1,\overline{\varphi }_2)$.

Regarding induction, the situation is tricky:

Theorem 4.17

(Hájek 2005) If $\mathrm {C_{{\L }}}$ is consistent, then $\mathrm {C_{{\L }}}$ extended by the rule

$$ \frac{\varphi (0), (\forall {x})(\varphi (x)\mathrel {\leftrightarrow }\varphi (s(x)))}{(\forall {x \in \omega })\varphi (x)}, $$

for any $\varphi$ not containing $\omega$, is consistent as well. However, $\mathrm {C_{{\L }}}$ extended by the same rule for any $\varphi$ (including those containing the constant $\omega$), is inconsistent.

Hájek (2005) demonstrated the latter inconsistency claim by developing arithmetic in the extended theory, constructing a truth predicate (cf. Sect. 4.4.2), and showing that it commutes with connectives, which yields inconsistency (Hájek et al. 2000).

In the variant of $\mathrm {C_{{\L }}}$ over standard $[0,1]$-valued Łukasiewicz logic (called $\mathrm {H}$, see footnote 9), the arithmetic of $\omega$ can be shown to be $\omega$-inconsistent (Yatabe 2007; cf.Restall 1995); i.e., $\mathrm { H}\vdash \varphi (\overline{n})$ for each numeral $\overline{n}$, but also $\mathrm { H}\vdash (\exists {n\in \omega }){\lnot }\varphi (n)$ for some formula $\varphi$. It is unclear, though, whether the result can be extended to $\mathrm {C_{{\L }}}$ (Hájek 2013b).

It can be shown that in every model of $\mathrm {C_{{\L }}}$, the set $\omega$ contains a crisp initial segment isomorphic to the standard model of natural numbers (Hájek 2013a). However, this segment need not represent a set of the model (cf. the $\omega$-inconsistency of $\mathrm {H}$).

Remark 4.4

In order to be able to handle such collections of elements that need not be sets, but are nevertheless present in models of $\mathrm {C_{{\L }}}$, extending $\mathrm {C_{{\L }}}$ with classes (which cannot enter the comprehension schema) has been proposed (Hájek 2013b; Běhounek 2010). Although this move may be technically advantageous and can possibly yield an interesting theory, admittedly it destroys the appeal of unrestricted comprehension by restricting it to class-free formulae. It should be kept in mind, though, that the tentative consistency of unrestricted comprehension in $\mathrm {C_{{\L }}}$ itself is only admitted by a restriction of its language (see Remark 4.3), and therefore does not apply the comprehension principle unrestrictedly anyway. As this is a common feature of substructural naïve set theories, it suggests that the consistency of naïve comprehension in certain contraction-free substructural logics (and so the necessity of contraction for Russell’s paradox) is in a sense “accidental”, and that a truly unrestricted comprehension principle would require other logical frameworks (such as paraconsistent or inconsistency-adaptive ones).

5.3 Naïve Comprehension over $\mathrm {MTL}$

In this section we shall discuss which of Hájek’s results in $\mathrm {C_{{\L }}}$ can survive the weakening of the underlying logic to the logic $\mathrm {MTL}$. We will only give an initial study, hinting at the main problems of this transition.

Naïve set theory over the first-order logic $\mathrm {MTL}$ axiomatized in the same way as in Definition 4.12 will be denoted by $\mathrm {C_{\mathrm {MTL}}}$. The basic set operations as well as inclusion and the two equalities can be conservatively introduced in $\mathrm {C_{\mathrm {MTL}}}$ in the same way as in Definitions 4.13–4.14. Cantini’s proof (2003) of the fixed-point theorem (Theorem 4.13; cf. Hájek 2005) works well in $\mathrm {C_{\mathrm {MTL}}}$; consequently, the set $\omega$ of natural numbers can be introduced in $\mathrm {C_{\mathrm {MTL}}}$ in the same self-referential way as in $\mathrm {C_{{\L }}}$ (see Sect. 4.5.2).

It can be easily observed that similarly as in $\mathrm {C_{{\L }}}$ (cf. Theorem 4.11), both equalities $=,\approx$ are fuzzy equivalence relations, inclusion $\subseteq$ is a fuzzy preorder whose min-symmetrization is $\approx$, and Leibniz equality implies intersubstitutivity (and therefore also co-extensionality). It will also be seen later that $\approx$ is provably fuzzy and differs from $=$ (so the extensionality of all sets is inconsistent with $\mathrm {C_{\mathrm {MTL}}}$, too), although these facts need be proved in a manner different from that of Hájek (2005).

In Hájek’s paper (2005), the crispness of $=$, or the provability of $(x=y)\mathrel {\vee }(x\ne y)$, is inferred from the fact that $\mathrm {C_{{\L }}}$ proves contraction (or $\mathbin { \& }$-idempotence) for the Leibniz equality, i.e., $({x=y})\mathrel {\rightarrow }({x=y})^2$. Hájek’s proof of the latter fact works well in $\mathrm {C_{\mathrm {MTL}}}$, too. However, since $\mathrm {MTL}$-algebras (unlike MV-algebras for Łukasiewicz logic) can have non-trivial $\mathbin { \& }$-idempotents, crispness in $\mathrm {MTL}$ does not generally follow from $\mathbin { \& }$-idempotence. Consequently, in $\mathrm {C_{\mathrm {MTL}}}$ Hájek’s proof only ensures the $\mathbin { \& }$-idempotence of the Leibniz identity.

Whether the crispness of $=$ can be proved in $\mathrm {C_{\mathrm {MTL}}}$ by some additional arguments appears to be an open problem. Below we give some partial results which further restrict the possible truth values of Leibniz identity; the complete solution is, however, as yet unknown. The question is especially pressing since so many proofs of Hájek’s advanced results (2005, 2013a) utilize the crispness of $=$ in $\mathrm {C_{{\L }}}$. In some cases, the results can be reconstructed in $\mathrm {C_{\mathrm {MTL}}}$ by more cautious proofs; examples of such theorems (though mostly simple ones) are given below. However, it is currently unclear which part of Hájek’s results on $\mathrm {C_{{\L }}}$ described in Sects. 4.5.1–4.5.2 can still be recovered in $\mathrm {C_{\mathrm {MTL}}}$.

For reference in further proofs, let us first summarize the properties of $\subseteq$, $=$, and $\approx$ that translate readily into $\mathrm {C_{\mathrm {MTL}}}$:

Theorem 4.18

(cf. Hájek 2005) $\mathrm {C_{\mathrm {MTL}}}$ proves:

• 1. ${x=x}$, ${x=y}\mathrel {\rightarrow }{y=x}$, ${x=y}\mathrel { \& }{y=z}\mathrel {\rightarrow }{x=z}$, and analogously for $\approx$

• 2. $x\subseteq x$, $x\subseteq y\mathrel { \& }y\subseteq z\mathrel {\rightarrow }x\subseteq z$, $x\approx y\mathrel {\leftrightarrow }x\subseteq y\mathrel {\wedge }y\subseteq x$

• 3. $x=y\mathrel {\rightarrow }(\varphi (x)\mathrel {\leftrightarrow }\varphi (y))$, for any $\mathrm {C_{\mathrm {MTL}}}$-formula $\varphi$.

• 4. $x=y\mathrel {\rightarrow }x\approx y$

• 5. $x=y\mathrel {\rightarrow }(x=y)^2$

Now let us reconstruct in $\mathrm {C_{\mathrm {MTL}}}$ some basic theorems of $\mathrm {C_{{\L }}}$, without relying on the crispness of Leibniz equality. First it can be observed that the $\mathbin { \& }$-idempotence of $=$ makes it irrelevant which of the two conjunctions is used between equalities. Consequently, $=$ is not only $\mathbin { \& }$-transitive (see Theorem 4.18(1)), but also $\mathbin {\wedge }$-transitive, so the notation $x=y=z$ can be used without ambiguity.

Theorem 4.19

$\mathrm {C_{\mathrm {MTL}}}$ proves:

• 1. $a=b\mathrel {\wedge }c=d\mathrel {\leftrightarrow }a=b\mathrel { \& }c=d$

• 2. $x=y\mathrel {\wedge }y=z\mathrel {\rightarrow }x=z$

Proof

The claims follow directly from Theorem 4.18(5) and Lemma 4.1. $\square$

Even without assuming the crispness of $=$, singletons and pairs (defined as in Definition 4.15) behave as expected. Unlike $\mathrm {C_{{\L }}}$, where crisp cases can be taken due to the crispness of $=$ and the proofs are thus essentially classical, $\mathrm {C_{\mathrm {MTL}}}$ requires more laborious proofs of these facts.

Theorem 4.20

$\mathrm {C_{\mathrm {MTL}}}$ proves:

• 1. $\{ a \}=\{ b \}\mathrel {\leftrightarrow }a=b$

• 2. $\{ a,b \}=\{ c,d \}\mathrel {\leftrightarrow }(a=c\mathrel {\wedge }b=d)\mathrel {\vee }(a=d\mathrel {\wedge }b=c)$

• 3. $\{ a,b \}\subseteq \{ c \}\mathrel {\leftrightarrow }a=b=c$; in particular, $\{ a,b \}\approx \{ a \}\mathrel {\leftrightarrow }a=b$

• 4. $\langle {a,b}\rangle =\langle {c,d}\rangle \mathrel {\leftrightarrow }a=c\mathrel {\wedge }b=d$

• 5. $\langle {x',y'}\rangle \in \{ \langle {x,y}\rangle \mid \varphi (x,y,\dots ) \}\mathrel {\leftrightarrow }\varphi (x',y',\dots )$

• 6. $y\approx y\cup \{ x \}\mathrel {\leftrightarrow }x \in y$

Proof

1. Right to left: by intersubstitutivity. Left to right: $\{ a \}=\{ b \} \longrightarrow \{ a \}\approx \{ b \} \longleftrightarrow (\forall {x})(x \in \{ a \}\mathrel {\leftrightarrow }x \in \{ b \}) \longleftrightarrow (\forall {x})(x=a\mathrel {\leftrightarrow }x=b) \longrightarrow a=a\mathrel {\leftrightarrow }a=b \longleftrightarrow a=b$.

2. Right to left: Both disjuncts imply the consequent by intersubstitutivity. Left to right:

$$\begin{aligned}&\{ a,b \}=\{ c,d \}\longrightarrow \{ a,b \}\approx \{ c,d \}\longleftrightarrow (\forall {x})(x=a\mathrel {\vee }x=b\mathrel {\leftrightarrow }x=c\mathrel {\vee }x=d)\longleftrightarrow \\&(\forall {x})(x=a\mathrel {\vee }x=b\mathrel {\rightarrow }x=c\mathrel {\vee }x=d)\mathrel {\wedge }(\forall {x})(x=c\mathrel {\vee }x=d\mathrel {\rightarrow }x=a\mathrel {\vee }x=b)\longleftrightarrow \\&(\forall {x})(x=a\mathrel {\rightarrow }x=c\mathrel {\vee }x=d)\mathrel {\wedge }(\forall {x})(x=b\mathrel {\rightarrow }x=c\mathrel {\vee }x=d)\mathrel {\wedge }\\&{\qquad }(\forall {x})(x=c\mathrel {\rightarrow }x=a\mathrel {\vee }x=b)\mathrel {\wedge }(\forall {x})(x=d\mathrel {\rightarrow }x=a\mathrel {\vee }x=b)\longrightarrow \\&(a=c\mathrel {\vee }a=d)\mathrel {\wedge }(b=c\mathrel {\vee }b=d)\mathrel {\wedge }(c=a\mathrel {\vee }c=b)\mathrel {\wedge }(d=a\mathrel {\vee }d=b) \end{aligned}$$

Distributivity then yields max-disjunction of 16 min-conjunctions, of which 14 are equivalent to $a=b=c=d$, one to $a=c\mathrel {\wedge }b=d$, and one to $a=d\mathrel {\wedge }b=c$.

3. Right to left: $x \in \{ a,b \}\longrightarrow x=a\mathrel {\vee }x=b\longleftrightarrow x=c\mathrel {\vee }x=c\longleftrightarrow x=c\longleftrightarrow x \in \{ c \}$; intersubstitutivity is used in the second step. Left to right:

$$\begin{aligned}&\{ a,b \}\subseteq \{ c \}\longleftrightarrow (\forall {x})(x=a\mathrel {\vee }x=b\mathrel {\rightarrow }x=c)\longleftrightarrow \\&(\forall {x})(x=a\mathrel {\rightarrow }x=c)\mathrel {\wedge }(\forall {x})(x=b\mathrel {\rightarrow }x=c)\longrightarrow a=c\mathrel {\wedge }b=c. \end{aligned}$$

4. Right to left: by Theorems 4.20(1)–(2). Left to right: By Theorem 4.20(2),

$$ \langle {a,b}\rangle =\langle {c,d}\rangle \mathrel {\leftrightarrow }(\{ a \}=\{ c \}\mathrel {\wedge }\{ a,b \}=\{ c,d \})\mathrel {\vee }(\{ a \}=\{ c,d \}\mathrel {\wedge }\{ a,b \}=\{ c \}). $$

Thus it is sufficient to show the following two implications:

$$ \begin{array}{ll} \{ a \}=\{ c \}\mathrel {\wedge }\{ a,b \}=\{ c,d \}\longleftrightarrow &{}\text {by Theorem } 4.20(1)\!--\!(2) \\ a=c\mathrel {\wedge }((a=c\mathrel {\wedge }b=d)\mathrel {\vee }(a=d\mathrel {\wedge }b=c))\longleftrightarrow &{}\text {by distributivity} \\ (a=c\mathrel {\wedge }a=c\mathrel {\wedge }b=d)\mathrel {\vee }(a=d\mathrel {\wedge }b=c\mathrel {\wedge }a=c)\longrightarrow &{}\text {by} \wedge \text {-transitivity of }= \\ a=c\mathrel {\wedge }b=d,\quad \text {and} \\ \{ a \}=\{ c,d \}\mathrel {\wedge }\{ a,b \}=\{ c \}\longrightarrow &{}\text {by Theorem 4.18(2)}\\ \{ c,d \}\subseteq \{ a \}\mathrel {\wedge }\{ a,b \}\subseteq \{ c \}\longrightarrow &{}\text {by Theorem 4.20(3)} \\ a=b=c=d\longrightarrow a=c\mathrel {\wedge }b=d. \end{array} $$

5. The claim is proved by the following chain of equivalences:

$$ \begin{array}{ll} (\exists {x})(\exists {y})(\langle {x',y'}\rangle =\langle {x,y}\rangle \mathrel { \& }\varphi (x,y,\dots ))\longleftrightarrow &{}\text {by Theorems 4.20(4) and 4.19} \\ (\exists {x})(\exists {y})(x=x'\mathrel { \& }y=y'\mathrel { \& }\varphi (x,y,\dots ))\longleftrightarrow &{}\text {in first-order}\,\mathrm {MTL}\\ (\exists {x=x'})(\exists {y=y'})(\varphi (x,y,\dots ))\longleftrightarrow &{}\text {by Lemma 4.3(3)} \\ \varphi (x',y',\dots ) \end{array} $$

6. The claim is proved by the following chain of equivalences (where the last one follows from Lemma 4.3(2)):

$$ \begin{array}{l} y\approx y\cup \{ x \}\longleftrightarrow (\forall {q})(q\in y\mathrel {\leftrightarrow }q\in y\mathrel {\vee }q=x)\longleftrightarrow \\ (\forall {q})(q\in y\mathrel {\rightarrow }q\in y\mathrel {\vee }q=x)\mathrel {\wedge }(\forall {q})(q\in y\mathrel {\rightarrow }q\in y)\mathrel {\wedge }(\forall {q})(q=x\mathrel {\rightarrow }q\in y)\longleftrightarrow \\ (\forall {q})(q=x\mathrel {\rightarrow }q\in y)\longleftrightarrow x \in y. \end{array} $$

$\square$

Several useful facts about the Leibniz equality can be derived from considering Russell’s set, $\mathrm {r}=_{\mathrm {df}}\{ x \mid x\notin x \}$. The following observation is instrumental for these considerations:

Theorem 4.21

$\mathrm {C_{\mathrm {MTL}}}$ proves: $(\mathrm {r}\in \mathrm {r})^2\mathrel {\leftrightarrow }\bot$.

Proof

By comprehension, $\mathrm {r}\in \mathrm {r}\mathrel {\leftrightarrow }\mathrm {r}\notin \mathrm {r}$; thus $\mathrm {r}\in \mathrm {r}\mathrel { \& }\mathrm {r}\in \mathrm {r}\longleftrightarrow \mathrm {r}\in \mathrm {r}\mathrel { \& }\mathrm {r}\notin \mathrm {r}\longleftrightarrow \bot$. $\square$

Since $\mathrm {r}\in \mathrm {r}\mathrel {\leftrightarrow }\mathrm {r}\notin \mathrm {r}$, the truth value of the formula $\mathrm {r}\in \mathrm {r}$ is the fixed point $\rho$ of negation in the $\mathrm {MTL}$-algebra of semantic truth values in any model of $\mathrm {C_{\mathrm {MTL}}}$. Consequently, $\mathrm {C_{\mathrm {MTL}}}$ has models only over $\mathrm {MTL}$-algebras possessing the fixed point (e.g., there is no model of $\mathrm {C_{\mathrm {MTL}}}$ over Chang’s MV-algebra). Moreover, Theorem 4.21 makes it possible to establish the inconsistency of extensionality in $\mathrm {C_{\mathrm {MTL}}}$ without the assumption of the crispness of Leibniz equality:

Corollary 4.1

$\mathrm {C_{\mathrm {MTL}}}$ plus the extensionality axiom $x\approx y\mathrel {\rightarrow }x=y$ is inconsistent.

Proof

Since $x=y\mathrel {\rightarrow }x\approx y$ is a theorem (Theorem 4.18(4)), under extensionality the equality relations $=$ and $\approx$ would coincide. Thus by Theorems 4.18(5) and 4.20(6), the relation $\in$ would have to yield idempotent values. However, by Theorem 4.21, $\mathrm {r}\in \mathrm {r}$ is not idempotent. $\square$

Theorem 4.21 shows that the fixed point $\rho$ of negation is nilpotent; consequently, there are no non-trivial idempotents smaller than $\rho$. As a corollary, the truth value of Leibniz identity cannot lie between $0$ and $\rho$:

Corollary 4.2

$\mathrm {C_{\mathrm {MTL}}}$ proves: $x\ne y\mathrel {\vee }(\mathrm {r}\in \mathrm {r}\mathrel {\rightarrow }x=y)$.

Proof

By Theorems 4.18(5) and 4.21, and the strong linear completeness of $\mathrm {MTL}$.

A direct proof in $\mathrm {C_{\mathrm {MTL}}}$ can easily be given as well: By prelinearity we can prove that

$$ (x=y\mathrel {\rightarrow }\mathrm {r}\in \mathrm {r})^2\mathrel {\vee }(\mathrm {r}\in \mathrm {r}\mathrel {\rightarrow }x=y). $$

Thus to prove Cor. 4.2 it is sufficient to prove $(x=y\mathrel {\rightarrow }\mathrm {r}\in \mathrm {r})^2\mathrel {\rightarrow }(x=y\mathrel {\rightarrow }\bot )$. Now, $x=y\longleftrightarrow (x=y)^2\longrightarrow (\mathrm {r}\in \mathrm {r})^2\longleftrightarrow \bot$, respectively by Theorem 4.18(5), the assumption $(x=y\mathrel {\rightarrow }\mathrm {r}\in \mathrm {r})^2$, and Theorem 4.21. $\square$

Thus, only sufficiently large truth values (namely, those larger than the truth value $\rho$ of $\mathrm {r}\in \mathrm {r}$) can be non-trivial idempotents in any model of $\mathrm {C_{\mathrm {MTL}}}$. This result can be extended by considering the following sets:

Definition 4.16

For each $n\ge 1$, we define $\mathrm {r}_n=_{\mathrm {df}}\{ x \mid (x\notin x)^n \}$

By definition, $\mathrm {r}_n\in \mathrm {r}_n\mathrel {\leftrightarrow }(\mathrm {r}_n\notin \mathrm {r}_n)^n$. Consequently, the semantic truth value $\rho _n$ of $\mathrm {r}_n\in \mathrm {r}_n$ satisfies $\rho _n=({\lnot }\rho _n)^n$. Clearly, $\rho _n>0$ for each $n$, since otherwise $0=\rho _n=({\lnot }\rho _n)^n=({\lnot }0)^n=1^n=1\ne 0$, a contradiction. The values $\rho _n$ form a non-increasing chain:

Theorem 4.22

For each $n\ge 1$, $\mathrm {C_{\mathrm {MTL}}}$ proves: $\mathrm {r}_{n+1}\in \mathrm {r}_{n+1}\mathrel {\rightarrow }\mathrm {r}_n\in \mathrm {r}_n$.

Proof

We shall prove that $(\mathrm {r}_n\in \mathrm {r}_n\mathrel {\rightarrow }\mathrm {r}_{n+1}\in \mathrm {r}_{n+1})^n\mathrel {\rightarrow }(\mathrm {r}_{n+1}\in \mathrm {r}_{n+1}\mathrel {\rightarrow }\mathrm {r}_n\in \mathrm {r}_n)$, whence the theorem follows by prelinearity.

First, by $(\mathrm {r}_n\in \mathrm {r}_n\mathrel {\rightarrow }\mathrm {r}_{n+1}\in \mathrm {r}_{n+1})^n$ we have $(\mathrm {r}_{n+1}\notin \mathrm {r}_{n+1}\mathrel {\rightarrow }\mathrm {r}_n\notin \mathrm {r}_n)^n$. Then we obtain:

$$\begin{aligned} \begin{array}{lll} \mathrm {r}_{n+1}\in \mathrm {r}_{n+1}&{}\longleftrightarrow {} (\mathrm {r}_{n+1}\notin \mathrm {r}_{n+1})^{n+1} &{}\quad \text {by definition} \\ &{}\longrightarrow {} (\mathrm {r}_{n+1}\notin \mathrm {r}_{n+1})^n &{}\quad \text {by weakening} \\ &{}\longrightarrow {}(\mathrm {r}_n\notin \mathrm {r}_n)^n &{}\quad \text {by }(\mathrm {r}_{n+1}\notin \mathrm {r}_{n+1}\mathrel {\rightarrow }\mathrm {r}_n\notin \mathrm {r}_n)^n \\ &{}\longleftrightarrow {}\mathrm {r}_n\in \mathrm {r}_n &{}\quad \text {by definition.} \end{array} \end{aligned}$$

$\square$

As a corollary to Theorems 4.21 and 4.22, the truth values $\rho _n$ are nilpotent for each $n$:

Corollary 4.3

$(\mathrm {r}_n\in \mathrm {r}_n)^2\mathrel {\leftrightarrow }\bot$

Proof

By Theorems 4.21 and 4.22, $(\mathrm {r}_n\in \mathrm {r}_n)^2\longrightarrow (\mathrm {r}_1\in \mathrm {r}_1)^2\longleftrightarrow \bot$. $\square$

The sequence of truth values $\rho _n$ is in fact strictly decreasing, and the sequence of ${\lnot }\rho _n$ strictly increasing:

Theorem 4.23

In any model of $\mathrm {C_{\mathrm {MTL}}}$, the truth values $\rho _n$ of $\mathrm {r}_n\in \mathrm {r}_n$ form a strictly decreasing chain and the truth values ${\lnot }\rho _n$ of $\mathrm {r}_n\notin \mathrm {r}_n$ form a strictly increasing chain.

Proof

By Theorem 4.22 we know that $\rho _{n+1}\le \rho _n$, so ${\lnot }\rho _n\le {\lnot }\rho _{n+1}$. Suppose ${\lnot }\rho _n={\lnot }\rho _{n+1}$. Then $\rho _{n+1}=({\lnot }\rho _{n+1})^{n+1}=({\lnot }\rho _n)^{n+1}=(({\lnot }\rho _n)^n\mathbin { \& }{\lnot }\rho _n) =(\rho _n\mathbin { \& }{\lnot }\rho _n)=0$, but we have already observed that $\rho _{n+1}>0$ for all $n$—a contradiction. Thus ${\lnot }\rho _{n+1}\ne {\lnot }\rho _n$, so ${\lnot }\rho _{n+1}>{\lnot }\rho _n$ and $\rho _{n+1}<\rho _n$. $\square$

As a corollary we obtain that the theory $\mathrm {C_{\mathrm {MTL}}}$ is infinite-valued, as each model’s $\mathrm {MTL}$-algebra contains an infinite decreasing chain of truth values below the fixed point of ${\lnot }$ and an infinite increasing chain of truth values above the fixed point of ${\lnot }$. Moreover, since $({\lnot }\rho _n)^n=\rho _n$, which by Corollary 4.3 is not idempotent, ${\lnot }\rho _n$ is not $n$-contractive.¹⁶ Consequently, there are no models of $\mathrm {C_{\mathrm {MTL}}}$ over $n$-contractive $\mathrm {MTL}$-algebras, for any $n\ge 1$:

Corollary 4.4

Naïve comprehension is inconsistent in all logics $\mathrm {C_ n MTL}$ of $n$-contractive $\mathrm {MTL}$-algebras (i.e., in $\mathrm {MTL}$ plus the axiom $\varphi ^{n-1}\mathrel {\rightarrow }\varphi ^n$), for any $n\ge 1$. Consequently, it is also inconsistent in any extension of any $\mathrm {C_ n MTL}$, which class includes all logics $\mathrm {S_ n MTL}$ of $n$-nilpotent $\mathrm {MTL}$-algebras (i.e., $\mathrm {MTL}$ plus the axiom $\varphi ^{n-1}\mathbin {\vee }{\lnot }\varphi$) as well as the logics $\mathrm {NM}$ and $\mathrm {WNM}$ of (weak) nilpotent minima.¹⁷

By Theorem 4.23, the truth values ${\lnot }\rho _n$ of $\mathrm {r}_n\notin \mathrm {r}_n$ form an increasing sequence. By Corollary 4.3, each ${\lnot }\rho _n$ is nilpotent, since $({\lnot }\rho _n)^{2n}=(({\lnot }\rho _n)^n)^2=\rho _n^2=0$. Non-trivial idempotents can thus only occur among truth values larger than all ${\lnot }\rho _n$:

Corollary 4.5

In any model of  $\mathrm {C_{\mathrm {MTL}}}$, all non-trivial idempotents are larger than all truth values ${\lnot }\rho _n$ of $\mathrm {r}_n\notin \mathrm {r}_n$. (In particular, they are larger than the fixed point $\rho _1$ of negation).

This fact is internalized in the theory by the following strengthening of Corollary 4.2:

Corollary 4.6

For all $n\ge 1$, $\mathrm {C_{\mathrm {MTL}}}$ proves: $x\ne y\mathrel {\vee }(\mathrm {r}_n\notin \mathrm {r}_n\mathrel {\rightarrow }x=y)$.

Proof

The proof is analogous to that of Corollary 4.2: by prelinearity, it is sufficient to prove $(x=y\mathrel {\rightarrow }\mathrm {r}_n\notin \mathrm {r}_n)^{2n}\mathrel {\rightarrow }x\ne y$, which obtains by $x=y\longleftrightarrow (x=y)^{2n}\longrightarrow (\mathrm {r}_n\notin \mathrm {r}_n)^{2n}\longleftrightarrow (\mathrm {r}_n\in \mathrm {r}_n)^2\longleftrightarrow \bot$, using the previous observations. $\square$

By Corollary 4.5, the truth values of the Leibniz equality can only be $0$ or sufficiently large (namely, larger than all $\rho _n$). At present it is, however, unclear whether they have to be crisp or not. As we have seen in Theorems 4.18–4.20, some basic properties of Leibniz equality known from $\mathrm {C_{{\L }}}$ can be proved in $\mathrm {C_{\mathrm {MTL}}}$ by more laborious proofs even without the assumption of the crispness of $=$. However, since most of Hájek’s results on arithmetic in $\mathrm {C_{{\L }}}$ rely heavily on the crispness of identity, it is unclear whether they can be reconstructed in $\mathrm {C_{\mathrm {MTL}}}$ or not.

6 Conclusions

In this chapter we have surveyed (and on a few occasions slightly generalized) the work in axiomatic fuzzy mathematics connected with Petr Hájek. A recurring pattern could be observed in Hájek’s work in this area: even in a non-classical setting of mathematical fuzzy logic, he made a point of employing the knowledge and methods he mastered during earlier stages of his career, for example, in comparing axiomatic theories using syntactic interpretations, or in relying on strong independence results in arithmetic.

Even though Hájek’s results remain a landmark of these investigations, it could also be seen from our exposition of them that the theories in question (as well as their metamathematics) are still at initial stages of their development, and many interesting questions remain still open. Hájek’s investigation into these theories opened the way for interesting research and demonstrated that some intriguing results can be achieved. One of the aims of this chapter was to gather the results in this field of research scattered in several papers and present them in a synoptic perspective, in order to promote further research in this area of axiomatic non-classical mathematics. We therefore conclude it with a list of open problems mentioned or alluded to in this chapter:

• Can a completeness theorem be proved for the ZF-style fuzzy set theory FST over $\mathrm {MTL}$?

• What is the difference between ${\mathrm {FST}_{\mathrm {BL}}}$ and ${\mathrm {FST}_{\mathrm {MTL}}}$?

• Can Peano arithmetic with a truth predicate over $\mathrm {MTL}$ (or some intermediate logic between $\mathrm {MTL}$ and ${\L }$) have standard models?

• Is $\mathrm {C_{{\L }}}$ (or $\mathrm {C_{\mathrm {MTL}}}$) consistent (relative to a well-established classical theory)?

• Is the Leibniz equality $=$ crisp in $\mathrm {C_{\mathrm {MTL}}}$?

• Is $\omega$ crisp in $\mathrm {C_{{\L }}}$ ($\mathrm {C_{\mathrm {MTL}}}$)?

• Is $\mathrm {C_{\mathrm {MTL}}}$ (essentially) undecidable and incomplete?

• Is there a method of constructing models of $\mathrm {C_{{\L }}}$ or $\mathrm {C_{\mathrm {MTL}}}$, so that the models would satisfy some required properties?