Parameter Structures for Parametrized Modal Operators

Introduction

Modal logics are used with various interpretations, as epis­ temic logic to express the knowledge of an agent, as doxastic logic to express belief, as temporal logic to express temporal relationships, as action logic to express the effect of actions in the world etc. Many of these interpretations require the modal operators to be parametrized with agents, actions, etc.

One interpretation of the parameters however has not yet been trie<t, namely the interpretation as probability values, such that for example [p]F with p e [0,1] expresses that F holds in at least (exactly, at most) p*100% of all cases (worlds). The reason might be that in this application numerical (or symbolic) computations with these parameters

* This work has been supported by the ESPRIT project MEDLAR and the SFB 314 of the German Science Foundation (DFG).

Thanks to Luis Fariftas del Cerro for useful discussions.

Andreas Herzig IRIT, Universite Paul Sabatier 118 route de Narbonne F-31062 Toulouse Cedex, France email: herzig@iritfr Tel. ... 33 6155 6764

have to be an essential part of the calculus. For example [.5][.6]F which expresses that in 50% of all cases it is true that in 60% of their subcases F holds, should imply [.3]F. That means we have to integrate the operations on the parameters-very deeply into the logic.

When we adopt the interpretation that [p ]F means at least p*100% (the other versions are similar) then there are more rules we would like to have:

(p ~ q A [p]F) => [q]F, i.e. [.6]F => [.5]F,

([p]F" [q]G) => max(O, J>+q-1)(F "G),

i.e. ([.6]FA[.7]F)=>[.3]F (conservative estimation for proba­ bility of simultaneous events based on minimal overlaps),

([p]F A [q]F) ~ [max(p,q)]F,

([p]F v [q]F) ~ [min(p,q)]F,

-,[p]F ~ [1-p]+-,F, i.e. -,[.4]F ~ [.6]+-,F,

where [.6]+F is true if F holds in more than 60% of all cases.

Unfortunately it turned out that the standard relational Kripke semantics for modal logic is not sufficient to support these rules. In classical modal logics there is one (or several) binary relations on worlds which is used to determine for the "actual world" the set of all accessible worlds [Kripke 59,63]. cF is true in the actual world iff F is true in all accessible worlds. At first glance it should be possible to use the standard accessibility relation and interpret [p]F: There is a p*100% subset U of the worlds accessible from the actual world and F holds in all these worlds U. This version, however, fails to support the rule [p][q]F => [p*q]F. The following picture of a typical possible worlds structure shows what goes wrong.

In order to overcome this problem we have to keep not only an actual world, but also an actual world set which serves as reference set against which to count the worlds. To this end we switch from the relational possible worlds struc­ ture to a kind of neighbourhood semantics [Rautenberg 79] or minimal model semantics [Chellas 80] and replace the accessibility relation by an access function cp(p,U) which computes for a parameter p and an actual world set 'll a set of sets of accessible worlds (neighbourhood structure). For example cp(.5, 'l1) may compute the set of all at least (exactly, at most) 50% subsets of 'll. If 'll is the actual world set then [p]F is interpreted: there is a set 'lie cp(p, 'l1) (a p* 100~ sub­ set of 'll) and F holds in all worlds of 'II. The nestmg of operators is no problem any longer. If 'lie cp(.5,'U) and '1/'e cp(.6, '0 then 'II' e cp(.3, 'll). Thus, [.5][.6] ~ [.3]F.

To our surprise it turned out that with this simple idea we have discovered a very general principle which permits a uniform treatment of many kinds of operations on parame­ ters in may applications of modal logic, new and old ones.

In order to demonstrate that the theory is of general nature we use the following five very different applications of the logic:

1. Epistemic logic with a single agent. [p]F means, agent p knows F.
2. Epistemic logic with a set of agents. [p]F means, every agent in the set p knows F.
3. Temporal Logic with duration parameters. [p )F means there is an interval I of length p and F holds at each instant in I.
4. Action Logic. [p]F means, after performing p, F holds.
5. Probabilistic Logic. [p]F means, F holds in at least p* 100 % of all cases. (Note that although we only use the interval [0 ... 1] for probability values, there can be arbi­ trary qualifications such as "may be", "very likely", etc.)

Common aspects which have shown up are for example that the multiplication of probability values corresponds (the same laws hold) to the sequencing of actions in the action logic interpretation. The operation max(O, p+q-1) corre­ sponds to parallel execution of independent actions.

