Introduction

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 [1,2,3,4,5,6,7,8], logically capturing important forms of nonmonotonic reasoning. Theoretically, we obtain a clear and simple monotonic framework for studying further language extensions and possible generalisations. From a practical point of view, we can check nonmonotonic deduction with a validity proving procedure in a corresponding monotonic setting.

The modal logic S4F (aka, S4.3.2) is obtained from S4 by adding the axiom schema F : (ϕ ∧ M L ψ) → L (M ϕ ∨ ψ) [9] in which L is the epistemic modal operator, and M is its dual, defined by ¬L¬. A first and detailed investigation of this logic was given in [10]; yet in time, S4F has also found interesting theoretical applications in Knowledge Representation [11,12,13,14,15,16,17]. S4F is characterised by the class of Kripke models (W, T , V) in which W = W 1 ∪ W 2 for some disjoint sets W 1 and W 2 such that W 2 is nonempty. Moreover, xT y if and only if y ∈ W 2 or x ∈ W 1 . V is the valuation function such that V(x) is a set of propositional variables for every x ∈ W. A cluster is simply a trivial S5 model (C, T , V) such that xT y for every x, y ∈ 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 (C 1 ,C 2 , V) in which C 1 and C 2 are disjoint cluster structures, C 2 ∅, and any world in C 2 can be accessed from every world in C 1 .

This paper follows a similar approach to [18] and [8]: the former captures the reflexive autoepistemic reasoning [19,20] of nonmonotonic SW5 [21,22,23]. The latter successfully embeds equilibrium logic [24,25], which is a logical foundation for answer set programming (ASP) [26,27,28], into a monotonic bimodal logic called MEM. All these works are, in essence, parts of a project that aims to reexamine the logical and mathematical foundations of nonmonotonic logics. The overall project will then culminate in a single monotonic modal framework, enabling us to obtain a unified perspective of various forms of nonmonotonic reasoning.

As a reference to the analogy between all such works, we here keep the same symbols T and S1 with [8,18] for the accessibility relations. Roughly speaking, [8,18] and this paper all propose Kripke models, composed of a union of 2-floor (disjoint) structures. In general, while the relation T helps access from 'bottom' (first floor) to 'top' (second floor), the relation S works in the opposite direction. However, the structures of bottom and top differ in all formalisms. In particular, the models here and in [18] are respectively the extensions of the Kripke models of S4F and SW5 with the S-relation; whereas MEM restricts top to a trivial cluster of a singleton, and forces all subsets of the top valuation to appear inside the bottom structure to check the minimality criterion of equilibrium models [24,25]. Similarly to [8,18], we also propose here a modal language L [T], [S] with two (unary) modal operators, namely [T] and [S]. The former is a direct translation of L in the language of S4F (L S4F ) into L [T],[S] via a mapping 'tr : L S4F −→ L [T],[S] '. The relations T and S respectively interpret the modal operators [T] and [S]. We call the resulting monotonic formalism MLF. We then add into MLF the negatable axiom, resulting in MLF * : modal logic of nonmonotonic S4F. The negatable axiom ensures that the cluster C 1 (bottom) of MLF frames is nonempty, so it turns our frames into exactly 2-floor structures in MLF * : both floors are maximal clusters w.r.t. the relation T . Essentially, this axiom enables us to refute any nontautology of L [T], [S] as it allows us to have all possible valuations in an MLF * model. Thus, we show that the formula T [T](ϕ ∧ [S]¬ϕ) characterises maximal ϕ-clusters in MLF * . This result paves the way to our final goal in which we capture nonmonotonic consequence (abbreviated ' | ≈ S4F ') of S4F in the monotonic modal logic MLF * :

ϕ | ≈ S4F ψ 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 w.r.t. both semantics. In Section 3, we extend MLF with the negatable axiom, and call the resulting logic MLF * . We introduce two kinds of model structures, K * and F * , and end with the soundness and completeness results. Section 3.1 recalls minimal model semantics of nonmonotonic S4F: we define the preference relation, and then give the definition of a minimal model for S4F. Section 3.2 first captures minimal models of S4F, and then embeds the consequence relation of S4F into MLF * . Section 4 discusses a general approach, allowing us to capture major nonmonotonic logics. Section 5 makes a brief overview of this paper, and mentions our future goals.

A monotonic modal logic related to nonmonotonic S4F

We here propose a new formalism called MLF, which is closely associated with S4F.

