A New Modal Framework for Epistemic Logic
Yanjing Wang
cs.AI cs.LO


 A new single-particle basis for nuclear many-body calculations.
    G. Puddu

       E-mail: giovanni.puddu@mi.infn.it

       Dipartimento di Fisica dell'Universita' di Milano,

       Via Celoria 16, I-20133 Milano, Italy
    Received: December 30, 2023/ Accepted: date
===============================================================================================================================================================




Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of ∃ x ϕ, e.g., knowing how to achieve ϕ roughly means that there exists a way such that you know that it is a way to ensure that ϕ. Moreover, the resulting logics are  decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality ^x, which packs exactly ∃ x together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t. first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between ^x and know-that operator in an epistemic setting.
 



§ INTRODUCTION



Standard epistemic logic studies valid reasoning patterns about knowing that. However, in natural language, knowledge is also expressed by knowing whether, knowing how, knowing what, knowing why and so on. Recent years witnessed a growing interest in the non-standard epistemic logics of such expressions (cf. e.g., <cit.> and the survey <cit.>).[This is not meant to be an exhaustive list, e.g., see also <cit.> about logics of knowing how in the setting of ATL.] In this line of work, various new modalities of know-wh are introduced,[Know-wh means verb know followed by a wh-word.] all of which share the general de re schema ∃ x ϕ(x) in their semantics, e.g, “knowing how to achieve ϕ” roughly means that there exists a way such that you know that it is a way to ensure that ϕ <cit.>; “knowing why ϕ” means that there exists an explanation such that you know that it is an explanation to the fact ϕ <cit.>. Actually, in the early days of epistemic logic, Hintikka already used such formulations to handle knowing who <cit.> (cf. the survey <cit.> for a detailed discussion on Hintikka's early contributions). Such interpretations are  grounded also in philosophy and linguistics (cf. e.g., <cit.>). 

Such a semantic schema is based on the so-called mention-some interpretation to the wh-questions embedded in those knowledge expressions <cit.>. There is also a mention-all interpretation <cit.>, which makes sense in many other situations, e.g., “knowing who came to the party”  means, under an exhaustive reading, that for each relevant person, you know whether (s)he came to the party or not, which can be summarized as ∀ x (ϕ(x)ϕ(x)). There are degenerated cases when the two interpretations coincide, e.g., “knowing [what] the value of c [is]” means, under the interpretation of mention-some, that there exists a value such that you know that it is the value of c, which is equivalent to the mention-all interpretation: for any value, you know whether it is the value of c, given there is one and only one real value of c.  

Given the experiences in dealing with those particular cases of know-wh, it is the time to lay out a general background  framework for the shared “logical core” of those  logics.[Note that this does not imply that we can simply use a single framework to cover all of those particular cases, since the details of the semantics in each setting matter a lot in deciding the characteristic axioms and rules in each different setting. Moreover, for example, in the setting of knowing how logics, we need to quantify over second-order objects (plans or strategies). ] This paper is the initial step towards this purpose by extending the  predicate language with the mention-some operator ^x, which is essentially a package of ∃ x. With the variable in place, we can say much more than those existing logics of know-wh, e.g., “I know a theorem of which I do not know any  proof” ^y Prove(y, x), or, in a multi-agent setting, “i knows a country which j knows its capital”: ^x_i^y_j Capital(y, x). Actually, when x does not appear in ϕ, ^xϕ is equivalent to ϕ, thus our language is indeed an extension of the standard modal language. Moreover, we will show that in the epistemic setting, this mention-some operator can also express mention-all. By having the predicate symbols in the language, we can also talk about the content of knowledge, which may be useful to bridge epistemic logic and knowledge representation. We also  believe that the new modality can be interpreted meaningfully not only in the epistemic context.  

From a technical point of view, what we discovered is a well-behaved yet powerful fragment of first-order modal logic (over arbitrary models), as the following main  technical contributions of this paper demonstrate: 


  * We propose a novel notion of bisimulation which can characterize the expressive power of our language within first-order modal logic precisely, over arbitrary models. 

  * Over arbitrary models, satisfiability of the equality-free fragment is not only decidable but also -complete, just as the complexity of basic propositional modal logic, demonstrated by a tableau-like method to show some strong finite-tree-model property.

  * We give a sound and complete proof system to our logic over epistemic (S5) models with the equivalence relation. However, we show that over S5 models, our logic is undecidable. 

Due to historical and technical reasons, first-order modal logic (FOML), in particular in the epistemic setting, has not been  thoroughly studied as its propositional brother (cf. e.g., <cit.>). Decidable fragments of first-order modal logic are usually obtained by restricting the occurrences of variables (particularly in the scope of ) (cf. e.g., <cit.>). We hope our framework and techniques can pave a new way to some interesting fragments of first-order modal logic, using new modalities to pack quantifiers and standard modalities together, which also reflects the “secret of success” of basic propositional modal logic as a nicely balanced logic between expressivity and complexity. 

In the rest of this paper, we introduce  the language and semantics of our framework in Section <ref>, study its expressivity over arbitrary models in Section <ref>, prove the complexity of the equality-free fragment in Section <ref>, give the proof systems in the epistemic setting in Section <ref>, and prove their completeness and undecidability in Section <ref>. 









































§ SYNTAX AND SEMANTICS
 

Throughout this paper we assume a fixed countably infinite set of variables , and a fixed set of predicate symbols . Furthermore, we assume that each predicate symbol is associated with a unique non-negative integer called its arity. We use x⃗ to denote a finite sequence of (distinct) variables in , in the order of a fix enumeration of . By abusing the notation, we also view x⃗ as a set of variables in x⃗ occasionally. In this paper, for the brevity of presentation, we focus on the following unimodal language, but the results and techniques can be generalized to the polymodal language.[We leave the discussion about the extension with constants or function symbols to the full version of the paper.] 
















 Given   and ,   


    ϕ::= x≈ y | Px⃗|ϕ| (ϕϕ)|ϕ

where x, y∈, P∈. We call the  equality-free fragment  (modal logic of mention-some). 

ϕ can be read as knowing some x such that ϕ(x) in the epistemic context. We use the usual abbreviations ⊤, , , →, and write  for , i.e., the dual of . We define the free and bound occurrences of variables as in first-order logic by viewing ^x as a quantifier. We call x is a free variable in ϕ (x∈ FV(ϕ)), if there is a free occurrence of x in ϕ. We write ϕ(x⃗) if all the free variables in ϕ are included in x⃗. Given an  formula ϕ and x, y∈, we write ϕ[y x] for the formula obtained by replacing every free occurrence of x by y. To simplify the discussion, we do not include constant symbols and function symbols in the language and leave them to a future occasion.[Note that constant and functions can be coded using  and ≈ in full  (cf. e.g., <cit.>). However, our language is a fragment of .]. 

As for the semantics, to be general enough, following <cit.> we use the first-order Kripke model with an increasing domain, and flesh out the intuitive idea of mention-some discussed in the introduction. 

An (increasing domain) model  for  is a tuple W, D, δ, R, ρ where: 


  W is a non-empty set.

  D is a non-empty set.

  R⊆ W× W is a binary relation over W.

  δ:W→ 2^D assigns to each w∈ W a non-empty local domain s.t. wRv implies δ(w)⊆δ(v) for any w,v∈ W. We also write D_w for δ(w).

  ρ:× W→⋃_n∈ω2^D^n such that ρ assigns each n-ary predicate on each world an n-ary relation on D.[Following <cit.>, we do not require that the interpretation of P at a world is based on the local domain. Actually, as we will see later in Corollary <ref>, this seemingly `counterintuitive' generalization does not affect the satisfiability or validity: each satisfiable formula ϕ is satisfiable in a model where ρ(P,w) is based on objects in D_w (cf. also <cit.>). ]  
 
A constant domain model is a model such that D_w=D for any w∈ W. A finite model is a model with both a finite W and a finite D. Given a model , we denote its components as W^, D^, δ^, R^, and ρ^. To interpret free variables, we also need a variable assignment σ: → D.

The formulas are interpreted on models with variable assignments. 


    [                      , w, σ x≈ y                                ⇔                        σ(x)=σ(y);               , w, σ P(x_1⋯ x_n)                                ⇔       (σ(x_1), ⋯, σ(x_n))∈ρ(P,w);                          , w, σϕ                                ⇔                         , w, σ⊭ϕ;                      , w, σ (ϕψ)                                ⇔              , w, σϕ and , w, σψ;                          , w, σϕ                                ⇔ there exists an a∈δ(w) such that;                                  , v, σ[x↦ a]ϕ for all v s.t. wRv;                                  ]



where σ[x↦ a] denotes another assignment just like σ except mapping x to a.


As an intuitive definition, following <cit.>, we say ϕ is valid, if ϕ is true on any , w w.r.t. any σ such that σ(x)∈δ^(w) for all x∈. Correspondingly, ϕ is satisfiable if ϕ is not valid, i.e., ,w,σϕ for some , w and σ such that σ(x)∈δ^(w) for all x∈.

It is not hard to see that if σ(x)=σ'(x) for all the free x in ϕ, , w, σϕ,w, σ'ϕ. In this light, we  write , wϕ [a⃗] to denote ,w,σϕ(x⃗) for any σ such that σ assigns free variables x⃗ of ϕ the corresponding objects in a⃗ given |x⃗|=|a⃗|, where |·| denotes the length.  


For comparison, the standard semantics for  is defined as:

    [                        , w, σϕ                              ⇔ for all v such that wRv, v, σϕ;                                ]

Truth conditions of ϕ and ϕ can then be defined  using ,:

    [                                        , w, σϕ                                              ⇔ there exists an a∈δ(w) such that , w, σ[x↦ a]ϕ;                                        , w, σϕ                                              ⇔                  for all a∈δ(w), , w, σ[x↦ a]ϕ;                                                ]

It is now clear that ϕ is equivalent to ϕ where  x∉FV(ϕ). Therefore  can be viewed as an extension of the basic propositional modal language. Therefore, in the context of , ϕ can be viewed as an abbreviation. It also becomes evident that ϕ and ϕ are essentially ∃ x ϕ and ∀ xϕ in  respectively. In the following we study the expressivity of  in comparison with .
































§ EXPRESSIVITY

 Note that our semantics for  has the ∃∀ pattern which is similar to the neighbourhood semantics for modal logic <cit.>. Moreover,  can be viewed as a fragment of the corresponding . Indeed, inspired by the world-object bisimulaion for  <cit.> and bisimulation for monotonic neighbourhood modal logic <cit.>, we propose a novel notion of bisimulation for . Before the formal definition, given a model , let D_^* be the set of (possibly empty) finite sequence of objects in D^. A partial isomorphism between a⃗∈D^*_ and b⃗∈D^*_ such that |a|=|b| is an isomorphism mapping a_i to b_i w.r.t. relevant interpretations of predicates (cf. e.g, <cit.>). It is partial since it is not about all the objects in D^ and D^. 
  Given two models  and , the relation Z⊆ (W^× D_^*)× (W^× D_^*) is call an ∃-bisimulation, if for every ((w,a⃗), (v, b⃗))∈ Z such that |a⃗|=|b⃗| the following holds (for brevity, comma in (w,a⃗) is omitted):


  PISO a⃗ and b⃗ form a partial isomorphism w.r.t. identity and interpretations of predicates at w and v respectively. 

  Zig For any c∈ D^_w, there is a d∈ D^_v such that for any v'∈ W^ if vR v' then there exists w' in W^ such that wR w' and w'a⃗c Z v'b⃗d. 

  Zag For any d∈ D^_v, there is a c∈ D^_w such that for any w'∈ W^ if wR w' then there exists v' in W^ such that vR v' and w'a⃗c Z v'b⃗d.


We say , wa⃗ and ,vb⃗ are -bisimilar (, wa⃗_,vb⃗) if |a|=|b| and there is an ∃-bisimulation linking wa⃗ and vb⃗. In particular, we say ,w and ,v are -bisimilar if , w_,v, i.e., when |a⃗|=|b⃗|=0.  

It is not hard to show that _ is indeed an equivalence relation. 


Note that our bisimulation notion is much weaker than isomorphism, in particular the domains of the two bisimilar models do not necessarily have the same cardinality.

Consider the constant domain models ,:

    @R-20pt:   w[r][dr]    v: Pa     :    s[r][dr]    t: Pc
          u: Pb              r

where D^={a,b}, D^={c}, ρ^(P,w)=ρ^(P,s)=ρ^(P,r)=∅, ρ^(P,v)={a}, ρ^(P,u)={b}, ρ^(P,t)={c}. Suppose P is the only predicate, we can show that ,w_,s by an ∃-bisimulation Z (pay attention to the switch of the two models in the second half of the definitions of Zig and Zag): 

    {(w,s), (va, tc), (ub, tc), (vb, rc), (ua, rc) }

Also note that Zig and Zag hold trivially for wa⃗ and vb⃗ if w and v do not have any successor, based on the fact that local domains are non-empty by definition.  


We write , wa⃗≡_, vb⃗ if |a⃗|=|b⃗| and for all any  formula ϕ(x⃗) such that |x⃗|=|a⃗|: , wϕ [a⃗] , vϕ[b⃗]. We can show that  is invariant under -bisimilarity.  

, wa⃗_,vb⃗ then , wa⃗≡_, vb⃗. 


It suffices to prove that if Z is an ∃-bisimulation linking wa⃗ and vb⃗ such that |a⃗|=|b⃗|,  then , wϕ [a⃗] , vϕ[b⃗].

Given a bisimulation Z, we do induction on the structure of ϕ. Supposing ϕ is an atomic formula, due to PISO, ,wϕ [a⃗] iff ,vϕ [b⃗] for any atomic formula ϕ (x⃗). 

Suppose ϕ is in the shape of ψ(x⃗) and  ,wϕ [a⃗]. By the semantics there is a c∈ D^_w such that ,w'ψ [a⃗c] for all the w' such that wRw'. According to Zig, there exists a d∈ D^_v such that the second half of the condition holds. We claim that  ,v'ψ [b⃗d] for any v' such that vRv'. Suppose not, then there is a v' such that ,v'⊭ψ [b⃗d] and vRv'. Then according to Zig, there is w' such that wRw' and  w'a⃗c Zv'b⃗d. By IH, ,w'⊭ψ [a⃗c]. Contradiction. 



, w_,v then for any closed -formula ϕ: 
, wϕ, vϕ.

By the above invariance results, we can show that many natural  combinations of quantifiers and modalities are not expressible in . 

∃ x Px, ∃ x  Px and ∃ x Px are not expressible in . 

 In this proof, we again consider constant domain models.  For ∃ x Px, consider the bisimilar models in Example <ref>. ∃ x Px holds on ,w but not on ,s, thus it is not expressible in . 








For ∃ x  Px and ∃ x Px, consider:  

    @R-20pt:   w[r][dr]    v: Pa     :    s[r]    t
          u

where D^={a,b}, D^={c} as before, ρ^(P,w)=ρ^(P,u)=ρ^(P,t)=ρ^(P,s)=∅, ρ^(P,v)={a}. Clearly, ∃ x Px and ∃ x Px are true at , w but false at , s. However, we can show that ,w_,s by an ∃-bisimulation Z: 

    {(w,s), (ua, tc), (vb, tc), (ub, tc)}.







To precisely characterize  within the corresponding , we need a notion of saturation. In the following, we write Γ(x⃗) if all the free variables in the set of -formulas Γ are included in  x⃗. Inspired by <cit.>, we can generalize the concept of m-saturation for propositional modal logic (cf. <cit.>) as follows:  

A model  is said to be -saturated, if for any w∈ W^, and any finite sequence a⃗∈D^*_, the following two conditions are satisfied: 


  ∃-type If for each finite subset Δ of a set Γ (y⃗x) where |y⃗|=|a⃗|, , w⋀Δ [a⃗],[Here we require y⃗ are assigned a⃗ correspondingly. This is only to avoid introducing extended language with constants for a⃗ as in standard model theory, since we did not define interpretation for constant symbols. Similarly below.] then there is a c∈ D^_w such that , wϕ[a⃗c] for all ϕ∈Γ, where x is assigned c.  

  -type If for each finite subset Δ of   Γ(x⃗) such that |x⃗|=|a⃗|, , w⋀Δ [a⃗], then , wϕ[a⃗] for each ϕ∈Γ.


Note that in the above definition, to simplify the presentation, we use , which are expressible in . -type condition is essentially the m-saturation adapted with variable assignments.  Recall that a finite model has a finite domain and finitely many worlds. It can be verified that:[Due to limited space, we omit some proofs and leave them to the extended version of this conference paper.] 
Every finite model is -saturated. 





We can obtain the Hennessy-Milner-type theorem (cf. <cit.>) to establish the equality between -bisimilarity and -equivalence.  

For -saturated models , and |a⃗|=|b⃗|: 
    , wa⃗_,vb⃗,w a⃗≡_,vb⃗
 


Due to Theorem <ref>, we only need to show the right-to-left direction. We define Z={(wa⃗, vb⃗)| w∈ W^, v∈ W^, a⃗∈ D_^*, b⃗∈ D_^*, |a⃗|=|b⃗|, , wa⃗≡_, vb⃗}. We need to show that Z is an ∃-bisimulation. PISO is straightforward as a⃗ and b⃗ are finite and partial isomorphism between them can be expressed by atomic formulas. We only show Zig since Zag is similar. Assuming wa⃗Z vb⃗ and there is a c∈ D^_w. Let Γ={ϕ(y⃗x)| wϕ [a⃗c], |y⃗|=|a⃗|}. Now for any finite set Δ⊆Γ we have w⋀Δ[a⃗]. Since  wa⃗≡_vb⃗, v⋀Δ[b⃗]. Now by ∃-type condition, we know there is a d∈ D^_v such that vϕ [b⃗d] for all ϕ∈Γ (⋆). Now take an arbitrary v' such that vR v', we show there is a w' such that wRw' and w'a⃗c≡_v'b⃗d. Let Σ={ϕ(x⃗)|,v'ϕ [b⃗d], |x⃗|=|b⃗d|}. It is clear that for each finite set Δ⊆Σ, v⋀Δ[b⃗d], namely v⋀Δ[b⃗d]. We can show w⋀Δ[a⃗c]. Suppose not, then w⋀Δ[a⃗c], thus ⋀Δ∈Γ. By (⋆), v⋀Δ[b⃗d], which is in contradiction with v⋀Δ[b⃗d]. Now it is clear that w⋀Δ[a⃗c] for each finite Δ⊆Σ. By the -type condition of -saturation, there is a successor w' of w such that w'Σ[a⃗c]. Therefore w'a⃗c≡_ v'b⃗d, namely (w'a⃗c, v'b⃗d)∈ Z. This completes the proof for Zig.


 For finite models: , wa⃗_,vb⃗,w a⃗≡_,vb⃗. For -saturated models: , w_,v , w  and ,v satisfies the same closed -formulas (sentences).
 
Now we can characterize  in the corresponding first-order language. 
 Given , as before, 
the corresponding  language is defined as follows: 

    ϕ::= x≈ y | Px⃗|ϕ| (ϕϕ)|∀ xϕ|ϕ

The corresponding two-sorted first-order language  is: 

    ϕ::= x≈ y | Q ux⃗| Ruv | Eux |ϕ| (ϕϕ)|∀ xϕ|∀ uϕ

where x, y∈ and u,v∈ which is a collection of world variables disjoint from ; Q∈ and  is the smallest collection of predicate symbols such that for each n-ary P∈ there is a unique Q_P∈ with the arity  n+1. E is a new predicate symbol to say which  object exists on which world.

It is trivial to define a translation r from  to the corresponding  by setting r(ϕ)=∃ x  r(ϕ). It is clear that this translation is truth preserving. To translate  into the formulas in the corresponding  (with u,v as the only world variables), we define the following t_u inspired by <cit.>:    


    [  t_u(x≈ y)= x≈ y      t_u(Px⃗)= Q_P(u, x⃗); t_u(ψ)= t_u(ψ)      t_u(ϕψ)=t_u(ϕ) t_u(ψ).;         t_u(ψ)=∃ x (Eux ∀ v (Ruv → t_v(ψ));                                            ]

t_v is defined symmetrically, by swapping u and v.

In this way, every -formula is translated into a two-world-variable formula of  with one free variable, similar to the standard translation of  basic modal language to first-order language. 

We can also view a model for  as a model for  by turning ρ(w, P) into the interpretation of the corresponding Q_P in the most natural way. It is not hard to show: 
 For any  formula ϕ: 

    ,w, σϕ, σ' ⊩ t_u(ϕ)

where σ' is σ extended by u↦ w, ⊩ is the standard semantics for  (cf. e.g. <cit.>).  

It follows from the compactness of  that:[ inherits the compactness from first-order logic since there is a truth preserving translation from  to  by using two new unary predicates S_1, S_2 for the two sorts, together with a single unrestricted quantifiers to mimic the two-sorted quantifiers. Note that we can also express the constraints on the sorts in  by θ(S_1,S_2)=∀ x ((S_1 x S_2x)  (S_1x S_2x)).] 

 is compact.






Based on Theorem <ref> and the compactness of , it is relatively routine to prove the van-Benthem-like characterization theorem using the strategy in <cit.>, which makes use of ω-saturation in first-order model theory.  We omit the proof due to limited space. 

A -formula ϕ(x⃗u) is equivalent to an -formula (over -models) iff it is invariant under -bisimilarity. 






























Since any  formula can also be viewed as a  formula ϕ(x⃗u), via a natural translation like t_u (cf. <cit.>), it follows that: 

A -formula is equivalent to an -formula iff it is invariant under -bisimilarity.  




§ SATISFIABILITY OF 
 

Note that by t_u we can translate an  formula to an equivalent  formula, and eventually to a  formula with one free world variable u (see Footnote <ref>). For example Px becomes 
    ϕ(u)=∃ x (S_1x  S_2u  Eux∀ v ((S_2v  Ruv)→ Q_Pvx))
 in the corresponding  language. Note that since we only consider increasing domain models, ϕ is equivalent to 

    ϕ(u)=∃ x (S_1x  S_2u  Eux∀ v ((S_2v  Ruv  Evx) → Q_Pvx))

which is in the (loosely) guarded fragment of first-order logic known to be decidable <cit.>. However, it does not directly imply that our logic is decidable, since, for example, to capture the increasing domain model we do need the following first-order constraint: 

    χ=∀ u∀ v ∀ x((S_2u S_2v S_1x Eux Ru v)→ Evx)

χ can be viewed as some form of transitivity, and it is not in the guarded fragment, since v and x are free in the consequent but they do not co-exist in any of the atomic guards in the antecedent. On the other hand, such a transitivity-like constrained predicate E only appears in the guards of the translations of -formulas, which may be handled by the techniques in <cit.> for the guarded fragment with transitive guards known to be decidable. We leave the detailed discussion connecting  to guarded fragments to a future occasion. 


In this section, we give an intuitive tableau-like method to decide whether an equality-free -formula is satisfiable, inspired by the  satisfiability games for various temporal logics <cit.>.[See <cit.> for tableau methods for first-order modal logic in general.] 

For the ease of presentation, we consider the following equivalent language of  in positive normal form (PNF), where negations only appear with atomic formulas:[PNF is often used in automata-theoretical methods to satisfiability problems of logics in computer science (cf. e.g., <cit.>).]

    ϕ::=  Px⃗| Px⃗| (ϕϕ) | (ϕϕ)|ϕ|ϕ

Note that for an arbitrary -formula ϕ, we can rewrite it into an equivalent formula in PNF by the following rewriting rules and the replacement of equals: 

    r( (ϕψ))=r(ϕ) r(ψ)   r(ϕ)= r(ϕ)    r(ϕ)=r(ϕ)

Note that |r(ϕ)|≤ 2|ϕ|. 

In the following, we will focus on the formulas that are clean in the sense that no variable occurs both free and bound,[ In particular, if  or  appears in the formula then x does not have any free occurrence, even when  and  do not bind any occurrence of x, e.g., ( Py)  Px is not clean.] and no two distinct occurrences of modalities bind the same variable. As in first-order logic, it is easy to show that any  formula can be relettered into an equivalent clean formula with the same length, by renaming the bounded variables.

We define the following tableau rules for all  formaulas in PNF. 
Tableau rules


































w: ϕ_1ϕ_2,Γ, σw:ϕ_1,Γ, σ| w:ϕ_2,Γ, σ ()    w: ϕ_1ϕ_2,Γ, σw:ϕ_1,ϕ_2,Γ,σ()

Given n≥ 0, m≥ 1:

w:ϕ_1, …, ϕ_n,ψ_1,…, ψ_m, l_1… l_k, σ{(wv^y_y_i: {ϕ_j| 1≤ j≤ n}, ψ_i[y y_i], σ') | y∈ Dom(σ'), i∈ [1,m]} ()

Given n≥ 1, k≥ 0:

w:ϕ_1, …, ϕ_n, l_1… l_k, σw: l_1… l_k, σ () 




where σ'=σ∪{(x_j, x_j)| j∈ [1,n] } and l_k∈ lit (the literals).



Those rules are used to generate tree-like structure, where the nodes are triples (w,Γ,σ) in which w is some name to denote a world, Γ is a finite set of -formulas, and σ is a partial function from  to  as an assignment. Note that Rule () is essentially a choice: given the numerator, you can only select one of the denominator to continue. On the other hand, the rule () is a branching one, which generates all the nodes in the denominator set (even when n=0 i.e., the -part is empty). It is a generalized version of the corresponding rule for basic modal logic (cf. <cit.>): 

    w: ϕ,ψ, l_1… l_lv: ϕ, ψ

The idea is that if there is a diamond formula then we need to generate a successor while keeping the information given by -formulas. Here the complication is to manage the variable assignment properly. Note that if there are merely -formulas without any -formula, then we do not need to generate any successor, as captured by the rule . 

A tableau starting from (w:Γ, σ) is a tree where the successors of a node are generated by applying the rules,  until no rule is applicable. Recall that you can only select one of the denominators to continue when applying (). Below is an example of a tableau where the (partial) function σ is represented by a set of ordered pairs: 






[w: {(Px Qx) Qy Pz, {(z,z)}   ()× 2
[w: {(Px Qx),  Qy,  Pz}{(z,z)}     ()
[wv^x_y: {Px Qx,  Qx}, {(x,x), (z,z)}   ()
[wv^x_y: {Px,  Qx}, {(x,x), (z,z)}]
]
[wv^z_y: {Px Qx,  Qz}, {(x,x), (z,z)} 
[wv^z_y: {Qx,  Qz}, {(x,x), (z,z)}]
]
]
]















Intuitively, () and () will `decompose' the formula until  is applicable. It is not hard to see that all the leaf nodes are in the shape of (w: l_1… l_k, σ). Moreover, any tableau starting from (w: Γ, σ), where Γ and σ are finite, is a finite tree, both in depth and width, since we only generate simpler formulas by the rules and the domain of the assignment is always finite. A tableau is called open if all its branches do not contain contradictions of literals at the same world, i.e. no Px⃗ and Px appear together.  

Given a tableau , we say a node (w: Γ, σ) is a branching node if it is branching due to the application of . We call (w: Γ, σ) the last node of w, if it is a leaf node or a branching node. Clearly, given a w appearing in a tableau , the last node of w always uniquely exists, since we always only select one of the denominators for the rule (). We denote the last node of w in a given  as t_w. Let 
    Dom(t_w)={[             Dom(σ') if t_w is branching;              Dom(σ)           otherwise ].

where σ is the assignment in t_w and σ' is the assignment defined as in  w.r.t. t_w.








Actually, the open tableaux are pseudo models.  
For any clean -formula θ in PNF, the following are equivalent: 


  * There is an open tableau from 
    (r: {θ}, σ_r={(x, x)| x  is free in θ}∪{(z,z)})
 where z∈ and it does not appear in θ.

  * θ is satisfiable in an increasing domain model.  




Before the main proof, we need the following handy observations about any tableau  starting from (r, {θ}, σ_r) where θ is clean. For any node (v: Γ, σ) in , we claim: 





  (1) If  () occurs in Γ, then it only occurs once and there is no  () occurring in Γ.


  (2) For all x∈ Dom(σ),  and  do not appear in Γ, thus all the occurrences of x in Γ are free.  

  (3) All the free variables x in Γ are in Dom(σ). 

  (4) If ϕ, ψ∈Γ then y is not a free variable in ϕ.

  (5) If ϕ, ψ∈Γ then y is not a free variable in ϕ and x is not a free variable in ψ. 

  (6) For any x in Dom(σ), σ(x)=x.



(1): We prove it by induction on the structure of  from the root: it is true for the clean formula θ by definition, and all the rules preserve this property since they never add any new occurrences of modalities.     

(2): Again, we prove it by induction from the root: at the root the claim is true by the definition of σ_r and the cleanness of θ (cf. also Footnote <ref>). Moreover, all the rules preserve this property. In particular, for the rule (), by induction hypothesis, for any variable x∈ Dom(σ), it only occurs free in the formulas of the numerator. Thus the occurrences of x∈ Dom(σ), if any, are also free in any ϕ_j and ψ_i[y y_i] which have less modalities to bind than the numerator. Now for x∈ Dom(σ')∖ Dom(σ), i.e.,  appears in the numerator, the statement also holds by Claim (1), since there is only one occurrence of any modality for such an x in the numerator.

(3): Again, we can show by induction: Dom(σ_r) has all the free variables in θ, and all the rules preserve this property. For the rule (), we need to check the free variables in those ϕ_j and ψ_i. Note that the only possible extra free variable in ϕ_j but not in ^x_jϕ_j is x_j but it is already included in Dom(σ'). The only possible extra free variable in ψ_i[y y_i] but not in ^y_iψ_i is y which is also already in Dom(σ').  

(4): Towards contradiction, suppose ϕ, ψ∈Γ, but y is a free variable in ϕ. According to Claim (3) y∈ Dom(σ), then by Claim (2),  does not appear in Γ, which is in contradiction with ψ∈Γ.   

(5): Similarly to (4).

(6): Obvious, by definition. 

Now we are ready to prove the main theorem. 

From top to bottom: Given an open tableau  from the root node (r:ϕ, σ_r), we define =W, D, δ, R, ρ where: 


  * W={w| (w, Γ, σ)  appears in  for some Γ and σ} 

  * w R v iff v=wv' for some v'.

  * δ(w)=Dom(t_w)

  * D=⋃_w∈ Wδ(w)


  * x⃗∈ρ(w, P) iff the atomic formula Px⃗ appears in t_w. 

where t_w is the last node of w in , as defined before. 
 
According to the rule () and the definition of δ,  is indeed an increasing domain model.[Note that it does not mean D_w is everywhere the same due to branching nodes in .] Since (z,z)∈ Dom(σ_r), D_w is not empty for any w∈ W. Moreover ρ is well-defined due to the openness of . Note that due to Claim (3), if the atomic formula Px⃗ appears in t_w then x⃗⊆ D_w. We will show that ,r is indeed a model of θ w.r.t. σ_r. 




From Claim (3), if (w: Γ, σ) appears in , then all the free variables are in Dom(σ)⊆ D_w=Dom(t_w), thus it makes sense to ask whether , w, σΓ (the assignment to the bound variables are irrelevant for the truth of formulas in Γ). To prove that , w, σΓ for all nodes (w: Γ, σ) in , we do induction on the nodes of  in a bottom-up fashion from leaf nodes, by following the the rules conversely. 


  Leaf For leaf nodes (w: l_1, …, l_k, σ), by definition of ρ, the statement holds based on the fact that σ(x)=x for all the free variable x in those literals by Claims (3), (6). 

   Supposing , w, σ l_1… l_k, then it is clear that , w, σϕ_1 …ϕ_n l_1… l_k since there is no outgoing transition from w, and D_w is not empty.  

  ,  Obvious. 

   Suppose , wv_y_i^y, σ'ψ_i[y y_i]⋀_1^nϕ_j for every y∈ Dom(σ') and i∈ [1, m], and (w: Γ, σ) is the branching predecessor where 
    Γ={^x_jϕ_j| j∈[1,n]}∪{^y_iψ_i| i∈[1,m]}∪{l_h| h∈[1,k]}.
 Note that D_w=Dom(t_w)=Dom(σ'). We need to show that , w, σΓ. 

The l_h part is as in the case of the leaf nodes. For ^x_jϕ_j, let x_j∈ Dom(σ')=D_w be the witness, we need to show that at all the successors wv_y_i^y of w, , wv_y_i^y, σ[x_j↦ x_j]ϕ_j . Now by Claim (4), all x_k such that k≠j are not free in ϕ_j. From the induction hypothesis (IH) that , wv_y_i^y, σ'ϕ_j for each wv_y_i^y, and the fact that σ[x_j↦ x_j] and σ' agree on the free variables in ϕ_j, we know , wv_y_i^y, σ[x_j↦ x_j]ϕ_j for each wv_y_i^y. Thus , w, σ^x_jϕ_j.  

As for each ^y_iψ_i, we show that for each y∈ D_w= Dom(σ'), , wv^y_y_i, σ[y_i↦ y]ψ_i. Note that y might be not in Dom(σ). By the IH, , wv_y_i^y, σ'ψ_i[y y_i]. Since σ' assigns y to y, we just need to show that σ[y_i↦ y] and σ' agree on all the free variables in ψ_i[y y_i] except y. Note that y_i is not a free variable in ψ_i[y y_i], therefore the only possible  differences between σ[y_i↦ y] and σ' are about those x_j where  x_j≠y. By Claim (5), we know that x_j is not a free variable in ψ_i[y y_i] if x_j≠ y. Therefore , wv^y_y_i, σ[y_i↦ y]ψ_i for each y∈ D_w, thus , w,σ^y_iψ_i for each i. 

It follows that ,r,σ_rθ. 


Now from bottom to top: We just need to show that the rule applications preserve the satisfiability of the formula set. Note that for () it suffices to show one outcome node is still satisfiable. In this way, there is an open tableau since if the formula sets at the leaf nodes and branching nodes are satisfiable,  then there is no contradiction among the literals. It is obvious that () and () preserves satisfiability, and one of the denominator of  preserves it too. We now show that  also does so. Supposing Γ={ϕ_1, …, ϕ_n,ψ_1,…, ψ_m, l⃗}, in some branching node (w: Γ, σ), is satisfiable, then there is a model , w and an assignment η such that η(x)∈ D_w for all x∈ and: 
    , w, η{ϕ_1, …, ϕ_n,ψ_1,…, ψ_m}     (∘)

By the semantics, we know there are a_1, …, a_n∈ D_w, such that for all the successors v of w:
, v, η[x_j↦ a_j] ϕ_j. Due to Claim (4), each x_j is not free in ϕ_k for k≠j thus we can safely obtain for all successor v of w: 
    , v, η[x⃗↦a⃗] {ϕ_1, …, ϕ_n}.      (A)


Now also by (∘) and the semantics for ^y_i, for each ψ_i and each b∈ D_w, there is a successor v^b_i of w such that 

    , v^b_i,η[y_i↦ b]ψ_i      (B)
 

From Claim (5), y_i is not one of x_j. Now from 
(A) and (B), we have for each ψ_i and each b∈ D_w, there is a successor v^b_i of w such that:   

    , v^b_i,η[x⃗↦a⃗, y_i↦ b]{ϕ_1, …, ϕ_n, ψ_i}    (⋆)
 
Now consider any y∈ Dom(σ') as in the denominator of the rule , we need to show {ϕ_1, …, ϕ_n, ψ_i[y y_i]} is satisfiable. Suppose that y∈ Dom(σ') and  η(y)=b∈ D_w. By Claim (2), y is free in ψ_i[y y_i], thus by (⋆):

    , v^b_i, η[x⃗↦a⃗]{ϕ_1, …, ϕ_n, ψ_i[y y_i]}






Therefore, {ϕ_1, …, ϕ_n, ψ_i[y y_i]} is satisfiable for each y∈ Dom(σ'). This completes the whole proof. 


A strong finite tree property then follows: [Interested readers may go back to Footnote <ref>.]

If an -formula ϕ (with length n) is satisfiable, then it is satisfiable in a finite tree model ,w, w.r.t. an assignment σ such that
|W^|≤ n^4n, |D^|≤ n, ρ(P, w)⊆ D_w^k (if P is k-ary), the depth of the tree is bounded by 2|ϕ|, and σ(x)∈ D^_w for each free variable x in ϕ.  

The upper bound for the depth of the tree comes from the bound on the length of the PNF of ϕ. The (very loose) upper bound on the size of W^ comes from the fact that each node in the tableau may contain up to n modalities and each modality may have n-successors (due to the size of the domain), and the depth of the tableau is up to 2n. As in normal modal logic <cit.>, we can force a binary branching tree by an -formula to get an exponential-sized model. 




Satisfiability problem of -formulas is -complete. 

(Sketch)
Note that standard modal logic formulas can be translated into our  by using 0-ary predicate P for each propositional letter. For example, p can be translated as ^y P. The -hardness then follows since satisfiability for basic normal modal logic is -complete <cit.>. For the upper bound, note that to rewrite a formula into PNF and to reletter the formula into a clean shape are efficient in space, and the length of the resulting formula is still linear in the length of the original formula. From then on, a standard -algorihm traversing a tree structure including all the the possible -branches suffices, as in standard modal logic, with some care about efficiently encoding the descriptions of each node and the result of the consistent checking.   


Our notion of the tableaux is closely related to two-player satisfiability games and alternating-tree automata <cit.>, which will give us the algorithmic tools for  in the future.

We conjecture that a similar tableau method would work for , with more careful assignment management by selecting representatives of provably equivalent variables w.r.t. ≈ as the local domain. We leave it to the extended version of the paper.    










































§ A NEW EPISTEMIC LOGIC 
 

In this session, we go back to the motivating epistemic setting, and give a complete axiomatization of our logic over epistemic models.


 §.§ Epistemic language

To ease the presentation of the proof system,  we also include the standard modality  as a primitive modality in the following language :[In the axiomatization we will make use of . If we do not introduce them explicitly then every time we need to use ϕ where x is not free in ϕ.]

    ϕ::= x≈ y | Px⃗|ϕ| (ϕϕ)|ϕ|ϕ

Recall that  is equally expressive as . In the epistemic setting, the intended reading of ϕ is i knows that ϕ, and the intended reading of ϕ is that i knows something such that ϕ. The semantics is as before, but we have two extra conditions on the model: 


  * Each R is an equivalence relation as in (idealized) standard epistemic logic S5. We also write ∼ for R. 

  * For all w∈ W, D_w=D.

Note that for an increasing domain model , if R is an equivalence relation, then for any two worlds w,v such that wRv, we have D_w=D_v. Therefore, we can simply assume that there is a constant domain over the whole model.[Without the condition of constant domain, different partitions w.r.t. ∼ may still have different local domains.] We also call such models S5-models, following the terminology in epistemic logic. ϕ∈ is valid if for any pointed S5-model ,w, any assignment σ, ,w,σϕ. Note that in constant domain models, we no longer need to give the restriction on the assignment: σ(x)∈ D=D_w for all assignment σ, all w∈ W_ and all x∈. 

 over S5-models is a quite powerful language. As we mentioned, the semantics for  is in line with the mention-some reading. We can also introduce a modal operator  based on mention-all semantics as below: 

    [                                           , w, σϕ                                                 ⇔ for each d∈ D, either, w, σ[x↦ d]ϕor, w, σ[x↦ d]ϕ;                                                   ]

Intuitively, ϕ means for all objects in the constant domain D, the agent knows whether ϕ, e.g., I know who came to the party means that for each person in concern, I know whether (s)he came or not. In terms of , ϕ is essentially ∀ x (ϕϕ). Note that  and  not only differ only in the quantifiers. On the other hand, the natural ∀-version of  is defined:

    [                  , w, σ^∀ xϕ                            ⇔ for each d∈ D, , w, σ[x↦ d]ϕ;                              ]

, w, σ^∀ xϕ only says that of each object, the agent knows that it satisfies property ϕ(x), which differs from the semantics of the mention-all operator.

There is also a very natural generalization of our  mention-some operator with multiple variables: ^x⃗: 

    [                                   , w, σ^x_1⋯ x_nϕ                                                  ⇔ there exist d_1,⋯, d_n∈ D such that , t, σ[x⃗↦d⃗]ϕ;                                                    ]



,^∀ x, and ^x⃗ can all be defined in  over S5-models: 








The following equivalences are valid for any -formula ϕ, based on the fact that ϕϕ and ϕϕ are valid on S5 models: 


  * ϕ (^x (ϕϕ))

  * ^∀ xϕϕ 

  * ^x⃗ϕ^x_1⋯^x_nϕ














 §.§ Proof system

In the rest of this section we propose a Hilbert-style proof system for the equality-free  and then extend it to a proof system for . 

First note that the following “K axiom” for  is not valid on S5-models, since the witnesses object for x in   (ϕ→ψ) and ϕ may be different: 

    (ϕ→ψ)→ (ϕ→ψ)

Therefore the modal logic of  is not normal, as  expected. We propose the following proof system: 



	
		2cSystem 

		
		Axioms   

		
		    all axioms of propositional logic

		    (ϕ→ψ)→ (ϕ→ψ)

		    ϕ→ϕ 

		    ϕ→ϕ

		    ϕ→ϕ

		   (ϕ[y x]) →ϕ (if ϕ[y x] is admissible)
	
             ϕ→ϕ (if x∉FV(ϕ))

   ϕ→ϕ  

            ⊤




	
Rules:

     φ,φ→ψψ       ⊢φ→ψ⊢φ→ψ 




where ϕ[y x] is admissible if no free occurrence of x in ϕ is in the scope of a modality binding y. 

The axioms are quite intuitive as they are, but they can be understood even more easily if we put them in some context to give concrete intuitive readings. For example, supposing we use ϕ(x) to express that the agent knows how to achieve  ϕ, then ,  express the (idealised) introspections of such goal-directed know-how: if you know how then you know you know how, and if you do not know how then you know you do not;  says that if you know that a particular way can achieve ϕ for sure, then you know how to achieve ϕ;  trivializes know-how to know-that, if x is irrelevant to ϕ;  says that if you know how to achieve ϕ then you know how to ensure that you know ϕ;  says we know tautologies;[This is a technical axiom to recover the necessitation rule for K from . Alternatively, we can also just include the necessitation rule for  instead of .] and  is the monotonicity rule for know-how. 


Actually, all the above axioms have incarnations in the logic system 𝕊𝕂ℍ of know-how proposed in <cit.>. Modulo the replacement of the know-how operator  by , all the axioms and rules in 𝕊𝕂ℍ are derivable in , except the composition axiom 𝙺𝚑𝙺𝚑𝚝𝚘𝙺𝚑 (ϕ→ϕ), which indeed captures the characteristic feature about know-how: the witness strategies can be composed. 


It is routine to verify the soundness, assuming the familiarity of first-order modal logic over S5-models.  

 is sound over S5 models. 

 is very powerful, as demonstrated by the following proposition: many usual “suspects” can be derived. 

The following theorems are derivable and the rules are admissible in : 





     ϕ→ϕ          ϕϕ (x∉FV(ϕ)) 

     ⊢φ⊢φ        ⊢φ⊢φ

    ⊢φψ⊢χ(ψ)χ(ϕ)          ⊢φ→ψ⊢φ→ψ (x∉FV(ψ)) 

    ⊤           ϕϕ[y x] (y  is not in ϕ))
 
    ϕ→ϕ         ϕ→ϕ





(Sketch)
 is based on  and . ϕ→ϕ is a special case of  when y=x. Together with  we have . Now from  and  we have . Then based on  and ,   and  follow from . The rule of Replacement of Equals () can be proved inductively based on .  is based on , ,  and .  The standard introspection axioms of  are special instances of inspection axioms  and  based on  and .[ can also be derived from  and  in the system  like in the case of propositional S5 system.] Let us now look at , which is the renaming axiom for bound variables. Right-to-left can be derived by starting with : ⊢(ϕ[y x])→ϕ, then since y does not appear in ϕ, we have ⊢(ϕ[y x])→ϕ by . For the other direction, note that ϕ=(ϕ[y x])[x y] if y is not in ϕ. Then since (ϕ[y x])[x y] is admissible, by , ⊢(ϕ[y x])[x y]→ϕ[y x], namely ⊢ϕ→ϕ[y x]. Then by , ⊢ϕ→ϕ[y x].   




Now we know that the S5 system of  is a subsystem of . We may also view ,  as analogues of the following axiom and rule respectively in first-order logic: 

    ∀ x ϕ→ϕ[y x]     ⊢ϕ→ψ⊢ϕ→∀ xψ(x∉FV(ϕ))

 is the rule of replacement and  allows us to reletter the bound variables, as in . Moreover, the Barcan formula (∀ xϕ→∀ xϕ), over S5-models, can be expressed as: 
    ϕ→ϕ
 which is also derivable in  due to .    

The following provable formula plays a role in the later completeness proof.

⊢_ (ϕ→ψ) →(ϕ→ψ).


Consider the contrapositive of the formula to be proved: 

(ϕψ)→ (ϕψ).
It is routine to show that ⊢(ϕψ) → (ϕψ). Now by  , , and , ⊢ϕϕ and ⊢ψψ. Therefore, by , ⊢(ϕψ)→ (ϕψ). 


In the following we define the Hilbert system  for  by extending  with the following two extra axiom schemata:


	

		
		Axioms   

		








            x≈ x

            x≈ y → (ϕ→ψ) if ϕ and ψ only differ in that
     some free occurrences of x in one formula 

           are replaced by free occurrences of y in another.











 is sound. 

It is routine to show: 

The following are provable in :


    x≈ y→ y ≈ x         x ≈ y y≈ z → x≈ z

    x≈ y→ (x≈ y)        x≉y→ (x≉y) 



  and  are due to . To derive , we first have ⊢ (x≈ x) by  and . By  we have ⊢ x≈ y→ ( (x≈ y)→ (x≈ x)). Therefore  is provable. 
 
For , from  we have ⊢ x≉y→ x≉y, thus ⊢ x≉y→  x≉y by  and . Note that ϕ→ϕ is derivable by  and . Therefore by taking ϕ=x≉y and using  we have ⊢. 





§ COMPLETENESS
 
Let us first focus on the completeness of  without axioms for equalities.  

We first extend the language of  with countably infinitely  many new variable symbols. Call the new language ^+ and the variable set ^+. In the following, we say a set of formulas is ^+-consistent if it is -consistent w.r.t. the extended language ^+. 



A set of ^+ formulas has ∃-property if for each ϕ∈^+ it contains a “witness” formula ϕ→ϕ[y x] for some y∈^+ where ϕ[y x] is admissible. 




The canonical model is a tuple W^c, D^c, ∼^c, ρ^c

 where: 


  * W^c is the set of maximal ^+-consistent sets  with ∃-property,

  * D^c=^+,

  * s∼^c t iff (s)⊆ t where (s):={ϕ|ϕ∈ s},

  * x⃗∈ρ^c(P,s) iff Px⃗∈ s.


It is routine to show that ∼^c is an equivalence relation, by using axioms , , and . 




If ψ∉s ∈ W^c then there exists a t∈ W^c such that s∼^ct and ψ∈ t.  


It is routine in normal modal logic to show that if ψ∉s then (s)∪{ψ} is consistent. Now we show that (s)∪{ψ} can be extended to an ^+-maximal consistent set with ∃-property. We follow the general strategy in <cit.> by adding witness formulas one by one. 

Let θ_0=ψ. We enumerate -formulas as: ϕ_1, ^x_2ϕ_2, … We define θ_k+1 as the formula: 

    θ_k (^x_k+1ϕ_k+1→ϕ_k+1[y x_k+1])

where y is the first variable in a fixed enumeration of ^+ such that ϕ_k+1[y x_k+1] is admissible and ^x_k+1ϕ_k+1→ϕ_k+1[y x_k+1] is consistent with {θ_k}∪(s). 

We now show that such θ_k+1 always exists (i.e., such a y exists), if {θ_k}∪(s) is consistent. Towards a contradiction, suppose that {θ_k}∪(s) is consistent but there is no such a y, i.e., for each y∈^+ such that ϕ_k+1[y x_k+1] is admissible there are χ_1,…,χ_n∈(s) such that 
    ⊢χ_1…χ_n→ ((^x_k+1ϕ_k+1→ϕ_k+1[y x_k+1])→θ_k).


By  and  and the fact that χ_i∈ s for 1≤ i≤ n, it is routine to show that ((^x_k+1ϕ_k+1→ϕ_+1[y x_k+1])→θ_k) is also in s. By  again, 

    (^x_k+1ϕ_k+1→ϕ_k+1[y x_k+1])→θ_k    (⋆)
 is in s for all y such that ϕ_k+1[y x] is admissible. 

Note that s has the ∃-property, therefore, ^x_k+1ϕ_k+1→ϕ_k+1[y^* x] is in s for some particular y^* such that ϕ_k+1[y^* x_k+1] is admissible. By Proposition <ref>, (^x_k+1ϕ_k+1→ϕ_k+1[y^* x_k+1]) is in s. By (⋆), we have θ_k is in s, thus θ_k∈(s) which is in contradiction with that {θ_k}∪(s) is consistent. 

Now since {θ_0}∪(s)={ψ}∪(s) is consistent, we can indeed construct all the θ_k. Let Γ={θ_k | k∈ℕ}∪(s). Γ is consistent and the ∃-property is essentially built-in.  We can then extend it into an ^+-maximal consistent set t. It then follows that s∼^ct and ϕ∈ t.   

Now comes the truth lemma. 
 Let σ^* be the assignment such that σ^*(x)=x for all x∈^+. For any ϕ∈^+, any s∈ W^c: 

    ^c, s, σ^* ϕϕ∈ s



We do induction on the structure of the formula ϕ. 


  Px⃗ By the definition of ρ^c and σ^*, it is obvious. 

  BoolBoolean cases are trivial.  

  ψ Routine, based on Lemma <ref>.  

  ψSupposing ψ∈ s, by ∃-property of s there exists ψ[y x]∈ s for some y such that ψ[y x] is admissible. By , ψ[y x]∈ s. Supposing s∼^c t, we have ψ[y x]∈ t due to the definition of ∼^c. By , ψ[y x]∈ t. By IH, , t, σ^* ψ[y x]. Due to the definition of σ^* and the fact that ψ[y x] is admissible, , t, σ^*[x↦ y] ψ for all t∼ s. Thus ,s, σ^*[x↦ y]ψ, it follows that , s, σ^* ψ. 

Suppose ψ∉s, by , ψ[y x]∉s for each y such that ψ[y x] is admissible. By IH, 

^c, s, σ^*ψ[y x] for each y such that ψ[y x] is admissible. Due to the special assignment σ^* such that σ^*(y)=y, it is  clear that ^c, s, σ^*[x↦ y]ψ for each y such that ψ[y x] is admissible. 

Now consider any y' such that ψ[y' x] is not admissible, then by , we can reletter the modalities of y' in ψ with some fresh variable to obtain ψ' such that ⊢ψψ' and ψ'[y' x] is admissible. Now by , ψ'∉s. We can then repeat the reasoning above to obtain ^c, s, σ^*[x↦ y']ψ' for this y'. Since ⊢ψψ', by soundness, ^c, s, σ^*[x↦ y']ψ. Therefore for each y, no matter whether ψ[y x] is admissible,  we have ^c, s, σ^*[x↦ y]ψ.
Therefore ^c, s, σ^* ψ.  
  


Note that not every ^+-consistent set of formulas can be extended into a world in ^c, e.g., {ϕ(x)}∪{ϕ(x)| x∈^+} cannot be extended consistently to obtain the ∃-property. However, every -consistent set can be extended into a world in W^c by adding the witness one by one using the new variables (cf. <cit.>). 

Every -consistent set of -formulas can be extended into an ^+-maximal consistent set of ^+-formulas with ∃-property. 








Now based on Lemma <ref> and Lemma <ref>, every -consistent set is satisfiable by some pointed model and an assignment. The completeness follows: 

 is strongly complete w.r.t.  over S5 models.  

The completeness of  is quite routine based on the completeness proof of . We only sketch the idea here following <cit.>. 

 is strongly complete w.r.t.  over S5 models.  





Unfortunately,  over (constant-domain) S5 models is indeed too powerful, we can code first-order formulas by replacing each quantifier in a first-order formula in the prenex form by  or  respectively. We can show that this translation preserves the satisfiability.  For example, we can translate ∃ x ∀ y ϕ (ϕ is quantifier-free) into an  formula ϕ, which is equivalent to the first-order modal formula ∃ x ∀ y ϕ over S5 models, and it implies ∃ x∀ y ϕ by reflexivity. If a first-order formula is satisfiable then we can build a single-world S5 model such that the translated -formula is also satisfiable. On the other hand, if the translated -formula is satisfiable in some pointed  S5 model, then we can just pick the designated world in that model as a first-order structure to satisfy the original first-order formula. This leads to the  undecidability of  due to the undecidability of first-order logic:

 is undecidable over S5 models. 

























































§ FUTURE WORK



Due to limited space, we omit several proofs and some additional results, and leave them to the extended version of this conference paper.




We believe that this is only the beginning of an interesting story. On the technical side, we may study potential properties of  such as interpolation, frame definability, characterization over finite models, axiomatization and (un)decidability on various frame classes (with or without extra constant symbols). Although the full  over S5 models is undecidable, the concrete “propositional” know-wh logics mentioned in the introduction are usually decidable. One explanation is that the existing know-wh logics are often similar to one-variable fragments of the first-order modal language, which may lead to decidability over S5 and other models <cit.>, e.g., the conditional  knowing value formulas  (ϕ,c) discussed in <cit.> are essentially ∃ x (ϕ→ c=x). A detailed comparison with known guarded-like fragments with extra frame constraints will be very useful to understand the new framework more deeply. Moreover, we believe our techniques and results can be generalized to poly-modal (multi-agent) settings. It then makes sense to discuss the mention-some version of common knowledge operator C^x:=∃ x C where C is the propositional common knowledge operator.[This is a rather strong notion of common knowledge, e.g., we commonly know how to prove the theorem in this sense means a fixed proof is also commonly known.] There is also a clear similarity with modal logic over neighbourhood models, which is worth exploring. 























eptcs

















































































































