Quantifiers and Operations on Modalities and Contexts

Tom Costello Computer Science Department Stanford University Stanford, CA 94305

Anna Patterson Computer Science Department Stanford University Stanford, CA 94305

Abstract

We can reason about theories, as well as in them. Many natural phenomena can be captured by theories, often by introducing a modality, true just of the theory. Rather than treat these phenomena as the sentences true in this modality, we can treat the entire theory or modality as an object. This point of view was proposed by McCarthy, who proposed calling these reified modalities contexts.

Contexts, viewed as theories or modalities, have structural properties, and associated natural structural operations, such as union and intersection. These structural properties are most naturally captured by an algebra, reminiscent of dynamic algebra. This algebra has a set of operations that can be applied to contexts to form new contexts.

We introduce an algebra, reminiscent of dynamic algebra, but which acts on modalities, not relations. This algebra allows the construction of modalities from simpler modalities. We use the natural correspondence between a modality and the underlying accessibility relation to make this connection. Thus the operations on modalities are induced by operations on the underlying relations which respect the properties required of modalities.

It becomes possible then to have a larger space of modalities than those that are explicitly named. We add quantifiers that range over modalities, so that we can state propositions like, “no context with the property P exists”, or “all contexts obey Q”. We give an axiomatization of these quantifiers which we show is complete with respect to a natural semantics.

1 PUTTING MODALITIES TOGETHER

1.1 MODALITIES

Modal operators are widely used to capture intensional aspects of knowledge, belief, temporality and action. They capture the notion that there may be different viewpoints from which a particular phenomena can be seen. These different vantage points can be agents beliefs, points in time, differing stages of knowledge, or different contexts.

A unifying semantics for these notions was proposed by Kripke. The essential idea is that a new syntactic operator, □, is semantically modeled by a set of possible worlds, W, and an accessibility relation on worlds R. Each world is given an assignment to propositional atoms^{1}, and the truth condition for □ϕ at a world w, is defined as the truth of ϕ in all worlds accessible from w.

A natural extension of this idea is to allow more than one modality. One popular use of multi-modal systems is to have modalities which represent the beliefs of each member of a set of believers. (Halpern 1995) provides a recent overview of this approach. It is then customary to label each modal operator with a distinguishing subscript. If □_{Sally} denotes the beliefs of Sally, and □_{Harry}, the beliefs of Harry, then if Sally believes that Harry believes that Sally likes Harry, we would write, □_{Sally}□_{Harry}Likes(Sally, Harry).

1Alternately, each world can have an associated first order structure, or even a non-standard semantical structure, such as a three valued model. The choice of a propositional valuation is only for simplicity as most of these results extend readily to richer valuation functions.

1.2 MAKING NEW MODALITIES FROM OLD

In this paper, we ask the broad question “What modalities should exist” and “Given that we already have a certain set of modalities, what other modalities must also exist”. Thus, we differ from previous work on indexed modalities in that we are interested in studying the structure of modalities themselves, not in stating facts that require multiple modalities for their expression.

We can imagine that we have the two modalities □_{Sally} and □_{Harry} that we considered earlier. It seems obvious that there is a set of beliefs that they share. This set of beliefs seems to be a well behaved modality. Other modalities are the union of the beliefs, the propositions they do not believe, and many others.

One way of posing the question of what other modalities might exist, is to ask “What would a system that quantified over modalities look like?” We first present a simple system that allows us to quantify over modalities, but gives us no way to generate these modalities. We then look at natural ways to generate modalities, using some notions from dynamic algebra.

1.3 IDENTITY CONDITIONS ON MODALITIES

As well as a theory of what modalities exist, we also need an identity criterion for modalities. We take the most obvious criterion, extensionality. That is, we consider two modalities equal if they agree on all sentences.

c = c′ =^{def} for all ϕ.□_{c}ϕ ≡ □_{c′}ϕ

We consider what structural properties this decision has on the underlying relations. We show it identifies all bisimilar models.

1.4 PLAN OF PAPER

We first look at Kripke models, which provide the basic model theory of modalities.

We give a sound and complete axiomatization for arbitrary universes of relations. This gives a simple system which allows quantification over modalities, but which does not have any closure conditions on what modalities should exist.

We then suggest three operators that make new modalities from old modalities. Therefore our universe of modalities will include all modalities definable using these operations. We give an axiomatization of these operators that we show is sound and complete for universes that include all first order definable functions on modalities. This shows that these three operators are sufficient to define all first order definable functions on modalities.

To prove this theorem we have to characterize all first order definable functions on modalities. We consider when the modalities Kripke models define are equivalent. This needs the notion of bisimulation. We then look at what functions on the relations in Kripke models give rise to functions on modalities. We then prove a theorem which characterizes the first order definable functions on relations that give rise to functions on modalities. We show that the syntactic class of first order definable functions on modalities can be captured by our three operations on modalities.

We conclude by looking at previous related work in AI, and suggesting some natural uses for the operators we have introduced.

2 MODALITIES AND RELATIONS

We now state the standard definitions of Kripke structures, and review how Kripke models can give a semantics to a normal modality.

2.1 KRIPKE MODELS

We define propositional modal languages in the usual way.

Definition 1 A propositional modal language over a set P of propositional atoms is the smallest set of formulas containing each element of P, and ¬φ, φ ∧ ψ, □φ, where ϕ and ψ are formulas.

We can define the other propositional connectives, ∨, →, ≡, and the modal operator ◇ϕ = ¬□¬ϕ in the usual way.

Definition 2 A Kripke structure for propositional modal logic over a set P of propositional atoms is a triple ⟨W, R, V ⟩ where W is a non-empty set (the set of worlds), R is a binary relation on W and V is a function assigning to every world a set of propositional atoms from P.