Language (L [T],[S] )

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:

ϕ p | ¬ϕ | ϕ → ϕ | [T]ϕ | [S]ϕ

where p ranges over P.

L [T],[S]

is therefore a bimodal language with the modalities [T]

and [S]. As usual,

def = ϕ → ϕ, ⊥ def = ¬(ϕ → ϕ), ϕ ∨ ψ def = ¬ϕ → ψ, ϕ ∧ ψ def = ¬(ϕ → ¬ψ),

and ϕ ↔ ψ def = (ϕ → ψ) ∧ (ψ → ϕ). Moreover, T ϕ and S ϕ respectively abbreviate ¬[T]¬ϕ and ¬[S]¬ϕ.

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 ∈ W,

(w, w) ∈ T refl(T ) (w, u) ∈ T and (u, v) ∈ T ⇒ (w, v) ∈ T trans(T ) (w, u) ∈ T , (u, w) T and (w, v) ∈ T ⇒ (v, u) ∈ T f(T ) (w, u) ∈ S ⇒ (u, u) ∈ S refl 2 (S) (w, u) ∈ S and (u, v) ∈ S ⇒ u = v wtriv 2 (S) (w, u) ∈ T ⇒ (u, w) ∈ T or (u, w) ∈ S msym(T , S) (w, u) ∈ S ⇒ w = u or (u, w) ∈ T wmsym(S, T ).

The first three properties above characterise the frames of the modal logic S4F [9]. Thus, a K-frame is an extension of an S4F frame by a second relation S. Given a Kframe F = (W, T , S), a K-model is a pair M = (F , V) in which V : W → 2 P is the map, assigning to each w ∈ W a valuation V(w). Then, given w ∈ W, a pointed K-model is a pair M w = (M, w), and similarly, a pointed K-frame is a pair F w = (F , w).

Truth conditions

The truth conditions are standard: (for p ∈ P)

M, w | = MLF p if p ∈ V(w); M, w | = MLF ¬ϕ if M, w | = MLF ϕ; M, w | = MLF ϕ → ψ if M, w | = MLF ϕ or M, w | = MLF ψ; M, w | = MLF [T]ϕ if M, u | = MLF ϕ for every u such that wT u; M, w | = MLF [S]ϕ if M, u | = MLF ϕ for every u such that wSu. We say that ϕ is MLF satisfiable if M, w | = MLF ϕ for some K-model M and w in M. Moreover, ϕ is MLF valid (for short, | = MLF ϕ) if M, w | = MLF ϕ for every w of every K- model M. Then, ϕ is valid in M (M | = MLF ϕ) when M, w | = MLF ϕ for every w in M.

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 -cluster 2 [22,29].

Definition 1. Given a K-frame (W, T , S), let C be a subset of W. Then, -C is a T -cluster if wT u for every w, u ∈ C; -C is maximal if no proper superset of C in W is a T -cluster.

-C is a T -cone if for every w ∈ W, and every u ∈ C, uT w implies w ∈ C; -C is final if wT u for every w ∈ W and every u ∈ C. Given a K-frame F = (W, T , S), the relation T partitions F into disjoint subframes F = (W , T , S) in which W = C 1 ∪C 2 for some maximal clusters C 1 ,C 2 ⊆ W ⊆ W such that C 1 ∩C 2 = ∅, and C 2 ∅ is a final cone in W . Thus, T | W = (W ×C 2 )∪(C 1 ×C 1 ). We now define the operators T (•), S(•) : 2 W −→ 2 W , respectively assigning to every X ⊆ W, T (X) = {u ∈ W : wT u for some w ∈ X}; S(X) = {u ∈ W : wSu for some w ∈ X}.

It follows from

When X={w}, 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 = (C 1 ,C 2 ) be a pair of disjoint subsets of W such that C 2 ∅. Then, C is called a component of F if: 1. C 1 and C 2 are maximal clusters; 2. T ∩ (C 1 × C 2 ) = C 1 × C 2 .

So, a component C = (C 1 ,C 2 ) has a 'two-layered' structure: C 1 is the first floor ('F1cluster'), and C 2 is the second floor ('F2-cluster'). Clearly, C 2 is the final cone of the structure C. Note that C can also be transformed into a special K-frame

F C = C 1 ∪ C 2 , (C 1 ∪ C 2 ) × C 2 ∪ (C 1 × C 1 ), (C 2 × C 1 ) ∪ ∆ C 1 (1)