In order to cover as many applications as possible we introduce generic operations on the parameters which have to be instantiated with concrete operations in each particular application. For each generic operation a correspondence bet­ ween a characteristic axiom schema (like [p)[q]F ~ [p®q]F) and a characteristic property of the access function cp is shown. This correspondence plays the same r6le as for ex­ ample the correspondence between the rule cF ~Fin classical modal logic and the reflexivity of the accessibility relation. Correspondences of this kind are essential for incor­ porating desired axiom schemas efficiently into semantics based deduction calculi [Fitting 83, Ohlbach 88, Herzig 89, Auffray & Enjalbert 89]. In this paper however we present only the basic logic itself and prove the correspondence theorems. The applications - the probabilistic application as well - are used to illustrate the ideas. They are not investigated themselves.

The logic we present is first order and permits arbitrary nesting of modal operators and quantifiers. For example Vx:human [.5]male(x) and [.5]Vx:human male(x) are both allowed formulae, but with totally different meaning. This is one of the differences to standard theories for dealing with uncertainty where this is usually not possible, as for example in probability theory [Frost 86], certainty theory [Shortcliff & Buchanan 75], Dempster Schafer theory of evidence [Schafer 76], possibility theory [Zadeh 78] or incidence calculus [Bundy 84]. In [Halpern 89] there has been given a possible worlds model for a probability logic ~here this problem is solved by introducing two different nobons: probabilities on the world and probabilities on the domain.

The reader is assumed to be familiar with modal logic ([Hughes & Cresswell86], [Chellas 80], [Fitting 83]).

In the sequel we use the following notational conven­ tions for writing formulae: Syntactic objects are written in standard letters, whereas semantic objects are written in italics. For example if x is a variable symbol, then ~denotes its interpretation with respect to a given variable assign­ ment. F, G, Hare used as meta symbols for formulae.

Syntax and Semantics