Definition 3 The satisfaction relation ⊧ for K = ⟨W, R, V ⟩, a Kripke structure over a set of propositional atoms P is a relation between worlds and modal formulas. We define this relation inductively over the structure of a formula. Thus, for any w ∈ W,

w, K ⊧ p  ≡  p ∈ V (w)
w, K ⊧ ¬φ  ≡  w, K |̸= φ
w, K ⊧ φ ∧ ψ ≡  w, K ⊧ φ and w, K ⊧ ψ
w, K ⊧ □φ  ≡ ∀w′ ∈W.wRw′ implies w′, K ⊧ φ

For the definition of negation we read, w, K |̸= φ as “it is not the case that w, K ⊧ φ”.

Definition 4 Let K = ⟨W, R, V ⟩ be a Kripke structure, then a formula φ is satisfied in K if and only if ∃w ∈ W. w , K ⊧ φ. A formula φ is valid in K, written K ⊧ ϕ, if and only if ∀w ∈ W. w , K ⊧ φ. A formula φ is valid if and only if φ is valid in all Kripke structures.

3 QUANTIFICATIONAL MODAL LOGIC

We look at quantifying over modalities in a modal logic. For simplicity, we start with the propositional case of the modal logic K^{2} with multiple modalities. We extend multi-modal K to also allow modal variables, which we write as subscripts, such as ◇_{x}. We write modal constants normally, as ◇_{c}, for the constant c. We then extend this language to consider quantifiers over modalities or contexts. We do not allow quantification over objects as our language is propositional. We also do not allow quantification over propositions as our language is not second order in this respect.

Later we use an alternate notation, ist(c, ϕ), where c plays the role of a modal constant or subscript. This allows a more traditional syntax in some respects.

3.0.1 Syntax

