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 [
In terms of Kripke models, S4F is captured by frames consisting of two clusters of points connecting by an accessibility relation: second
oor rst oor r2 r1
W2 W1 The points in each cluster, W1; W2, are re exive. 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 re exivity on points; so, while the basic picture is the same, some points in W1; W2 are now irre exive.
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 nite model property with respect to given semantics. In section 3 we give the characterization of nite 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. 2
Following Tarski's suggestion to treat modality as the derivative of the
topological space, Esakia [
syntax
language with an in nite set of propositional letters p; q; r:: and connectives _; ^; ; :,
The axioms are all classical tautologies plus the following axioms: > $ >, (p ^ q) $ p ^ p ! p ^ }(q ^ p ^ p,
q, :p) !
(q _ }q):
2.2
Kripke semantics The Kripke semantics for the modal logic wK4F is provided by one-step, weaktransitive Kripke frames. Below we give the de nition of these frames.
(8x; y; z)(xRy ^ yRz ^ x 6= z ) xRz): W
Of course every transitive relation is weakly-transitive also. Moreover it is not di cult to see that weakly-transitive relations di er from transitive ones just by the occurrence of irre exive points in clusters. As one can see, the frame in the picture is weakly transitive, but not transitive.
The picture represents the diagramatic view of kripke structure. Irre exive points are colored by grey and re exive points are uncolored. Arrows represent the relation between two distinct points. So as we can see yRx and xRy, but y 6 Ry, which contradicts transitivity, but not weak transitivity as y = y.
if the following two conditions are satis ed: x
y pic. 1 W
1)(8x; y; z)((xRy ^ yRz) ) (yRx _ zRy)), 2)(8x; y; z)((xRy ^ :(yRx) ^ xRz) ) (zRx _ (zRy _ yRz))).
As the reader can see the rst 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 gure on the right hand side, while the gures 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 e ect points on the bottom.
For the sake of completeness we will just brie y recall the main de nitions in modal logic, like: Kripke frame, satisfaction and validity of modal formulas.
If we additionally have a third component V : P rop W ! f0; 1g, 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 de ned inductively. We just state the base and modal cases here.
De nition 2.24 For a given kripke model M = (W; R; V ) the satisfaction of a formula at a point w 2 W is de ned inductively as follows: w p i V (p; w) = 1, the boolean cases are standard, w i (8v)(wRv ) v ).
Note: From the de nition of }, (} (9v)(wRv ^ v ). : : ) it follows that w } i
So far we de ned the modal logic wK4F syntactically and we gave the de nition 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.
step 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 [
Take an arbitrary, weakly-transitive, one-step frame (W; R). Take an arbitrary valuation V and assume at some point w 2 W that w p ^ }(q ^ :p). By the de nition of satisfaction this implies that w p and there exists w0 such that wRw0, w0 q and it is not the case that w0Rw as much as w0 :p. Now take an arbitrary v such that wRv. By the second condition in the de nition of one-step relation we have that either vRw or vRw0 ^ w0Rv. If v = w0 we immediately have that v q since w0 q. In case v 6= w0 we have two subcases vRw0 ^ w0Rv or vRw ^ wRv. In both cases by weak-transitivity of the relation R we have at least vRw0, which implies that v }q and hence w (q _ }q).
Proof. We do not give the details here as far as the proof uses standard
techniques given in [
We have seen that the class of nite, 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 nite, rooted, weakly-transitive and one-step Kripke frames and their bounded morphisms in terms of quadruples of natural numbers.
de ned as a set R(A) = Sfy : x 2 A&xRyg.
w 2 W such that the upper cone R(fwg) = W ; w is called the root of the frame. Note 1. The root is not necessarily unique. For example on the rst picture both x and y are roots.
Let N 4 be the set of all quadruples of natural numbers and let N 4 = N 4 f(n; m; 0; 0)jn; m 2 N g. The following theorem states that the set of nite, rooted, one-step, weakly-transitive frames can be viewed as the set N 4. Let K denote the class of all rooted, nite, one-step, weakly-transitive frames considered up to isomorphism.
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 de nition of "strict" height and width, but it should be clear from the intuitive explanation after the de nitions 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 di cult to verify that any such frame (W; R) is of the form (W1; W2), where W1 [ W2 = W , W1 \ W2 = ? and (8u 2 W1; 8v 2 W2)(uRv). Besides because of the weak-transitivity, we have that (8u; u0 2 W1)(u 6= u0 ) uRu0) and the same for every two points v; v0 2 W2. We will call W1 the rst oor and W2 the second oor of the frame (W; R). Pictorially any rooted, weak-transitive and one-step Kripke frame can be represented as in the picture below.
second
oor rst oor i2 r2 i1 r1
W2 W1 Note 2. It is possible that W1 or W2 is equal to ? i.e. the frame has only one oor. In this case we treat the only oor of the frame as the second oor.
Now let us describe how to construct the function from K to N 4. With every frame (W; R) 2 N 4 we associate the quadruple (i1; r1; i2; r2), where i1 is the number of irre exive points in W1, r1 is the number of re exive points in W1, i2 is the number of irre exive points in W2 and r2 is the number of re exive points in W2. We will call the quadruple (i1; r1; i2; r2) the characteriser of the frame (W; R). In case the frame (W; R) has only one oor, 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 de nes 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 nite, rooted, weakly-transitive, one-step Kripke frames (W; R) and (W 0; R0). That they are distinct in K means that they are non-isomorphic i.e. either jW j 6= jW 0j or R 6' R0. In the rst case it is immediate that Ch(W; R) 6= Ch(W 0; R0) since jW j = i1 + i2 + r1 + r2. In the second case we have three subcases:
1) jW1j 6= jW10j. In this subcase i1 + r1 6= i01 + r10 and hence Ch(W; R) 6= Ch(W 0; R0).
2) The number of re exive (irre exive) points in jW1j di ers from the number of re exive (irre exive) points in jW10j. In this subcase i1 6= i01 and again Ch(W; R) 6= Ch(W 0; R0).
3) The number of re exive (irre exive) points in jW2j di ers from the number of re exive (irre exive) points in jW20j. This case is analogous to the previous.
It is straightforward to see that if none of these cases above occur i.e. jW j = jW 0j, jW1j = jW10j, jfwjw 2 W1 ^ wRwgj = jfw0jw0 2 W10 ^ w0R0w0gj and jfwjw 2 W2 ^ wRwgj = jfw0jw0 2 W2 ^ w0R0w0gj then (W; R) is isomorphic to (W 0R0) and hence (W; R) = (W 0; R0) in K.
claim 2: Ch is surjective. Take any quadruple (i1; r1; i2; r2) 2 N 4. Let us show that the pre-image Ch 1((i1; r1; i2; r2)) is not empty. Take the frame (W; R) = (W1; W2), where jW1j = i1 + r1, jW2j = i2 + r2, W1 contains i1 irre exive and r1 re exive points and jW2j contains i2 irre exive and r2 re exive points. Then by the de nition of Ch, we have that Ch(W; R) = (i1; r1; i2; r2).
called a bounded morphism if the following two conditions are satis ed: (1) wRv ) f (w)R0f (v), (2) f (w)R0v0 ) (9v 2 W )(wRv ^ f (v) = v0):
The bijection given in theorem 3.09 can be extended to bounded morphisms. In the following theorems we characterise the bounded morphisms between two nite, rooted, weakly-transitive, one-step frames in terms of conditions on the quadruples of natural numbers. We split the proof into three di erent theorems to make it much more readable; besides each case is interesting on its own. In the rst theorem we will give the characterisation for frames with the characterisers (0; 0; i; r) i.e. for frames with only one oor, then we will give the characterisations for frames where one has two oors and the second is one oor frame and the third theorem will give the condition for frames where both have two oors. We will omit zeroes in the quadruple (0; 0; i; r) and just write it as (i; r). Theorem 3.011 The nite, rooted, weakly-transitive, one-step frame (W 0; R0) with the characteriser (i0; r0) is a bounded morphic image of the nite, rooted, weakly-transitive, one-step frame (W; R) with the characteriser (i; r) i the following conditions are satis ed: r0 = 0 ) (i; r) = (i0; r0), i i0, 2 (r0 r) i i0.
m = 0 Proof. For the left to right direction assume f : (W; R) (W 0; R0). This means that i + r i0 + r0, sincef is a surjection. First let us state some general observations which will help in proving the theorem.
for every irre exive point w0 2 W 0, we have that f 1(w0) is one irre exive point. Assume not. Then either f 1(w0) contains some re exive point w 2 W , or it contains at least two irre exive points u; v 2 W . In the rst case we have wRw but not f (w)R0f (w), so we obtain a contradiction. In the second case we have uRv ^ vRu but not f (v)R0f (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 satis ed.
case 1 Assume r0 = 0 but (i; r) 6= (i0; r0). So either r 6= 0 or i 6= i0. In both cases we get a contradiction by the above observation, as re exive points cannot be mapped to irre exive ones and also two irre exive points can not be mapped to one irre exive point.
case 2 Assume i < i0. Then there is at least one point v0 2 W 0 such that f 1(v0) = ?. The reason is that there are not enough irre exive points in W to cover all irre exive points in W 0. And we know (by above remarks) we cannot map re exive points to irre exive ones. So we get a contradiction.
case 3 Assume 2 (r0 r) > i i0. This means that r0 > r. So there are r0 r re exive points in W 0 with the pre-image not containing a re exive point. But then there is at least one re exive point w0 2 W 0 such that f 1(w0) contains less than 2 irre exive points. This is because by assumption there are not enough pairs of irre exive points in W for all re exive points with pre-image not containing re exive ones. But this gives a contradiction because either f is not surjective (in case f 1(w0) = ?) or f is not a bounded morphism (in case f 1(w0) = v with v irre exive).
Now let us prove the converse direction. Let us enumerate points in W in the following way: Let w1; :::wr be the re exive points and v1; :::vi irre exive points. Let us use the same enumeration for points in W 0 with the di erence that we add 0 to every point. So for example w10 is the re exive and v20 is the irre exive point in W 0. In case r0 = 0 we know that (i; r) = (i0; r0) and we can take f to be bijection mapping wi to w0.
i In case r0 6= 0 we distinguish two subcases. case 1 When r > r0. Let us de ne f : W ! W 0 in the following way: f (vj ) = vj0 for j 2 f1; ::; i01g, f (wj ) = wj0 for j 2 f1; ::; r10 1g, f (vi0+1) = f (vi0+2) = ::: = f (vi) = f (wr0+1) = :: = f (wr) = wr0.
case 2 When r r0. Let us de ne f : W ! W 0 in the following way: f (vj ) = vj0 for j 2 f1; ::; i0g, f (wj ) = wj0 for j 2 f1; ::; rg, f (vi0+2k 1) = f (vi0+2k) = wr0+k for k 2 f1; ::; r0 r f (vi0+2(r0 r) 1) = f (vi0+2(r0 r)) = :: = f (vi) = wr0. 1g,
In other words we send each re exive point wj 2 W to the re exive point wj0 2 W 0 and each irre exive point vj 2 W to the irre exive point vj0 2 W 0. Inasmuch as we have that i i0 and r r0, there may be left some irre exive points in W on which we have not yet de ned f and also some re exive points in W 0 which have no pre-image, so we associate to every pair of such irre exive points one re exive point which has no pre-image. We continue this process until we are left with only one re exive point without pre-image (we know this exists by the condition r0 6= 0) and associate to it all the remaining irre exive points on which f was not de ned. The condition 2 (r r0) i0 i guarantees that there are at least two such irre exive points left. It is easy to check that f de ned in the following way is indeed a bounded morphism.
Now let us consider the case, where the rst frame has two oors, while the second is a one oor frame. Note that the only di erence from the conditions in 3.011 is that we require that the second frame contains at least one re exive point. This is because we want to map all rst oor points of the rst frame to this particular re exive point.
Theorem 3.012 The nite, rooted, weakly-transitive, one-step frame (W 0; R0) with the characteriser (i0; r0) is a bounded morphic image of the nite, rooted, weak-transitive, one-step frame (W; R) with the characteriser (i1; r1; i2; r2), where i1 + r1 > 0 and i2 + r2 > 0 i the following conditions are satis ed: r0 6= 0; i2 i0, 2 (r0 r2) i2
i0.
Proof. Assume r0 = 0. This means that all points in (W 0; R0) are irre exive. Now as (W; R) has two oors we can represent it as a pair (W1; W2) where both sets are non-empty. This implies that there are at least two points u 2 W1 and v 2 W2, such that f (u) 2 W 0 and f (v) 2 W 0. Since (W 0; R0) is a cluster, we have that f (u)R0f (v) and f (v)R0f (u). But this contradicts the property that f is a bounded morphism. This is because not Ru while f (v)R0f (u) and as f (u) is irre exive there does not exist a point w 2 W , with u 6= w and f (w) = f (v) (see the rst observation in the proof of lemma 3.011).
Assume i2 < i0. Again by rst observation in the proof of lemma 3.011 we know that the pre-image of the irre exive point cannot be re exive. This means that there exists a point u0 2 W 0, such that, u0 is irre exive and f 1(u0) \ W2 = ?. Di erent from the analogous case in the proof of lemma 3.011 the possibility arises that some irre exive point u 2 W1 is mapped to the point u0. Let us show that this cannot happen. Assume u 2 W1 and f (u) = u0. As u is a rst oor point, there exists some v 2 W2 with uRv. As f is bounded morphism we have that f (u)R0f (v). As (W 0; R0) is a cluster we have that f (v)R0f (u) as well. Now we get a contradiction as there is no successor of v which is mapped to f (u) = u0.
Assume the third condition does not hold. This means that 2 (r0 r2) > i2 i0. In this case we have that there is at least one point u0 2 W 0 such that u0 is re exive and f 1(u0) \ W2 is either the empty set or it contains only one point u with u 6 Ru. This gives a contradiction, since u0R0u0 while there is no successor v of u with f (u) = u0.
For the converse direction we construct f : W W in the following way: fjW1 = v0, where v0 is an arbitrary re exive point in W 0 (we know that such a point exists from the rst condition of the lema). fjW2 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 oors.
Theorem 3.013 The nite, rooted, weakly-transitive, one step-frame (W 0; R0) with the characteriser (i01; r10; i02; r20), where i01 + r10 > 0 and i02 + r20 > 0 is a bounded morphic image of the nite, rooted, weakly-transitive, one step-frame (W; R) with the characterisers (i1; r1; i2; r2), where i1 + r1 > 0 and i2 + r2 > 0 i the following hold: r10 = 0 ) (i1; r1) = (i01; r10), r20 = 0 ) (i2; r2) = (i02; r20), i1 i01, i2 i02, 2 (r10 r1) i1 i01, 2 (r20 r2) i2 i02.
m > n. m = 0 if Proof. The theorem follows from the previous theorem and the following observation:
If (W 0; R0) is a two oor frame i.e. i01 + r10 > 0 and i02 + r20 > 0 then (W; R) is also two oor frame. Assume not. Then there exist points w; v 2 W such that vRw and f (v) 6 R0f (w) as f (v) is a second oor point while f (w) is a rst oor point. points from the second oor cannot be mapped to points on the rst oor. For the contradiction assume that the point f (w) is a rst oor point while w is a second oor point. This means that there exists v0 2 W 0 such that f (w)R0v0 and not v0R0f (w). Then as f is a bounded morphism there exists v 2 W such that wRv and f (v) = v0. As w is a second oor point, wRv , vRw and we get a contradiction as we have vRw while not f (v)R0f (w).
points from the rst oor cannot be mapped to the points on the second oor. For the contradiction assume that the point f (w) is a second oor point while w is a rst oor point. Now either there is another point w1 2 W on the rst oor with f (w1) also on the rst oor or all points including w from the rst oor of W are mapped to the second oor of W 0. In the rst case wRw1 and not f (w)Rf (w1) 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 oor frames so there is at least one point on the rst oor in W 0 left with empty pre-image. This is because by above observation second oor points cannot be mapped to rst oor points.
The converse direction is proved just by repetition of the case for one oor frames for the other oor. 4
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, irre exive 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, irre exive 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.
re exive, weakly-transitive, nite, rooted, one-step Kripke frames and the class of all nite minimal topological spaces.
Proof. Assume (W; R) is a nite, rooted, weakly transitive and one step relational structure and besides R is irre exive. (Note that as the frame is irre exive its characteriser has the form (i1; 0; i2; 0), where i1 + i2 = jW j.) Let W1 be the rst oor and W2 the second oor of the frame, then the topology we construct is fW; ?; W2g. It is immediate that the space (W; R), where R = fW; ?; W2g, is a minimal topological space.
Let us show that the correspondence we described is injective. Take two arbitrary distinct irre exive, nite, rooted, weakly transitive frames (W; R) and (W 0; R0). As they are distinct, either W 6= W 0 or R 6= R0. In the rst case it is immediate that (W; R) 6= (W 0; R0 ). In the second case as both R and R0 are irre exive the second oors are not the same, so W2 6= W20 and hence R 6= R0 . For surjectivity take an arbitrary minimal topological space (W; ), where = fW; ?; W0g for some subset W0 W . Take the frame (W; R), where R = (W0 W0 f(w; w)jw 2 W0g)[( W0 W0 f(w; w)jw 2 W0g)[f(w; w0)jw 2
W0; w0 2 W0g. In words every two distinct points are related in W0 by R and the same in the complement W0 = W W0, besides every point from the W0 is related to every point from W0. what we get is the rooted two step relation which is weakly transitive, with the second oor equal to W0. As we didn't allow wRw for any point w 2 W , the relation R is also irre exive.
Now we will give the de nition of a derived set (or set of accumulation points) of a set in a topological space. This de nition is needed to give the semantics of modal formulas in arbitrary topological spaces.
say that w 2 W is an accumulation point of A if for every neighborhood Uw of w the following holds: Uw \ A fwg 6= ?. The set of all accumulation points of
Derived sets serve to give the semantics of the diamond modality in an arbitrary topological space. Below we give the de nition of satisfaction in a derived set topological semantics of modal logic.
De nition 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 2 W is de ned by: w
w }p i p i
w 2 V (p); w 2 der(V (p)); boolean cases are standard. Validity in a frame and class of frames of a formula is de ned in a standard way.
let (W; R) be its Allexandrof space. For every modal formula the following holds: (W; R) i (W; R) .
the class of all minimal topological spaces.
Proof. Proof. Soundness can be checked directly so we do not prove it here. For completeness assume 0 . By theorem 2.26 there exists a nite, one-step, weaktransitive frame (W; R) which falsi es . Assume that Ch(W; R) = (i1; r1; i2; r2).
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.