The logic is defined as an extension of many sorted first order logic. For the purpose of this paper it is not necessary to fix the particular kind of the sort structure. Any kind of logic which allows different sorts will do, for example logics of [Walther 87, Schmidt-SchauB 89, Cohn 87]. We only dis­ tinguish one sort as a "parameter sort". In the sequel we use "P" as the name of this sort and we call terms of sort P "P­ terms". For this sort we further presuppose the existence of the following function and predicate symbols: function sym­ bols n, u, n, lY and®, all of them of sort PxP~P. a func­ tion symbol - of sort P~P and a predicate symbol E of sort PxP. The sort P together with these symbols make up the parameter signature I.p = (P, n, u, li"ii, lYI, ®,-,E).

The formulae are built in the usual way using the logical connectives and quantifiers -,, A, v, ~. <=>, V, 3. Further­ more there are the parametrized modal operators [p] and <p>. The syntax rule for these operators is: If p is a P-term and F a formula then [p]F and <p>F are formulae. The <p> opera­ tor is used as an abbreviation for -,[p)-,.

Algebras and homomorphisms [Grntzer 79] are the basic building blocks for the defmition of the semantics of well sorted terms and well formed formulae. A I.-algebra J'l for a signature r. containing the available syntactic objects con­ sists of a carrier set D ;;r: and a set of functions which corre­ spond tor. in the right way. The carrier set is divided into subsets according to I.'s sort structure. A special I.-algebra is the algebra of free terms where the carrier set consists of the well sorted terms themselves and the functions are construc­ tor functions for terms. This fact can be exploited to define the semantics of terms just by an homomorphism from the free term algebra into a corresponding I.-algebra. A I.-algebra does not contain objects that correspond to predicate symbols. Therefore I.-structures are I.-algebras together with relations as denotations for the predicate symbols. We write QJI for the interpretation of the symbol Q in the I.­ structure or I.-algebra Jt

Definition 1 Semantics

A frame <I> = ('W, P, cp) over a parameter signature I.p, i.e. a signature containing the syntactic components of the parameter sort P, consists of

• a set 'J1/ of worlds,
• a I.p-structure P of parameter values,

• cp is a function cp: Px 2'W ~ 22w, i.e. cp computes for a parameter and a set of worlds the neighbourhood as a set of sets of worlds. We call cp the access function.

For a signature l: containing l:p, a l:-interpretation g =(ell, 'U, u. E, 8) consists of

• a frame ell= ('W, P, cp),
• the actual world set 'l1 ~ 'HI,
• the actual world u e 'U,
• an assignment E of worlds to l:-structures. The substruc­ ture corresponding to l:p is the same in all worlds, and
• a variable assignment 8, i.e. a mapping from variables to domain elements.

We say the interpretation g is «1>-based.

In the sequel g[x/~ is like g and 8[x/~ is like e except that e maps the variable x to the value ~ There is an induced homomorphism g h which interprets terms in the actual world u. We usually write g(t) instead of gh(t) to denote t's value in the particular interpretation g.

• The satisfiability relation F is defined as follows: Let g = (ell, 'll, u. E, 8) be an interpretation.
• g F P(t1, ...· tn) iff (g(t1), ... ,g(tn)) e P:::(u)·
• g F 'v'x:S F iff for all ~e S:::(u) g [x/~ F F.
• g F [p] F

iff there is a set '1/e cp(g(p), 'll) such that ve 'Iliff (ell, o/, v, E, 8) F F. (We say that F holds exactly in V.)

• The interpretation of the logical connectives -,, "· v, =>, <=>, 3 and <p> is as usual.

For a frame ell:

• ell F F iff g F F for all ell-based interpretations g. A frame satisfying a formula, i.e ell F F is called a model for F. If every frame satisfies F we say that F is valid. ·

Like in standard modal logics, the differenciation between frames and interpretations allows us to fix certain properties of the semantic structure for all interpretations based on a frame. Traditionally these are properties of the accessibility relation like reflexivity etc. Classes of frames with the same property then make up a logic (e.g. K, T, S4 etc.). We included in the definition of a frame not only the access func­ tion cp as a substitute for the accessibility relation, but also the parameter structure. This permits the distinction of logics according to certain properties of the access function and the parameter structure.

Our semantics differs in a key point from standard neigh­ bourhood semantics. We need the neighbourhood not of the actual world, but of the actual world set. Therefore the function cp accepts a set of worlds as input and returns the neighbourhood of this set. In the case of unparametrized modal operators this makes no difference to standard neighbourhood semantics. For the parameterized case, however it is essential for interpreting the parameters as probability values which count worlds.

In the concrete definition of the access function cp, the intuition about the actual application can be manifested. For example in the epistemic interpretation with a single agent, cp returns the basic set of worlds the agent considers in his mind together with its supersets. If different frames of mind are to be modeled in which the agent may believe controver­ sial things then several different basic sets are returned [Fagin & Halpern 88]. In the epistemic interpretation with a set of agents, cp returns a single basic set with the union of all worlds the agents consider (again together with their supersets). In the temporal interpretation with duration parameter, cp(p, .. ) returns the set of intervals with length p. In the action logic interpretation, cp returns the sets of worlds which are caused by each action. Finally in the probabilistic interpretation, cp(p, 'll) returns the set of subsets of 'l1 with at least p*100% of its elements.

Some theorems which carry over from modal logic with standard neighbourhood semantics are collected in the follow­ ing lemma [Chellas 80, Rautenberg 79].

Lemma 2

1. IfF<=> G is valid then [p]F <=> [p]G is valid.
2. For all frames ell the following statements are equivalent: l. IfF=> G is valid then [p]F => [p]G is valid in ell.
3. The access function cp is upwardly closed, i.e. if '1/e cp(p,'ll) then all supersets of '1/are in cp{p/ll).
4. In frames with upwardly closed access functions the following axiom schemas are valid:

[p](F A G) => [p]F" [p]G and

[p]F v [p]G => [p](F v G).

The converse implications do not hold.

·

From now on we choose "F holds in at least p*100% of all cases" as the probabilistic reading of [p]F, and require thus cp to be upwardly closed in this case.

Characterizing the Parameter Structure

In a sequence of theorems we investigate the correlations between the operations ·· n, u, n, l!l, ®, - on the parameter structure and characteristic formula schemas. We start with the ·-relation.

Theorem 3 For evey frame ell = ( 'W, P, cp) the following statements are equivalent:

1. ell F (p 50 q" [q]F) => [p]F.
2. For p, qe P, p!ii qimplies for all 'U: cp(q, 'll) ~ cp(p, 'll). IEQf: "1~2": Let pli qand '1/e cp(q, 'll) for some 'U. Take a predicate F and a ell-based interpretation g with actual world set '1/where F holds exactly in '1/:S worlds. g satisfies [q]F and p 50 q and, by 1) also [p]F. Therefore there is a 'II' e cp(p, 'll) and F holds exactly in 'II'. Since F holds exactly in o/, 'II' = '1/ E cp{p, 'U).

"2~1": IfF holds in a set '1/ofworlds computed by cp(q, 'll), and cp(q, 'll) ~ cp(p, 'U) where p · q, '1/e cp(p, 'll). Thus, :r holds also in a set of worlds computed by cp(p, 'll) and therefore the implication 1) must be true. ·

Possible meanings of the !;-predicate in the different applications of the logic are as follows. In the epistemic interpretation with a single agent, p E; q means that p knows everything q knows. In the epistemic interpretation with a set of agents, p s; q is just the subset relation. In the tempo­ ral interpretation with duration parameters, p Iii q enforces that q denotes a shorter period than p. In the action logic interpretation, p Iii q is a specialization relation. For example move Iii walk expresses that everything that can be achieved with the action 'move' can also be achieved with the action 'walk'. In the probability interpretation Iii is just the less equal relation on numbers.

If the sr-relation has top and bottom element - assume they are denoted by 1 and 0 - according to theorem 3 the axioms [1]F => (p]F and (p] => [O]F hold. This allows for some interesting interpretations of these top and bottom elements. In the epistemic interpretation with a single agent, a top element is a gossip. What he knows everybody knows. A bottom element is ''big brother". He knows everything the other agents know. In the epistemic interpretation with a set of agents, 0 denotes the empty set and 1 denotes the set of all agents. In the temporal interpretation with duration parameters, 0 denotes the empty period and 1 a longest period (day, month or whatsoever). In the action logic inter­ pretation, there is no meaningful bottom element. A top element might be "do-something". In the probability inter­ pretation the top and bottom elements are simply the num­ bers 1 and 0 expressing "certainly" and "no information".

Next we consider the n operation which corresponds to the intersection of sets of accessible worlds.

Theorem 4 For all frames cl> = ('W, P, q>) the following statements are equivalent:

1. For all operator free formulae F and G: cl> t= ([p]F" [q]G) => (pli"'lq](F" G).
2. For all p. q e P, for all 'U: <p(p, 'l1) n q>(q, 'l1) !:: <p(pn q, 'l1) where A r'l B =deda n b I a e A, be B}

fulQf: "1~2": Let~ q>(p. 'll) r'l q>(q. 'll).

There are o/pe q>(p, 'll) and 'V'qe q>(q, 'l1) with 'II= 'llpn '11 1 Take predicates F and G and a cl>-based interpretation 5 where F holds exactly in 'lip's worlds and G holds exactly in 'V'q's worlds. Thus, [p]F A [q]G is satisfied and therefore, by 1) also [pnq](F " G). That means, F " G holds exactly in a set '!/' e <p(pii q, 'll). Since F holds exactly in 'lip and G holds exactly in 'V'qo 'II'= 'llpn 'V'q= o/e <p(pn q, 'U).

"2~ 1": If [p]F " [q]G is satisfied then F holds exactly in a set 'lip e <p(p, 'll) and G holds exactly in a set 'V'q e <p(q, 'll). Since F and G are operator free, F " G holds exactly in 'lip n 'V'q and because of 2), 'lip n 'V'qe q>(pn q, 'll) and therefore [pliilq](F" G) is satisfied as well. +

There are meanings of n in all applications we consid­ ered. In the epistemic interpretation with a single agent, IV computes a common close confidant (maybe a father confes­ sor) who knows everything the two agents know. In the epistemic interpretation with sets of agents, IV computes the intersection of two sets of agents. In the action logic interpretation, p ll'il q means parallel execution of independent actions. In the temporal interpretation, n computes minimal overlaps with respect to a maximal interval length. For example from [12h]shining(sun) and [13h]-,shining(sun)

with respect to a maximal interval length of 24 hours we get [1h = 12hn13h] (shining(sun) A -,shining(sun)), i.e. a con­ tradiction. In the probabilistic interpretation n also com­ putes minimal overlaps. In this case p n q = max(O, p+q-1). This is the lower bound for the intersection of events. Therefore for example [.6]F A [.7]G yields [.3](F" G).

The result for n is slightly stronger than that for n:

Theorem 5 For all frames cl> = ( 'W, P, <p) the following statements are equivalent:

1. For operator free formulae: cl> t= ([p]F" [q]F) ¢::> [pnq]F.

2) For all p, q, U <p(p, 'l1) n q>(q, 'l1) = <p(pn q, 'll).

£rom: "1~2": The proof of the "!::"-direction is similar to that for the n operation. To establish the inclusion in the other direction, let o/e <p(pn q, 'll). Take a predicate F and a cl>-based interpretation 5 with actual world set 'l1 where F holds exactly in o/'s worlds. Thus, 5 satisfies [pnq]F and with 1) [p]F" [q]F as well. Therefore there are sets 'lip e <p(p, 'll) and 'V'q e <p( q, 'll) such that F holds exactly in 'lip and in 'V'q. SinceFholds exactly in 'II, 'V'p='V'q='V'e <p(p,'U)n q>(q, 'll).

"2~1": For the=> direction, let[p]F" [q]F hold exactly in 'U, i.e. F holds exactly in a set 'lip e <p(p, 'll) and in a set 'V'q e <p{q, 'U). As F is operator free, 'lip= 'Ill/" Using 2) we get that 'lip e <p(pn q, 'll). Thus, [pnq]F holds as well. The proof of the"~" direction is similar. +

Note that in the case of upwardly closed <p, validity of the formula ([p)F" [q]F) ¢::> [pnq]F entails validity of the formula ([p]F " [q]G) => [pnq](F v G) by Lemma 2.b). In the probabilistic interpretation n computes lower bounds for the union of events: In this case pnq = max(p,q). The validity of ([p]F 1\ [q]G) => [pnq](F v G) can be interpreted as follows: "If the probability ofF is at least p and that of G at least q, then that ofF v G is at least max(p,q)". E.g. [.6]F " [.7]G yields [.7](F v G). Dual ton is u.

Theorem 6 For every frame cl> = ( 'W, P, <p) the following statements are equivalent:

1. For all formulae F: cl> I= ([p)F v [q]F) ¢::> [puq]F.

2) For all p, q, 'U: <p(p, 'll) u <p(q, 'll) = q>(p u q, 'll).

Proof: The proof is similar to the previous one.

+

Dually, in the case of upwardly closed <p, validity of the formula ([p]F v [q]F) ¢::> [puq]F entails validity of the formula [puq](F" G)=> [p]F v [q]G by Lemma 2.b). In the probabilistic interpretation u computes upper bounds for the intersection of events: In this case puq = min(p,q). Now the validity of (-,[p]F 1\ -,[q]G) => -,[puq](F A G) can be interpreted as follows: "If the probability of F is less than p and that of G less than q, then that of F " G is less than min(p,q)". E.g. -,[.6]F" -,[.7]G yields -,[.6](F" G).

Next we consider the multiplication operation ® which allows to collapse sequences of operators into a single opera­ tor. On the semantic side, p® qmust be a parameter such that q>(p® q, 'll) collects the sets of worlds, that correspond to applying fU"St <p(p .. . ) and then <p(q .·. ) to its results.

Theorem 7 For every frame <l> = ( 'W, P, cp) the following statements are equivalent:

1. <l> F [p][q]F ~ [p®q]F.
2. For all p, q, 'll: 'II e ~' 'll) cp(q, 'II) = cp{p® q, 'll).

Proof: "1~2. c; part": Let 'II' e 'lie ~p,'ll) cp(q, 'II). Take a predicate F and a <1>-based interpretation 5 where F holds exactly in 'll''s worlds. As there is a 'lie cp(p, 'll) such that '11' e cp(q, 'II), [p][q]F is satisfied and with 1) [p®q]F as well. Therefore there is a set o/ e cp{p® q, 'll) and F holds in o/. Since F holds exactly in 'll', o/ = '11' e cp{p® q, 'll).

"1~2.;:! part": The proof is similar.

''2~1 ": [p][q]F is satisfied iff there is a set 'lie cp{p, 'l1) such that F holds exactly in a set '11' e cp(q, ""'· By 2) this is equivalent to F holds exactly in a set '11' e cp(p® q, 'll), which means that (p®q]F is satisfied. ·

In the epistemic interpretations there is no obvious inter­ pretation of the multiplication function. In the temporal interpretation p®q = q. For example [12h][6h]shinig(sun)~ [6h]shinig(sun). In the action logic, ® obviously denotes sequencing of actions. Finally in the probability interpreta­ tion ® can be used to compute the overall probability of nested probabilities. For example [.6][.5]F ~ [.3]F.

The inverse operation - we are going to introduce now is useful for turning negative information into positive infor­ mation using the equivalence -,[p]F ~ [-p]+ -,F. The moti­ vation comes again from the probabilistic interpretation where we want to express something like: if it is not the case that F holds in at least p% of all worlds then -,F must hold in more than 100-p % of all worlds. This schema, how­ ever holds only under a number of restrictions to the access function (which are fulfilled in the probabilistic application). Therefore we first introduce a couple of additional notions.

Definition 8 For a set A of sets let basis(A) =def { B e A I there is no subset of B in A}. u-cl(A, 'l1) =def {B u C I B e A, C e 2'll}, i.e. u-cl(A, 'l1) contains all supersets in 'll of all its sets. Hence an access function cp in a frame <l> = ('W, P, cp) is upward! y closed iff u-cl( cp(p,'U), ~ = cp(p, 'll). Let

~p,'ll)) =def u-cl( { 'll\ '111 'lie basis(cp(p,'Zl)}, ~.

An access function cp is called

• restricting iff basis(cp(p,'ll)) ~ 2'll, i.e. cp yields subsets of 'll.
• covering iff it is restricting and for all 'II e basis( cp(p, 'll)) all other subsets of 'llwith the same cardinality as 'II are also in cp{p, 'll).

The formal semantics of the [p]+ operator is:

5 I= [p]+F iff F holds in a proper superset of some set '}I e cp{p, 'll).

+

Theorem 9 For all frames <l> = ('W, P, cp) with upwardly closed and covering access function cp the following statements are equivalent:

1. For all formulae F: <l> F -,[p]F ~ [-p]+ -,F
2. For all p e P, for all 'U: ~,'ll) = cp(-p, 'll).

Proof: "1~2. c part": Let 'lie 'lf'(p,'ll).

~: 'lie basis('lp(p,'ll)), i.e. there is a 'VC e cp(p, 'll) with

'II= 'VC\ 'll. If 'VC= 0 then 'II= 'll e cp(-p, 'l1) because cp is re­ stricting and cp(-p, 'l1) is upwardly closed. Therefore assume 'VC :1:- 0. Take a predicate F and a <1>-based interpretation 5 where -,F holds exactly in a set 'llu { w} :1:- o/. That means F holds only in a proper subset of 'VC. Since 'VC e basis( cp(p, 'Zl)), no proper subsets of IJIC are in cp{p, 'll). Therefore 5 does not satisfy [p]F, but, by 1) 5 satisfies [-p]+ -,F, i.e. -,F holds in a proper superset '11' of some set '11'' e cp(-p, 'll). Since -,F holds exactly in 'llu { w}, '11'!;; 'llu ( w}, and therefore 1'11"1 ~ I'J.-1. Since cp is covering, cp(-p, 'l1) contains a subset of 'lland with cp being upwardly closed, we obtain 'II e cp{-p, 'll).

Case 2: If '11 I! basis(qf(p, 'll))) there is a subset of 'IIi n basis(tp(p,'Zl))) which by case 1 is also in cp(-p(p), 'll) and because cp is upwardly closed, 'lie cp(-'l(p), 'll).

"1 ~2.;:! part": Let 'lie cp(-p(p), 'l1) and 'jiC = 'll\o/. If 'J!C = 0 then again 'll= 'll e 'lf'(p,'ll)). Therefore assume '11:~:- 0. Take a <1>-based interpretation 5 where -,F holds exactly in a set 'llu { w} :~:- 'II. Thus, 5 satisfies [-p]+ -,F and with 1) -,[p]F as well. If there was a 'II' e basis( cp{p), 'll) with 1'111 $ I'U\(fu{ w})l then coveringness and upward closedness would enforce 'll\ ('llu { w}) e cp(p, 'll). In this case, however, F is satisfied in 'U\ ('llu { w}) which contradicts -,[p]F. Therefore for all '1/'e basis(cp(p,'Zl)) 1'111 ~ I'Jt'l and l'll\'111 $l'lti. Cove­ ringness and upward closedness of cp now yields 'lie ~p, 'll).

"2~ 1, ~ part": Let 5 be a <I>-based interpretation with actual world set 'll, and let 5 satisfy -,[p]F. Let 1£be the set of 'll's subsets satisfying -,F. 1£can be ordered by c. Since all elements of 1£are subsets of 'll, every ordered chain in 1£ has a maximal element. Applying the lemma of Zorn we obtairr a maximal element 'll' e 1£ and -,F holds in 'll'. That means every 'lie cp(p,'Zl) must intersect 'll ', otherwise [p]F would hold. Since cp is covering, there is a 'lie basis(cp(p,'ll)) with 'jiC = 'l.t\'11 c 'll'. Furthermore 'jiC e 'lf'(p,'ll) = cp(-p, 'l1) (by 2) and therefore -,F holds in a proper superset of 'jiC e cp(-p, 'll). Thus, [-p]+ -,F is satisfied as well.

"2~1. ¢::part": Assume [-p]+-,F holds, i.e. -,F holds in a proper superset of some 'lie basis(cp(-p, 'll)). Using 2) we obtain '11'= 'lt\'lle basis(qr(p,'ll)). Every set satisfying F must be a proper subset of 'j~Cand cannot be in-( cp(p, 'll), 'll). Therefore, -,[p]F must hold as well. ·

