We introduce and study a modal logic wK4F which is closely related to the logic S4F that is important in the context of epistemic logics for representing and reasoning about an agent's knowledge. It is obtained by adding the axiom F to the modal logic wK4, or dropping from S4F the T axiom. We show that wK4F is sound and complete with respect to the class of all minimal topological spaces i.e. topological spaces with only three open sets. We characterize the rooted frames of the logic wK4F by quadruples of natural numbers and in the same fashion we give a characterization of p-morphic images of rooted wK4F frames.
In epistemic logic and formalisms for representing an agent's knowledge, the paradigm of minimal knowledge has played an important role [1]. S4F is a reflexive normal modal logic first introduced and studied by Segerberg [2]. Later its importance for knowledge representation and reasoning was discovered by Truszczynski [3] and Schwarz and Truszczynski [4] who used it to investigate the idea of minimal knowledge. They showed that the nonmonotonic version of the logic S4F captures, under some intuitive encodings, several important approaches to knowledge representation and reasoning. They include disjunctive logic programming under answer set semantics [5], (disjunctive) default logic [6]; [7], the logic of grounded knowledge [8], the logic of minimal belief and negation as failure [10] and the logic of minimal knowledge and belief [4]. Recently, Truszczynski [11] and Cabalar [12] have revived the study of S4F in the context of a general approach to default reasoning.
In terms of Kripke models, S4F is captured by frames consisting of two clusters of points connecting by an accessibility relation: The points in each cluster, W 1 , W 2 , are reflexive. In this paper we study a logic closely related to S4F , called wK4F . It is obtained by dropping from S4F the T axiom and therefore the condition of reflexivity on points; so, while the basic picture is the same, some points in W 1 , W 2 are now irreflexive.
Since S4F and wK4F are closely related, many results about the latter can be transferred to the former. In this paper we examine wK4F , prove a completeness theorem and show that there is a close relation between wK4F and the class of minimal topological spaces. We leave for future work the study of the non-monotonic variant of wK4F as well as multi-modal versions that may be used to represent common knowledge. However we point out that by a standard translation technique there is a natural embedding of wK4F into S4F . The embedding is obtained by so called splitting translation the main clause of which is given by Sp( φ) = φ ∧ φ.
The paper is organized in the following way. In section 2 we present the syntax and kripke semantics of the modal logic wK4F . We prove the completeness and finite model property with respect to given semantics. In section 3 we give the characterization of finite one-step, weak-transitive frames and their bounded morphisms in terms of quadruples of natural numbers. In section 4 we prove the main theorem of the paper, which states that wK4F is the complete and sound logic of all minimal topological spaces. The last section gives the conclusion and questions for future work.
Following Tarski's suggestion to treat modality as the derivative of the topological space, Esakia [13] introduced the modal logic wK4 as the modal logic of all topological spaces, with the desired (derivative operator) interpretation of the modal ♦. The modal logic wK4F is a normal modal logic obtained by adding the axiom weak-F to the modal logic wK4. wK4F is a weaker logic then S4F discussed in Segerberg [2]. In particular we get the modal logic S4F by adding axiom T to the logic wK4F . Thus in this sense wK4F is of interest for S4F also as some results are easily carried over and simplified from one to another.
Definition 2.11 The normal modal logic wK4F is defined in a standard modal language with an infinite set of propositional letters p, q, r.. and connectives ∨, ∧, , ¬,
• The axioms are all classical tautologies plus the following axioms:
• The rules of inference are: Modus ponens, Substitution and Necessitation.
The Kripke semantics for the modal logic wK4F is provided by one-step, weaktransitive Kripke frames. Below we give the definition of these frames.
Of course every transitive relation is weakly-transitive also. Moreover it is not difficult to see that weakly-transitive relations differ from transitive ones just by the occurrence of irreflexive points in clusters. As one can see, the frame in the picture is weakly transitive, but not transitive.
x y pic. 1
The picture represents the diagramatic view of kripke structure. As the reader can see the first condition restricts the "strict" height of the frame to two. Where informally by "strict" we mean that the steps are not counted within a cluster. So for example we cannot have the situation on the left hand side of the picture below, while we can have the situations in the middle and on the right hand side.
The second condition is more complicated. Nevertheless it is not too hard to verify that it restricts the "strict" width of the frame to one. So again we cannot have for example the figure on the right hand side, while the figures in the middle and on the left are allowed. Here we cheat slightly as indeed the frame is not allowed to fork as in the picture on the right, but condition 2) does not restrict the reversed fork i.e. frame with two points on the bottom and one on the top. So strict width does not effect points on the bottom.
For the sake of completeness we will just briefly recall the main definitions in modal logic, like: Kripke frame, satisfaction and validity of modal formulas. Definition 2.23 The pair (W, R), with W an arbitrary set (set of possible worlds) and R ⊆ W × W is called a Kripke frame.
If we additionally have a third component V : P rop × W → {0, 1}, then we say that we have a Kripke model M = (W, R, V ) (where P rop denotes the set of all propositional letters).
The satisfaction and validity of a modal formula are defined inductively. We just state the base and modal cases here. Definition 2.24 For a given kripke model M = (W, R, V ) the satisfaction of a formula at a point w ∈ W is defined inductively as follows: w p iff V (p, w) = 1, the boolean cases are standard, w φ iff (∀v)(wRv ⇒ v φ).
Note: From the definition of ♦, (♦φ ≡ ¬ ¬φ) it follows that w ♦φ iff (∃v)(wRv ∧ v φ).
So far we defined the modal logic wK4F syntactically and we gave the definition of one-step and weakly-transitive Kripke frames. The following two propositions link these two things. The proof uses standard modal logic completeness techniques, so we will not enter into all the details.
The modal logic wK4F is sound w.r.t. the class of all onestep and weakly-transitive Kripke frames.
Proof. We give the proof only for the fourth axiom of the modal logic wK4F . The proofs for other axioms are analogous. The reader may also consult [13].
Take an arbitrary, weakly-transitive, one-step frame (W, R). Take an arbitrary valuation V and assume at some point w ∈ W that w p ∧ ♦(q ∧ ¬p). By the definition of satisfaction this implies that w p and there exists w such that wRw , w q and it is not the case that w Rw as much as w ¬p. Now take an arbitrary v such that wRv. By the second condition in the definition of one-step relation we have that either vRw or vRw ∧ w Rv. If v = w we immediately have that v q since w q. In case v = w we have two subcases vRw ∧ w Rv or vRw ∧ wRv. In both cases by weak-transitivity of the relation R we have at least vRw , which implies that v ♦q and hence w (q ∨ ♦q).
The modal logic wK4F is complete w.r.t. the class of all finite, one-step and weakly-transitive Kripke frames.
Proof. We do not give the details here as far as the proof uses standard techniques given in [13]. First we take the canonical model for wK4F and then apply the minimal filtration to it.
3 The class of finite, rooted, weakly-transitive and one-step Kripke frames and their bounded morphisms.
We have seen that the class of finite, weakly-transitive and one-step Kripke frames fully captures the modal logic wK4F . This class can be reduced to a smaller class of frames which are rooted. In this section we characterise finite, rooted, weakly-transitive and one-step Kripke frames and their bounded morphisms in terms of quadruples of natural numbers.
Definition 3.08 A Kripke frame (W, R) is called rooted if there exists a point w ∈ W such that the upper cone R({w}) = W ; w is called the root of the frame.
Note 1. The root is not necessarily unique. For example on the first picture both x and y are roots.
Let N 4 be the set of all quadruples of natural numbers and let
The following theorem states that the set of finite, rooted, one-step, weakly-transitive frames can be viewed as the set N 4 . Let K denote the class of all rooted, finite, one-step, weakly-transitive frames considered up to isomorphism. Theorem 3.09 There is a one-to-one correspondence between the set K and the set N 4 .
Proof. We know that any one-step frame has "strict" width one and "strict" height less than or equal to two (We didn't give the formal definition of "strict" height and width, but it should be clear from the intuitive explanation after the definitions 2. 22 and 2.21 what we mean by this). If additionally we have that the frame is rooted, the case where width is greater than one at the bottom is also restricted. It is not difficult to verify that any such frame (W, R) is of the form (W 1 , W 2 ), where
Besides because of the weak-transitivity, we have that (∀u, u ∈ W 1 )(u = u ⇒ uRu ) and the same for every two points v, v ∈ W 2 . We will call W 1 the first floor and W 2 the second floor of the frame (W, R). Pictorially any rooted, weak-transitive and one-step Kripke frame can be represented as in the picture below.
the frame has only one floor. In this case we treat the only floor of the frame as the second floor. Now let us describe how to construct the function from K to N 4 . With every frame (W, R) ∈ N 4 we associate the quadruple (i 1 , r 1 , i 2 , r 2 ), where i 1 is the number of irreflexive points in W 1 , r 1 is the number of reflexive points in W 1 , i 2 is the number of irreflexive points in W 2 and r 2 is the number of reflexive points in W 2 . We will call the quadruple (i 1 , r 1 , i 2 , r 2 ) the characteriser of the frame (W, R). In case the frame (W, R) has only one floor, by note 2 above it is treated as the frame (∅, W ). Hence it's characteriser has the form (0, 0, i, r). Now it is clear that the correspondence described above defines a function from the set K to the set N 4 . Let us denote this function by Ch.
claim 1: Ch is injective. Take any two distinct finite, rooted, weakly-transitive, one-step Kripke frames (W, R) and (W , R ). That they are distinct in K means that they are non-isomorphic i.e. either
In the second case we have three subcases:
1)
2) The number of reflexive (irreflexive) points in |W 1 | differs from the number of reflexive (irreflexive) points in |W 1 |. In this subcase i 1 = i 1 and again Ch(W, R) = Ch(W , R ).
3) The number of reflexive (irreflexive) points in |W 2 | differs from the number of reflexive (irreflexive) points in |W 2 |. This case is analogous to the previous.
It is straightforward to see that if none of these cases above occur i.e.
claim 2: Ch is surjective. Take any quadruple (i 1 , r 1 , i 2 , r 2 ) ∈ N 4 . Let us show that the pre-image Ch −1 ((i 1 , r 1 , i 2 , r 2 )) is not empty. Take the frame (W, R) = (W 1 , W 2 ), where
and r 1 reflexive points and |W 2 | contains i 2 irreflexive and r 2 reflexive points. Then by the definition of Ch, we have that Ch(W, R) = (i 1 , r 1 , i 2 , r 2 ). Definition 3.010 The function f between two frames (W, R) and (W , R ) is called a bounded morphism if the following two conditions are satisfied:
The bijection given in theorem 3.09 can be extended to bounded morphisms. In the following theorems we characterise the bounded morphisms between two finite, rooted, weakly-transitive, one-step frames in terms of conditions on the quadruples of natural numbers. We split the proof into three different theorems to make it much more readable; besides each case is interesting on its own. In the first theorem we will give the characterisation for frames with the characterisers (0, 0, i, r) i.e. for frames with only one floor, then we will give the characterisations for frames where one has two floors and the second is one floor frame and the third theorem will give the condition for frames where both have two floors. We will omit zeroes in the quadruple (0, 0, i, r) and just write it as (i, r). Theorem 3.011 The finite, rooted, weakly-transitive, one-step frame (W , R ) with the characteriser (i , r ) is a bounded morphic image of the finite, rooted, weakly-transitive, one-step frame (W, R) with the characteriser (i, r) iff the following conditions are satisfied:
Note that the operation minus is defined within the natural numbers i.e. n−m = 0 if m > n.
Proof. For the left to right direction assume f : (W, R) (W , R ). This means that i + r ≥ i + r , sincef is a surjection. First let us state some general observations which will help in proving the theorem.
• for every irreflexive point w ∈ W , we have that f −1 (w ) is one irreflexive point. Assume not. Then either f −1 (w ) contains some reflexive point w ∈ W , or it contains at least two irreflexive points u, v ∈ W . In the first case we have wRw but not f (w)R f (w), so we obtain a contradiction. In the second case we have uRv ∧ vRu but not f (v)R f (u) and again this contradicts f being a bounded morphism. Now we are ready to begin the proof of the theorem. Let us check that all conditions are satisfied.
case 1 Assume r = 0 but (i, r) = (i , r ). So either r = 0 or i = i . In both cases we get a contradiction by the above observation, as reflexive points cannot be mapped to irreflexive ones and also two irreflexive points can not be mapped to one irreflexive point. case 2 Assume i < i . Then there is at least one point v ∈ W such that f −1 (v ) = ∅. The reason is that there are not enough irreflexive points in W to cover all irreflexive points in W . And we know (by above remarks) we cannot map reflexive points to irreflexive ones. So we get a contradiction. case 3 Assume 2 × (r − r) > i − i . This means that r > r. So there are r − r reflexive points in W with the pre-image not containing a reflexive point. But then there is at least one reflexive point w ∈ W such that f −1 (w ) contains less than 2 irreflexive points. This is because by assumption there are not enough pairs of irreflexive points in W for all reflexive points with pre-image not containing reflexive ones. But this gives a contradiction because either f is not surjective (in case f −1 (w ) = ∅) or f is not a bounded morphism (in case f −1 (w ) = v with v irreflexive). Now let us prove the converse direction. Let us enumerate points in W in the following way: Let w 1 , ...w r be the reflexive points and v 1 , ...v i irreflexive points. Let us use the same enumeration for points in W with the difference that we add to every point. So for example w 1 is the reflexive and v 2 is the irreflexive point in W . In case r = 0 we know that (i, r) = (i , r ) and we can take f to be bijection mapping w i to w i .
In case r = 0 we distinguish two subcases. case 1 When r > r . Let us define f : W → W in the following way:
case 2 When r ≤ r . Let us define f : W → W in the following way:
In other words we send each reflexive point w j ∈ W to the reflexive point w j ∈ W and each irreflexive point v j ∈ W to the irreflexive point v j ∈ W . Inasmuch as we have that i ≥ i and r ≤ r , there may be left some irreflexive points in W on which we have not yet defined f and also some reflexive points in W which have no pre-image, so we associate to every pair of such irreflexive points one reflexive point which has no pre-image. We continue this process until we are left with only one reflexive point without pre-image (we know this exists by the condition r = 0) and associate to it all the remaining irreflexive points on which f was not defined. The condition 2 × (r − r ) ≤ i − i guarantees that there are at least two such irreflexive points left. It is easy to check that f defined in the following way is indeed a bounded morphism. Now let us consider the case, where the first frame has two floors, while the second is a one floor frame. Note that the only difference from the conditions in 3.011 is that we require that the second frame contains at least one reflexive point. This is because we want to map all first floor points of the first frame to this particular reflexive point. Theorem 3.012 The finite, rooted, weakly-transitive, one-step frame (W , R ) with the characteriser (i , r ) is a bounded morphic image of the finite, rooted, weak-transitive, one-step frame (W, R) with the characteriser (i 1 , r 1 , i 2 , r 2 ), where i 1 + r 1 > 0 and i 2 + r 2 > 0 iff the following conditions are satisfied:
Proof. Assume r = 0. This means that all points in (W , R ) are irreflexive. Now as (W, R) has two floors we can represent it as a pair (W 1 , W 2 ) where both sets are non-empty. This implies that there are at least two points u ∈ W 1 and v ∈ W 2 , such that f (u) ∈ W and f (v) ∈ W . Since (W , R ) is a cluster, we have that f (u)R f (v) and f (v)R f (u). But this contradicts the property that f is a bounded morphism. This is because not Ru while f (v)R f (u) and as f (u) is irreflexive there does not exist a point w ∈ W , with u = w and f (w) = f (v) (see the first observation in the proof of lemma 3.011).
Assume i 2 < i . Again by first observation in the proof of lemma 3.011 we know that the pre-image of the irreflexive point cannot be reflexive. This means that there exists a point u ∈ W , such that, u is irreflexive and f −1 (u ) ∩ W 2 = ∅. Different from the analogous case in the proof of lemma 3.011 the possibility arises that some irreflexive point u ∈ W 1 is mapped to the point u . Let us show that this cannot happen. Assume u ∈ W 1 and f (u) = u . As u is a first floor point, there exists some v ∈ W 2 with uRv. As f is bounded morphism we have that f (u)R f (v). As (W , R ) is a cluster we have that f (v)R f (u) as well. Now we get a contradiction as there is no successor of v which is mapped to f (u) = u .
Assume the third does not hold. This means that 2 × (r − r 2 ) > i 2 − i . In this case we have that there is at least one point u ∈ W such that u is reflexive and f −1 (u ) ∩ W 2 is either the empty set or it contains only one point u with u Ru. This gives a contradiction, since u R u while there is no successor v of u with f (u) = u .
For the converse direction we construct f : W W in the following way: f |W1 = v , where v is an arbitrary reflexive point in W (we know that such a point exists from the first condition of the lema). f |W2 is constructed in exact analogy with the construction in 3.011.
And at last we can give the characterisation for the case where both frames have two floors. Theorem 3.013 The finite, rooted, weakly-transitive, one step-frame (W , R ) with the characteriser (i 1 , r 1 , i 2 , r 2 ), where i 1 + r 1 > 0 and i 2 + r 2 > 0 is a bounded morphic image of the finite, rooted, weakly-transitive, one step-frame (W, R) with the characterisers (i 1 , r 1 , i 2 , r 2 ), where i 1 + r 1 > 0 and i 2 + r 2 > 0 iff the following hold:
The operation minus is defined within the natural numbers i.e. n − m = 0 if m > n.
Proof. The theorem follows from the previous theorem and the following observation:
• If (W , R ) is a two floor frame i.e. i 1 + r 1 > 0 and i 2 + r 2 > 0 then (W, R) is also two floor frame. Assume not. Then there exist points w, v ∈ W such that vRw and f (v) R f (w) as f (v) is a second floor point while f (w) is a first floor point.
• points from the second floor cannot be mapped to points on the first floor. For the contradiction assume that the point f (w) is a first floor point while w is a second floor point. This means that there exists v ∈ W such that f (w)R v and not v R f (w). Then as f is a bounded morphism there exists v ∈ W such that wRv and f (v) = v . As w is a second floor point, wRv ⇔ vRw and we get a contradiction as we have vRw while not f (v)R f (w).
• points from the first floor cannot be mapped to the points on the second floor. For the contradiction assume that the point f (w) is a second floor point while w is a first floor point. Now either there is another point w 1 ∈ W on the first floor with f (w 1 ) also on the first floor or all points including w from the first floor of W are mapped to the second floor of W . In the first case wRw 1 and not f (w)Rf (w 1 ) so we get a contradiction. In the second case we get that f is not surjective inasmuch as both frames were supposed to be two floor frames so there is at least one point on the first floor in W left with empty pre-image. This is because by above observation second floor points cannot be mapped to first floor points.
The converse direction is proved just by repetition of the case for one floor frames for the other floor.
In this section we show that that the modal logic wK4F is the modal logic of minimal topological spaces. A topological space is minimal if it has only three open sets. It is well known that there is a bijection between Alexandrof spaces and weakly transitive, irreflexive Kripke frames. It is also well known that this bijection preserves modal formulas. In this section we show that the special case of this correspondence for minimal topological spaces gives one step, irreflexive and weakly transitive relations as a counterpart. As a corollary it follows that the logic wK4F is sound and complete w.r.t. the class of minimal topological spaces.
Theorem 4.014 There is a one-to-one correspondence between the class of irreflexive, weakly-transitive, finite, rooted, one-step Kripke frames and the class of all finite minimal topological spaces.
Proof. Assume (W, R) is a finite, rooted, weakly transitive and one step relational structure and besides R is irreflexive. (Note that as the frame is irreflexive its characteriser has the form (i 1 , 0, i 2 , 0), where i 1 + i 2 = |W |.) Let W 1 be the first floor and W 2 the second floor of the frame, then the topology we construct is {W, ∅, W 2 }. It is immediate that the space (W, Ω R ), where Ω R = {W, ∅, W 2 }, is a minimal topological space.
Let us show that the correspondence we described is injective. Take two arbitrary distinct irreflexive, finite, rooted, weakly transitive frames (W, R) and (W , R ). As they are distinct, either W = W or R = R . In the first case it is immediate that (W, Ω R ) = (W , Ω R ). In the second case as both R and R are irreflexive the second floors are not the same, so W 2 = W 2 and hence Ω R = Ω R .
For surjectivity take an arbitrary minimal topological space (W, Ω), where Ω = {W, ∅, W 0 } for some subset W 0 ⊆ W . Take the frame (W, R), where R = (W 0 ×W 0 −{(w, w)|w ∈ W 0 })∪(−W 0 ×−W 0 −{(w, w)|w ∈ −W 0 })∪{(w, w )|w ∈ −W 0 , w ∈ W 0 }. In words every two distinct points are related in W 0 by R and the same in the complement −W 0 = W − W 0 , besides every point from the −W 0 is related to every point from W 0 . what we get is the rooted two step relation which is weakly transitive, with the second floor equal to W 0 . As we didn't allow wRw for any point w ∈ W , the relation R is also irreflexive. Now we will give the definition of a derived set (or set of accumulation points) of a set in a topological space. This definition is needed to give the semantics of modal formulas in arbitrary topological spaces. Definition 4.015 Given a topological space (W, Ω) and a set A ⊆ W we will say that w ∈ W is an accumulation point of A if for every neighborhood U w of w the following holds: U w ∩ A − {w} = ∅. The set of all accumulation points of A will be denoted by der(A) and will be called the derived set of A.
Derived sets serve to give the semantics of the diamond modality in an arbitrary topological space. Below we give the definition of satisfaction in a derived set topological semantics of modal logic. Definition 4.016 A topological model (W, Ω, V ) is a triple, where (W, Ω) is a topological space and V : P rop → P (W ) is a valuation function. Satisfaction of a modal formula in a topological model (W, Ω, V ) at a point w ∈ W is defined by: w p iff w ∈ V (p), w ♦p iff w ∈ der(V (p)), boolean cases are standard. Validity in a frame and class of frames of a formula is defined in a standard way. Fact 4.017 Let (W, R) be a finite, weakly transitive and irreflexive frame and let (W, Ω R ) be its Allexandrof space. For every modal formula α the following holds:
Note that here on the left hand side denotes the validity in Kripke frames while on the right hand side it denotes the validity in topological frames in derived set semantics.
Theorem 4.018 The modal logic wK4F is sound and complete with respect to the class of all minimal topological spaces.
Proof. Proof. Soundness can be checked directly so we do not prove it here. For completeness assume φ. By theorem 2.26 there exists a finite, one-step, weaktransitive frame (W, R) which falsifies φ. Assume that Ch(W, R) = (i 1 , r 1 , i 2 , r 2 ).
By theorems 3.011, 3.012 and 3.013 there exists a one-step, weak-transitive frame (W , R ) such that R is irreflexive and (W, R) is p-morphic image of (W , R ). For example such a frame could be (W , R ) = Ch −1 (i 1 + 2 × r 1 , 0, i 2 + 2 × r 2 , 0). The surjection immediately yelds that (W , R ) φ. Now the result immediately follows from theorem 4.014, and the fact 4.017.
We have characterised the logic wK4F and established its relation to minimal topological spaces. The logic is closely related to the model logic S4F that has been shown to capture several important kinds of knowledge representation systems and, in its non-monotonic version, can be viewed as a logic of minimal knowledge. In future work we plan to study the non-monotonic version of wK4F and its relation to S4F in more detail. It may also be interesting to consider multi-model versions and their suitability for modeling common knowledge.