A Minimal Temporal Logic with Multiple Fuzzy Truth-Values

Abstract

Temporal logic is a very important branch of non-classical logic, systematically studying formal reasoning over time, which actually is a kind of modal logic with the truth-value set of $\{0,1\}$. However, in real life, propositions that concern with tense are not always absolutely true or false. To this end, this paper fuzzifies the minimal temporal logic system. Specifically, we fuzzify propositions’ truth values to six fuzzy linguistic truth values, and thus we build a new multi-valued temporal logic system. We also prove the completeness and soundness of our logic system. In addition, we illustrate our system by a real life example.

1 Introduction

Temporal logic is a kind of modal logic, studying tense propositions and formal reasoning about tense propositions. The research on modal logic is originated by Aristotle in his book entitled “Physics”, where he gave a rough form of first-order two-valued temporal logic. In modern time, it is logician Arthur Prior who started the study of temporal logic, and established the first formal axiom system of temporal logic [20]. Since 1960s, the results of temporal logic gradually increased considerably. For example, Pnueli [18] established a linear temporal first order logic with two temporal operator: next and until. In 1984, Emerson [9] established Branching Time Logic, which covers Linear Temporal Logic as its special case. In 1986, Moszkowski [16] established Interval Temporal Logic, which is also linear and first-order, but can only deal with finite sequence of statements. In 1990, Emerson [8] introduced Proposition Linear Temporal Logic and Branching Time Logic, and proved that these two kinds of temporal systems are modal complete. In 1997, Marx and Venema [14] introduced dimensional temporal logic, called Arrow Logic, discussing the relation theory of interval temporal logic and modal logic. In 2007, Akama [1] had noticed the uncertainty of future, and thus established a new temporal logic system which is three-valued, and proved its completeness and soundness. All in all, temporal logic has developed into a much more mature logic branch, and has an important impact in computer science and philosophy.

The propositions in these existing various forms of temporal logic are still either absolutely true or absolutely false. Nonetheless, in real life it is not always the case, but multiple truth-values are required. For example, in weather forecast, for a prediction of future weather, it cannot be absolutely correct. So a kind of temporal logic with multiple fuzzy truth-values is required to make temporal logic more practical, worthy while and reliable. To this end, in this paper we try to fuzzify the minimal temporal logic system [15] to establish a new temporal logic system. More specifically, we will give its syntax, semantics, and axiom system, and prove that this system is complete and sound.

There are some work on fuzzy temporal logic, but few of them deal with multiple fuzzy truth-values of temporal proportions. For example, [10, 17] focus on fuzzy notations of time, [19] employs fuzzy logic to deal with time constraints of incomplete information, and [12] mainly discusses fuzzy temporal events and fuzzy temporal states defined on a linear time model. On the other hand, some studies (e.g., [4, 11]) deal with modal logic with multiple fuzzy truth-values, but their modal logic is not a kind of temporal logic.

The rest of the paper is structured as follows. Section 2 recaps some basic notations and methods of fuzzy set theory. Section 3 defines our fuzzy logic system. Section 4 proves the completeness and soundness of our fuzzy temporal logic. Section 5 gives a real life example to illustrate the usability of our logic system. Finally, Section 6 concludes the paper and points out future work.

2 Preliminaries

This section recaps some basic concepts and notations of fuzzy set theory.

The following is Zadeh’s concept of fuzzy sets [21]:

Definition 1

(Fuzzy set). A fuzzy set is a pair $(U, \mu )$, where U is a set (called the universe of the fuzzy set) and $\mu$ is a mapping from U to [0, 1] (called the membership function of the fuzzy set). And $\forall x \in U$, the value of $\mu (x)$ is called the membership degree of x in U.

Baldwin [2] defined the following fuzzy linguistic truth-value set, which is used in some fuzzy logic systems (e.g., [11, 13]):

Definition 2

(Fuzzy Linguistic Truth). A linguistic truth-value set is defined as follows:

(1)

For convenience, we denote

(2)

(3)

The semantics of the terms in this term set are defined as shown in Table 1 and drawn graphically in Fig. 1.

Table 1. The membership functions of linguistic truth (where $x \in [0, 1]$)

Fig. 1.

The curves of linguistic truth

In real life, it is difficult for people to deal with continuous numbers, thus we can assume the membership functions of the linguistic truths is on the set of discrete points $0,0.1,0.2, \dots , 1.0$. Thus, for example, we can represent $\tau _{\phi }=true$ and $\tau _{\psi } =false$ as follows:

$$\begin{aligned}&\tau _{\phi }=\frac{0}{0}+\frac{0.1}{0.1}+\frac{0.2}{0.2}+\frac{0.3}{0.3}+\frac{0.4}{0.4}+\frac{0.5}{0.5}+\frac{0.6}{0.6}+\frac{0.7}{0.7}+\frac{0.8}{0.8}+\frac{0.9}{0.9}+\frac{1.0}{1.0}, \end{aligned}$$

(4)

$$\begin{aligned}&\tau _{\psi } =\frac{1.0}{0}+\frac{0.9}{0.1}+\frac{0.8}{0.2}+\frac{0.7}{0.3}+\frac{0.6}{0.4}+\frac{0.5}{0.5}+\frac{0.4}{0.6}+\frac{0.3}{0.7}+\frac{0.2}{0.8}+\frac{0.1}{0.9}+\frac{0}{1.0}. \end{aligned}$$

(5)

In fuzzy logic, t-norms ($\bigtriangleup$) and t-connorms ($\bigtriangledown$) are used to deal with conjunction and disjunction, respectively. The following is their definition [6, 7]:

Definition 3

(t-norm and t-connorm). A binary operator $\circ$ on [0, 1] is a triangular norm (t-norm), denoted as $\bigtriangleup$, if it satisfies:

• (1) commutativity: $a \circ b=b\circ a$,

• (2) associativity: $(a\circ b)\circ c=a\circ (b\circ c)$,

• (3) monotonicity: $a\le b \Rightarrow a\circ c \le b\circ c$,

• (4) unit element: $a\circ 1=a$.

A binary operator $\circ$ on [0, 1] is a triangular connorm (t-connorm), denoted as $\bigtriangledown$, if it satisfies: (1), (2), (3) and

• $(4^\prime )$ unit element: $a\circ 0=a$.

A typical pair of typical t-norm $\bigtriangleup$ and t-conorm $\bigtriangledown$ is as follows:

$$\begin{aligned} \bigtriangleup (x, y)&=\min \{x, y\}, \end{aligned}$$

(6)

$$\begin{aligned} \bigtriangledown (x, y)&=\max \{x, y\}. \end{aligned}$$

(7)

The following definition gives the properties that a complement operator should obey:

Definition 4

(Complement operator). A mapping C : $[0, 1]\rightarrow [0, 1]$ is a complement operator if it satisfies the following conditions:

• (1) $C(0)=1, C(1)=0$;

• (2) $C(C(x))=x$; and

• (3) if $a \le b$ then $C(a) \ge C(b).$

A common complement operator is:

$$\begin{aligned} C(x)=1-x. \end{aligned}$$

(8)

The following method can be used to extend a function on the crisp sets to the one on fuzzy sets.

Definition 5

(Extension Principle). Suppose f is a function with n arguments $x_{1}, \ldots , x_{n}$. Let $A_{i}$ be the fuzzy set of $x_{i}$. Then we can extend function f to taking fuzzy arguments $A_{1}, \ldots , A_{n}$, which result is a fuzzy set defined by:

$$ \mu _{B}(y)=\sup \{ \mu _{A_{1}} (x_{1} ) \wedge \ldots \wedge \mu _{A_{n}} (x_{n} ) \mid f(x_{1}, \ldots x_{n} )=y \}, $$

where $\sup$ denotes the supremum operation on a set. For convenience, the operation of the extension principle is denoted as $\otimes$.

If the results of an operator on fuzzy linguistic true-values is not closed on the set of fuzzy linguistic true-values, we need the following linguistic approximation technology:

Definition 6

(Linguistic Approximation). Given $\tau \in LTTS, \tau _{1} \in LTTS$ being the closest to $\tau$ should satisfy:

$$\begin{aligned} \forall \tau _{2} \in LTTS, ED(\tau , \tau _{1} ) \le ED(\tau , \tau _{2} ), \end{aligned}$$

where ED is the Euclidean Distance, which is defined as follows: for two fuzzy linguistic terms $\tau _{1}$ and $\tau _{2}$ on $U=\{0.1,0.2,\cdots ,1\}$:

$$\begin{aligned} ED(\tau _{1}, \tau _{2})=\sqrt{ \sum \{ (\mu _{\tau _{1}} (x)-\mu _{\tau _{2}} (x))^2\mid x\in U\} }. \end{aligned}$$

(9)

For convenience, the operation of linguistic approximation is denoted as $\odot$.

3 Logic System

This section will present the syntax and semantics of our fuzzy temporal logic system (denoted as $FK_{t}$).