The most obvious meaning the inverse function can have is in the probability interpretation. In this case -p is defined as 1-p. This means e.g. -,(.6]F ~ [.4]+-,F, i.e. if it is not the case that in at least 60% of all cases F holds then its negation must hold in at least 40% of all cases. There is an analogous meaning in the temporal case where the interval lengths are determined relative to the actual interval.

Conclusion

We have presented an extended possible worlds semantics for modal logics. It is based on the idea of neighbourhood semantics and it supports the incorporation of correlations between different parameters into the logic in applications requiring parameterized modal operators. This permits new applications of the idea of possible worlds semantics. For each application, the theory we have presented gives a con­ crete guidance for the development of the parameter structure and the corresponding operations on these parameters.

In particular there is an interpretation as a probabilistic logic where the modal operator [p ]F expresses that F holds in at least p*100% of all cases. Since the logic is full first order, probability values and quantifiers can be arbitrarily mixed. Non-numerical parameters are also allowed.

The way to develop applications of our general frame­ work is as follows: As usual in modal logic, truth is defmed relative to a class of frames. For each application there is a class of frames which best approximates the intuition behind the application. The buttons we can tum in order to specify the class of frames are the properties of the access functions and the properties of the parameter structure. The weak homomorphism conditions in the statements 2 of the theo­ rems 3-9, however, set the limits on these manipulations. The stronger we restrict the class of parameter structures we allow in an application, the stronger we restrict the class of access functions. Therefore it has always to be proved that there is still at least one access function that satisfies these weak homomorphism conditions. Typically, however, we proceed the other way round. We define a class of access functions first. Then we have to look how far we can restrict the class of parameter structures without further restricting the class of access functions.

