Logic is commonly defined as the analysis of methods of reasoning[63]. In the presentation of modern symbolic logic, the form of a statement and its content are usually separated, and are defined by the syntax and the semantics of the logic respectively. The syntax of a logic defines a formal language by some grammatical rules and its semantics stipulates the truth conditions of the formulas in the language.
2.2.1 Propositional logic
The syntax of propositional logic (PL) is based on the combinations of simple sentences in various ways to form more complicated sentences. The combinations are truth-functional in the sense that the truth value of the new sentence is determined by those of its component sentences. The alphabet of PL consists of a set of primitive propositions, Φ0, and the logical symbols ¬(negation),
∧(and), ∨(or), and ⊃(material implication). The logical symbols of PL are also called Boolean connectives. The set of well-formed formulas (wffs) of propositional logic is defined as the smallest set Φ such that Φ0 ⊆ Φ and
• if ϕ ∈ Φ, then ¬ϕ ∈ Φ;
• if ϕ and ψ ∈ Φ, then ϕ ∧ ψ, ϕ ∨ ψ, and ϕ ⊃ ψ ∈ Φ.
The auxiliary parentheses symbols are usually employed to disambiguate the reading of a sentence.
The equivalence connective ≡ is defined as an abbreviation, i.e., ϕ ≡ ψ is an abbreviation of (ϕ ⊃ ψ) ∧ (ψ ⊃ ϕ).
The semantic models of PL are simply truth assignments to the primitive propositions. Mathe-matically, an interpretation (or a model) of a PL is a function π : Φ0 → {0, 1}. The interpretation π can be extended to the whole domain Φ by the following recursion rules:
1. π(¬ϕ) = 1 − π(ϕ),
2. π(ϕ ∧ ψ) = min(π(ϕ), π(ψ)), 3. π(ϕ ∨ ψ) = max(π(ϕ), π(ψ)), 4. π(ϕ ⊃ ψ) = max(1 − π(ϕ), π(ψ)).
We say that a wff ϕ is true (resp. false) under the interpretation π if π(ϕ) = 1 (resp. π(ϕ) = 0).
A wff ϕ is valid if it is true under all interpretations and satisfiable if it is true under some interpretation. A wff that is not satisfiable is said to be unsatisfiable. Note that ϕ is valid iff ¬ϕ is unsatisfiable.
2.2.2 Modal logic
As shown by the well-known Stone representation theorem, classical set theory has the intimate connection with the Boolean logic[83]. Analogously, rough set theory is closely related to modal logic[7]. The most well-known relationship is the connection of approximation space with possible world semantics for the modal epistemic logic S5.
The alphabet of S5 consists of a set of primitive propositions, Φ0, and the logical sym-bols ¬(negation), ∧(and), ∨(or), ⊃(material implication), (necessity modal operator), and
♦(possibility modal operator). The set of well-formed formulas (wffs) of S5 is defined as the smallest set Φ such that Φ0 ⊆ Φ and
• if ϕ ∈ Φ, then ¬ϕ, ϕ, and ♦ϕ ∈ Φ
• if ϕ and ψ ∈ Φ, then ϕ ∧ ψ, ϕ ∨ ψ, and ϕ ⊃ ψ ∈ Φ.
A Kripke model for S5 is a triple M = (W, R, π), where W is a set of possible worlds, R is an equivalence relation on W , called an accessibility relation, and π : Φ0 → 2W is a truth assignment that map a primitive propositions to the set of worlds in which it is evaluated to be true. The function π can be extended to all wffs recursively in the following way:
1. π(¬ϕ) = W − π(ϕ) 2. π(ϕ ∧ ψ) = π(ϕ) ∩ π(ψ) 3. π(ϕ ∨ ψ) = π(ϕ) ∪ π(ψ) 4. π(ϕ ⊃ ψ) = π(¬ϕ) ∪ π(ψ)
5. π(ϕ) = {w | ∀u((w, u) ∈ R ⇒ u ∈ π(ϕ))}
6. π(♦ϕ) = {w | ∃u((w, u) ∈ R ∧ u ∈ π(ϕ))}
For each model M and wff ϕ, π(ϕ) is called the truth set of ϕ (in M ).
Obviously, if M = (W, R, π) is a Kripke model for S5, then (W, R) is an approximation space, and for each wff ϕ, π(ϕ) is a subset of W and denote some concept in the approximation space, so we can consider its lower and upper approximations. A direct but interesting relationship between S5 and rough set theory is then established as follows:
Rπ(ϕ) = π(ϕ), Rπ(ϕ) = π♦ϕ).
2.2.3 Arrow logic (AL)
In this section, we review the basic syntax and semantics of AL in order to lay the foundation for the development of arrow decision logic. AL is the basic modal logic of arrows [61, 87]. An arrow can represent a state transition in a program’s execution, a morphism in category theory, an edge in a directed graph, etc. In AL, an arrow is an abstract entity; however, we can usually interpret it as a concrete relationship between two objects, which results in a pair-frame model [61, 87]. We now present the syntax and semantics of AL.
The basic alphabet of AL consists of a countable set of propositional symbols, the Boolean connectives ¬ and ∨, the modal constant δ, the unary modal operator ⊗, and the binary modal operator ◦. The set of AL wffs is the smallest set containing the propositional symbols and δ, closed under the Boolean connectives ¬ and ∨, and satisfying
• if ϕ is a wff, then ⊗ϕ is a wff too;
• if ϕ and ψ are wffs, then ϕ ◦ ψ is also a wff.
In addition to the standard Boolean connectives, we also abbreviate ¬ ⊗ ¬ϕ and ¬(¬ϕ ◦ ¬ψ) as
⊗ϕ and ϕ◦ψ respectively.
Semantically, these wffs are interpreted in arrow models.
Definition 2.5
1. An arrow frame is a quadruple F = (W, C, R, I) such that C ⊆ W × W × W , R ⊆ W × W and I ⊆ W .
2. An arrow model is a pair M = (F, π), where F = (W, C, R, I) is an arrow frame and π is a valuation that maps propositional symbols to subsets of W . An element in W is called an arrow in the model M.
3. The satisfaction of a wff ϕ on an arrow w of M, denoted by w |=M ϕ (as usual, the subscript M can be omitted), is inductively defined as follows:
(a) w |= p iff w ∈ π(p) for any propositional symbol p, (b) w |= δ iff w ∈ I,
(c) w |= ¬ϕ iff w 6|= ϕ,
(d) w |= ϕ ∨ ψ iff w |= ϕ or w |= ψ,
(e) w |= ϕ ◦ ψ iff there exist s, t such that (w, s, t) ∈ C, s |= ϕ, and t |= ψ, (f ) w |= ⊗ϕ iff there is a t with (w, t) ∈ R and t |= ϕ.
Example 2.2 Let us use the (multi-)graph shown in Figure 2.1 to explain the basic concept of arrow models. As shown in the figure, the arrow frame is characterized as F = (W, C, R, I), where
• W = {a1, a2, . . . , a10},
• C = {(a1, a4, a5), (a1, a4, a7), . . . , (a8, a8, a10)}
• R = {(a5, a6), . . . , (a10, a10)}
• I = {a9, a10}
If x1, x2, x3, and x4 denote four cities and ai(1 ≤ i ≤ 10) denote routes between these them, then I denote the set of intra-city routes, whereas the others are inter-cities routes. A route ai is a reverse route of another route aj if (ai, aj) ∈ R. For example, a6 is a reverse route of a5. Also, (ai, aj, ak) ∈ C if aj followed by ak is an alternative route of ai. For example, a3 is a direct route connecting the cities x1 and x3. However, alternatively, we can also go from x1 to x2 through route a4 and then from x2 to x3 through the route a5. Thus, a4 followed by a5 is an alternative route to a3. Now, let us consider an arrow logic language with two propositional symbols p and q meaning “the route is in congestion” and “the route is in bad situation” respectively. Assume that the valuation π of the arrow model is given as follows:
π(p) = {a1, a2, a3, a9, a10}, π(q) = {a1, a4, a6, a8, a10}.
Then, in the model (F, π), we have a9 |= δ since a9 is an intra-city route. We also have a7 |=
¬q∧(⊗q) which means that a7 is not in bad situation, but one of its reverse routes is. Furthermore, we have a3 |= p ∧ (q ◦ (¬p ∧ ¬q)) which means that a3 is in congestion and there is an alternative route with a section (a4) in bad situation followed by a section (a5) neither in bad situation nor in congestion.
Intuitively, in the arrow frame (W, C, R, I), W can be regarded as the set of edges of a directed graph; I denotes the set of identity arrows3; (w, s) ∈ R if s is a reversed arrow of w; and (w, s, t) ∈ C if w is an arrow composed of s and t. This intuition is reflected in the following definition of pair frames.
Definition 2.6 An arrow frame F = (W, C, R, I) is a pair frame if there exists a set U such that W ⊆ U × U and
1. for x, y ∈ U , if (x, y) ∈ I then x = y,
2. for x1, x2, y1, y2 ∈ U , if ((x1, y1), (x2, y2)) ∈ R, then x1 = y2 and y1 = x2,
3. for x1, x2, x3, y1, y2, y3 ∈ U , if ((x1, y1), (x2, y2), (x3, y3)) ∈ C, then x1 = x2, y2 = x3, and y1 = y3.
An arrow model M = (F, π) is called a pair model if F is a pair frame. A pair model is called a (full) square model if the set of arrows W = U × U .
3An identity arrow is an arrow that has the same starting point and endpoint.
a
1a
2a
3a
4a
5a
6a
7a
8x1
x2
x3
a
10a
9x4
I={ a
9a
10}
R ={(a
5, a
6) , (a
6, a
5) (a
7, a
6) , (a
6, a
7) (a
9, a
9) (a
10, a
10)}
C ={(a
1, a
4, a
5), (a
1, a
4, a
7), (a
2, a
4, a
5), (a
2, a
4, a
7), (a
3, a
4, a
5) ,(a
3, a
4, a
7) , (a
8, a
8, a
9), (a
8, a
8, a
10) }
W={ a
1, a
2, …., a
10}
Figure 2.1: An arrow model