The symbols of our language, denoted L_{ℂ,ℙ} include a countable set of propositional letters ℙ, a countable set of modal constants ℂ, and a countable set of modal variables which we denote by x_{j} and y_{j} where j ∈ ω. We also include symbols for the usual classical connectives, ∧ and ¬, the modal symbol □, parentheses ) and (, and lastly the quantifier symbol ∀. We use ϕ → ψ as an abbreviation for ¬(ϕ ∧ ¬ψ) as usual.

The set of formulas of our language is the smallest set containing

• All propositional letters, ℙ.

• If ϕ and ψ are formulas, then (ϕ ∧ ψ) and (¬ψ) are formulas.

• If ϕ is a formula, and i is a modal constant, or a modal variable, then (□_{i}ϕ) is a formula.

• If ϕ is a formula, and x is a modal variable, then (∀x.ϕ) is a formula.

In the above definition, the formulas ϕ and ψ are subformulas of the resulting formula, furthermore, the sub-formula property is transitive. We say an occurrence of a variable x is bound in a formula ϕ, if it is contained in a sub-formula of ϕ, of the form ∀x.ψ. We assume variables are renamed to avoid clashes in the usual way. We say an occurrence of a variable x is free in a formula if it is not bound. We call a formula with no free variables a sentence.

3.1 SEMANTICS

The usual semantics of modal logic we just presented and is based around a set of worlds, and a binary relations over worlds. For multi-modal models we need a set of binary relations over worlds, one for every modal constant. Hence every modality is associated with a relation, which we call its accessibility relation. We also have a valuation function, that is a function that assigns a set of propositional atoms to each world.

Definition 5 A structure for propositional quantified modal logic over a set P of propositional atoms is a quadruple ⟨W, U, V, A⟩ where W is a non-empty set (the set of worlds), U is a non-empty universe of binary relations on W and V is a function assigning to every world a set of propositional atoms from P and A is an assignment function from modal variables and constants to elements of U.

We often denote the accessibility relation of A applied to constant c, as A_{c}, similarly A_{x} for modal variable x. We write A_{i} to mean that i is either a modal constant or variable.

The semantics of quantified modal logic, i.e. our language L_{ℂ,ℙ}, is defined as follows.

Definition 6 The satisfaction relation ⊧ for S = ⟨W, U, V, A⟩, a structure for quantified modal logic over a set of propositional atoms P is a relation between worlds and quantified modal formulas. We define this relation inductively over the structure of a formula.

2classical propositional logic plus the modality □ with modal distribution and necessitation

Thus, for any w ∈ W,

w, S ⊧_{∀} p  ≡ p ∈ V (w)
w, S ⊧_{∀} ¬ϕ  ≡ w, S |̸=_{∀} ϕ
w, S ⊧_{∀} ϕ ∧ ψ ≡ w, S ⊧_{∀} ϕ and w, S ⊧_{∀} ψ
w, S ⊧_{∀} □_{i}ϕ ≡ ∀w′.wA_{i}w′ implies w′, S ⊧_{∀} ϕ
w, S ⊧_{∀} ∀x.ϕ ≡ ∀R ∈ U.w, S[A[R/x]/A] ⊧_{∀} ϕ

where S[A[R/x]/S] is the structure S except that A has been replaced with A[R/x] where A[R/x] is like A with the possible difference that it assigns the relation R to the variable x.

Definition 4 lifts naturally to our definition of satisfaction in the quantified modal logic setting. For the remainder we use those terms as defined.

We have placed no restrictions on the universe of relations U. We now ask the question, what relations should be included in the universe U.

3.2 JUST CONSTANTS

We can follow the lead of first order logic by considering all non-empty domains of relations possible. For quantified modal logic this is not an appropriate long-term solution because our domains should satisfy certain closure conditions. That is a relation can be constructed from other relations using natural operations that we define in Section 3.7 such as union. This means that we can construct a relation by unioning two relations in the universe but find that its union does not exist in the universe. We would like our universes to be closed under all appropriate operations, but first we need to study the simple case of universes and determine what are the “appropriate operations” for combining modalities.

As a starting point, we give an axiomatization of the case where there is no restriction placed upon the universe of relations.

3.2.1 Axiomatics

The following are the axioms and rules of our minimal system, which we call ∀. We assume a Gentzen style system for concreteness.

All valid principles of propositional logic

⊢ □_{i}(ϕ → ψ) → (□_{i}ϕ → □_{i}ψ) Modal Distribution

\frac{⊢ ϕ}{⊢ □_{i}ϕ} Necessitation

\frac{Γ ⊢ ψ}{Γ ⊢ ∀x.ψ}

provided that x does not occur free in Γ

\frac{Γ ⊢ ∀x.ψ}{Γ ⊢ ψ[i/x]} where ψ[i/x] is the result

of substituting each free occurrence of x by i

We define logical derivation in the standard way, and denote it ⊢_{∀}. We say Γ ⊧_{∀} ϕ, read, ϕ is a valid consequence of Γ, if, for all models S = ⟨W, U, V, A⟩ and for all worlds w in W, that satisfy each formula in Γ, it is the case that w, S ⊧_{∀} ϕ. We now show soundness and completeness for this basic case.

Theorem 7 If ϕ is a sentence in L_{ℂ,ℙ}, then ⊢_{∀} ϕ implies ⊧_{∀} ϕ.

Proof: We show that the axioms are satisfied in all models and that the rules of inference preserve validity. Let S be an arbitrary quantified modal logic model i.e. some S = ⟨W, U, V, A⟩.

We have one non-propositional axiom.

• □_{i}(ϕ → ψ) → (□_{i}ϕ → □_{i}ψ). We show this is satisfied in all models, by deriving the right-hand side from the definition of the left hand side and the definition of ⊧_{∀}.

First assume that S models □_{i}(ϕ → ψ) which expands to w, S ⊧_{∀} □_{i}(ϕ → ψ) ≡ ∀w′.wA_{i}w′ implies w′, S ⊧_{∀} (ϕ → ψ) By the definition of entailment of → this gives, ∀w′.wA_{i}w′ implies

(w′, S ⊧_{∀} ϕ implies w′, S ⊧_{∀} ψ) We now assume the left part i.e. ∀w′.wA_{i}w′ implies w′, S ⊧_{∀} ϕ to obtain∀w′.wA_{i}w′ implies w′, S ⊧_{∀} ψ Discharging our assumptions gives w, S ⊧_{∀} □_{i}(ϕ → ψ) → (∀w′.wA_{i}w′ implies w′, S ⊧_{∀} ϕ) → (∀w′.wA_{i}w′ implies w′, S ⊧_{∀} ψ) Which by the definition of → and □ gives w, S ⊧_{∀} □_{i}(ϕ → ψ) → w, S ⊧_{∀} □_{i}ϕ → □_{i}ψ.

We have two quantifier rules.

• Our inductive assumption gives us that Γ ⊧_{∀} ψ. Hence, in all models S where Γ is satisfied, ψ is satisfied. We also given that x does not occur in Γ; hence the A_{x} component of any satisfying world in S is never referenced when satisfying Γ. Therefore any A_{x} will suffice. This is just the condition under which Γ ⊧_{∀} ∀x.ψ.

• Our inductive assumption gives us that Γ ⊧_{∀} ∀x.ψ. Hence, in all models S the worlds w where Γ is satisfied, ∀x.ψ is satisfied. The definition of satisfaction for ∀ gives us that w, S ⊧_{∀} Γ implies ∀R ∈ U.w, S ⊧_{∀} ψ. But we note that this implies that in particular the interpretation of i, can be used, giving. w, S[A[i/x]/A] ⊧_{∀} ψ. This is equivalent to w, S ⊧ ψ[i/x], for each free occurrence of x, as required.

We now show the other rules preserve validity. We assume the assumptions logically entail the premises and derive the conclusion from the assumptions.

• Propositional rules. Immediate.

• Nec: If ϕ is true without assumptions, then it is true in all world/model pairs. Therefore, it is true in all worlds in a particular model. In that model, we have □_{i}ϕ, as it is true in all i accessible worlds.

Theorem 8 If ϕ is a sentence in L_{ℂ,ℙ} and Γ is a set of sentences of L_{ℂ,ℙ}, where Γ ⊧_{∀} ϕ, then Γ ⊢_{∀} ϕ

Proof: It suffices to show that every consistent set Σ of sentences has a model. We take any consistent set of sentences Σ, and extend it to a maximal consistent set of sentences Σ′.

We then add a countable number of new modal constants C′ = {c′_{n}|n ∈ ω}, as witnesses for every existential. A countable number suffices as our language L_{ℂ,ℙ} is countable. This gives the new set of sentences, Σ′′, in the language L_{ℂ∪C′,ℙ}. We note that Σ′′ is a maximal consistent set, as we chose each constant to be a witness for an existential that was already completely defined.

We now construct a model M = ⟨W, U, V, A⟩, from this set of sentences Σ′′ and show that this model contains a world w that satisfies all of the sentences in Σ.

First we construct a function I from which M will be defined:

Let s, s′ denote finite sequences of modal constants and denote concatenation by ·. The empty sequence is denoted ϵ and the singleton sequence is denoted by its element.

We now define I′.

• I′(ϵ) = Σ′′

• I′(c) = {φ | □_{c}φ ∈ Σ′′} where c ∈ ℂ ∪ C′.

• I′(c · s′) = {φ | □_{c}φ ∈ I′(s′)} where c ∈ ℂ ∪ C′

We can associate with a set of sentences Δ its set of maximal consistent extensions of Δ. Thus I(s) returns this set of maximal consistent extensions of I′(s). I and I′ are deeply related for φ ∈ I′(s) if and only if ∀w.w ∈ I(s) implies φ ∈ w. We need this correspondence when appealing to the construction of M in the completeness proof.

From left to right we only use that I(s) is the maximal consistent extensions of s. From right to left we use the property of intersection and maximal consistency to conclude that if I′(s) is a theory (i.e. logically closed) then it is equal to the intersection of its maximal consistent extensions. To show that I′(s) is a theory we need that it only obeys necessitation and distribution. For this we use induction and the base case that Σ′′ is closed under these rules.

Construction of W: We take as our set of worlds W, the union of the range of I. This means each world is a maximal consistent set of sentences.

Construction of A: We construct A_{c} for each c ∈ ℂ ∪ C′ as the relation, {⟨w, w′⟩|∃s.w ∈ I(s) ∧ w′ ∈

I(c · s)}.

Construction of U: We take as our universe of relations U = {A_{c}|c ∈ ℂ ∪ C′}.

Construction of V: V (w) if and only if p ∈ w.

At this juncture technically, we must show M is a quantified modal model by showing that W and U are non-empty. W is non-empty by construction and that U is non-empty follows from the non-emptiness of W.

Finally we need to show that the restriction of this model M = ⟨W, V, U, A⟩, to the constants in ℂ is a model of Σ.

We show this by induction on the structure of sentences in Σ′′. We show that every set of sentences w in I(s), is satisfied in M at w by showing that ∀w.∀γ.[γ ∈ w if and only if w, M ⊧_{∀} γ]. As we are doing our induction on sentences, rather than formulas, we will need to use the fact that we introduced sufficient witnesses so that every existential had a witness.

• γ = p. We immediately get that p ∈ w if and only if w, M ⊧_{∀} p because w, M ⊧_{∀} p if and only if p ∈ V (w) and our structure is defined such that p ∈ w if and only if p ∈ V (w).

• γ = ϕ ∧ ψ. We have by assumption that ϕ ∈ w if and only if w, M ⊧_{∀} ϕ and ψ ∈ w if and only if w, M ⊧_{∀} ψ. Since w is a set of maximal consistent set of sentences then ϕ∧ψ are in w and by definition of ⊧_{∀} and the hypotheses we have that w, M ⊧_{∀} ϕ ∧ ψ.

• γ = ¬ϕ. We have that ϕ ∉ w if and only if w, M |̸=_{∀} ϕ. By the definition of satisfaction in a model w, M ⊧_{∀} ¬ϕ and because w is maximal consistent ¬ϕ ∈ w.

• γ = □_{c}ϕ. We need that □_{c}ϕ ∈ w if and only if w, M ⊧_{∀} □_{c}ϕ. We assume that ϕ ∈ w if and only if w, M ⊧_{∀} ϕ.

The satisfaction condition for w, M ⊧_{∀} □_{c}ϕ is ∀w′.wA_{c}w′ implies w′M ⊧_{∀} ϕ.

Let s be any sequence such that w ∈ I(s). Then, consider s′ = c · s. By construction ϕ ∈ w′ ∈ I(s′) if and only if wA_{c}w′, therefore all accessible worlds model ϕ, hence w, M ⊧_{∀} □_{c}ϕ. Our induction hypothesis gives us that all accessible worlds w′ have ϕ as an element.

Now □_{c}ϕ must be in w; if it were not then ¬□_{c}ϕ would be in w as w is maximal consistent. However, we have shown that ϕ ∈ w′ for all accessible w′ hence ¬□_{c}ϕ cannot be in w hence □_{c}ϕ must be in w.

• γ = ∀x.ϕ. We need that ∀x.ϕ ∈ w if and only if w, M ⊧_{∀} ∀x.ϕ. We assume that ϕ ∈ w if and only if w, M ⊧_{∀} ϕ.

The satisfaction condition for w, M ⊧_{∀} ∀x.ϕ is that ∀R ∈ U.M[A[R/x]/A] ⊧_{∀} ϕ.

As w is complete and consistent if ∀x.ϕ ∈ w and ¬ϕ[c/x] ∈ w for some c, then we could derive a contradiction. Since w contains ϕ[c/x] for each c ∈ ℂ∪C′, we can apply our induction hypothesis and the definition of satisfaction in a model to conclude that ∀x.ϕ ∈ w implies w, M ⊧_{∀} ∀x.ϕ.

If w, M ⊧_{∀} ∀x.ϕ then have ∀R ∈ U.M[A[R/x]/A] ⊧_{∀} ϕ whence we apply our induction hypothesis and consistency to conclude that ∀x.ϕ ∈ w.

Σ′′ ⊃ Σ hence M above suffices.

3.3 ALL UN-NESTED MODAL FORMULAS

We now return to our question. What should the universe of modalities look like. In order to determine the correct closure conditions, we would like to know something about possible operations under which the universe should be closed.

We are going to consider what operations on modalities should exist.

3.3.1 Test

A simple way of making modalities is to make a modality from a modal formula.

If B is a modal propositional formula without modalities then we can define ◇_{i:B?}ϕ, as

◇_{i:B?}ϕ ≡ (◇_{i}ϕ) ∧ B  (1)

Before we get carried away defining operations, we must ensure that each operation actually satisfies the properties of a modality.

We show that this Test operator always defines a modality. We must show that we do not imply that ◇_{i:B?}⊥, as this denies a theorem that for all i □_{i}⊤. If we substitute ⊥ for ϕ in the above we see that so long as ◇_{i}⊥ is false, ◇_{i:B?}⊥ will be false. We also get that the boxed form of the operation obeys necessitation and modal distribution which can be checked simply by expanding the definitions.

3.3.2 Union

Other ways of defining new modalities suggest themselves. Perhaps the most natural of these is to allow the definition of a new modality in terms of combining two old modalities via union.

Thus, given modalities, ◇_{1} and ◇_{2}, we can allow ourselves to make their union as follows,

◇_{1∪2}ϕ ≡ ◇_{1}ϕ ∨ ◇_{2}ϕ  (2)

Again due to a similar argument ◇_{1∪2}ϕ will not be false unless one of the original modalities is false. The boxed form of this union operation obeys necessitation and modal distribution. This can be checked simply by expanding the definitions.

3.3.3 Intersection and Negation?

However, it is worthwhile noticing that

◇_{1∩2}ϕ ≡ ◇_{1}ϕ ∧ ◇_{2}ϕ

does not define a new modality, nor does

◇_{−1}ϕ ≡ ¬◇_{1}ϕ.

The second can be shown by noting that ¬◇_{1}¬(p∨¬p) is equivalent to □_{1}p ∨ ¬p, which is valid by necessitation. Therefore ◇_{−1}¬(p ∨ ¬p) is true for all modalities ◇_{1}, but we have that ¬◇_{−1}¬(p ∨ ¬p) — a contradiction. Therefore adding the above definition would render the system inconsistent.

The definition of ◇_{1∩2} does not define a modality unless ◇_{1}ϕ → ◇_{2}ϕ or vice-versa. In this case it yields the stronger. If there is a ϕ such that ◇_{1}ϕ ∧ ◇_{2}¬ϕ, then we have ◇_{1∩2}ϕ ∨ ¬ϕ but not ◇_{1∩2}ϕ or ◇_{1∩2}¬ϕ, which is inconsistent with modal distribution.

3.4 NESTED BELIEFS

Another natural operation to add is to allow nested modalities in the defining formula. Thus we could allow the definition of a modality corresponding to Sally’s opinion of Harry’s beliefs.

3.4.1 Composition

◇_{x;y}ϕ ≡ ◇_{y}◇_{x}ϕ  (3)

Again due to a similar argument ◇_{x;y}ϕ will not be false unless one of the original modalities is false. The boxed form of this union operation obeys necessitation and modal distribution. This can be checked simply by expanding the definitions.

3.5 OPERATIONS AND UNIVERSES

Adding these operations means that universes for quantified modal logic would have to be closed under these operations. For if not then we might have two modalities ◇_{y} and ◇_{x} without their union or composition.

Therefore we now consider a system which corresponds to the universe of relations being closed under union, intersection with the worlds that satisfy a property, and relational composition i.e. composition of two binary relations R and S, is defined as , ∀x y.S; R(x, y) ≡ ∃z.R(x, z) ∧ S(z, y).

We call the derivability relation with these new axioms 1, 2 and 3 ⊢_{∀ ∀ ∀}.

Definition 9 We extend the satisfaction relation ⊧_{∀} for S = ⟨W, U, V, A⟩, a structure for quantified modal logic inductively over the structure of the additional formulae and denote the extension ⊧_{∀ ∀ ∀}. Thus, for any w ∈ W,

\begin{aligned}w, S ⊧_{∀ ∀ ∀} ◇_{i:p?} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{i}ϕ ∧ p \\ w, S ⊧_{∀ ∀ ∀} ◇_{x∪y} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{x}ϕ or w, S ⊧_{∀ ∀ ∀} ◇_{y}ϕ \\ w, S ⊧_{∀ ∀ ∀} ◇_{x;y} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{y}◇_{x}ϕ \end{aligned}

Definition 10 A quantified modal model 𝕄 = ⟨W, U, V, A⟩ is closed if the set U is closed under all first order definable functions f on modalities.

A function f: 2^{(W ×W)} → 2^{(W ×W)} is a first-order definable function on modalities if there is some function g such that g(⟨W, R, V ⟩) = ⟨W, f(R), V ⟩.

The annotation about the induced function g is that f must not be a relation, nor must it must take Kripke structures with the same theory to Kripke structures with a different theory. We saw before that intersection of modalities (although first-order definable) is not a function on modalities.

Definition 11 We say that ϕ is valid under ⊧_{∀ ∀ ∀}, denoted ⊧_{∀ ∀ ∀} ϕ, if for all closed quantified modal models 𝕄 = ⟨W, U, V, A⟩ and all worlds w ∈ W, w, 𝕄 ⊧_{∀ ∀ ∀} ϕ.

Theorem 12 If ϕ is a sentence in L_{ℂ,ℙ}, then ⊢_{∀ ∀ ∀} ϕ implies ϕ is valid under ⊧_{∀ ∀ ∀}.

Proof Outline: We need to check the new axioms. The axioms involving modal sentences can be seen to be true by considering the truth conditions.

Theorem 13 If ϕ is a sentence in L_{ℂ,P} and ⊧_{∀ ∀ ∀} ϕ, then ⊢_{∀ ∀ ∀} ϕ

The proof relies on some technical material about what constitutes a function on modalities that is presented in the next section. In particular we need to show that every first order definable function on modalities is representable by our three operations, union, composition and i: B?.

Proof: We add sufficient constants, with definitions, so that we have a constant corresponding to every every point in the free algebra of the introduced operations. We need to show that each of these constants is correctly interpreted. That is we need to show that the function I we defined in the proof of Theorem 8 correctly models sequences containing the newly defined modal terms. We show this by showing that we can find a set of worlds which models the modality.

We assign these by induction on the terms i.

• i = (j: B?) · s This is assigned the set, I(j · s) ∩

{w′|B ∈ w′ ∈ W }.

• i = (j∪k)·s This is assigned I(i) = I(j·s)∪I(k·s).

• i = (j; k) · s This is assigned I(i) = I(k · (j · s)).

Now that we have interpreted all the new constants, we need to check that they are interpreted correctly. This follows immediately from their construction.

We then need to show that this structure we have defined is closed under first order definable functions on modalities.

We use Corollary 18 in the next section.

By construction all modalities constructed from ∪, c: B? and c; c′ are in our structure, thus Corollary 18 lets us conclude that our structure is closed under all first order definable functions on modalities.

The rest of the proof follows as before.

3.6 BISIMULATION

We now introduce a notion, bisimulation, that we will use to define equality of modalities. In order to relate the syntactic question of when two modalities are true of the same formulas to the semantic question of a relation between accessibility relations we consider bisimulation.

Van Benthem showed the close connection between bisimulation (or more precisely p-morphisms) and definability in modal logics (1983). Using the classical transformation of modal formulas to first order formulas, he showed that a first order formula is preserved under bisimulation exactly when it is equivalent to the translation of a modal formula. We use this result to determine when the two Kripke models are extensionally equal. A key part of checking that a function on relations lifts to a function on modalities is recognizing that equal modal structures are sent to equal modal structures.

Definition 14 Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two Kripke structures over propositional atoms P, then K is bisimilar to K′, K \underline{↔} K′, if there is a relation S ⊆ W × W′ such that

• ∀w ∈ W ∃w′ ∈ W′ such that w S w′, and

• ∀w′ ∈ W′ ∃w ∈ W such that w S w′, and

• x S y implies V (x) = V′(y), and

• x S y implies ∀x′ ∈ W. x R x′ → (∃y′ ∈ W′. y R′ y′ ∧ x′ S y′), and

• x S y implies ∀y′ ∈ W′. y R′ y′ → (∃x′ ∈ W. x R x′ ∧ x′ S y′).

This notion of bisimulation captures exactly that two models agree on all modal sentences.

Theorem 15 ((Benthem 1983)) Two Kripke structures M and N are bisimilar, M \underline{↔} N if and only if

(M ⊧ ϕ if and only if N ⊧ ϕ) for all modal formulas ϕ.

We use this theorem in the next section as our identity condition on first order relations. We need the identity condition on relations that corresponds to extensional equality on modalities, as we wish to consider what functions on modalities exists, in terms of their characterization as functions on relations.

Thus Kripke structures agree on all modal formulas if and only if they are bisimilar. Thus any function on from Kripke structures to Kripke structures is a function on modalities if and only if it maps bisimilar structures to bisimilar structures.

3.7 FIRST ORDER TRANSLATIONS

The propositional modal language we have introduced may be embedded into first order predicate logic, by the following standard translation, where φ[y/x] is the result of replacing all free occurrences of x by y in φ.

(p)^{∗}  = P x
(¬φ)^{∗}  = ¬(φ)^{∗}
(φ ∧ ψ)^{∗}  = (φ)^{∗} ∧ (ψ)^{∗}
(□φ)^{∗}  = ∀y(R(x, y) → (φ)^{∗}[y/x])
for some  new variable y

In fact, only two variables are needed. We then have the following theorem.

Theorem 16 [(Benthem 1983)] A first order formula is (equivalent to) a translation of a modal formula if and only if it is invariant for bisimulation.

In the next section we use this theorem to show that our new operators can define all first order modalities.

3.8 DEFINABLE RELATIONS

We now ask what definable functions f on relations give rise to functions on modalities g(⟨W, R, V ⟩) = ⟨W, f(R), V ⟩). If we define a new Kripke model, by generating a new binary relation on worlds, when does this definition map Kripke models that have the same theory to Kripke models with the same theory?