where

∆ C 1 is the diagonal of C 1 × C 1 , i.e., ∆ C 1 = {(w, w) : w ∈ C 1 }. Given any two dif- ferent components C = (C 1 ,C 2 ) and C = (C 1 ,C 2 ) of a K-frame F , C 1 ∪C 2 and C 1 ∪C 2

are disjoint, and C and C 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 sufficient 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 = (C 1 ,C 2 )

, having a component structure.

We now define a function µ : The proof easily follows from the frame properties of K.

F → K, assigning a K-frame µ(C) = F C (see (1)) to each F-frame C. As two distinct components C and C give rise to two distinct K-frames F C and F C , µ is 1-1, but not onto 3 . Thus, F is indeed a (proper) subclass of K. Proposition 1. Given a K-frame F = (W, T , S), let C = (C 1 ,C 2 ) be a component of F , and w ∈ C 1 ∪ C 2 , then 1. if w ∈ C 1 , then T (w) = C 1 ∪ C 2 ,

Corollary 1. For a K-frame F =(W, T , S), and a component C=(C 1 ,C 2 ) of F , we have:

1. T (C 1 ∪ C 2 ) = C 1 ∪ C 2 ; 2. S(C 1 ∪ C 2 ) ⊆ C 1 ∪ C 2 . Corollary 2. Given a pointed K-frame F w , let C = T (w)\C 1 if w is in an F1-cluster C 1 ; else if w is in an F2-cluster C 2 , let C = T (w). Take C =S(C) \C. Then, C F w =(C ,C) ∈ F.

Note that the component generated by w ∈ 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 F w an F-frame C F w . Clearly, ν is not 1-1, but is onto. Finally, {ν(F w ) : w ∈ W} identifies all the components in F . The following proposition generalises this observation.

Proposition 2. Given an F-frame C = (C 1 ,C 2 ) and w ∈ C 1 ∪C 2 , we have ν(µ(C), w) = C.

These transformations between frame structures of MLF enable us to define valuations also on the components C ∈ 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 ∈ µ(F) and a valuation V, one can transform

F C to a component ν(F C w ) = C ∈ F for some w ∈ C 1 ∪C 2 (see Proposition 2)

. This discussion allows us to define pairs (C, V) in which C ∈ 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)=(C 1 ,C 2 , V) and w ∈ C 1 ∪C 2 , (C, V), w | = MLF [T]ψ if and only if -if w ∈ C 1 then (C, V), v | = MLF ψ for all v ∈ C 1 ∪ C 2 (i.e., (C, V) | = MLF ψ); -if w ∈ C 2 then (C, V), v | = MLF ψ for all v ∈ C 2 . (C, V), w | = MLF [S]ψ if and only if -if w ∈ C 1 then (C, V), w | = MLF ψ; -if w ∈ C 2 then (C, V), v | = MLF ψ for all v ∈ C 1 if C 1 ∅; else 'no strict conclusion'.

The next result reveals the relation between the Kripke and the floor sematics of MLF.

Proposition 3 (corollary of Proposition 2). For anF-model (C, V), w ∈ C, and ϕ ∈ L [T],[S] , (C, V), w | = MLF ϕ if and only if (F C , V), w | = MLF ϕ.

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 [30]. The monotonic logic defined by Table 1 is MLF. The schemas T 2 ([S]) and WTriv 2 ([S]) can be combined

K([T]) the modal logic K for [T] K([S]) the modal logic K for [S] T([T]) [T]ϕ → ϕ 4([T]) [T]ϕ → [T][T]ϕ F([T]) (ϕ ∧ T [T]ψ) → [T]( T ϕ ∨ ψ) T 2 ([S]) [S]([S]ϕ → ϕ) WTriv 2 ([S]) [S](ϕ → [S]ϕ) MB([T], [S]) ϕ → [T]( T ϕ ∨ S ϕ) WMB([S], [T]) ϕ → [S](ϕ ∨ T ϕ) Table 1. Axiomatisation of MLF

Soundness and completeness of MLF

The axiom schemas given in Table 1 precisely characterise the class K of MLF frames. We only show that F([T]) describes the property f(T ) of K-frames, but the rest is similar.

-Let M=(W, T , S, V) be a K-model, satisfying f(T ). We want to show that F( Here, we only need to show that the inference rules of MLF are validity-preserving.

[T]) is valid in M. Let w ∈ W be such that M, w | = MLF ϕ ∧ T [T]ψ ( ).