There are of course still a lot of things to do. An additional implication H can be introduced which is more natural e.g. in the probabilistic application. It permits the interpretation of PH [.2]Q as "Q holds in 20 % of the cases where P holds".

A logic without a calculus is as useless as a pro­ gramming language without an interpreter or compiler. Therefore the most important step is to develop a calculus for this logic. Experience with classical (first order) modal logics has shown that it is no good idea to develop a calcu­ lus operating on the original logic directly. Therefore we aim at a translation method which permits the translation of mo­ dal formulae into predicate logic such that standard predicate logic deduction methods can be applied [Ohlbach 88, Herzig 89, Farii'las & Herzig 90]. Applied to our case the method translates for example a formula [p]Q into 3X "i/x x e X(p) => Q'(x). The interpretation of this translated formula is: X is a function which, applied to p yields a particular set of functions x mapping the actual world to some world where the predicate Q' holds.

Since our logic has no built in assumptions at all it contains none of the paradoxes, other theories of certainty suffer from. Moreover, it should be possible to axiomatize the other theories within our framework. For example the statistic probability of independent events multiplies whereas we have the logically sound, but sometimes too weak minimal solution max(O, p+q-1). We can however easily add an axiom "i/p,q [p]P 1\ [q]Q => [p*q](P 1\ Q) such that for particular P and Q where [p*q](P A Q) can be derived, this subsumes the built in inference [max(O, p+q-1)] (P 1\ Q). We have to investigate how far we can go in this direction.