The answer to this can be derived from the previous theorem—the only formulas that are invariant for bisimulation are those that are equivalent to modal formulas. In this case it suffices to be able to find a formula ψ[q] such that ⟨W, R′, V ⟩ ⊧ ◇ϕ if and only if ⟨W, R, V ⟩ ⊧ ψ[ϕ/q].

Theorem 17 Let K = ⟨W, R, V ⟩ be a Kripke structure over propositional atoms {p_{1}, … p_{n}}.

Let v: W → 2^{{p_{1},...p_{n}}} range over valuation functions and let P_{1}, …, P_{m} be unary predicates on W, such that (p_{i})^{∗} = P_{i}(x).

For all S ⊆ W × W,

\begin{matrix}∀v.⟨W, S, v⟩ \underline{↔} ⟨W, R, v⟩ implies \\ ∀v.⟨W, f(R), v⟩ \underline{↔} ⟨W, f(S), v⟩, \end{matrix}

if and only if, there is a modal formula ψ in the modal language with atoms p_{1}, …, p_{n}, q, such that

(ψ(q))^{∗} ≡ ∃y.f(R)(x, y) ∧ Q(y)

where q is a new propositional letter, with (q)^{∗} = Q(x) and ≡ is equivalence in first-order classical logic.

In fact, ψ can be chosen so that every occurrence of q in ψ(q) is scoped by an even number of negations, and ∧ does not occur outside any pair of modalities that bind q.