Theorem 1. MLF is complete w.r.t. the class of K-frames.

Proof. We use the method of canonical models (see [29]), so we first define the canonical model

M c = (W c , T c , S c , V c ) in which -W c

is the set of maximally consistent sets of MLF.

-T c and S c are the accessibility relations on W c with:

ΓT c Γ if and only if {ψ : [T]ψ ∈ Γ} ⊆ Γ ; ΓS c Γ if and only if {ψ : [S]ψ ∈ Γ} ⊆ Γ . -V c is the valuation s.t. V c (Γ) = Γ ∩ P, for every Γ ∈ W c .

By induction on ϕ, we prove a truth lemma saying:

"Γ | = MLF ϕ iff ϕ ∈ Γ" for every ϕ ∈ L [T],[S]

. Then, it remains to show that M c satisfies all constraints of K, and so is a legal K-model of MLF. We here give the proof only for wtriv 2 (S) and wmsym(S, T ). The schema WTriv 2 ([S]) guarantees that M c satisfies wtriv 2 (S): let Γ 1 S c Γ 2 ( ) and Γ 2 S c Γ 3 ( ). Assume for a contradiction that Γ 2 Γ 3 . Thus, there exists ϕ ∈ Γ 2 with ¬ϕ ∈ Γ 3 , implying that S ¬ϕ ∈ Γ 2 by the hypothesis ( ). Since Γ 2 is maximally consistent, ϕ ∧ S ¬ϕ ∈ Γ 2 . So, using the hypothesis ( ), we get S (ϕ ∧ S ¬ϕ) ∈ Γ 1 .

However, since Γ 1 is maximally consistent, any instance of WTriv 2 ([S]) is in Γ 1 . Thus, [S](ϕ→[S]ϕ) ∈ Γ 1 , and it contradicts the consistency of Γ 1 .

The schema WMB([S], [T]) ensures that wmsym(S, T ) holds in M c : suppose that ΓS c Γ ( ) for Γ, Γ ∈ W c . W.l.o.g., let Γ Γ . Then, there exists ψ ∈ Γ with ¬ψ ∈ Γ. We need to show that Γ T c Γ. So, let ϕ be such that [T]ϕ ∈ Γ . As Γ is maximally consistent, we have both 3 Where we capture nonmonotonic S4F: Modal logic MLF * We here propose an extension of MLF with a new axiom schema

ϕ ∨ ψ ∈ Γ and [T]ϕ ∨ [T]ψ ∈ Γ . We know that [T]ϕ ∨ [T]ψ → [T](ϕ ∨ ψ) is a theorem of MLF, so it is in Γ . Then, by Modus Ponens (MP), we get [T](ϕ ∨ ψ) ∈ Γ , further implying (ϕ ∨ ψ) ∧ [T](ϕ ∨ ψ) ∈ Γ since we already have (ϕ ∨ ψ) ∈ Γ . The assumption ( ) gives us that S ϕ ∨ ψ ∧ [T] ϕ ∨ ψ ∈ Γ. Since Γ is maximally consistent, any instance of WMB([S], [T]) is in Γ; in particular, so is S (ϕ ∨ ψ) ∧ [T](ϕ ∨ ψ) → (ϕ ∨ ψ).

Neg([S], [T]): T [T]ϕ → T S ¬ϕ

where ϕ ∈ 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 | = MLF * ¬ϕ. Every F * -model (C 1 ,C 2 , V) now has an exactly 'two-floor' form: C 1 ∅, and C 1 includes a world w, at which a propositional nontheorem ϕ, valid in C 2 , 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, Neg([S], [T]) is valid in M if and only if M is a K * -model. 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 ϕ ∈ Prop such that M | = MLF ϕ.

Clearly, [T]ϕ, [S]ϕ and [T][S]ϕ are all valid in M, but then so is T [T]ϕ (thanks to the reflexivity of T ). This implies that T [T]ϕ ∧ [T][S]ϕ is also valid inF-model (C, V) = (C 1 ,C 2 , 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]): T [T]ϕ → T S (¬ϕ ∧ Q) of Neg([S], [T]

) in which ϕ ∈ Prop is a nontheorem, and Q is a conjunction of a finite set of literals (i.e., p or ¬p, for p ∈ P) such that the set {¬ϕ, Q} is consistent. We finally transform a valuated cluster (C, V) into an F * -model. We first construct a set C 1 = {x ϕ : for every ϕ ∈ Prop such that ¬ϕ ⊥, (C, V) | = MLF ϕ and x ϕ C} into which we put a point x ϕ C for every nontheorem ϕ that is valid in C. So, C ∩C 1 = ∅. Then, we extend the universal relation T on

