In the paper we introduce logical calculi for representation of propositions with modal operators indexed by fuzzy values. There calculi are called Heyting-valued modal logics. We introduce the concept of a Heyting-valued Kripke model and consider a semantics of Heyting-valued modal logics at the class of Heyting-valued Kripke models. The formalism of propositional modal logic and its proof technique is one of the most powerful approaches for knowledge representation and reasoning about dynamic systems, databases, etc. In the present paper we introduce more general modal propositional formalism, which allows to express propositions with modalities indexed by elements of a complete Heyting algebra. In this formalism any proposition A can be augmented with a modal operator of the form a, which can be interpreted, for example, as a value of necessity of A (or a value of con dence of A, or a value of plausibility of A, or a probability of A, or something else). This formalism can be considered as a logical foundation for { reasoning about objects that are incomplete and inconsistent, such as databases with incomplete and unclear information, { model checking for discrete models which are rough approximations of analyzed systems. Mathematical approaches to representation of knowledges with taking into account an uncertainty and incompleteness of knowledges were considered in several papers, in particular, in [3]{[13]. The most of them are related to quantitative evaluation of uncertainty. Uncertainty of information can appear by several causes.
But because the original system and its model are essentially not identical, then their properties can di er. Thus, for correct investigation of the system on the base of such model it is necessary to have an approach to evaluation the di erence between properties of a rough model and properties of original system. Values of the di erence can be not only quantitative, but also qualitative. For example, the set of such values can be a boolean algebra of subsets of some set of situations (i.e. states of an environment), in which the analyzed system does work. A value of equivalence between the system and its model (with respect to the properties under checking) can be de ned for example as a set of situations in which these properties are equivalent for the original system and for its model. A value of truth of the properties under checking can be de ned as a subset of this set, which consists of situations, in which the analysed properties does hold. These situations can be augmented by quantitative parameters (their weights, probabilities, etc.), and the set of such values can be more complex (if the sets of the parameters are totally ordered sets, then the set of values of truth is a Heyting algebra).
The main goal of the present paper is to construct a logical framework, which can serve as a logical foundation for representation of such uncertain information. The proposed formalism can be used also for design of speci cation languages of a behavior of dynamic systems with uncertain information about their structure and behavior, by analogy with the speci cation languages based on temporal logic for description of properties of program systems and electronic circuits ([2]). Some recent approaches to logic representation of propositions with fuzziness can be found in [16], [17].
The paper is organized as follows. In section 2 we introduce the syntax of Heyting-valued modal logics and de ne a minimal Heyting-valued modal logic HV K. In section 3 we introduce the concept of a Heyting-valued Kripke model and de ne the semantics of Heyting-valued modal formulas at the class of Heyting-valued Kripke models. We also consider an example of a Heytingvalued Kripke model related to description logics. In section 4 we introduce a concept of a canonical model of a Heyting-valued modal logic, and in section 5 we use the concept of a canonical model for the proof of completeness for minimal Heyting-valued modal logic HV K at the class of Heyting-valued Kripke models. In the conclusion we summarize the results of the paper and describe problems for future research. 2
2.1
We shall assume that a set of fuzzy values which can occur in formulas of Heytingvalued modal logics has some algebraic properties, namely, it is a complete Heyting algebra. In this section we remind a de nition of this concept.
A complete lattice is a partially ordered set H, such that for every subset H there are elements inf(Q) and sup(Q) of H such that for every b 2 H (8q 2 Q (8q 2 Q b q q) b) , , b
inf(Q); sup(Q) b:
The elements inf(H) and sup(H) will be denoted by the symbols 0 and 1 respectively.
For every nite subset the elements inf(Q) and sup(Q) will be denoted by the symbols respectively.
These elements will be denoted also by the symbols
Q = fa1; : : : ; ang
H a1 ^ : : : ^ an and
a1 _ : : : _ an and Below the symbol H denotes some xed complete Heyting algebra. For every a; b 2 H the symbol a $ b denotes the element a ! b . b ! a
One of the most important examples of a complete Heyting algebra is a set of n{tuples
f(a1; : : : ; an) j a1 2 M1; : : : ; an 2 Mng where M1; : : : ; Mn are complete totally ordered sets (for example, every Mi is a segment [0; 1]), and (a1; : : : ; an) (b1; : : : ; bn) i for every i = 1; : : : ; n ai bi. For every pair a = (a1; : : : ; an); b = (b1; : : : ; bn) a ! b = (c1; : : : ; cn); where ci = 1; if ai bi bi; otherwise
Let P V be a countable set, elements of which will be called propositional variables.
The set F m of Heyting-valued modal formulas (HVMFs) is de ned inductively as follows.
{ Every p 2 P V is a HVMF. { Every a 2 H is a HVMF. { If A and B are HVMFs, then the strings A ^ B, A _ B, and A ! B are
HVMFs. { If A is a HVMF, and a 2 H, then aA if a HVMF.
The symbols a are called Heyting-valued modal operators. A HVMF aA can be interpreted as the proposition
\the plausibility value of A is equal to a".
For every list A1; : : : ; An of HVMFs the strings
A1 ^ A2 ^ : : : ^ An and A1 _ A2 _ : : : _ An are the restricted notations of the HVMFs
A1 ^ (A2 ^ (: : : ^ An) : : :) and A1 _ (A2 _ (: : : _ An) : : :) respectively.
These HVMFs will be denoted also by the symbols and where p1; : : : ; pn are distinct variables, and A1; : : : ; An are HVMFs.
For every substitution (
Let A and B be HVMFs. We shall say that B is obtained from A by an equivalent transformation, if { there is a subformula of A of the form a ^ b; a _ b, or a ! b, where a; b 2 H, { B is a result of a substitution in A the corresponded element of H instead of this subformula.
We shall consider HVMFs A and B as equal (and write A = B) i the pair (A; B) belongs to the least equivalency relation generated by pairs of the form (C; D), where D can be obtained from C by an equivalent transformation.
Let A be a HVMF without modal operators, and the list of variables of A
has the form (p1; : : : ; pn): A is said to be a tautology, if (A) = 1 for every
substitution (
A Heyting-valued modal logic (HVML) is a set L of HVMFs such that { every tautology belongs to L, { for every A; B of HVMFs and every a 2 H a
A B $ aA aB 2 L; { for every a 2 H { for every HVMF A and every a 2 H { for every HVMFs A; B a ! a1
2 L; aA ! a 2 L; { for every HVMF A and every substitution { for every HVMFs A; B and every a; b 2 H if then B
2 L A 2 L and A ! B
2 L if
A 2 L then (A) 2 L if
a ! (A ! B) 2 L
then a ! ( bA !
bB) 2 L
(
This de nition implies that there is a minimal (with respect to the inclusion) HVML, which we shall denote by the symbol HV K.
It is not so di cult that the inference rule is admissible for every HVML.
For every HVMF A and every HVML L the symbol
denotes a supremum of the set
This de nition and (
Remind ([1]) that a Heyting{valued set (HS) (over a complete Heyting algebra H) is a pair
W = (X; )
{ X is a set (which is called a support of W ), and
{ is a mapping of the form
if
8x; y; z 2 X
(x; y) = (y; x)
(x; y)
(y; z)
(x; z)
3
3.1
where
(
For example, let { X be a set of humans, { fa1; : : : ; ang be a list of some their characteristics (age, sex, salary, reputation, health, etc.), { M1; : : : ; Mn are complete totally ordered sets of similarity values related to the characteristics a1; : : : ; an respectively, { a Heyting algebra H has the form
M1 : : :
Mn
We can consider X as a Heyting{valued set over (
For every x 2 X the element (x; x) is called a membership value of x at
the HS (
Let W = (X; ) be a HS. A Heyting{valued binary relation (HR) on W is a mapping R of the form R : X X ! H, such that 8x; y; x0; y0 2 X 8 R(x; y) 9 < (x; x0) = : (y; y0) ; { for every HS W its support will be denoted by the same symbol W , { for every pair of elements of the support the similarity value between x and y will be denoted by the symbol W (x; y), and { for every x 2 W the membership value of x at the HS W will be denoted by the symbol W (x). (21) (22)
M = (W; fRa j a 2 Hg; ) where { W is a HS, elements of which are called objects (or worlds), { fRa j a 2 Hg is a H{tuple of HRs on W , which are called transition relations, { is a mapping of the form
: P V ! Sub(W ) which is called an evaluation of variables. 3.3
For every HVMF A and every HVKM (21) an evaluation of A at M is the mapping
[[A]]M : W ! H; which maps every x 2 W to the element [[A]]x 2 H, which is de ned as follows: { if A = p 2 P V , then [[A]]x d=ef (p)(x); { if A = a 2 H, then [[A]]x d=ef aW (x) ; { if A = B ^ C, then [[A]]x d=ef [[B]]x ^ [[C]]x; { if A = B _ C, then [[A]]x d=ef [[B]]x _ [[C]]x; { if A = B ! C, then [[A]]x d=ef [W[B(]]xx)! [[C]]x ; { if A =
8 a 9 aB, then [[A]]x d=ef <> inf (Ra(x; y) ! [[B]]y) = : > y2W >: W (x) ;>
It is not so di cult to prove that [[A]]M is a HSS of the HS W . 3.4
In this section we give an example of a HVKM related to description logic ([14]).
Description Logic is a language for formal description of complex concepts on the base of atomic concepts and binary relations, called atomic roles. Assume that there are given { a set I of individuals, { a set C of atomic concepts, and every atomic concept c 2 C represents a subset [[c]] I { a set R of atomic roles, and every atomic role r 2 R represents a binary relation [[r]] I I.
Description Logic allows to represent complex notions by concept terms, i.e. expressions that are built from atomic concepts and atomic roles with use of the concept constructors: { boolean operations (conjunction (u), etc.), and { quanti er operations of the form 8r, where r 2 R.
Every concept term represents a subset [[t]] as follows: { [[t1 u t2]] d=ef [[t1]] \ [[t2]], { [[8r:t]] d=ef fa 2 I j for every b 2 I
For example (the example is borrowed from [15]), if (a; b) 2 [[r]] ) b 2 [[t]]g.
I, which is de ned by induction { I consists of all humans, { the atomic concept Woman is interpreted as the set of all women, and { the atomic role child is interpreted as the set of all pairs (a; b) of humans, such that b is a child of a then the concept of all women having only daughters can be represented by the concept term
Woman u 8child:Woman Let R be the set of all nite sequences of elements of R.
Every sequence r = (r1; : : : ; rn) 2 R represents a binary relation [[r]] d=ef [[r1]] : : : [[rn]]
I
I Elements of R can be interpreted as derivative roles, and will be referred brie y as roles.
Let H be the set P(R ) of all subsets of the set R . H is a complete Heyting algebra, because it is a complete boolean algebra.
We can consider the set I of humans as a Heyting-valued set (over H = P(R )), where for every pair (x; y) 2 I I the similarity value I(x; y) consists of all roles r 2 R such that x and y are equal with respect to r (we do not clarify the concepts of equality of humans with respect to a role, because it seems to be intuitively clear, but the precise de nition of this notion requires a strong linguistic foundation).
A HVKM related to this example has the following components. { Objects of this HVKM are humans, and similarity value between them was described above. { For every 2 H and every pair x; y of humans the set R (x; y) consists of all roles r 2 such that (x; y) 2 [[r]]. { The set PV is equal to the set C of atomic concepts, and for every c 2 C the evaluation is de ned as follows: for every human x 2 I
(c) : I ! P(R ) (c)(x) d=ef
I(x); if x 2 [[c]] ;; otherwise: 3.5
A HVMF A is said to be true at an object x of a HVKM (21), if [[A]]x = W (x): (23)
A HVMF A is said to be true at a HVKM (21), if A is true at every object of (21).
It is not so di cult to prove that every HVMF A 2 HV K is true at every
HVKM, because
{ every tautology is true at every HVKM,
{ HVMFs from (
Below we prove the inverse statement: if a HVMF A is true at every HVKM, then A 2 HV K.
4 4.1 4.2 Let (24) A HVML L is consistent, if for every a 2 H a 2 L ) a = 1.
It is not so di cult to prove that HV K is consistent.
Below every HVML under consideration is assumed to be consistent.
{ L be a consistent HVML, and { u be a set of HVMFs.
The set u is said to be L{consistent, if for { every nite subset of the set u, which has the form (where a1; : : : ; an 2 H; fa1 ! A1; : : : ; an ! Ang A1; : : : ; An are HVMFs, and For every pair u1; u2 of sets of HVMFs the inequality means that for every HVMF of the form a ! A 2 u1 a = 0 or 9 b
a : b ! A 2 u2:
Theorem 1. For every pair u1; u2 of sets of HVMFs the inequality (27) implies that u2 is L{consistent ) u1 is L{consistent: { every b 2 H the statement implies the inequality (25) (26) (27) (28) Theorem 2. Every consistent HVML is a L{consistent set.
Below the symbol L denotes some xed consistent HVML.
{ u be a L{consistent set, { A be a HVMF, and { Q be the set of all elements a 2 H such that
Then for every a 2 H u [ fa ! Ag
is L{consistent. a , a 2 Q:
The element sup(Q), which corresponds to A and u, will be denoted by the symbol
The de nition of the element [[A]]u implies that for every set u of HVMFs the following implication holds: u is L{consistent u [ f[[A]]u ! Ag [[A]]u: 4.4
Let x be a set of HVMFs.
The set x is said to be L{complete, if { x is L{consistent, and { for every HVMF A [[A]]x ! A 2 x: 4.5 Let
{ u be a L{consistent set, and { x be a L{complete set.
x is said to be a completion of u, if u
x Theorem 7. For every L{consistent set u there is its completion x. Below we shall assume that H satis es the additional condition: 8 a 2 H
(a ! 0) ! 0 = a: This condition is equivalent to the condition that H is a boolean algebra with respect to the operations ^; _; :, where 8a 2 H :a d=ef a ! 0: (30) (31) (32) (33) (34) (35) (36) (37)
A canonical model of a HVML L is a HVKM
ML d=ef (WL; fRL;a j a 2 Hg; L) the components of which are de ned as follows.
{ WL consists of all L{complete sets.
For every pair x; y 2 WL Note that this de nition implies that
WL(x; y) d=ef inf ([[A]]x $ [[A]]y)
A2F m 8x 2 WL
WL(x) = 1: { For every a 2 H
RL;a is a HR on WL, RL;a : WL
WL ! H, where 8x; y 2 WL RL;a(x; y) d=ef inf ([[ aA]]x ! [[A]]y)
A2F m 8x 2 WL
L(p)(x) d=ef [[p]]x: { L is a mapping of the form L : P V ! Sub(WL), where for every p 2 P V the HSS L(p) : WL ! H is de ned as follows:
It is not so di cult to prove that
{ WL satis es (
Theorem 8. For every HVMF A and every x 2 WL [[A]](x) = [[A]]x: 5
Theorem 9. If a HVMF A is true at every HVKM, then A 2 HV K.
Assume that A 62 HV K. Prove that A is not true at a certain object of the canonical model of HV K.
Note that the set f([[A]]HV K ! 0) ! (A ! 0)g (38) (39) (40) (41) (42) (44) (45) (46) (47) (48) (49) (50) is HV K{consistent, because for every b 2 H the statement implies the inequality Indeed, (44) implies that (A ! 0) ! b (b ! 0) ! A
2 HV K b ! 0 (42), (46) and (47) imply the inequality which is equivalent to the inequality [[A]]HV K ! 0
[[A]](x) ! 0 [[A]](x) Prove that A is not true at the object x.
If A is true at x, then (23) and (39) imply that (49) and (50) imply the equality [[A]]HV K = 1, which implies A 2 HV K.
This contradicts to the assumption that A 62 HV K. 6
In the paper we have introduced a new framework for representation of propositions which can contain fuzzy modalities. We have de ned the concept of a Heyting-valued modal logic and have proved the completeness theorem for the minimal Heyting-valued modal logic. The directions of further research related to the introduces concepts and results can be the following. 1. Prove the completeness theorem without the condition (a ! 0) ! 0 = a for every a 2 H. 2. Investigate the problems of nite model property and decidability of minimal
HVML. 3. De ne the concept of a Heyting-valued proof for rst-order logics, and introduce a Heyting-valued provability logics related to the concept of a Heytingvalued proof, investigate properties of Heyting-valued provability logics. 4. Design a speci cation language and model checking algorithms for Heytingvalued dynamic systems based on the proposed framework.