Proof: ⇐ We are given an equivalence, and we need to show that a definition f preserves bisimulation. To show that ⟨W, f(R), V ⟩ \underline{↔} ⟨W, f(S), V ⟩ it suffices to show that they agree on all modal formulas. We prove this by induction on formulas. As we have proved the equivalence for arbitrary q we can use it for arbitrary formulas φ. This gives us truth conditions for statements of the form ⟨W, f(R), V ⟩ ⊧ ◇φ in terms of ⟨W, R, V ⟩ ⊧ ψ[φ/q]. Thus we can reduce the truth of all formulas in ⟨W, f(R), V ⟩ to the truth of formulas in ⟨W, R, V ⟩. We can similarly reduce the truth of all formulas in ⟨W, f(S), V ⟩ to the truth of the same formulas in ⟨W, S, V ⟩. As by assumption if ⟨W, R, V ⟩ \underline{↔} ⟨W, S, V ⟩ then these models agree on all formulas. Therefore the new models agree, and are thus bisimilar, as required.

⇒ We are given that f preserves bisimulations and need to show that there exists a formula ψ. As f preserves bisimulations, ∃y.f(R)(x, y) ∧ Q(y) is preserved thus by Theorem 16 is thus equivalent to a modal formula, as required.

Syntactic Characterization To see that q is scoped by an even number of negations in ψ is suffices to note that Q occurs only positively in the right hand side of a formula equivalent to (ψ[q])^{∗}. This means q must not occur negatively in an essential way.