C to T = C 1 ∪ C × C ∪ (C 1 × C 1 ) on C ∪ C 1 . The valuation V defined over C is also extended to V : C 1 ∪ C −→ P satisfying: V | C = V, and V (x ϕ ) is designed to falsify ϕ. Hence, by definition, (C 1 ,C, V ) ∈ 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 M c = (W c , T c , S c , V c ) of MLF * (see Theorem 1 for the details). Then, we define a valuated component

(C c , V c ) = (C c 1 ,C c 2 , V c ) for C c 1 ,C c 2 ⊆ W c

as in Section 2.5. We want to show that (C c , V c ) 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 ∈ C 1 ∪ C 2 . Thus, such µ(C c ), V c is a submodel of M c since it is a K * -frame. For nontautological ϕ ∈ Prop, let us assume Γ | = MLF * ϕ (i.e., ϕ ∈ Γ) for every Γ ∈ C c 2 (so, ϕ is consistent). This implies that (C c , V c ), Γ | = MLF * [T]ϕ (i.e., [T]ϕ ∈ Γ), for every Γ ∈ C c 2 . Using the fact that µ(C c ) is part of the canonical model M c , we have T c | C c 1 ∪C c 2 ⊃ (C c 1 ∪ C c 2 ) × C c 2 . Thus, (C c , V c ), Γ | = MLF * T [T]ϕ for every Γ ∈ C c 1 ∪C c 2 . As any instance of Neg([S], [T]) is valid in (C c , V c ), T S ¬ϕ ∈ Γ for every Γ ∈ C c 1 ∪ C c 2 .

In other words, (C c , V c ) | = MLF * T S ¬ϕ. Thus, there exists

Γ ∈ W c such that ΓT c Γ and Γ | = MLF * S ¬ϕ (i.e., S ¬ϕ ∈ Γ ). As T (C ∪ A) = C ∪ A in F, we have Γ ∈ C c 1 ∪ C c 2 .

Moreover, there also exists Γ ∈ W c such that Γ S c Γ and

Γ | = MLF * ¬ϕ. By Corollary 1, S(C c 1 ∪ C c 2 ) ⊆ C c 1 ∪ C c

2 , yet from our initial hypothesis, we obtain

Γ ∈ C c 1 . To sum up, Γ is a maximally consistent set in C c such that (C c , V c ), Γ | = MLF * ϕ.

Minimal model semantics for nonmonotonic S4F

This section recalls the minimal model semantics for nonmonotonic S4F [22]. We first define a preference relation between S4F models, enabling us to check minimisation. We abbreviate it by N (C, V). A valuated cluster (C, V) is then a minimal model of a theory (finite set of formulas)

Definition 4. An S4F model N = (N, R, U) is preferred over a valuated cluster (C, V) if -N = C ∪ C 1 for some (nonempty) set C 1 of possible worlds such that C ∩ C 1 = ∅; -R = N × C ∪ (C 1 × C 1 )Γ in S4F if -(C, V), x | = Γ for every x ∈ C (i.e., (C, V) | = Γ); -N | = Γ for every N such that N (C, V).

Finally, a formula ϕ is a logical consequence of a theory Γ in S4F (abbreviated Γ | ≈ S4F ϕ) if ϕ is valid in every minimal model of Γ. For example, q | ≈ S4F ¬p ∨ q, yet ¬p ∨ q | S4F q.

Embedding nonmonotonic S4F into MLF *

We here embed nonmonotonic S4F into MLF * . With this aim, we first translate the language of S4F (L S4F ) into L

) | = ψ (•), but N | = ψ. Therefore, there exists r ∈ C viz. N, r | = ψ (i.e., N, r | = ¬ψ). (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) | = T [T]ϕ → T S (¬ϕ ∧ Q) for a non-theorem ϕ ∈ Prop of L MLF * ,

and a conjunction of a finite set of literals Q such that {¬ϕ, Q} is consistent. ( 4) By (•) in the item (2) and also using Lemma 7.1, we get (C, V), u