3.1 Syntax

First we present the rules that define a logic formula in our logic system.

Definition 7

(Language). Let PV be a countable set of proposition letters. A proposition formula in $FK_{t}$ is defined by

$$\begin{aligned} \phi : : = p\mid \lnot \phi \mid \phi \wedge \psi \mid P \phi \mid F\phi , \end{aligned}$$

where $p\in PV$, P is the weak past operator, meaning “happened once in past”; and F is the weak future operator, meaning “will happen once in future”. And strong future operator, denoted as G, which means “will happen all the time in future”, is defined as:

$$\begin{aligned}&G\phi =_{df} \lnot F \lnot \phi ; \end{aligned}$$

(10)

and strong past operator, denoted as H, which means “happened all the time in past”, is defined as:

$$\begin{aligned}&H\phi =_{df} \lnot P \lnot \phi . \end{aligned}$$

(11)

We also need the following abbreviations:

$$\begin{aligned}&\phi \vee \varphi =_{df}\lnot ( \lnot \phi \wedge \lnot \varphi ), \end{aligned}$$

(12)

$$\begin{aligned}&\phi \rightarrow \varphi =_{df} \lnot \phi \vee \varphi . \end{aligned}$$

(13)

The axioms (which are used as the start points of inference in our logic system) and proof rules (which are used for inference) are as follows:

Definition 8

(Axioms and proof rules). Suppose that $\varphi _1$ and $\varphi _2$ are formulas in $FK_{t}$. The axiomatization of $FK_{t}$ contains:

• (A1) all propositional tautologies,

• (A2) $G(p \rightarrow q) \rightarrow (Gp \rightarrow Gq)$,

• (A3) $H(p \rightarrow q) \rightarrow (Hp \rightarrow Hq)$,

• (A4) $p \rightarrow GPp$,

• (A5) $p \rightarrow HFp$,

with the following rules of proof:

• (1) Modus ponens: if $\phi$ and $\phi \rightarrow \varphi$, then $\varphi$.

• (2) Uniform substitution: if $\varphi$ is obtained from $\phi$ by uniformly replacing proposition letters in $\phi$ by arbitrary formulas, then $\phi$ implies $\varphi$.

• (3) Future Generalisation: if $\phi$, then $G \phi$.

• (4) Past Generalisation: if $\phi$, then $H \phi$.

Once we have a set of axioms and a set of inference rules, under certain conditions we can prove a logic formula. Formally, we have:

Definition 9

(Proof). Let $\varGamma$ is a set of formulas in $FK_{t}$. In $FK_{t}$ a formula $\phi$ is provable from $\varGamma$, denoted as $\varGamma \vdash \phi$, if there is a sequence of formulas $<\phi _1,\cdots ,\phi _n>$ in $FK_{t}$ such that $\phi _n = \phi$ and for each $\phi _i$ $(1\le i < n)$, either $\phi _i$ is one of the axioms or $\phi _i \in \varGamma$ or $\phi _i$ can be obtained from the earlier items by applying the rules of proof. If $\varGamma$ is empty, we abbreviate it as $\vdash \phi$.

Intuitively, if from a set of propositions we can prove a proposition not only true but also false, then the set of proposition is inconsistent. Formally, we have:

Definition 10

(Consistent). Suppose that $\varGamma$ is a set of formulas in $FK_{t}$. $\varGamma$ is inconsistent if there exists a formula $\phi$ such that $\varGamma \vdash \phi$ and $\varGamma \vdash \lnot \phi$. $\varGamma$ is consistent if it is not inconsistent.

3.2 Semantics

Basically, the syntax of our logic is the same as that of crisp temporal logic. However, the semantics of our fuzzy one is quite different from that of crisp one.

Informally, in each world (time point), we designate a fuzzy linguistic truth value for each proposition in temporal logic $FK_{t}$. Formally, we have:

Definition 11

(Model). A fuzzy temporal model $\mathcal {M}$ is a triple (T, R, V), where:

• (1) T is a non-empty finite set of all time possible worlds;

• (2) R is a binary relation on T; and

• (3) V is a mapping from $\hbox { Var}\times T \rightarrow LTTS$, called a fuzzy truth evaluation, where $\hbox { Var}=\{p_{1}, \dots , p_{n} \}$ is a set of countable propositional variables, and LTTS is the linguistic truth-value set defined as formula (1).

The rules for calculate the truth-value of a logic formula are as follows:

Definition 12

