Abstract
The symmetric implicational methods for fuzzy reasoning characterizes the solution B* (A*) of the formula (A → 1B) → 2 (A* → 1B*) for the fuzzy modus ponens (fuzzy modus tollens), where →1 and →2 are two different implications. In this study, we provide a predicate formal representation of the solution for the symmetric implicational methods based on the LΠ formal logic system, including detailed logic proofs. We bring the symmetric implicational methods within a logical framework and provide a sound logic foundation for the symmetric implicational methods of fuzzy reasoning.
Introduction
It is well known that the most fundamental inference forms of fuzzy reasoning are fuzzy modus ponens (FMP) and fuzzy modus tollens (FMT), which can be respectively expressed as follows (see [18, 19]).
FMP(A, B, A*). For a given rule A → B and an input A*, calculate the output B*.
FMT(A, B, B*). For a given rule A → B and an input B*, calculate the output A*.
In order to deal with the above inference forms, Zadeh [18] proposed the compositional rule of inference (CRI) method. Since the CRI method was proposed, many other methods of fuzzy reasoning have been proposed introduced (see [14, 20]). As a revision or a supplement for the Zadeh’s CRI method, Wang [16] proposed the full implication triple I (TI) method, whose solution was the smallest B* ∈ F (V) (or the largest A* ∈ F (U)) such that, for any u ∈ U, v ∈ V,
Tang et al. [14] generalized the TI method to the symmetric implicational (SI) method, which changed (1) into
In the research area of fuzzy reasoning, one of the interesting problems is the analysis of reliability and reasonableness of fuzzy reasoning. To solve this problem, one approach is to formalize the fuzzy reasoning algorithms and their consistency. In this way, fuzzy reasoning is put rigorously into the framework of pure fuzzy logic and thus have a rigorous logic foundation. Novák [9] discussed CRI algorithms based on the fuzzy predicate logic BL (see [7]). Pei [10–12] considered the formalization problem of the TI algorithms based on the monoidal t-norm based fuzzy logic MTL (see Esteva and Godo [4]) and revised Kleene logic K* (see [4, 13]). Luo et al. [8] studied the formalization problem for quintuple implication (QI) algorithms [20] based on MTL. However, to the best of our knowledge, the logical foundation of the SI algorithms has not been studied previously. Our main aim is to formalize the solutions for SI algorithms to the FMP and FMT problems and provide a sound logic foundation for the SI algorithms of fuzzy reasoning. But one problem is: which logic framework of formal systems? They are many formal systems such as BL, MTL and K*. Since the SI method allows different fuzzy implications to be employed, these formal systems dealing with a fixed (class of) fuzzy implication are not suitable logical framework for SI method. The formal system LΠ [1, 5] contains three common implications, Lukasiewicz, product and Gödel implications. Many researchers have considered various methods of fuzzy reasoning including SI methods for these three implications [14, 20]. Thus in this paper, we consider the problem of formalizing the solutions for SI method based on LΠ.
The remainder of this paper is organized as follows. Section 2 provides some basic definitions and LΠ logic. Section 3 gives the predicate formal representation of the solutions for the SI algorithms based on LΠ logic and the strict logic proofs. We give our conclusions in Section 4.
LΠ logic [1, 5] is a combination of the Lukasiewicz and the product logics, which are two extensions of the basic logic BL introduced by Hájek in [7]. BL is based on two basic connectives & and → and one truth constant
A ∧ B = A & (A → B)
A ∨ B = ((A → B) → B) ∧ ((B → A) → A)
A ↔ B = (A → B) & (B → A)
BL consists of the deduction rule MP (modus ponens) and the following axioms: (A → B) → ((B → C) → (A → C)) (A & B) → A (A & B) → (B & A) A & (A → B) → B & (B → A) (A → (B → C)) → ((A & B) → C) ((A & B) → C) → (A → (B → C)) ((A → B) → C) → (((B → A) → C) → C)
The predicate version of the BL is built in [7], here are the logical axioms on quantifiers: (∀ x) A (x) → A (t), where t is substitutable for x in A; A (t) → (∃ x) A (x), where t is substitutable for x in A; (∀ x) (A → B) → (A → (∀ x) B), where x is not free in A; (∀ x) (A → B) → ((∃ x) A → B), where x is not free in B; (∀ x) (A ∨ B) → ((∀ x) A ∨ B), where x is not free in B.
A → A (A → (B → C)) → (B → (A → C)) (∀ x) A (x) → A (x) (∀ x) A (x) → (∃ x) A (x) A → (B → A & B) A → (B → A) (A → B) → (A & C → B & C) (B → C) → ((A → B) → (A → C)) A (x) → (∃ x) A (x) {A → B, B → C} ⊢ A → C.
BL can be extended to the Lukasiewicz and the product logics:
The LΠ logic [5] has one truth constant
The LΠ logic consists of the following axioms Axioms of the Łukasiewicz logic Axioms of the product logic Π without (BL7) ¬
P
A →
L
¬
L
A Δ (A →
L
B) ≡
L
(A →
P
B) A ⊙ (B ⊖ C) ≡
L
(A ⊙ B) ⊖ (A ⊙ C)
and the deduction rules are the modus ponens MP for Łukasiewicz implication and the necessitation of Δ (from A infer ΔA).
Cintula [2] defined a new deduction rule, denoted
The predicate version of the LΠ logic, denoted LΠ∀, is given by adding the following axiomatic schema: (∀ x) A (x) →
L
A (t), where t is substitutable for x in A; (∀ x) (A →
L
B) →
L
(A →
L
(∀ x) B), where x is not free in A;
and the inference rule generalization, denoted
Formalization of symmetric implicational algorithms
In this section, we formalize the SI algorithms of fuzzy reasoning. First, we introduce the following concepts.
⊢ (∀ x) (∀ y) ((A (x) → 1B (y)) → 2 (A* (x) → 1B* (y))); If C is any unary predicate with the type (s2) satisfying ⊢ (∀ x) (∀ y) ((A (x) → 1B (y)) → 2 (A* (x) → 1C (y))) , then ⊢ (∀ y) (B* (y) → 2C (y)).
Where →1, → 2 ∈ {→
L
, →
P
, →
G
}.
If D is any unary predicate with the type (s2) satisfying ⊢ (∀ x) (∀ y) ((A (x) → 1B (y)) → 2 (D (x) → 1B* (y))) , then ⊢ (∀ x) (D (x) → 2A* (x)).
Where →1, → 2 ∈ {→
L
, →
P
, →
G
}.
Formalization of SI algorithms for FMP
For the SI algorithm of the FMP problem, we can obtain the following results.
((A (x) →
P
B) ⊙ A* (x)) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x)) (∃1) (((A (x) →
P
B) ⊙ A* (x)) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x))) →
P
((A (x) →
P
B) →
P
(A* (x) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x)))) (BL5b) (A (x) →
P
B) →
P
(A* (x) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x))) (1°, 2°, MP) (A (x) →
P
B) →
L
(A* (x) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x))) (3°, ModusT) (∀ x) (∀ y) ((A (x) →
P
B) →
L
(A* (x) →
P
(∃ x) ((A (x) →
P
B) ⊙ A* (x)))) (4°, GEN) (∀ x) (∀ y) ((A (x) →
P
B (y)) →
L
(A* (x) →
P
C (y))) (Hypot) (A (x) →
P
B (y)) →
L
(A* (x) →
P
C (y)) (∀1) (A (x) →
P
B (y)) →
P
(A* (x) →
P
C (y)) (2°, ModusT) ((A (x) →
P
B (y)) →
P
(A* (x) →
P
C (y))) →
P
((A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y)) (BL5a) (A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y) (3°, 4°, MP) ((A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y)) →
P
(∀ x) ((A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y)) (∀1) (∀ x) ((A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y)) (5°, 6°, MP) (∀ x) ((A (x) →
P
B (y)) ⊙ A* (x) →
P
C (y)) →
P
(∃ x) ((A (x) →
P
B (y)) ⊙ A* (x)) →
P
C (y) (∃2) (∃ x) ((A (x) →
P
B (y)) ⊙ A* (x)) →
P
C (y) (7°, 8°, MP) B* (y) →
P
C (y) (9°, Abbr.) B* (y) →
L
C (y) (10°, ModusT) (∀ y) (B* (y) →
L
C (y)) (11°, GEN)
The following formula sequence is a proof of (SI2):
For the SI algorithm of the FMT problem, we can obtain the following results.
((A (x) →
P
B (y)) →
P
B* (y)) →
P
((A (x) →
P
B (y)) →
P
B* (y)) (T1)
((A (x) →
P
B (y)) →
P
(((A (x) →
P
B (y)) →
P
B* (y)) →
P
B* (y)) ) →
P
((A (x) →
P
B (y)) →
P
(((A (x) →
P
B (y)) →
P
B* (y)) →
P
B* (y)) ) (T2) (A (x) →
P
B (y)) →
P
(((A (x) →
P
B (y)) →
P
B* (y)) →
P
B* (y)) (1°, 2°, MP) (∀ v) ((A (x) →
P
B (v)) →
P
B* (v)) →
P
((A (x) B (y)) →
P
B* (y)) (T3)
((∀ v) ((A (x) →
P
B (v)) →
P
B* (v)) →
P
((A (x) B (y)) →
P
B* (y)) ) →
P
((((A (x) →
P
B (y)) →
P
B* (y)) →
P
B* (y)) →
P
((∀ v) ((A (x) →
P
B (v)) →
P
B* (v)) →
P
B* (y)) ) (BL1) (((A (x) →
P
B (y)) →
P
B* (y)) →
P
B* (y)) →
P
((∀ v) ((A (x) →
P
B (v)) →
P
B* (v)) →
P
B* (y)) (4°, 5°, MP) (A (x) →
P
B (y)) →
P
(A* (x) →
P
B* (y)) (3°, 4°, 6°, HS) (A (x) →
P
B (y)) →
L
(A* (x) →
P
B* (y)) (7°, ModusT) (∀ x) (∀ y) ((A (x) →
P
B (y)) →
L
(A* (x) →
P
B* (y))) (8°, GEN) (∀ x) (∀ y) ((A (x) →
P
B (y)) →
L
(D (x) →
P
B* (y))) (Hypot.) (A (x) →
P
B (y)) →
L
(D (x) →
P
B* (y)) (1°, T3, MP) (A (x) →
P
B (y)) →
P
(D (x) →
P
B* (y)) (2°, ModusT)
((A (x) →
P
B (y)) →
P
(D (x) →
P
B* (y)) ) →
P
(D (x) →
P
((A (x) →
P
B (y)) →
P
B* (y)) ) (T2) D (x) →
P
((A (x) →
P
B (y)) →
P
B* (y)) (3°, 4°, MP) (∀ y) (D (x) →
P
((A (x) →
P
B (y)) →
P
B* (y))) (5°, GEN) D (x) →
P
(∀ y) ((A (x) →
P
B (y)) →
P
B* (y)) (6°, ∀2, MP) D (x) →
P
A* (x) (7°, Abbr.) D (x) →
L
A* (x) (8°, ModusT) (∀ x) (D (x) →
L
A* (x)) (9°, GEN)
The following formula sequence is a proof of (SI3):
Similarly, we have the following results.
FSTI solution B* of FMP problem given by Theorem 3.1 is L-reductive.
FSTI solution B* of FMP problem given by Theorem 3.2 is L-reductive.
FSTI solution B* of FMP problem given by Theorem 3.3 is L-reductive.
FSTI solution A* of FMT problem given by Theorem 3.4 is L-reductive.
FSTI solution A* of FMT problem given by Theorem 3.5 is L-reductive.
FSTI solution A* of FMT problem given by Theorem 3.6 is L-reductive.
(A (x) →
P
B (y)) →
P
(A (x) →
P
B (y)) (T1)
((A (x) →
P
B (y)) →
P
(A (x) →
P
B (y)) ) →
P
((A (x) →
P
B (y)) ⊙ A (x) →
P
B (y) ) (BL5a) (A (x) →
P
B (y)) ⊙ A (x) →
P
B (y) (1°, 2°, MP) (∀ x) ((A (x) →
P
B (y)) ⊙ A (x) →
P
B (y)) (3°, GEN) (∀ x) ((A (x) →
P
B (y)) ⊙ A (x) →
P
B (y)) →
P
(∃ x) ((A (x) →
P
B (y)) ⊙ A (x) →
P
B (y)) (T4) (∃ x) ((A (x) →
P
B (y)) ⊙ A (x) →
P
B (y)) (4°, 5°, MP) B* (y) →
P
B (y) (6°, Abbr.) B* (y) →
L
B (y) (7°, ModusT) (∀ y) (B* (y) →
L
B (y)) (8°, GEN) A (x) →
P
(B (y) →
P
A (x) ⊙ B (y)) (T5) B (y) →
P
(A (x) →
P
B (y)) (T6)
(B (y) →
P
(A (x) →
P
B (y)) ) →
P
(A (x) ⊙ B (y) →
P
A (x) ⊙ (A (x) →
P
B (y)) ) (T7) A (x) ⊙ B (y) →
P
A (x) ⊙ (A (x) →
P
B (y)) (2°, 3°, MP)
(A (x) ⊙ B (y) →
P
A (x) ⊙ (A (x) →
P
B (y)) ) →
P
((B (y) →
P
A (x) ⊙ B (y)) →
P
(B (y) →
P
A (x) ⊙ (A (x) →
P
B (y))) ) (T8) (B (y) →
P
A (x) ⊙ B (y)) →
P
(B (y) →
P
A (x) ⊙ (A (x) →
P
B (y))) (4°, 5°, MP) A (x) →
P
(B (y) →
P
A (x) ⊙ (A (x) →
P
B (y))) (1°, 6°, HS) (A (x) →
P
B (y)) ⊙ A (x) →
P
(∃ x) ((A (x) →
P
B (y)) ⊙ A (x)) (T9) (B (y) →
P
A (x) ⊙ (A (x) →
P
B (y))) →
P
(B (y) →
P
(∃ x) ((A (x) →
P
B (y)) ⊙ A* (x)) (8°, T8, MP) A (x) →
P
(B (y) →
P
B* (y)) (1°, 6°, 9°, HS, Abbr.) (∀ x) (A (x) →
P
(B (y) →
P
B* (y))) (10°, GEN) (∀ x) (A (x) →
P
(B (y) →
P
B* (y))) →
P
(∃ x) A (x) →
P
(B (y) →
P
B* (y)) (T4) (∃ x) A (x) →
P
(B (y) →
P
B* (y)) (11°, 12°, MP) (∃ x) A (x) (Hypot.) B (y) →
P
B* (y) (13°, 14°, MP) B (y) →
L
B* (y) (15°, ModusT) (∀ y) (B (y) →
L
B* (y) (16°, GEN)
Then we prove ⊢ (∀ y) (B (y) →
L
B* (y)).
Based on the variety of TI method of fuzzy reasoning, SI method is an extension of TI method. Obviously, SI method is more flexible because two different implications are used. In this paper, we provided the predicate formal representation and logic proof of the solutions for SI method based on the LΠ logic, which handles three implication connectives, i.e., Łukasiewicz, product and Gödel implications. Moreover, we can formalize the consistency of the SI method in the logical systems LΠ∀. Thus, we have placed SI method for these implications in the framework of pure fuzzy logic and provided a sound logical foundation for SI method of fuzzy reasoning.
As we know, there are other logics that contain two different implication connectives, such as non-commutative fuzzy logics [3, 6]. Thus, it is interesting to put SI method of fuzzy reasoning into the framework of these fuzzy logics.
Footnotes
Acknowledgments
The work is supported by the Opening Foundation of Guangxi Colleges and Universities Key Laboratory of Complex System Optimization and Big Data Processing (Grant No.2017CSOBDP0103).
