This note describes possible world semantics for a constructive modal logic CK. The system CK is weaker than other constructive modal logics K as it does not satisfy distribution of possibility over disjunctions, neither binary (3(A ∨ B) → 3A ∨ 3B) nor nullary (3⊥ → ⊥). We are interested in this version of constructive K for its application to contexts in AI [dP03]. However, our previous work on CK described only a categorical semantics [BdPR01] for the system, while most logicians interested in contexts prefer their semantics possible worlds style. This note fills the gap by providing the possible worlds model theory for the constructive modal system CK, showing soundness and completeness of the proposed semantics, as well as the finite model property and (hence) decidability of the system. Wijesekera [Wij90] investigated possible worlds semantics of a system similar to CK, without the binary distribution, but satisfying the nullary one. The semantics presented here for CK is new and considerably simpler than the one of Wijesekera.
There are many varieties of constructive modal logics in the literature. Several of these were arrived at as solutions to the problem of deciding which is the most elegant way of combining the accessibility relations usually associated with the modal operators (necessity 2 and possibility 3) to the accessibility relation usually associated with (propositional) intuitionistic implication.
This note describes the possible world semantics for one constructive modal logic, the system CK, which is unusual in that it first had a proof-theory and a categorical semantics[BdPR01], before we decided to investigate its possible-worlds semantics.
One reason why we are interested in this, rather weak version of constructive K, is its possible application to the notion of contexts in AI[dP03]. This we discuss briefly in the next section. Moreover, the system CK can also be seen as a natural generalization of our previous work on a constructive version of the modal logic S4, CS4, described in [AMdPR01,BdP00].
Contexts as Constructive Modalities In this section we discuss our motivation to study the logic CK. The main reason is the suggestion that this constructive logic may be an adequate basis for dealing with notions of context in logic-based knowledge representation.
Notions of context abound in artificial intelligence and computational linguistics, to mention only two of the several fields that use more or less formalized notions of context. The number of existing logical systems dedicated to formally modeling contexts, in several disciplines, is quite staggering.
In previous work ([dP03]) we surveyed several of the logical systems that arose out of McCarthy’s original intuitions [McC93] that context ought to be a first-class object in a logical system devised to reason using common sense. Using purely prooftheoretical criteria we concluded in [dP03] that it would be worth investigating a constructive multi-modal version of K, which is the essential core of several context logics. The previous work did not discuss semantics much, simply citing categorical semantics for the unimodal case in the companion paper [BdPR01]. This note fills part of the gap between motivation and application by providing possible worlds semantics for the unimodal system CK. An adequate Kripke semantics for the multi-modal system (assuming the modalities to be independent) should be easy to design as a generalization of the structures presented here.
To set the scene, in the long term, our research project is to devise a system of logic, which is appropriate to produce logical representations of sentences in natural language. There is very little need to explain how ubiquitous natural language documents are and how useful it would be to automatically produce logical representations from simple text. Clearly if representations that are faithful to what humans mean can be constructed automatically, they can be used in several applications, such as information retrieval, information extraction, dialogue systems, question answering, etc.
It also seems clear that when creating logical formulae from sentences, a notion of context would be very convenient. For example, when confronted with a paragraph like “Gulf ImpEx imported five shipments of medical goods in 1999. Their shipping records claim that none of the shipments contained any dual use materials. We have learned that at least one shipment contained two tons of fissile material. Most of this was of such low radioactivity as to prevent its dual use. We do not know whether the remainder of the fissile material could have been dual use.” one’s first reaction is to try to separate the information into classes or contexts: what is claimed, what is learned, what is known, what is declared, what is prevented, etc.. It is clear that on an individual basis these classes are easy to deal with: if some source X claimed some assertion Y , it is not necessarily the case that Y is true, while if a reliable source tells us that it has learned that Y , at least as far as that source is concerned, Y is true. But when so many different kinds of context interact, in nested ways, things become less clear and help from a formal system might start to pay for its up-keeping.
A logic where contexts are first-class objects, as suggested by McCarthy, might be able to help when reasoning with representations that model these kinds of concepts. Some discussion, from a systems building perspective, of how these notions of context could and would be useful can be found in [CCS+01,CCS+03]. Some discussion on how we are already implementing some version of contexts using a rewriting system can be found in [Cro05]. A preliminary logical discussion of what kinds of inferences this desired system of contexts needs to perform is presented in [BCC+05]. But the mathematical connection between CK and the ideas and implementations on the papers just mentioned is not direct. Rather, the mathematics explained in this paper provides a safety net for the other work, in the sense that it gives a precise logical basis1 for the work discussed in the systems’ papers.
A common denominator of several logics of context is the notion of a modality, written as istrue(c, p). The idea of using syntactic modalities to model contexts is appealing as modalities allow some control over the way in which expressions are evaluated in the logic. In other words, modalities act as syntactic “boxes” that contain the reasoning/evaluation process. Another point in favor of modalities (as opposed to first-order predicates) is that modalities avoid problems with self-referential paradoxes. But most modal logics are not very well-behaved proof-theoretically: providing natural deduction and/or sequent calculus formalizations for most modal logics is hard, which implies complicated implementations and a hard time translating between systems. Summing up we want to design ourselves a system that is as well-behaved proof-theoretically as we can get it, given that it has simple modalities. By ‘simple’ we mean that we do not prejudge the interpretation of these modalities and leave the question of which properties they satisfy as open as possible. Lastly we insist on a constructive logic, as a constructive system can be easily adapted to yield a classical one by adding the excluded middle or a double negation axiom, while the converse process of extracting the constructive fragment of a classical system is much more complicated. It seems to us that for most of the applications we have in mind a constructive setting is more appropriate. For example, if one thinks about contexts as (a collection of) alternative knowledge bases then the reasoning we do ought to be constructive by definition, since this reasoning is about the information already present in the individual knowledge bases, not about some platonic world of non-decidable truths. If the collection of knowledge bases provides us with a logical disjunction A ∨ B we expect that for some context it is true that A holds or for some context it is true that B holds, a version of the disjunction property, which is true constructively, but not classically. Thus some form of the disjunction property is an intuitive requirement of the system that is easily met by having a constructive basis of the logic. Working on these principles we arrived at the system CK.
Wijesekera [Wij90] investigated a constructive system similar to CK and provided possible-worlds semantics for it. We hoped that a direct adaptation of Wisejekera’s results would work for us. The adaptation chosen meant that the proof of completeness could be streamlined and made similar to our previous work ([AMdPR01]) on a constructive and categorical version of modal S4, known as CS4, which is just a special axiomatic theory of CK. The work on CS4 has had many applications within computer science (for examples see [DP01,SDP01,dPGM04]), which thus are also applications 1 Other kinds of logical foundations are reasonable too and are also being investigated [BdP03,SG02]. of CK. Since CK is a more general system then CS4 it should support an even wider range of concrete interpretations. 3
CK and its Model Theory The logical system we call CK is given by the Hilbert system of intuitionistic propositional logic IPL extended by the following axioms and rule 2K : 2(A → B) → (2A → 2B) 3K : 2(A → B) → (3A → 3B) Nec : If A is a theorem then 2A is a theorem. This system could be called the ‘non-normal’ version of Wijesekera’s system[Wij90], because it is the system we obtain if we consider only the propositional fragment of Wijesekera’s system and drop from it the axiom ¬3⊥. But care must be taken as different authors use “normal” for different properties of modal systems.
The symbol `CK denotes deduction in the CK Hilbert system. For instance, the formula 2A ∧ 3B → 3(A ∧ B) is derivable by the following deduction: axiom of IPL from 1. by Nec from 2.,2K by MP by 3K from 4. by IPL from 3.,5. by MP from 6. by IPL
In a very similar way one can derive the formula (2A ∧ 3(A → B)) → 3B which is listed by Wijesekera [Wij90] as an axiom. Generally, the above derivation shows that if (A ∧ B) → C is a theorem of CK (in particular, a theorem of IPL), then (2A ∧ 3B) → 3C is a theorem of CK, too.
Wijesekera seems to be one of the first authors to point out that, unlike distribution of necessity over conjunctions, which seems accepted by all intuitionistic modal logicians, the distribution of possibility over disjunctions, both binary (3(A ∨ B) → 3A ∨ 3B) and nullary (¬3⊥ or 3⊥ → ⊥) is much more debatable. If the operator 3 models a constructive notion of possibility or satisfiability-in-context then it is natural to expect that, in general, these distributions fail. The fact that a disjunction A ∨ B is satisfiable in a context does not warrant the conclusion that one of the disjuncts is satisfiable, e.g., if satisfiability-in-context involves a non-deterministic process. Similarly, in a constructive reading of possibility 3 we do not expect that possibly false (3⊥) implies false (⊥). Thus we need to allow some contexts to be inconsistent and we drop the distribution axioms.
We introduce the notion of a Kripke-style model for CK, simply called CK-model in the sequel: Definition 1. A Kripke model of CK is a structure M = (W, ≤, R, |=), where W is a non-empty set, ≤ is a reflexive and transitive binary relation on W , R is any binary relation on W , and |= a relation between elements w ∈ W and propositions A, written w |= A (“A is satisfied at w in M ”) such that: – ≤ is hereditary with respect to propositional variables, that is, for every variable p and worlds w, w0, if w ≤ w0 and w |= p, then w0 |= p. – The relation |= has the following properties: w |= >; w |= A ∧ B iff w |= A and w |= B; w |= A ∨ B iff w |= A or w |= B; w |= A → B iff ∀w0(w ≤ w0 ⇒ (w0 |= A ⇒ w0 |= B)) w |= 2A iff ∀w0(w ≤ w0 ⇒ ∀u(w0Ru ⇒ u |= A)) w |= 3A iff ∀w0(w ≤ w0 ⇒ ∃u(w0Ru ∧ u |= A)) Notice that we do not have the clause w 6|= ⊥, i.e. we allow inconsistent worlds.
Instead, we have – if w |= ⊥ and w ≤ w0 or wRw0, then w0 |= ⊥ and – if w |= ⊥, then for every propositional variable p, w |= p (to make sure that ⊥ → A is valid).
We sometimes write M, w |= A instead of just w |= A when we want to make the model explicit. As usual, a formula A is true in a model M , written M |= A, if for every w ∈ W , M, w |= A. A formula A is valid (|= A) if it is true in all models. All notions are extended to sets of formulae as usual in the universal way.
The fact that our models do not satisfy ¬3⊥ or more intuitively that 3⊥ → ⊥ is not provable comes from the possibility that fallible worlds, i.e. those satisfying ⊥, could be reached via an R-step from non-fallible worlds.
In [AMdPR01] is was shown that the system CS4 coincides with the theory of CS4 models, which are like the CK models but where R is a preordering relation. Here we want to verify that CK coincides with the theory of CK models.
Local and Global Assumptions The purpose of Hilbert deduction is to derive necessary truths, hence the Necessitation Rule. Semantically, a deduction Γ `CK B of B from assumptions Γ says that if all A ∈ Γ are true in some model M , then B, too, is true in M . It does not claim that if all A ∈ Γ are true in some model at a given world then at that world B must be true. Indeed, if this local, world-wise notion of semantic consequence were valid, Hilbert deduction `CK would enjoy the Deduction Theorem. But it does not. For we have A `CK 2A by Nec, while from soundness of `CK it will follow that 6`CK A → 2A.
As pointed out by Fitting [Fit94] and Simmons [Pop94] it is useful in modal logics to distinguish between local and global notions of validity, and local and global assumptions. We use the following terminology to make this precise: Let Γ1 and Γ2 be sets of formulae. A formula B is a semantic consequence of global assumptions Γ1 and local assumptions Γ2, written Γ1; Γ2 |= B, if for every model M such that M |= Γ1 and each world w in M with M, w |= Γ2, we have M, w |= B. A formula B is a deductive consequence of global assumptions Γ1 and local assumptions Γ2, written Γ1; Γ2 `CK B, if there exists a finite set Γ20 ⊆ Γ2 such that Γ1 `CK V Γ20 → A, where V Γ for a finite set Γ = {A1, A2, . . . , An} abbreviates A1 ∧ A2 ∧ · · · ∧ An. The degenerate case V ∅ = > is included.
Theorem 1. The system CK is sound and strongly complete with respect to the class of models defined above, that is, for all sets of formulae Γ1, Γ2 and formula A, we have Γ1; Γ2 |= A iff Γ1; Γ2 `CK A.
Observe that soundness is equivalent to the condition that Γ ; ∅ `CK A implies Γ ; ∅ |= A, or in standard terminology that Γ `CK A implies Γ |= A. This is not difficult to prove by induction on derivations.2 All axioms are necessary truths on CK-models, and the rules of Modus Ponens and Necessitation preserve necessary truths.
Completeness can be reduced to the special case of empty global assumptions, viz.,that ∅; Γ |= A implies ∅; Γ `CK A. The key is the following lemma: and 2n+1Γ d=ef {2φ | φ ∈ Γ }. (i) If Γ1; Γ2 |= A, then ∅; 2∗Γ1 ∪ Γ2 |= A (ii) If ∅; 2∗Γ1 ∪ Γ2 `CK A then Γ1; Γ2 `CK A Lemma 1. For any set of formulae Γ let 2∗Γ be the set Sn≥0 2nΓ , where 20Γ d=ef Γ Proof. (i) Assume that Γ1; Γ2 |= A. Given a model M and a world w in M with M, w |= Sn≥0 2nΓ1 as well as M, w |= Γ2, we must show that M, w |= A. To this end construct the generated sub-model Mw of M with root w, i.e.the least sub-model of M that contains w and is closed under the condition that if x ∈ Mw and x ≤ y or xRy, then y ∈ Mw too. One can show that all worlds in this sub-model have the same truths as in the original larger model M . Hence, in particular, Mw, w |= Γ2. Moreover, we have Mw, u |= Γ1 for all worlds u ∈ Mw. This follows from the fact that M, w |= Sn≥0 2nΓ1 and that each world u in Mw is reachable by finite sequence of ≤ or R steps from the root w. Thus, overall, Mw |= Γ1. But then the assumption Γ1; Γ2 |= A implies A, hence Mw |= A.
(ii) Suppose ∅; 2∗Γ1 ∪ Γ2 `CK A. Then, there are finite subsets Γ10 ⊆ 2∗Γ1 and Γ20 ⊆ Γ2 such that `CK V(Γ10 ∧ V Γ20) → A. Since each φ ∈ Γ10 is of the form 22 · · · 2ψ for some ψ ∈ Γ1 we have Γ1 `CK φ by repeated applications of Necessitation. But this means, using Modus Ponens and IPL, that Γ1 `CK V Γ20 → A, which implies Γ1; Γ2 `CK A. 2 Wijesekera [Wij90] derives soundness for CK plus the axiom ¬3⊥ (for infallible models) by reducing the Hilbert system to a sequent calculus. However, the relevant equivalence in his Lemma 1.5.1 assumes the Deduction Theorem for the Hilbert system, which is wrong. As a consequence Wijesekera’s proof remains inconclusive in establishing soundness of CK.
With Lemma 1 the completeness direction of Theorem 1 reduces to the following Model Existence Theorem: Theorem 2. If ∅; Γ `CK A is not true then there exists a model M = (W, ≤, R, |=) and a world w0 such that M, w0 |= Γ but it is not the case that M, w0 |= A.
The counter-model construction establishing Theorem 2 employs a suitable generalization of the Lindenbaum construction, in which worlds are triples (Γ, Δ, Θ) of sets of formulae, called theories. The intuition is that at a world w = (Γ, Δ, Θ) the formulae in Γ are validated at w, the formulae in Δ are falsified at w and the formulae in Θ are falsified at every world R-reachable from w. This representation of worlds has been introduced originally for propositional lax logic PLL [FM97].3 Definition 2. A theory (Γ, Δ, Θ) is consistent if for every choice of formulae N1, N2, . . . , Nn in Δ and K1, K2, . . . Kk in Θ such that n + k ≥ 1 it is not the case that
∅; Γ `CK N1 ∨ N2 . . . ∨ Nn ∨ 3(K1 ∨ . . . ∨ Kk).
A theory is maximally consistent if it is consistent and for every formula M either M ∈ Γ or M ∈ Δ.
We have the following central “Saturation” lemma whose proof is standard and is hence omitted.
Lemma 2. Every consistent theory(Γ, Δ, Θ) has a maximally consistent extension (Γ ∗, Δ∗, Θ). Furthermore, every maximally consistent theory satisfies: – Γ ∗ is deductively closed, i.e. if ∅; Γ ∗ `CK A then A ∈ Γ ∗; – If A ∨ B is in Γ ∗ then either A is in Γ ∗ or B is in Γ ∗.
Note, if ∅; Γ `CK ⊥, then by consistency of (Γ, Δ, Θ) we must have Δ = Θ = ∅, in which case the above construction will produce the maximally consistent extension (U, ∅, ∅), where U stands for the set of all formulae.
We now proceed to define the generic CK-Kripke model M = (W, ≤, R, |=) that falsifies the formula A.
Definition 3. Our canonical model consists of maximally consistent theories (Γ, Δ, Θ). The accessibility relations are (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) iff Γ ⊆ Γ 0 (Γ, Δ, Θ) R (Γ 0, Δ0, Θ0) iff 2−1Γ ⊆ Γ 0 & Θ ⊆ Δ0, (1) (2) where 2−1Γ = {φ | 2φ ∈ Γ }. We say (Γ, Δ, Θ) |= A iff A ∈ Γ .
Note that the relation ≤ is a preordering and not antisymmetric in general, while R can be arbitrary. 3 The sets Δ are actually redundant in the world structure but technically convenient for phrasing the saturation conditions in a simple form.
Lemma 3. The canonical structure is a Kripke model of CK.
Proof. Clearly, ≤ is hereditary. For every pair of worlds (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) we have Γ ⊆ Γ 0 and thus for all formulae A, if (Γ, Δ, Θ) |= A then (Γ 0, Δ0, Θ0) |= A.
Let us consider inconsistent, i.e., fallible worlds. If (Γ, Δ, Θ) |= ⊥, i.e., ⊥ ∈ Γ then by deductive closure Γ is the set of all formulae (and Δ = Θ = ∅ by consistency). Thus, the first component Γ 0 of every accessible world (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) or (Γ, Δ, Θ) R (Γ 0, Δ0, Θ0) must be the set of all formulae, too. In other words, once a theory is fallible it remains fallible along all ≤ and R steps. Needless to point out, in a fallible (Γ, Δ, Θ) all formulae are true.
Also, obviously, (Γ, Δ, Θ) |= >. The other clauses of Definition 1 are proved by induction of the structure of formulae. The following conditions follow easily from Lemma 2: (Γ, Δ, Θ) |= A ∧ B iff (Γ, Δ, Θ) |= A and (Γ, Δ, Θ) |= B; (Γ, Δ, Θ) |= A ∨ B iff (Γ, Δ, Θ) |= A or (Γ, Δ, Θ) |= B;
Suppose (Γ, Δ, Θ) |= A → B and (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) |= A. Then, both A → B ∈ Γ ⊆ Γ 0 and A ∈ Γ 0, so that by deductive closure of Γ 0 we have B ∈ Γ 0. Conversely, suppose A → B 6∈ Γ . Then consider the theory (Γ ∪ {A}, {B}, ∅). It must be consistent, for otherwise, we would have ∅; Γ, A `CK B which implies ∅; Γ `CK A → B by definition of `CK and the properties of IPL. We can thus pick any maximally consistent extension (Γ ∗, Δ∗, Θ∗) of (Γ ∪ {A}, {B}, ∅). For such a theory it holds that (Γ, Δ, Θ) ≤ (Γ ∗, Δ∗, Θ∗) and (Γ ∗, Δ∗, Θ∗) |= A as well as (Γ ∗, Δ∗, Θ∗) 6|= B.
It remains to tackle the two clauses of Definition 1 concerning the modal operators. Assume 2A ∈ Γ . Then in all situations (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) R (Γ 00, Δ00, Θ00) it holds that A ∈ 2−1Γ ⊆ 2−1Γ 0 ⊆ Γ 00. By induction hypothesis, (Γ 00, Δ00, Θ00) |= A.
To take the other direction, let us suppose that 2A 6∈ Γ , i.e., 2A ∈ Δ. Obviously, (Γ, Δ, ∅) is maximally consistent and (Γ, Δ, Θ) ≤ (Γ, Δ, ∅). Consider the theory (2−1Γ, {A}, ∅) which is trivially consistent. For if there exist M1, M2, . . . , Mm ∈ 2−1Γ such that ∅; M1, M2, . . . , Mm `CK A, then the rules of CK yield
∅; 2M1, 2M2, . . . , 2Mm `CK 2A from which it follows that ∅; Γ `CK 2A in contradiction to our assumption (deductive closure of Γ ). Take any maximally consistent extension (Γ ∗, Δ∗, Θ∗) of (2−1Γ, {A}, ∅). It satisfies A 6∈ Γ ∗, since A ∈ Δ∗, as well as (Γ, Δ, ∅) R (Γ ∗, Δ∗, Θ∗). Our induction hypothesis gives us (Γ ∗, Δ∗, Θ∗) 6|= A together with (Γ, Δ, Θ) ≤ (Γ, Δ, ∅) R (Γ ∗, Δ∗, Θ∗).
Assume 3A ∈ Γ . Then, for all (Γ 0, Δ0, Θ0) such that (Γ, Δ, Θ) ≤ (Γ 0, Δ0, Θ0) we have 3A ∈ Γ 0. We claim that (2−1Γ 0 ∪ {A}, Θ0, ∅) must be consistent. For otherwise, if there exist M1, M2, . . . , Mm ∈ 2−1Γ 0 and N1, N2, . . . , Nn ∈ Θ0 such that ∅; M1, M2, . . . , Mm, A `CK N1 ∨ N2 ∨ · · · ∨ Nn, then by the rules of CK we could derive ∅; 2M1, 2M2, . . . , 2Mm, 3A `CK 3(N1 ∨ N2 ∨ · · · ∨ Nn), and consequently ∅; Γ 0 `CK 3(N1 ∨ N2 ∨ · · · ∨ Nn) contradicting consistency of theory (Γ 0, Δ0, Θ0). Since (2−1Γ 0 ∪ {A}, Θ0, ∅) is consistent we can let (Γ ∗, Δ∗, Θ∗) be a maximally consistent extension of (2−1Γ 0 ∪ {A}, Θ0, ∅). We have (Γ 0, Δ0, Θ0) R (Γ ∗, Δ∗, Θ∗) and A ∈ Γ ∗. By induction hypothesis, (Γ ∗, Δ∗, Θ∗) |= A which proves (Γ, Δ, Θ) |= 3A.
Assume 3A 6∈ Γ . Then, (Γ, ∅, {A}) is consistent, since ∅; Γ `CK 3A under deductive closure of Γ would imply 3A ∈ Γ contradicting the assumption. So, by Lemma 2 there is a maximally consistent extension (Γ ∗, Δ∗, Θ∗) of (Γ, ∅, {A}), with Γ ⊆ Γ ∗ and A ∈ Θ∗. Moreover, (Γ, Δ, Θ) ≤ (Γ ∗, Δ∗, Θ∗). Now let any R-successor (Γ 0, Δ0, Θ0) of (Γ ∗, Δ∗, Θ∗) be given. By definition of R we have A ∈ Θ∗ ⊆ Δ0, which implies A 6∈ Γ 0. Hence, by induction hypothesis, (Γ 0, Δ0, Θ0) 6|= A as desired.
It is worthwhile to point out that our proof in fact simplifies4 considerably Wijesekera’s model representation of CK. Wijesekera’s models use sets of sets (second order), called segments, where we have simple sets Θ.
Finally we complete the story, proving our main theorem: Proof (Theorem1). Suppose Γ1; Γ2 6`CK A. Then, by (ii) of Lemma 1 we have ∅; 2∗Γ1∪ Γ2 6`CK A. The Model Existence Theorem 2 yields a counter model M and a world w0 for which M, w0 |= 2∗Γ1 ∪ Γ2 but M, w0 6|= A. Thus, 2∗Γ1 ∪ Γ2 6|= A, which finally implies Γ1; Γ2 6|= A by (i) of Lemma 1. 4
Finite Model Property and Decidability We now show that CK has the finite model property, which implies decidability. Both results can be obtained also from general work on many-dimensional modal logics [GKWZ03] by encoding CK into a classical bi-modal (S4,K) system, thus making the underlying intuitionistic accessibility explicit. We find it instructive, nevertheless, to give a direct proof in order to shed more light on the structure of the canonical models. Also, from our concrete construction it can be shown that if we require ≤ to be antisymmetric, then the finite model property is lost.
Theorem 3 (Finite Model Property). |= A iff M |= A for all finite CK-models M . Proof. (Sketch) Let M = (W, ≤, R, |=) be a fixed but arbitrary CK-model and A a proposition. To preserve the forcing of A on M two flavors of local information are relevant at any given world w. Firstly, there is the set T (w) of all sub-formulae that are validated at w, i.e.the set
T (w) d=ef {N | N ∈ Sf(A) & w |= N }, where Sf(A) refers to the set of sub-formulae of A, including ⊥, T, which we consider sub-formulae of every formula. Secondly, we need to preserve the set of sub-formulae of A that are refuted on all R-reachable successors of w, i.e.
Fm(w) d=ef {N | N ∈ Sf(A) & ∀v. wRv ⇒ v 6|= N }.
Note that if w ≤ v then both T (w) ⊆ T (v) and if w R v then 2−1T (w) ⊆ T (v) as well as Fm(w) ∩ T (v) = ∅. 4 This is not a consequence of our dropping of axiom ¬3⊥ but seems applicable also for Wijesekera’s (normal) system.
The two sets (T (w), Fm(w)) characterize the behavior of w inside model M with respect to the sub-formulae Sf(A).5 These pairs are finite theories, called A-theories. More generally, an A-theory in M is a pair (X, Z) of subsets X, Z ⊆ Sf(A) such that there exists a world w in M with X = T (w) and Z ⊆ Fm(w). Let the (finite!) set of all A-theories in M be denoted by T hM (A). Note that for any world w in any CK-model M , the pair w≡ = (T (w), Fm(w)) is an A-theory, whence T hM (A) is non-empty whatever the A and M .
M |A = (T hM (A), ≤ |A, R |A, |= |A) (X, Z) ≤ |A (X0, Z0) iff X ⊆ X0 (X, Z) R |A (X0, Z0) iff 2−1X ⊆ X0 & Z ∩ X0 = ∅ and forcing such that (X, Z) |= |AK if K ∈ X or ⊥ ∈ X, for both propositional constants K = p and falsity K = ⊥. For all other propositions N we define (X, Z) |= |AN according to the inductive conditions stated in Def. 1. Note that w ≤ v implies w≡ ≤ |Av≡ and wRv implies w≡R |Av≡. It is easy to verify that M |A indeed is a well-defined finite CK-model.
Finally, we show that for all N ∈ Sf(A) and Z ⊆ Fm(w), w |= N iff (T (w), Z) |= |AN. (3) by induction on the structure of N , which completes the proof of Theorem 3.
We can now prove the completeness direction of Theorem 3. Suppose 6|= A for some formula A. Then there exists a counter model M and a world w in M such that w 6|= A. Construct the finite filtration model M |A as above relative to A. Since trivially A ∈ Sf(A), (3) gives us w≡ 6|= |AA. Thus, we have found a finite counter model for A.
As a corollary to the soundness and completeness (Thm 1) and finite model property (Thm 3) we obtain decidability of CK: Theorem 4. The theory CK is decidable. 5
Conclusions This fairly technical note shows that CK can be given a sensible possible worlds semantics, under which the system is sound and complete, has the finite model property and hence is decidable. The proof considerably simplifies the canonical model construction of Wijesekera’s in the propositional case and it also accommodates fallible worlds. We hope to extend this semantics to the first-order case in the future.
The existence of these proofs vindicates our belief that “whenever we can get a categorical semantics, we can get a possible worlds one”. The work here is inspired by the need to provide formal proof theory and semantics for the system that we started 5 The standard filtration would only consider T (w), so we are somewhat finer here. describing in [BCC+05]. Further research will have to substantiate the claims that the system is adequate for the application at hand, contexts in AI. Observe that the system CK does satisfy our requirement of imposing only minimal constraints on abstract modalities. Thus it provides a convenient playground to investigate various special context modalities in the way of correspondence theory, linking different proof-theoretic extensions with particular classes of Kripke models. While it is clear that many tradeoffs between expressivity and simplicity/efficiency of use will have to be adressed to adequately model contexts in AI, the discussion of these trade-offs needs a solid mathematical basis to build on. It is the mathematical basis that we have addressed in this note. [GKWZ03] D.M. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional
Modal Logics: Theory and Applications. Norht-Holland, 2003. [McC93] J McCarthy. Notes on formalizing context. In Proc. of the 13th Joint Conference on
Artificial Intelligence (IJCAI-93), 1993. [Pop94] S. Popkorn. First Steps in Modal Logic. Cambridge University Press, 1994. [SDP01] C. Schurmann, J. Despeyroux, and F. Pfenning. Primitive Recursion for Higherorder Abstract syntax. Theoretical Computer Science, 266:1–57, 2001. [SG02] L. Serafini and F. Giunchiglia. Ml systems: A proof theory for contexts. Journal of
Logic, Language and Information, 11(4):471–518, 2002. [Wij90] D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic, 50:271–301, 1990.