(Truth evaluation of $FK_{t}$ ). For any formula $\phi$, let $V(\phi , \mathcal {M}, t)$ be the fuzzy truth value of $\phi$ in world t. Then

• (1) $V(\lnot \phi , \mathcal {M}, t)=\odot (\otimes (V(\phi , \mathcal {M}, t), C))$;

• (2) $V(\phi \wedge \psi , \mathcal {M}, t)=\odot (\otimes (V(\phi , \mathcal {M}, t), V(\psi , \mathcal {M}, t), \bigtriangleup ))$;

• (3) $V(\phi \wedge (\phi \rightarrow \psi ),\mathcal {M}, t)$, denoted as $\tau '_{\psi }$, is defined as follows:

  $$\begin{aligned} \tau '_{\psi } =\odot (\tau ''_{\psi } ), \end{aligned}$$

  (14)

  where $\mu _{ \tau ''_{\psi } } (y)=\sup \{ \mu _{V( \phi , \mathcal {M}, t) } (x) \bigtriangleup \mu _{V(\phi \rightarrow \psi ,\mathcal {M}, t)} (x, y)\};$

• (4) $V(F\phi , \mathcal {M}, t)=\max \{V(\phi , \mathcal {M}, t^{'} )\mid t^{'} \in T, R(t, t^{'}) )\}$; and

• (5) $V(P\phi , \mathcal {M}, t)=\max \{V(\phi , \mathcal {M}, t^{'} )\mid t^{'} \in T, R(t^{'}, t)\}$.

Table 2. The conjunctive operator of fuzzy temporal logic

Table 3. The complement operator of fuzzy temporal logic

By Definition 12, from $V(\phi , \mathcal {M}, t)$ and $V(\psi , \mathcal {M}, t)$, we can find the truth-value of $\phi \wedge \psi$ as showed in Table 2, and that of $\lnot \phi$ as showed in Table 3. Now we give an example of how we calculate the truth evaluation of $\tau _{\phi } \wedge \tau _{\psi }$. Suppose that $\tau _{\phi }=true$, which is defined as formula (10), and $\tau _{\psi } =false$, which is defined as formula (11). Then by the extension principle (see Definition 5) and the evaluation of conjunction operator (see Definition 12), we have:

$$\begin{aligned}&\!\!\!\!\!\!\!\!\!\!\!\!\!\!\mu _{\phi \wedge \psi }(0.1)\\ =\max \{&\min (\mu _{\phi }(0.1),\mu _{B}(0.1)), \min (\mu _{\phi }(0.1),\mu _{B}(0.2)),\\&\min (\mu _{\phi }(0.1),\mu _{\psi }(0.3)), \min (\mu _{\phi }(0.1),\mu _{\psi }(0.4)), \min (\mu _{\phi }(0.1),\mu _{\psi }(0.5)), \\&\min (\mu _{\phi }(0.1),\mu _{\psi }(0.6)), \min (\mu _{\phi }(0.1),\mu _{\psi }(0.7)), \min (\mu _{\phi }(0.1),\mu _{\psi }(0.8)),\\&\min (\mu _{\phi }(0.1),\mu _{\psi }(0.9)) \min (\mu _{\phi }(0.1),\mu _{\psi }(1.0)), \\&\min (\mu _{\phi }(0.2),\mu _{\psi }(0.1)), \min (\mu _{\phi }(0.3),\mu _{\psi }(0.1)) \min (\mu _{\phi }(0.4),\mu _{\psi }(0.1)),\\&\min (\mu _{\phi }(0.5),\mu _{\psi }(0.1)), \min (\mu _{\phi }(0.6),\mu _{\psi }(0.1)), \min (\mu _{\phi }(0.7),\mu _{\psi }(0.1)),\\&\min (\mu _{\phi }(0.8),\mu _{\psi }(0.1)), \min (\mu _{\phi }(0.9),\mu _{\psi }(0.1)), \min (\mu _{\phi }(1.0),\mu _{\psi }(0.1))\}\\ =\max \{&\min \{0.1,0.9\}, \min \{0.1,0.8\},\\&\min \{0.1,0.7\}, \min \{0.1,0.6\}, \min \{0.1,0.5\}, \\&\min \{0.1,0.4\}, \min \{0.1,0.3\}, \min \{0.1,0.2\},\\&\min \{0.1,0.1\}, \min \{0.1,0\}, \\&\min \{0.2, 0.9\}, \min \{0.3, 0.9\}, \min \{0.4, 0.9\},\\&\min \{0.5, 0.9\}, \min \{0.6, 0.9\}, \min \{0.7, 0.9\},\\&\min \{0.8, 0.9\}, \min \{0.9, 0.9\}, \min \{1.0, 0.9\}\}\\&\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!= 0.9 . \end{aligned}$$

The calculation of $\mu _{\phi \wedge \psi }$ at other points are similar to the above. Then we have

$$\begin{aligned} \tau _{\phi \wedge \psi }=\frac{1.0}{0}+\frac{0.9}{0.1}+\frac{0.8}{0.2}+\frac{0.7}{0.3}+\frac{0.6}{0.4}+\frac{0.5}{0.5}+\frac{0.4}{0.6}+\frac{0.3}{0.7}+\frac{0.2}{0.8}+\frac{0.1}{0.9}+\frac{0}{1.0}. \end{aligned}$$

Finally, by Linguisitic Approximation (see Definition 6), $\tau _{\phi \wedge \psi }$ is nearest to linguistic truth-value false. That is, the truth evaluation of $\phi \wedge \psi$ is false.

In Definition 12, we did not give the formulas for calculating $V(G\phi , \mathcal {M}, t)$, $V(H\phi ,\mathcal {M}, t)$ and $V(\phi \rightarrow \psi ,\mathcal {M}, t)$, but we can use formulas (10), (11) and (13) to transfer them into the ones that can be calculated according to the formulas given in Definition 12. That is:

$$\begin{aligned}&V(G\phi , \mathcal {M}, t)=\min \{V(\phi , \mathcal {M}, t^{'} )\mid t^{'} \in T, R(t, t^{'}) \},\end{aligned}$$

(15)

$$\begin{aligned}&V(H\phi ,\mathcal {M}, t)=\min \{V(\phi , \mathcal {M}, t{'} )\mid t^{'} \in T, R(t^{'},t) \} . \end{aligned}$$

(16)

Definition 13

(Satisfaction). Given a temporal model $\mathcal {M} =(T, R, V)$, any proposition p in $\mathcal {M}$ is satisfiable in world t, denoted as $\mathcal {M}, t\vDash p$, which can be defined recursively as follows:

• (1) $\mathcal {M}, t\vDash \psi$ iff $V(\psi , \mathcal {M}, t) \in LTTS_{t}$ or ($V(\phi \rightarrow \psi ,\mathcal {M}, t) \in LTTS_{t}$ and $V(\phi , \mathcal {M}, t) \in LTTS_{t} )$.

• (2) $\mathcal {M}, t\vDash \lnot \phi$ iff $V(\phi , \mathcal {M}, t) \in LTTS_{f}$.

• (3) $\mathcal {M}, t\vDash \phi \wedge \psi$ iff $\mathcal {M}, t\vDash \phi$ and $\mathcal {M}, t\vDash \psi$.

• (4) $\mathcal {M}, t\vDash F\phi$ iff there exists at least one $u \in T$ and R(t, u) such that $\mathcal {M}, u\vDash \phi$.

• (5) $\mathcal {M}, u\vDash P\phi$ iff there exists at least one $t \in T$ and R(t, u) such that $\mathcal {M}, t\vDash \phi$.

By the above definition and formulas (10)–(13), we have:

• (1) $\mathcal {M}, t\vDash G\phi$ iff for all $u \in T$ and R(t, u), $\mathcal {M}, u\vDash \phi$.

• (2) $\mathcal {M}, u\vDash H\phi$ iff for all $t \in T$ and R(t, u), $\mathcal {M}, t\vDash \phi$.

• (3) $\mathcal {M}, t\vDash \phi \vee \psi$ iff $\mathcal {M}, t\vDash \phi$ or $\mathcal {M}, t\vDash \psi$.

• (4) $\mathcal {M}, t\vDash \phi \rightarrow \psi$ iff $\mathcal {M}, t\vDash \lnot \phi$ or $\mathcal {M}, t\vDash \psi$.

Definition 14

(Semantic consequence). Suppose that $\varGamma$ is a set of formulas in $FK_{t}$ and $\phi$ is a formula in $FK_{t}$. $\phi$ is the semantic consequence of $\varGamma$ (denoted by $\varGamma \vDash \phi$) if for all valuations, models and possible worlds such that every formula in $\varGamma$ is satisfiable, $\phi$ is satisfiable. If $\varGamma$ is empty, then we abbreviate it as $\vDash \phi$ and say that $\phi$ is valid.

4 Soundness and Completeness

This section will prove the soundness and completeness of our logic system.

4.1 Soundness

The soundness of a logic system means that if a formula in the logic can be proved from its axioms of the logic by its inference rules, then the formula is a semantic consequence. Formally, we have:

Theorem 1

(Soundness). Fuzzy minimal temporal logic system is sound with respect to the class of all frames, meaning if $\varSigma \vdash \phi$ then $\varSigma \vDash \phi$.

Proof

First, we will prove that the rules of proof preserve validity: (i) Suppose modus ponens does not preserve validity, then we have $\vDash p \rightarrow q$, $\vDash p$ but $\nvDash q$. Hence, there is a model $\mathcal {M} = (T,R,V)$ such that $\mathcal {M},t\vDash p \rightarrow q$, $\mathcal {M},t\vDash p$ and $\mathcal {M},t\nvDash q$. Since $\mathcal {M},t\vDash p \rightarrow q$, $\mathcal {M},t \nvDash p$ or $\mathcal {M},t\vDash q$. But we have $\mathcal {M},t\vDash p$ and $\mathcal {M},t\nvDash q$, contradicting the result above. Thus, modus ponens preserves validity. (ii) It is easy to verify that future generalisation preserves validity. Suppose $\vDash p$, then by Definition 14, for any model $\mathcal {M} = (T,R,V)$ and any $t \in T$, $\mathcal {M},t \vDash p$. Then $\vDash G p$. If not, there is a model and a world in this model such that p is not satisfiable, which contradicts to our hypothesis. So, future generalisation preserves validity. The proof of past generalisation is similar.

Now we will prove that every axiom is valid: (i) Suppose $\phi$ is propositional tautology, then in every possible world t, the truth value of $\phi$ is in $LTTS_{t}$. (ii) To prove $\vDash G(p \rightarrow q) \rightarrow (Gp \rightarrow Gq)$, we need prove that for every possible world t in any model $\mathcal {M}$,

$$V(G(p \rightarrow q) \rightarrow (Gp \rightarrow Gq), \mathcal {M}, t) \in LTTS_{t} ,$$

which means that when $V(G(p \rightarrow q), M, t)\in LTTS_{t}$, definitely $V((Gp \rightarrow Gq), \mathcal {M}, t)\in LTTS_{t}$. So, when $V(G(p \rightarrow q), \mathcal {M}, t)\in LTTS_{t}$, in possible world $t'$ satisfying $R(t, t')$ we have $V((p \rightarrow q), \mathcal {M}, t')\in LTTS_{t}$. That is, when $V(p, \mathcal {M}, t')\in LTTS_{t}$, there must be $V(q, M, t')\in LTTS_{t}$. When $V(Gp, \mathcal {M}, t)\in LTTS_{t}$, there must be $V(Gq, \mathcal {M}, t)\in LTTS_{t}$, and thus $V((Gp \rightarrow Gq), \mathcal {M}, t)\in LTTS_{t}$. So, $V(G(p \rightarrow q) \rightarrow (Gp \rightarrow Gq), \mathcal {M}, t) \in LTTS_{t}$ is proved. (iii) $\vDash H(p \rightarrow q) \rightarrow (Hp \rightarrow Hq)$ can be proved similarly to (ii). (iv) We prove $\vDash \phi \rightarrow GP\phi$. For any $\phi$, on the one hand, suppose $V(\phi , \mathcal {M}, t) \in LTTS_{t}$. In possible world $t'$ which is accessed by possible world t, by Definition 12,

$$V(P\phi , \mathcal {M}, t')=\max \{V(\phi , \mathcal {M}, t'')\mid R(t'', t') \} ,$$

and t access to $t'$. So since $V(\phi , \mathcal {M}, t) \in LTTS_{t}$, $V(P\phi , \mathcal {M}, t')$ must be in $LTTS_{t}$.

When we look back to see possible world t, by Definition 12 we know

$$V(GP\phi , \mathcal {M}, t) =\min \{V(P\phi , \mathcal {M}, t')\mid R(t, t')\} ,$$

which means $V(GP\phi , \mathcal {M}, t)\in LTTS_{t}$. On the other hand, if $V(\phi , \mathcal {M}, t) \in LTTS_{f}$ then $V(\lnot \phi , \mathcal {M}, t) \in LTTS_{t}$. So, $\vDash \phi \rightarrow GP\phi$. (v) We prove $\vDash \phi \rightarrow HF\phi$. For any $\phi$, on the one hand, suppose $V(\phi , M, t) \in LTTS_{t}$. In possible world $t'$, which is accessed by possible world t, by Definition 12,

$$V(F\phi , \mathcal {M}, t') =\max \{V(\phi , \mathcal {M}, t'')\mid R(t', t'') \}$$

and t access to $t'$. So since $V(\phi , M, t) \in LTTS_{t}$, $V(F\phi , \mathcal {M}, t')$ must be in $LTTS_{t}$. When we look back to see possible world t, by Definition 12,

$$V(HF\phi , \mathcal {M}, t)=\min \{V(F\phi , \mathcal {M}, t')\mid R(t', t)\} ,$$

which means $V(HF\phi , \mathcal {M}, t) \in LTTS_{t}$. On the other hand, if $V(\phi , M, t) \in LTTS_{f}$, $V(\lnot \phi , \mathcal {M}, t) \in LTTS_{t}$. So, $\vDash \phi \rightarrow HF\phi$.    $\square$

4.2 Completeness

Now we are going to discuss the completeness of our logic, meaning that if a formula is correct semantically, then it is correct syntactically.

Before giving the completeness theorem of our logic, we need more concepts.

Definition 15

(Maximal consistent set). A set of formulas $\varGamma$ is maximal consistent if and only if

• (1) $\varGamma$ is consistent; and

• (2) $\varGamma$ is maximal: there does not $\varGamma '$ such that $\varGamma \subset \varGamma '$ and $\varGamma '$ is consistent.

Definition 16

(Fuzzy consistency). Let $\varGamma$ be a set of formulas, we say $\varGamma$ is consistent, if for any formula $\phi \in \varGamma$, it is impossible that $V(\phi , \mathcal {M}, t)\in LTTS_t$ and $V(\lnot \phi , \mathcal {M}, t) \in LTTS_t$.

Definition 17

(Canonical model). The canonical model $\mathcal {M} ^{c} =(T^{c}, R^{c}, V^{c} )$ is defined as follows:

• (1) $T^{c}$ is the set of all possible worlds;

• (2) $R^{c}$ is a transitive, irreflexive, and asymmetrical binary relation on $T^{c}$ such that $(t,t')\in R^{c}$ if for all formulas $\psi$, $t \vdash F\psi$ implies $t' \vdash \psi$, and $t' \vdash P\psi$ implies $t \vdash \psi$; and

• (3) $V^{c}: \text{ Var } \times T \rightarrow LTTS$ is a fuzzy truth evaluation such as $V^{c}(p,\mathcal {M},t)\in LTTS_{t}$ if and only if $t \vdash p$, where $p\in \text{ Var }=\{p_{1}, \dots , p_{n} \}$ (i.e., a set of countable propositional variables).

In order to prove completeness, we also need some lemmas as follows:

Lemma 1

Suppose that $\varGamma$ is a maximally consistent set, then:

• (1) for all formulas $\phi$: $\phi \in \varGamma$ or $\lnot \phi \in \varGamma$;

• (2) for all formulas $\phi$, $\varphi$: $\phi \vee \varphi \in \varGamma$ iff $\phi \in \varGamma$ or $\varphi \in \varGamma$.

The proof of the above lemma can be found in [3].

Lemma 2

(Lindenbaum’s Lemma [5]). If $\varGamma$ is consistent, then there exists a $\varGamma _{l}$ is maximal and consistent, where $\varGamma \subseteq \varGamma _{l}$.

Lemma 3

(Truth Lemma). Suppose that $t \in T^{c}$. For any $\phi$, $t\vdash \phi$ iff $(\mathcal {M} ^{c}, t) \vDash \phi$.

Proof

We prove by induction on the length of $\phi$. The base case follows from the definition of $V^{c}$. The boolean cases follow from Lemma 1. It remains to deal with the modalities. Suppose that $\phi = F \varphi$. $\mathcal {M}^{c},t \vDash F \varphi$ iff $\exists t'\in T^{c}$ $(tR^{c}t' \wedge \mathcal {M}^{c} \vDash \varphi$) iff (by induction hypothesis) $\exists t (tR^{c}t' \wedge t'\vdash \varphi )$ iff $t\vdash F \varphi$. The proof for the case $\phi = P \varphi$ is similar to the proof above.    $\square$

Now we can give our completeness theorem.

Theorem 2

(Completeness). Fuzzy minimal temporal logic system is complete, i.e., $\varGamma \vDash \phi$ implies $\varGamma \vdash \phi$.

Proof

To prove it, we need prove the converse-negative proposition: if $\varGamma \nvdash \phi$, then $\varGamma \nvDash \phi$. If $\varGamma \nvdash \phi$, we can know $\varGamma \cup \{\lnot \phi \}$ is a consistent set, by Lindenbaum’s Lemma (i.e., Lemma 2), there is a maximal consistent set $\varGamma _{l}$. We will use canonical model to find this maximal consistent set $\varGamma _{l}$ to make $\varGamma _{l} \supseteq \varGamma \cup \{\lnot \phi \}$. By Truth Lemma (i.e., Lemma 3) and fuzzy consistent, we know $V^{c}(\phi , M^{c}, t) \in LTTS_{t}$ iff $\phi \in \varGamma _{l}$, then $\lnot \phi \in \varGamma _{l}$, $\lnot \phi \in \varGamma$. Thus $\varGamma \nvDash \phi$ is proved.    $\square$

Table 4. Truth value of $\phi$

Table 5. Truth value of $\psi$

5 Example

Let us consider an example in real life. Suppose Mary plans to have a holiday of three days $d_{1}$, $d_{2}$, and $d_{3}$. During the holiday, she plans to visit two different cities within two days, and there are four optional cities $c_{1}$, $c_{2}$, $c_{3}$, and $c_{4}$. She likes a city which is not rainy and above 20 Celsius degree. Now suppose we know the truth-values of that these four cities in three days are “not raining” (denoted as $\phi$) and “above 20 Celsius degree” (denoted as $\psi$) as shown in Tables 4 and 5, and the accessible relation between these four cities are:

$$\begin{aligned}&R(c_{1}, c_{2}), R(c_{1}, c_{4}), R(c_{2}, c_{3}), R(c_{2}, c_{4}), R(c_{3}, c_{4}). \end{aligned}$$

We give an example to show how to calculate the fuzzy linguistic truth-value of a modal proposition. By Definition 12 and Table 2, we have:

$$\begin{aligned} V(G\phi _{d_{1}}, M, c_{1} )=&\min \{ V(\phi _{d_{1}}, M, c_{1}), V(\phi _{d_{2}}, M, c_{2}) \} \\ =&\min \{fairly\text{- }true,very\text{- }true\}\\ =&fairly\text{- }true, \\ V(G\phi _{d_{2}} , M, c_{1})=&\min \{ V(\phi _{d_{2}}, M, c_{1} ), V(\phi _{d_{3}}, M, c_{2} ) \\ =&\min \{true,true\}\\ =&true, \\ V(G\psi _{d_{1}}, M, c_{1} )=&\min \{ V(\psi _{d_1}, M, c_{1} ), V(\psi _{d_2}, M, c_{2} )\} \\ =&\min \{ true,false\}\\ =&false, \\ V(G\psi _{d_{2}}, M, c_{1} ) =&\min \{ V(\psi _{d_{2}}, M, c_{1} ), V(\psi _{d_{3}} , M, c_{2}) \\ =&\min \{fairly\text{- }true, true\}\\ =&fairly\text{- }true. \end{aligned}$$

Then again by Definition 12 and Table 2, we have:

$$\begin{aligned} V(G\phi _{d_{1}} \wedge G\psi _{d_{1}} ), M, A) =&\min \{V(G\phi _{d_{1}}, M, c_{1} ),V(G\psi _{d_{1}}, M, c_{1} )\} \\ =&\min \{fairly\text{- }true, false \} \\ =&false, \\ V(G\phi _{d_{2}} \wedge G\psi _{d_{2}} ), M, A ) =&\min \{V(G\phi _{d_{2}} , M, c_{1}),V(G\psi _{d_{2}}, M, c_{1} )\} \\ =&\min \{ true, fairly\text{- }true\}\\ =&fairly\text{- }true. \end{aligned}$$

Accordingly, Mary should spend the holiday in city $c_{1}$ on day 2.

6 Conclusions

On the one hand, temporal logic has proved to be an important kind of modal logic since 1960s. On the other hand, the development of fuzzy logic lets us see that the original two-valued logic system can have much more widespread applications in real-life if they are extended by fuzzy logic theory. As a result, in this paper we fuzzified the minimal temporal logic system by extending its truth-value set of $\{0,1\}$ to the one of six linguistic truth-values. In particular, we define the semantics of this logic system, and we also prove that this logic system is soundness and completeness. Moreover, to show the applicability of our new system, we discuss a real-life example with our system. However, fuzzy temporal logic system can be more applicable not only in real life but also in computer science. So in further work, it is worth exploring how to apply fuzzy temporal logic into different areas, specially the area of Artificial Intelligence.