Finally using the fact from Example 3.3.3 that new modalities can not be defined by conjoining modalities, there are no two modalities that scope q that are in the scope of the same conjunction. .

Corollary 18 First order definable functions from Kripke models to Kripke models are exactly those that are definable using our three operations x; y, x ∪ y and x: B?.

We get this from the syntactic considerations of ψ in the proof above.

4 OTHER WORK

4.1 MCCARTHY’S APPROACH

McCarthy (1993) introduced the notion of a context as a formal object. He argued that contexts should objects in a theory. This led him to introduce the modality, ist(c, ϕ), which states that a formula ϕ is true in a context c.

McCarthy saw contexts as capturing the unstated features of an utterance. He thought these features could be made more explicit by showing how contexts were related. His proposal was to characterize these relations by writing sentences that relate one context to another, lifting axioms. If ϕ being true in a context c implied that ψ was true in a context c′, he would write, ist(c, ϕ) → ist(c′, ψ).

While McCarthy was developing the idea of contexts a student of his, Guha (1991) applied the ideas to Cyc (Lenat 1995, Guha and Lenat 1992). In Cyc contexts were used to capture “microtheories”, or sets of facts about a particular domain. This compartmentalization of information is useful when data sources from different producers need to be merged, cf. (Farquhar et al. 1995).