| = MLF * tr(ψ) for every u ∈ C. Since (C, V) is an F * -model, we also have (C, V), u | = MLF * [T]tr(ψ); even (C, V), u | = MLF * T [T]tr(ψ) for every u ∈ C (♣). Moreover, we know that tr(ψ) is not a tautology; otherwise N, r | = ψ. Let Q = p∈ P α ∩U(r) p ∧ q∈ P α \U(r) ¬q . It is clear that N, r | = Q , but we also know that N, r | = ¬ψ, so we have N, r | = ¬ψ ∧ Q . We so conclude that {¬ψ, Q } is consistent; then so is {¬tr(ψ), Q }. As (C, V) is an F * - model,

Relation to other nonmonotonic formalisms

In this section, we briefly discuss a general strategy, unifying some major nonmonotonic reasonings among which are autoepistemic logic (AEL) [31], reflexive autoepistemic logic (RAEL) [23], equilibrium logic (and so ASP), and nonmonotonic S4F. The emphasis is on the 2-floor semantics; the second floor charaterises the minimal model of a formula, and the first floor checks the minimality criterion. This approach can be generalised to other formalisms such as default logic [32] and MBNF [33] as there exists a good amount of research in the literature, studying such relations [34,35,36,15]. In particular, nonmonotonic S4F and default logic has a strong connection as it is explained and analysed in [14,15]. So, the MLF * encoding of nonmonotonic S4F leads the potential encoding of default logic. AEL and RAEL [21,23] are the nonmonotonic variants [22] of respectively the modal logics KD45 and SW5 [9,29]. We have recently proposed two new monotonic modal logics called MAE * and MRAE * , respectively capturing AEL and RAEL. They are obtained from MLF * by replacing only the axioms characterising S4F (i.e., S, 4, F) by ones, characterising respectively KD45 and SW5 (i.e., groups of axioms D, 4, 5 and T, 4, W5). The models of MAE * , MRAE * , and MLF * are all composed of a union of 2-floor structures: in each, the second floor is a maximal cluster which is a final cone of the 2-floor part of the model; where they differ is the structure of the first floor. While a first floor in MLF * is a maximal cluster, that of MAE * contains irreflexive and isolated worlds w.r.t. the T -relation (in a sense that, any two different worlds of the first floor are not related to each other by the accessibility relation T ). Moreover, the MRAE * models are nothing, but the reflexive closures of the MAE * models w.r.t. the relation T . Interestingly, the same mechanism applied to S4F performs successfully for KD45 and SW5 as well when everything else remains the same: the implication [T] tr(α) ∧ [S]¬tr(α) → [T]tr(β), capturing nonmonotonic consequence of S4F, and the formula T [T] tr(α) ∧ [S]¬tr(α) characterising minimal model semantics in S4F perfectly work for the nonmonotonic variants of KD45 and SW5 as well.

Our research has also a large overlap with [8], embedding equilibrium logic (and so, ASP) into a monotonic bimodal logic called MEM. The models of MEM are roughly described in the introduction. The main result of this paper is also given via a similar implication: the validity of tr(α) ∧ [S]¬tr(α) → tr(β) in MEM captures the nonmonotonic consequence, α | ≈ β, of equilibrium logic. However, it is easy to check that the formula [T] tr(α) ∧ [S]¬tr(α) → [T]tr(β) of this paper also gives the same result. This analogy between all these works enables us to classify MEM under the same approach. Still, we need to provide a stronger result that would help reinforce the relations between MEM and MLF * . For instance, [14] proves that the well-known Gödel's translation into the modal logic S4 is still valid for translating the logic of here-and-there (a 3-valued monotonic logic on which equilibrium logic is built) [37,25] into the modal logic S4F. A natural question that may arise is whether a similar translation can be used to encode MEM into MLF * , which is the subject of a future work.

Conclusion and further research

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 [38,4,5,6], by which he captures four kinds of nonmonotonic logic, including autoepistemic logic: his language has two modal operators, namely B and N. B is similar to [T]. N is characterised by the complement of the relation, interpreting B. Levesque's frame constraints on the accessibility relation differ from ours, and he identifies the nonmonotonic consequence 'α | ≈ β' with the implication 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 [8] stand a very strong initiative by their possible straightforward implementations to different kinds of nonmonotonic formalisms of similar floor-based semantics. Such research will then enable us to compare various forms of nonmonotonic formalisms in a single monotonic modal setting.