This paper introduces a novel monotonic modal logic, allowing us to capture the nonmonotonic variant of the modal logic S4F: we add a second new modal operator into the original language of S4F, and show that the resulting formalism is strong enough to characterise the logical consequence of (nonmonotonic) S4F, as well as its minimal model semantics. The latter underlies major forms of nonmonotonic logic, among which are (reflexive) autoepistemic logic, default logic, and nonmonotonic logic programming. The paper ends with a discussion of a general strategy, naturally embedding several nonmonotonic logics of a similar floor structure on which a (maximal) cluster sits.
The use of monotonic modal logics for describing nonmonotonic inference has a long
tradition in Artificial Intelligence. There exists a considerable amount of research in
the literature [
The modal logic S4F (aka, S4:3:2) is obtained from S4 by adding the axiom schema
F : (' ^ M L ) ! L (M ' _ )
[
S4F is characterised by the class of Kripke models (W; T ; V ) in which W = W1 [ W2 for some disjoint sets W1 and W2 such that W2 is nonempty. Moreover, xT y if and only if y 2 W2 or x 2 W1. V is the valuation function such that V (x) is a set of propositional ? I am grateful to Luis Farin˜as del Cerro, Andreas Herzig, and Levan Uridia for motivation, and the anonymous reviewers for their useful comments. This paper has been supported by the institution “Fundac¸a˜o para a Cieˆncia e a Tecnologia (FCT)”, and the research unit “Centro de Matema´tica, Aplicac¸o˜es Fundamentais e Investigac¸a˜o Operacional (CMAF-CIO)” of the University of Lisbon, Portugal via the grant, identified by the number “UID/MAT/04561/2013”. variables for every x 2 W. A cluster is simply a trivial S5 model (C; T ; V) such that xT y for every x; y 2 C. In terms of Kripke semantics, S5 is the modal logic, characterised by models in which the accessibility relation is an equivalence relation: it is reflexive, symmetric, and transitive. Now, we can alternatively identify an S4F model with the ordered triple (C1; C2; V) in which C1 and C2 are disjoint cluster structures, C2 , ;, and any world in C2 can be accessed from every world in C1.
This paper follows a similar approach to [
As a reference to the analogy between all such works, we here keep the same
symbols T and S1 with [
if and only if [T] tr(') ^ [S]:tr(') ! [T]tr( ) is valid in MLF :
The rest of the paper is organised as follows. Section 2 introduces the monotonic
modal logic MLF: we first define its bimodal language, and then propose two classes
of frames, namely K and F. They are respectively based on standard Kripke frames,
and the cluster-based component frames, which are in the form of a floor structure. We
axiomatise the validities of our logic, and finally prove that MLF is sound and complete
1 The symbols T and S of [
We here propose a new formalism called MLF, which is closely associated with S4F. 2.1
Throughout the paper we suppose P an infinite set of propositional variables, and P' its restriction to those of a formula '. We also consider Prop as the set of all propositional formulas of our language. The language L[T];[S] is formally defined by the grammar: ' F p j :' j ' ! ' j [T]' j [S]' and ' $ :[T]:' and :[S]:'. where p ranges over P. L[T];[S] is therefore a bimodal language with the modalities [T] and [S]. As usual, > d=ef ' ! ', ? d=ef :(' ! '), ' _ d=ef :' ! , ' ^ d=ef :(' ! : ), d=ef (' ! ) ^ ( ! '). Moreover, hTi' and hSi' respectively abbreviate 2.2
Kripke semantics for MLF
We now describe the class K of Kripke frames for MLF. A K-frame is a triple (W; T ; S):
– W is a non-empty set of possible worlds.
– T ; S W W are binary relations such that for every w; u; v 2 W,
(w; w) 2 T
(w; u) 2 T and (u; v) 2 T ) (w; v) 2 T
(w; u) 2 T ; (u; w) < T and (w; v) 2 T ) (v; u) 2 T
(w; u) 2 S ) (u; u) 2 S
(w; u) 2 S and (u; v) 2 S ) u = v
(w; u) 2 T ) (u; w) 2 T or (u; w) 2 S
(w; u) 2 S ) w = u or (u; w) 2 T
refl(T )
trans(T )
f(T )
refl2(S)
wtriv2(S)
msym(T ; S)
wmsym(S; T ):
The first three properties above characterise the frames of the modal logic S4F [
M; w j=MLF p M; w j=MLF :' M; w j=MLF ' ! M; w j=MLF [T]' M; w j=MLF [S]' if p 2 V(w); if if if if
M; w 6j=MLF '; M; w 6j=MLF ' or M; w j=MLF ; M; u j=MLF ' for every u such that wT u;
M; u j=MLF ' for every u such that wSu: We say that ' is MLF satisfiable if M; w j=MLF ' for some K-model M and w in M. Moreover, ' is MLF valid (for short, j=MLF ') if M; w j=MLF ' for every w of every Kmodel M. Then, ' is valid in M (M j=MLF ') when M; w j=MLF ' for every w in M. 2.3
Cluster-based floor semantics for MLF
We here define the frames of a floor structure for MLF, and call their class F. The
underlying idea is due to the property ‘f(T )’ of K-frames, and in fact, F is only a
subclass of K. However, F-frames with some additional properties play an important
role in the completeness proof. We now start with the definition of a T -cluster2 [
It follows from Definition 1 that the restriction of T to a T -cluster C (abbreviated T jC) is a universal relation, viz. T jC = C C. So, (C; T ) happens to be a trivial S5 frame.
Given a K-frame F = (W; T ; S), the relation T partitions F into disjoint subframes F 0 = (W0; T ; S) in which W0 = C1 [C2 for some maximal clusters C1; C2 W0 W such that C1 \C2 = ;, and C2 , ; is a final cone in W0. Thus, T jW0 = (W0 C2) [ (C1 C1). We now define the operators T ( ); S( ) : 2W ! 2W , respectively assigning to every X W, T (X) = fu 2 W : wT u for some w 2 Xg;
S(X) = fu 2 W : wSu for some w 2 Xg: When X=fwg, we simply write T (w) (resp. S(w)), denoting the set of all worlds that w can access via T (resp. S). Note that T ( ) and S( ) are homomorphisms under union:
T (X [ Y) = T (X) [ T (Y) and S(X [ Y) = S(X) [ S(Y): We now formally define the above-mentioned partitions of a K-frame w.r.t. T . Definition 2. Given a K-frame F = (W; T ; S), let C = (C1; C2) be a pair of disjoint subsets of W such that C2 , ;. Then, C is called a component of F if: 1. C1 and C2 are maximal clusters; 2 Unless specified otherwise, any definition of this paper is given w.r.t. the relation T . 2. T \ (C1
C2) = C1
So, a component C = (C1; C2) has a ‘two-layered’ structure: C1 is the first floor (‘F1cluster’), and C2 is the second floor (‘F2-cluster’). Clearly, C2 is the final cone of the structure C. Note that C can also be transformed into a special K-frame F C = C1 [ C2; (C1 [ C2) C2 [ (C1
C1); (C2 where C1 is the diagonal of C1 C1, i.e., C1 = f(w; w) : w 2 C1g. Given any two different components C = (C1; C2) and C0 = (C10; C0 ) of a K-frame F , C1 [ C2 and C10 [ C20 2 are disjoint, and C and C0 are disconnected in the sense that there is no T -access (nor an S-access) from one to the other. As a result, a K-frame F is composed of an arbitrary union of components; however, when F contains a component in which the F1-cluster is empty, and S , ; (and so, S is arbitrary), (1) is not su cient to recover F . This ambiguity in the transformation will be solved in the following section as the proposed logic MLF does not accept components whose F1-cluster is empty.
Definition 3. An F-frame is a pair C = (C1; C2), having a component structure.
We now define a function : F ! K, assigning a K-frame (C) = F C (see (1)) to each F-frame C. As two distinct components C and C0 give rise to two distinct K-frames F C and F C0 , is 1-1, but not onto3. Thus, F is indeed a (proper) subclass of K. Proposition 1. Given a K-frame F = (W; T ; S), let C = (C1; C2) be a component of F , and w 2 C1 [ C2, then 1. if w 2 C1, then T (w) = C1 [ C2, and S(w) = fwg; 2. if w 2 C2 , then T (w) = C2, and S(w) = C1 when C1 , ;; otherwise S(w) is arbitrary. The proof easily follows from the frame properties of K.
Corollary 1. For a K-frame F =(W; T ; S), and a component C=(C1; C2) of F , we have:
Corollary 2. Given a pointed K-frame Fw, let C = T (w)nC1 if w is in an F1-cluster C1; else if w is in an F2-cluster C2, let C = T (w). Take C0=S(C) nC. Then, CFw =(C0; C) 2 F. Note that the component generated by w 2 F is exactly the one in which w is placed. So, any point from the same component forms itself. Using Corollary 2, we now define another function , assigning to each pointed K-frame Fw an F-frame CFw . Clearly, is not 1-1, but is onto. Finally, f (Fw) : w 2 Wg identifies all the components in F . The following proposition generalises this observation.
Proposition 2. Given an F-frame C = (C1; C2) and w 2 C1 [C2, we have ( (C); w) = C. 3 Note that there is no F-frame being mapped to (i) a K-frame containing more than one component structure in it, and (ii) a K-frame composed of only one component with a single (nonempty) cluster structure in which S , ;.
These transformations between frame structures of MLF enable us to define valuations also on the components C 2 F, resulting in an alternative semantics for MLF via Fmodels. The new semantics can be viewed as a reformulation of the Kripke semantics: given a K-model M = (F C; V) for some Kripke frame F C 2 (F) and a valuation V, one can transform F C to a component (FwC) = C 2 F for some w 2 C1 [ C2 (see Proposition 2). This discussion allows us to define pairs (C; V) in which C 2 F, and V is the valuation restricted to C. Such valuated components are called ‘F-models’, and they make it possible to transfer K-satisfaction to F-satisfaction.
Truth conditions (the modal cases) for an F-model (C; V)=(C1; C2; V) and w 2 C1 [C2, (C; V); w j=MLF [T] if and only if – if w 2 C1 then (C; V); v j=MLF – if w 2 C2 then (C; V); v j=MLF for all v 2 C1 [ C2 (i.e., (C; V) j=MLF ); for all v 2 C2. (C; V); w j=MLF [S] – if w 2 C1 then (C; V); w j=MLF ; – if w 2 C2 then (C; V); v j=MLF for all v 2 C1 if C1 , ;; else ‘no strict conclusion’. The next result reveals the relation between the Kripke and the floor sematics of MLF.
L[T];[S], (C; V); w j=MLF ' if and only if (F C; V); w j=MLF '. 2.4
Axiomatisation of MLF
We here give an axiomatisation of MLF, and prove its completeness. Recall that K([T]),
T([T]), 4([T]) and F([T]) characterise the modal logic S4F [
Case (2): let (u; w) < T : Then, by the assumption (?), M; w j=MLF hTi[T] . Thus, there is v 2 W such that (w; v) 2 T and M; v j=MLF [T] . As M satisfies f(T ), we get (v; u) 2 T . As M; v j=MLF [T] , we have M; u j=MLF ; hence, M; u j=MLF hTi' _ . – Let F =(W; T ; S) be a K-frame in which f(T ) fails. So, there exists w; u; v 2 W with (u; w) < T while (w; u) 2 T and (w; v) 2 T ; yet (v; u) < T . Thanks to the last 2 claims, we have w,v (otherwise (v; u) < T would contradict (w; u) 2 T ). Due to the first 2 claims, w , u (otherwise, (w; u)=(u; w), and (u; w) 2 T ). We now take a valuation V satisfying: M; w j=MLF ' (N), but M; x 6j=MLF ' for any x , w; similarly, M; u 6j=MLF (H), but M; y j=MLF for every y , u. Since (v; u) < T , and thanks to the choice of V, M; v j=MLF [T] . As (w; v) 2 T , and also by using (N), we have M; w j=MLF ' ^ hTi[T] . On the other hand, M; u j=MLF [T]:' since (u; w) < T and w is the only point satisfying '. Then, (H) further implies that M; u j=MLF [T]:' ^ : .
Since (w; u) 2 T , we also get M; w j=MLF hTi([T]:' ^ : ). So, we are done. Corollary 3. MLF is sound w.r.t. the class K of frames.
Here, we only need to show that the inference rules of MLF are validity-preserving. Theorem 1. MLF is complete w.r.t. the class of K-frames.
Proof. We use the method of canonical models (see [
T c 0 if and only if f : [T] 2 g Sc 0 if and only if f : [S] 2 g 0; 0: – Vc is the valuation s.t. Vc( ) = \ P, for every 2 Wc.
By induction on ', we prove a truth lemma saying: “ j=MLF ' i ' 2 ” for every ' 2 L[T];[S]. Then, it remains to show that Mc satisfies all constraints of K, and so is a legal K-model of MLF. We here give the proof only for wtriv2(S) and wmsym(S; T ). I The schema WTriv2([S]) guarantees that Mc satisfies wtriv2(S): let 1Sc 2 (?) and 2Sc 3 (??). Assume for a contradiction that 2 , 3. Thus, there exists ' 2 2 with :' 2 3, implying that hSi:' 2 2 by the hypothesis (??). Since 2 is maximally consistent, ' ^ hSi:' 2 2. So, using the hypothesis (?), we get hSi(' ^ hSi:') 2 1. However, since 1 is maximally consistent, any instance of WTriv2([S]) is in 1. Thus, [S]('![S]') 2 1, and it contradicts the consistency of 1.
I The schema WMB([S]; [T]) ensures that wmsym(S; T ) holds in Mc: suppose that
Sc 0 (?) for ; 0 2 Wc. W.l.o.g., let , 0. Then, there exists 2 0 with : 2 . We need to show that 0T c . So, let ' be such that [T]' 2 0. As 0 is maximally consistent, we have both ' _ 2 0 and [T]' _ [T] 2 0. We know that [T]' _ [T] ! [T](' _ ) is a theorem of MLF, so it is in 0. Then, by Modus Ponens (MP), we get [T](' _ ) 2 0, further implying (' _ ) ^ [T](' _ ) 2 0 since we already have (' _ ) 2 0. The assumption (?) gives us that hSi ' _ ^ [T] ' _ 2 . Since is maximally consistent, any instance of WMB([S]; [T]) is in ; in particular, so is hSi (' _ ) ^ [T](' _ ) ! (' _ ). Finally, again by MP, we have ' _ 2 . Since : 2 , it follows that ' 2 .
Soundness and completeness of MLF w.r.t. F. Since any component C 2 F can be converted to a K-frame (C), soundness follows from Corollary 3 and Proposition 2. As to completeness, for a non-theorem ' 2 L[T];[S], :' is consistent. Let :' be a maximally consistent set in the canonical model Mc such that :' 2 :'. As the canonical frame Mc = (Wc; T c; Sc) is a member of the class K, Proposition 1 and Proposition 2 allow us to define the component Cc = (C1c; C2c) with :' 2 C1c [ C2c. Moreover, by Corollary 1, Cc
1 [ C2c is closed under the operators T c( ) and Sc( ). Therefore, modal satisfaction is preserved between Mc and Cc. As a result, Cc; :' 6j=MLF ' (i.e., Cc; :' j=MLF :'). 3
We here propose an extension of MLF with a new axiom schema
Neg([S]; [T]): hTi[T]' ! hTihSi:' where ' 2 Prop is non-tautological. We call this schema ‘negatable axiom’ and the resulting formalism MLF . MLF -models are of 2 kinds, namely K and F . They are obtained respectively from the classes K and F by adding a ‘model’ constraint: neg(S; T ): for every P
P; there exists a world w such that P = V(w): In other words, MLF -models can falsify any nontheorem of our logic, i.e., for every such ', there exists a world w such that w j=MLF :'. Every F -model (C1; C2; V) now has an exactly ‘two-floor’ form: C1 , ;, and C1 includes a world w, at which a propositional nontheorem ', valid in C2, is refuted. A K -model is indeed an arbitrary combination of F -models. Below we show that Neg([S]; [T]) precisely corresponds to neg(S; T ). Proposition 4. Given a K-model M = (W; T ; S; V) in MLF,
Proof. Let M = (W; T ; S; V) be a K-model of MLF. (=)): Assume that M is not a K -model. Then, there exists a nontautological propositional formula ' 2 Prop such that M j=MLF '. Clearly, [T]', [S]' and [T][S]' are all valid in M, but then so is hTi[T]' (thanks to the reflexivity of T ). This implies that hTi[T]' ^ [T][S]' is also valid in M. Thus, Neg([S]; [T]) is not valid in M. ((=): Let M be a K -model ( ). Let ' 2 Prop be a nontheorem. Take = hTi[T]' ! hTihSi:'. We need to show that M j=MLF . Let w 2 W be such that M; w j=MLF hTi[T]'. We first consider the F-model C = (C1; C2; V), generated by w as in Corollary 2. By construction, ' is valid in C2, and ( ) implies an existence of u 2 C1 such that u refutes '. By the frame properties of F, there exists v 2 C2 satisfying vSu and M; v j=MLF hSi:'. Regardless of the floor to which w belongs, wT v, and v 2 C2. Thus, M; w j=MLF hTihSi:'. Proposition 5. Given an F-model (C; V) = (C1; C2; V) in MLF,
Neg([S]; [T]) is valid in (C; V) if and only if (C; V) is an F -model. Neg([S]; [T]) has an elegant representation. However, as it makes the reasoning clear in the demanding proofs of this section, we find it handier to use the equivalent version
Neg’([S]; [T]): hTi[T]' ! hTihSi(:' ^ Q) of Neg([S]; [T]) in which ' 2 Prop is a nontheorem, and Q is a conjunction of a finite set of literals (i.e., p or :p, for p 2 P) such that the set f:'; Qg is consistent. Proposition 6. For a K -model M=(W; T ; S; V) and w 2 W,
M; w j=MLF Neg([S]; [T]) if and only if
M; w j=MLF Neg’([S]; [T]): Proof. The right-to-left direction is straightforward: take Q = ; and the result follows. For the opposite direction, we first assume that M; w j=MLF Neg([S]; [T]) (N). Let ' 2 Prop be a nontheorem of MLF viz. M; w j=MLF hTi[T]' (H). Let Q be a conjunction of finite literals such that :' ^ Q is consistent. Then, ' _ :Q 2 Prop is a nontheorem of MLF . Moreover, from the assumption (H), we also get M; w j=MLF hTi[T](' _ :Q). Lastly, by the hypothesis (N), we have M; w j=MLF hTihSi(:' ^ Q).
We finally transform a valuated cluster (C; V) into an F -model. We first construct a set
C1 = fx' : for every ' 2 Prop such that :' 0 ?; (C; V) j=MLF ' and x' < Cg into which we put a point x' < C for every nontheorem ' that is valid in C. So, C \ C1 = ;. Then, we extend the universal relation T on C to T 0 = C1 [ C C [ (C1 C1) on C [ C1. The valuation V defined over C is also extended to V0 : C1 [ C ! P satisfying: V0jC = V, and V0(x') is designed to falsify '. Hence, by definition, (C1; C; V0) 2 F . Soundness and completeness of MLF We have seen that MLF is sound w.r.t. F, so Proposition 5 implies that MLF is sound w.r.t. F . Since any K -model is a combination of F -models, we can generalise this result to K . We here show that MLF is complete w.r.t. F : first we take a canonical model Mc = (Wc; T c; Sc; Vc) of MLF (see Theorem 1 for the details). Then, we define a valuated component (Cc; Vc) = (C1c; C2c; Vc) for C1c; C2c Wc as in Section 2.5. We want to show that (Cc; Vc) is an F -model. So, it is enough to prove that Neg([S]; [T]) ensures the property neg(S; T ).
First recall that every F-frame C corresponds to a K-frame (C) = F C, and by Proposition 2, (C); w = C for w 2 C1 [ C2. Thus, such (Cc); Vc is a submodel of Mc since it is a K -frame. For nontautological ' 2 Prop, let us assume j=MLF ' (i.e., ' 2 ) for every 2 C2c (so, ' is consistent). This implies that (Cc; Vc); j=MLF [T]' (i.e., [T]' 2 ), for every 2 C2c. Using the fact that (Cc) is part of the canonical model Mc, we have T cjC1c[C2c (C1c [ C2c) C2c . Thus, (Cc; Vc); j=MLF hTi[T]' for every 2 C1c [C2c. As any instance of Neg([S]; [T]) is valid in (Cc; Vc), hTihSi:' 2 for every 2 C1c [c C02c.aInndother words, (Cc; Vc) j=MLF hTihSi:'. Thus, there exists 0 2 Wc such that T 0 j=MLF hSi:' (i.e., hSi:' 2 0). As T (C [ A) = C [ A in F, we have 0 2 C1c [ C2c. Moreover, there also exists 00 2 Wc such that 0Sc 00 and 00 j=MLF :'. By Corollary 1, S(C1c [ C2c) C1c [ C2c, yet from our initial hypothesis, we obtain 00 2 C1c. To sum up, 00 is a maximally consistent set in Cc such that (Cc; Vc); 00 6j=MLF '. 3.1
Minimal model semantics for nonmonotonic S4F
This section recalls the minimal model semantics for nonmonotonic S4F [
We abbreviate it by N (C; V). A valuated cluster (C; V) is then a minimal model of a theory (finite set of formulas) in S4F if – (C; V); x j= for every x 2 C – N 6j= for every N such that N (i.e., (C; V) j= );
(C; V).
Finally, a formula ' is a logical consequence of a theory in S4F (abbreviated j S4F ') if ' is valid in every minimal model of . For example, q j S4F:p _ q, yet :p _ q j0S4Fq. 3.2
Embedding nonmonotonic S4F into MLF We here embed nonmonotonic S4F into MLF . With this aim, we first translate the language of S4F (LS4F) into L[T];[S] via a mapping ‘tr’: we simply and only replace L 2 L[T];[S] by [T]. The following proposition proves that this translation is correct, and clarifies how to characterise minimal models of S4F in MLF .
Proposition 7. Given an F -model (C; V) = (C1; C; V), and 2 LS4F, we have: 1. (C; V); w j=MLF tr( ), for every w 2 C if and only if (C; VjC) j= . 2. (C; V) j=MLF hTi[T] tr( )^[S]:tr( ) if and only if (C; VjC) is a minimal model of . Proof. The proof of the first item is by induction on . As to the second item, for the proof of the ‘only if ’ part, we first assume (C; V) j=MLF hTi[T](tr( ) ^ [S]:tr( )) ( ). (1) From ( ), we obtain that (C; V); u j=MLF tr( ) (N), and (C; V); u j=MLF [S]:tr( ) (H) for every u 2 C (consider: for w 2 C1, ( ) implies that there is u 2 C1 [ C such that wT u and (C; V); u j=MLF [T](tr( ) ^ [S]:tr( )). So, u 2 C; otherwise it yields a contradiction). Then, using Proposition 7.1 and (N), we get (C; VjC) j= . So, the first condition holds. (2) By definition, it remains to show that N 6j= for every S4F model N such that N (C; VjC). Let N = (N; R; U) be a preferred model over the valuated cluster (C; VjC) satisfying: N = C [C0 for some (cluster) C0 such that C \C0 = ;, R = N C [ (C0 C0), and UjC = VjC . By Definition 4, we also know that there exists 2 Prop such that (C; VjC) j= ( ), but N 6j= . Therefore, there exists r 2 C0 viz. N ; r 6j= (i.e., N ; r j= : ). (3) As (C; V) is an F -model, Neg([S]; [T]) is valid in it; due to Proposition 6, so is Neg’([S]; [T]). Hence, (C; V) j= hTi[T]' ! hTihSi(:' ^ Q) for a non-theorem ' 2 Prop of LMLF , and a conjunction of a finite set of literals Q such that f:'; Qg is consistent. (4) By ( ) in the item (2) and also using Lemma 7.1, we get (C; V); u j=MLF tr( ) for every u 2 C. Since (C; V) is an F -model, we also have (C; V); u j=MLF [T]tr( ); even (C; V); u j=MLF hTi[T]tr( ) for every u 2 C (|). Moreover, we know that tr( ) is not a tautology; otherwise N ; r j= . Let Q0 = Vp2 P \U(r) p ^ Vq2 P nU(r) :q . It is clear that N ; r j= Q0, but we also know that N ; r j= : , so we have N ; r j= : ^ Q0. We so conclude that f: ; Q0g is consistent; then so is f:tr( ); Q0g. As (C; V) is an F model, an instance of the negatable axiom, namely hTi[T]tr( ) ! hTihSi(:tr( ) ^ Q0), is valid in (C; V). So, (|) implies that (C; V); u j=MLF hTihSi(:tr( ) ^ Q0) for every u 2 C. This means that there exists a point x 2 C1 such that (C; V); x j=MLF :tr( ) ^ Q0, i.e., (C; V); x j=MLF :tr( ) and (C; V); x j=MLF Q0. As a result, V(x ) \ Ptr( ) = U(r) \ P . (5) Note that r and x agree on P . By (H), we also have (C; V); x j=MLF :tr( ) for every x 2 C1; in particular, (C; V); x j=MLF :tr( ). To summarise the observation above: 1. The pointed model fx g; C; Vj(C[fx g) ; x in MLF , and the pointed model (N ; r) in S4F have the similar structure: both contain the same maximal valuated cluster (C; VjC) and one additional reflexive point that can have access to all points of C; 2. P = Ptr( ) and V(x ) \ Ptr( ) = U(r) \ P ; 3. Both and tr( ) are the exact copies of each other, except that one contains L wherever the other contains [T] (note that tr( ) contains neither [S] nor hSi). Then, it follows that N ; r 6j= , which further implies that N 6j= . By definition, (C; VjC) is a minimal model for . The other part of the proof is similar.
We are now ready to show how we capture the logical consequence of S4F in MLF .
j S4F i j=MLF [T](tr( ) ^ [S]:tr( )) ! [T]tr( ).
Proof. We first take = [T](tr( ) ^ [S]:tr( )) ! [T]tr( ). (=)): Assume that j S4F in S4F (N). Let (C; V) = (C1; C2; V) be an F -model. Then (C2; VjC2 ) is a valuated cluster over C2. We need to show that (C; V) j=MLF . “For every w 2 C1, (C; V); w j=MLF ” trivially holds: by the frame constraints w.r.t. T in MLF , (C; V); w 6j=MLF [T](tr( ) ^ [S]:tr( )) for any w 2 C1 (otherwise, (C; V) j=MLF tr( ), but also (C; V) j=MLF :tr( ), yielding a contradiction). Let x 2 C2 be such that (C; V); x j=MLF [T](tr( ) ^ [S]:tr( )). We know that T jC2 is a universal relation, so “for all x 2 C2, (C; V); x j=MLF hTi[T](tr( ) ^ [S]:tr( ))” trivially follows. Then, by Proposition 7.2, we conclude that (C2; VjC2 ) is a minimal model for . Then, as j S4F by the hypothesis (N), is valid in (C2; VjC2 ), i.e., (C2; VjC2 ) j= . Thus, Proposition 7.1 gives us that (C; V); z j=MLF tr( ) for every z 2 C2. Since C2 is a cluster which is a final cone, we also have (C; V); z j=MLF [T]tr( ) for every z 2 C; in particular, (C; V); x j=MLF [T]tr( ). ((=): Assume that is valid in MLF (H). We need to prove that j S4F . Let (C; V) be a minimal model of . Then, we take an S4F model N = (C [ C0); R; U preferred over (C; V). viz. N (C; V). Thus, N 6j= ( ). Now, let us construct (C; V) = (C1; C2; V) as follows: take C2 as the maximal -cluster C (i.e., exactly the same cluster C as in (C; V)), and C1 = fr : N ; r 6j= g. Simply, restrict R and U to C1 [C2, respectively resulting in T and V. Finally, arrange S in a way that would satisfy all the frame constraints of MLF. Thus, (C; V) is clearly an F -model. By the minimal model definition, (C; V) j= . Then, Proposition 7.1 and ( ) imply that (C; V); x j=MLF tr( ) for every x 2 C2, and for every y 2 C1, (C; V); y j=MLF :tr( ). As (C; V) is an F -model, we have (C; V); x j=MLF [S]:tr( ) for every x 2 C2. As a result, (C; V); x j=MLF tr( ) ^ [S]:tr( ) for every x 2 C2. Since C2 is a cluster which is a final cone, we further have (C; V); x j=MLF [T](tr( ) ^ [S]:tr( )) for each x 2 C2. From (H), it also follows that (C; V); x j=MLF [T]tr( ) for every x 2 C2. Clearly, tr( ) is also valid in C2. Finally, Proposition 7.1 implies that (C; V) j= in S4F. Corollary 4. For 2 LS4F, has a minimal model if and only if [T](tr( ) ^ [S]:tr( )) is satisfiable in MLF . (hint: take = ? in Theorem 2.) 4
In this section, we briefly discuss a general strategy, unifying some major
nonmonotonic reasonings among which are autoepistemic logic (AEL) [
AEL and RAEL [
Our research has also a large overlap with [
In this paper, we design a novel monotonic modal logic, namely MLF , that captures nonmonotonic S4F. We demonstrate this embedding by translating the language of S4F into that of MLF . This way, we see that MLF is able to characterise the existence of a minimal model as well as logical consequence in nonmonotonic S4F.
Our work provides an alternative to Levesque’s monotonic bimodal logic of only
knowing [
B tr( ) ^ N :tr( ) ! B tr( ): Levesque attacked the same problem with an emphasis on the only knowing notion. However, his reasoning does not attempt to unify, and does not provide a general mechanism either. In particular, he applied his approach to neither SW5 nor S4F.
As a future work, we will implement this general methodology to capture
minimal model reasoning, underlying many other nonmonotonic formalisms. This paper,
together with other works on KD45, SW5, and ASP [