Independently Giunchiglia (1993) introduced the notion of a multi-language system. Based on intuitions from proof theory, he attempts to capture how patterns of reasoning in different languages can be integrated. Giunchiglia et al. (1993) address issues of nonomniscient belief, while our contexts are all logically closed. Clearly there is a clear relationship between how patterns of reasoning are related, and theories are related.

4.2 QUOTING APPROACHES

Montague (1963) showed that modal logic cannot be mimicked by a naive quoting machinery if the underlying language is sufficiently powerful. This might be thought to render such approaches impossible, but Attardi and Simi (1995b) have developed a system that avoids these problems. They call their syntactic modalities, viewpoints. The key idea of Attardi and Simi is to use reflection principles added to a standard first order logic with names for terms. They show that useful reasoning can be done in consistent theories, while allowing self reference etc., but blocking the paradoxes of Montague.

While quoting approaches are natural to a certain extent, the difficulties that avoiding paradoxes raise justify other approaches, which draw on other intuitions.

4.3 MODAL APPROACHES

Montague (1970) considers introducing modalities as objects in a system extending Montague Grammar, a version of intensional higher order logic. Naturally, his modalities are non-extensional. This led him away from considering structural properties, as his interests lay in the application of these ideas to natural language. Contexts in natural language are intensional, according to many linguists.

Ohlbach, while looking at more efficient ways of reasoning in modal logics (Ohlbach 1988), considered representing modalities in a first order language by reifying the worlds, and explicitly introducing the accessibility relation. This led him to consider context logics (Ohlbach 1989). His interest lay mainly in the extra expressive power this gave over standard modalities.

Shoham (1991) considered a class of modal operators each of which characterized a context. He considered many possibilities for uses of contexts, and gives a set of 14 possible axioms for contexts, as a benchmark for comparison. Buvač, Buvač and Mason (1995) have looked at modal logics with these operators and the additional assumption that each operator has complete information about how the other operators behave. That is, their systems assume, □_{1}□_{2}ϕ∨□_{1}¬□_{2}ϕ. This axiom does not seem justified, even for the applications they consider. There is no reason why a database should have complete information about the contents of other databases. This limitation has been noticed by (Attardi and Simi 1995a).

(Buvač 1996) considers a simple notion of quantification over contexts, which corresponds to our first completeness theorem, with the assumption □_{1}□_{2}ϕ ∨ □_{1}¬□_{2}ϕ, and a 5 like assumption that multiple modalities may always be reduced to a single modality.

Similar systems to this (Gabbay and Nossum 1997) based on fibering one logic over another (Gabbay 1996) have been proposed. Our focus is on the role quantification over structures should play, an issue that is not the primary focus of fibering. (Akman and Surav 1996) provides a survey of formal approaches to contextual reasoning.

A related area outside AI is the study of programming constructs that are safe for bisimulation (Glabbeek 1990, Glabbeek 1993, van Benthem 1993, Hollenberg 1996). Van Benthem (1993) proves that a first order formula ϕ(x, y) is safe for bisimulation if and only if it is expressible by means of atomic transactions, tests of modal formulas, and the operations of relational composition and union. These correspond closely to the functions we propose that make new modalities. The functions we found, with another second order function, recursion, are safe for bisimulation in this sense. These constructs were originally developed in the framework of Dynamic Logic, (Pratt 1990). The functions we consider are also suggested by (Catach 1988) as ways of making new modalities.

Bisimulation, and its relation to nonwellfounded set theory are explored in detail in (Barwise and Moss 1996). Non-wellfounded set theory has also been considered as a natural model of situation theory (Barwise and Perry 1983) which bears much similarity with context (Akman and Surav 1997, van Benthem 1997), though is more focussed on natural language. Barwise and Moss (1996) show that non-wellfounded set theory, based on bisimulation, is a very natural model of modalities. Thus bisimulation is a unifying theme between the areas of programming constructs, nonwellfounded set theory, situation semantics, and our theory of context.

5 CONCLUSION AND APPLICATIONS

We have presented a sound and complete model theory for a quantificational logic of contexts. We began by considering models which included arbitrary universes of relations. This gave a simple system which allowed quantification over modalities, but which did not have any closure conditions on what modalities should exist.

We then looked at some operations that seemed natural on accessibility relations such as union, intersection and complement. We saw that some operations were not functions from modalities to modalities. The operation intersection can take two modalities and form a relation which does not behave as a modality.

Operations that allow us to take the union of contexts and test a context for satisfaction of given statement do define functions on modalities. These operations are very natural in combining knowledge sources, and considering the knowledge in common of different sources. Taking the union of two modalities results in the intersection of their theories.

Another valid operation on modalities is the relational composition which naturally models the beliefs that one agent has about another. New modalities of this sort are natural when we consider multiple agents.

We then suggested that our universe be closed under these three operators that make new modalities from old modalities. Therefore our universe of modalities includes all modalities definable using these operations. We gave an axiomatization of these operators that we show is sound and complete for universes that include all first order definable modalities.

We then showed that these three operators are sufficient to define all first order definable functions on modalities. To prove this theorem we characterized all first order definable functions on modalities. We considered when modalities are equivalent. This needed the notion of bisimulation. We then look at what functions on the relations in Kripke models give rise to functions on modalities. We then proved a theorem which characterizes the first order definable functions on relations that give rise to functions on modalities. We showed that the syntactic class of first order definable functions on modalities can be captured by our three operations on modalities.

Acknowledgments

This authors thank Rob van Glabbeek, Fausto Giunchiglia and John McCarthy for many helpful discussions on this and related work. We would also like to thank the attendees of CommonSense ’98 and the anonymous referees.

This research was partly funded by DARPA (ONR) grant # N00014-94-0775 under ARPI and by the Air Force Office of Scientific Research Grant # F49620-97-1-0207 under the DARPA HPKB project and New World Vistas.

References

Akman, V., and M. Surav. 1996. Steps toward formalizing context. AI Magazine 17(3):55–72.

Akman, V., and M. Surav. 1997. The use of situation theory in context modeling. Computational Intelligence 13(3):427–438.

Attardi, G., and M. Simi. 1995a. Beppe had a dream. In AAAI 1995 Fall Symposium on Formalizing Context. AAAI.

Attardi, G., and M. Simi. 1995b. A formalization of viewpoints. Fundamenta Informaticae 23(3).

Barwise, J., and L. Moss. 1996. Vicious Circles. CSLI.

Barwise, J., and J. Perry. 1983. Situations and Attitudes. Cambridge: MIT Press.

Benthem, J. v. 1983. Modal Logic and Classical Logic. Naples: Bibliopolis.

Buvač, S. 1996. Quantificational logic of context. In Proceedings of the Thirteenth National Conference on Artificial Intelligence.

Buvač, S., V. Buvač, and I. A. Mason. 1995. Metamathematics of contexts. Fundamenta Informaticae 23(3).

Catach, L. 1988. Normal Multimodal Logics. In Proc. National Conference on Artificial Intelligence (AAAI ’88), 491–495, Saint Paul, MI. AAAI.

Farquhar, A., A. Dappert, R. Fikes, and W. Pratt. 1995. Integrating information sources using context logic. Technical Report KSL-95-12, Knowledge Systems Laboratory, Stanford University. Also appears in the 1995 AAAI Spring Symposium Series on Information Gathering from Distributed, Heterogeneous Environments.

Gabbay, D. 1996. Fibred semantics and the weaving of logics: Part I: Modal and intuitionistic logics. Journal of Symbolic Logic 61(4):1057–1120.

Gabbay, D., and R. Nossum. 1997. Structured contexts with fibred semantics. In Proceedings of the International and Interdisciplinary Conference on Context.

Giunchiglia, F. 1993. Contextual reasoning. Epistemologia, special issue on I Linguaggi e le Macchine XVI:345–364.

Giunchiglia, F., L. Serafini, E. Giunchiglia, and M. Frixione. 1993. Non-omniscient belief as contextbased reasoning. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence.

Glabbeek, R. v. 1990. The linear time – branching time spectrum (extended abstract). In J. Baeten and J. Klop (Eds.), Proceedings CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, August 1990, Vol. 458, 278–297.

Glabbeek, R. v. 1993. The linear time – branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In E. Best (Ed.), Proceedings CONCUR’93, 4^{th} International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, Vol. 715, 66– 81.

Guha, R. V. 1991. Contexts: A Formalization and Some Applications. PhD thesis, Stanford University.

Guha, R., and D. Lenat. 1992. Language, representation and contexts. Journal of Information Processing 15(3):340–349.

Halpern, J. 1995. Reasoning About Knowledge: A Survery. In D. Gabbay and J. Hogger, C. Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. IV, 1–34. Clarendon Press, Oxford.

Hollenberg, M. 1996. Safety for bisimulation in monadic second-order logic. Logic Group Preprint Series 170, Dept. of Philosophy, Utrecht University, November.

Lenat, D. B. 1995. Cyc: A large-scale investment in knowledge infrastructure. Communications of the Association for Computing Machinery 38 (11).

McCarthy, J. 1993. Notes on formalizing context. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’93).

Montague, R. 1963. Syntactical treatments of modality, with corollaries on reflection principles and finite axiomatizations. Acta Philosophica Fennica 16:153–167.

Montague, R. 1970. Universal grammar. Theoria 36:373–398.

Ohlbach, H. J. 1988. A Resolution Calculus for Modal Logics. PhD thesis, Kaiserslautern.

Ohlbach, H. J. 1989. Context logic. Technical report, Kaiserslautern.

Pratt, V. 1990. Dynamic algebras as a well-behaved fragment of relation algebras. In Algebraic Logic and Universal Algebra in Computer Science, LNCS 425, 77–110, Ames, Iowa, June 1988. Springer-Verlag.

Shoham, Y. 1991. Varieties of context. In V. Lifschitz (Ed.), Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy. Academic Press. van Benthem, J. 1993. Programming operations that are safe for bisimulation. Technical Report 93-179, CSLI, Center for the Study of Language and Information, Stanford University. To appear in Studai Logica.

van Benthem, J. 1997. Changing contexts and shifting assertions. In Computing Natural Language. CSLI Publications. Distributed by Cambridge University Press.