A Model Theory for a
Quantified Generalized Logic of Contexts


[$Working$ $draft$ $Revision: 1.34$ - $please$ $do$ $not$ $distribute$]

Selene Makarios

Abstract:

We investigate the formal semantics of a quantified version of a generalization of the logic of contexts that uses the operator $ist(c,\phi)$ introduced by Guha 3 (3) and consonant to the notion of context logic as proposed by McCarthy 8 (8). We propose a model theory for this logic, one in which various properties on contexts, deemed as being intuitively desirable, hold in all models. We believe this to be the first offering of a full, rigorous, model-theoretic treatment of the quantified context-logic formalism, since context logic was first described in 1987.

Introduction

The notion of formalized contexts was proposed 8 (8) as a way of addressing the problem of generality in AI. The original idea was to create AI systems that never get ``stuck'' with the set of concepts they are using at any given moment, always being able to transcend any given context to a more general one.

Another perspective is that, for the sake of tractability, contexts allow humans to temporarily fix a domain of discourse and a set of interpretations, for purposes of performing some cognitive or communicative task. Without this ability, that is, if humans were required to always account for all entities, relationships, and the interpretations thereof, while performing a cognitive or communicative task, all such tasks would likely become unmanageable.

McCarthy's and Guha's approach to formalizing context 3 (3); 4 (4); 2 (2) was to introduce an operator `$ist$' , with the intended intuitive meaning that if $c$ is a context, and $\phi$ is a proposition, then the expression

$$ist(c,\phi)$$ (1)

is considered true exactly in case the proposition $\phi$, interpreted in the context $c$, is true. The name `$ist$' is derived from `is true' (according to the account of a given context).

The notion of ``context'' itself is taken as a mathematical primitive in the formalism discussed here. Regardless of what motivating conception of context one employs, what matters is that propositions can be asserted in a context, and then other propositions can be derived in it, or possibly in other contexts that are related to it.

The following are some examples of motivating conceptions of context: a constraint upon time, such as in the Middle Ages, or last Tuesday afternoon; a constraint upon place, such as in the Gobi desert; the context of a given conversation; the context of a particular news report; the context of a fictitious universe, such as the world of Sherlock Holmes; the context of a set of beliefs; a linguistic context, such as a particular tongue, or a collection of application-specific verbal efficiencies¹.

As originally described 8 (8); 4 (4), context logic was a relatively informal idea, presented as a syntax with a framework of examples and intuitions, and suggested approaches to applications. Since that time, the goal of providing a complete semantic account of what the language of context logic really says, and what its operations really do - especially for the quantificational case - has proved difficult to achieve.

We believe the present work to be the first offering of a full, rigorous, model-theoretic treatment of quantificational context logic, during the time since context logic was proposed as a technique in Artificial Intelligence almost twenty years ago. In addition to providing semantics, the formalism described here further generalizes the original concept of $ist$, allowing an elaboration where the truth-conditions that determine a system's modalities can themselves be vary with context - in other words, the meaning of $ist$ itself can be context-dependent.

The Context Logic Language $\cL$

Abstract Syntax.

The syntax of context logic is not, as is customarily the case with formal languages, defined over the collection of sequences of some set of symbols, though it is generally convenient to project context logic expressions onto paper as arrangements of typographic symbols.

The reason for this decision is that there may exist in one's mind a qualitative distinction between ``terms'' and ``sentences''. First-order logic makes this distinction quite formal. But in context logic, we will need to move smoothly from the idea of propositions whose arguments are merely (what might be called) ``terms'', to propositions having arguments that are (what might be called) ``sentences''.

Thus we avoid the expressions ``symbol'', ``term'', and ``sentence'' altogether. Following the approach proposed by McCarthy 5 (5), define the syntax of context logic in terms of ``abstract syntax-objects'' and ``constructs''. It helps to imagine constructs as data-structures, built up from syntax-objects and other constructs via constructors; the entities that do such building will in fact be called ``constructors''. So, the current sentence is the last place the reader will find the words ``symbol'', ``term'', or ``sentence'' used in this work.

The language $\cL$ of context logic is defined over a signature

$$\Tuple{\cF,\cP,\cC,\cA} \comma$$ (2)

where $\cF$ contains function-objects, $\cP$ contains predicate-objects, and $\cC$ and $\cA$ each contain constant-objects. $\cC$ and $\cA$ are disjoint, and intuitively, $\cC$ represents the collection of context objects, while $\cA$ represents the collection of ``ordinary'' or ``domain'' objects. Note that we are still in the realm of syntax here - these are not intended to be semantic objects.

Constructors.

The syntax of context logic employs constructors corresponding to the standard logical connectives $\land$, $\lor$, and $\lnot$ (we will liberally use constructors for implication as well, assuming their analogous definitions in terms of the other constructors); the context-logic specific quantifier-constructors ${\forall_{\mbox{{\scriptsize\texttt{C}}}}{}{}}$, $\forall_{\mbox{{\scriptsize\texttt{A}}}}{}{}$, $\forall_{\mbox{{\scriptsize\texttt{L}}}}{}{}$, and $\forall_\circ$, for quantifying respectively over contexts, over domain objects, over proposition-objects in $\cL$ itself, and over the objects associated with various contexts (in a way to be made precise); the existential counterparts $\exists_{\mbox{{\scriptsize\texttt{C}}}}{}{}$, $\exists_{\mbox{{\scriptsize\texttt{A}}}}{}{}$, $\exists_{\mbox{{\scriptsize\texttt{L}}}}{}{}$, and $\exists_\circ$ of each universal quantifier-construct; and finally, the constructor $\Istsymb{}$.

The constructor $\Istsymb{}$ is the `$ist$' constructor, which is a two-place constructor over $\Times{\cC }{\cL }$. Intuitively, the construct

$$\Ist{}{c}{\phi} \comma$$ (3)

to be formally defined later, produces a proposition-object concerning the status of $\phi$ according to the account of the context $c$.

The set of predicate-objects $\cP$ optionally includes $\Istsymb{}$. This inclusion corresponds to the case where $ist$ is allowed to nest, that is, where the truth of some proposition asserted relative to a context is itself asserted relative to some context. The function-objects in $\cF$ may only apply to term-objects, which are either domain-objects in $\cA$, or are the result of applying function-objects in $\cF$ to term-objects. The predicate-objects in $\cP$, except for $\Istsymb{}$ if it is included, may likewise only apply to term-objects.

For brevity, we may resort to using the expressions ``term'', ``function'', ``predicate'', and ``object'' as abbreviations for ``term-object'', ``function-object'', ``predicate-object'', and ``domain-object'', respectively, with the understanding the use of these expressions is simply a convenience with no ontological significance.

Proposition-Objects

The language $\cL$ has two kinds of ``atomic'' constructs,

$$\FuncApp{P}{\Dots{x_1}{x_k}}$$ (4)

and

$$\Ist{}{c}{\phi} \comma$$ (5)

where $\phi$ is itself a construct in $\cL$, in which $\Istsymb{}$ is not allowed to appear, unless $\Istsymb{}$ is included in $\cP$. If constructs $\phi$ and $\psi$ are in $\cL$, then so are constructs $\Land{\phi}{\psi}$, $\Lor{\phi}{\psi}$, $\Lnot{\phi}$, and $\Limplies{\phi}{\psi}$. If $\phi$ is in $\cL$, then so are

$$% {\forall_{\mbox{{\scriptsize\texttt{C}}}}{(c)}{(\phi)}} \comma$$ (6)

where $c$ is in $\cC$ and occurs free in $\phi$, and

$$% \forall_{\mbox{{\scriptsize\texttt{A}}}}{(a)}{(\phi)} \comma$$ (7)

where $a$ is in $\cA$ and occurs free in $\phi$, and

$$% \forall_{\mbox{{\scriptsize\texttt{L}}}}{(\psi)}{(\phi)} \comma$$ (8)

where $\psi$ is in $\cL$ and occurs free in $\phi$. If $\phi$ is in $\cL$, $c$ is in $\cC$, and $a$ is in $\cA$, then

$$% \forall_\circ {(c)}{(a)}{(\phi)} \comma$$ (9)

where $a$ occurs free in $\phi$, is in $\cL$. There are analogous constructors $\exists_{\mbox{{\scriptsize\texttt{C}}}}{}{}$, $\exists_{\mbox{{\scriptsize\texttt{A}}}}{}{}$, $\exists_{\mbox{{\scriptsize\texttt{L}}}}{}{}$, and $\exists_\circ {}{}$. The construct $\forall_\circ {(c)}{(a)}{(\phi)}$ from (9) will henceforth be abbreviated as

$$\forall_{{c}}{(a)}{(\phi)} \comma$$ (10)

with a similar abbreviation for $\exists_\circ$. In all quantificational forms, parentheses are optional and will be used as needed for clarity.

Semantics of $\cL$

Extending Classical Structures

Our notion of a semantic structure is an extension of the classical notion of a semantic structure for first-order logic. For each $c$ in $\cC$, our context logic structure $\cS$ assigns a context object ${{c}^{\cS }_{}}$, a function ${{f}^{{\cS }{c}}_{}}$ to each $f$ in $\cF$, a predicate ${{P}^{{\cS }{c}}_{}}$ to each $P$ in $\cP$, and a domain object ${{a}^{{\cS }{c}}_{}}$ to each $a$ in $\cA$. The structure $\cS$ will also assign a semantic proposition-object ${{\phi}^{{\cS }{c}}_{}}$ to each $\phi$ in $\cL$, as will be discussed in more detail later.

Thus all $c$ in $\cC$ are rigid designators with respect to context-relative interpretation, but this turns out not to matter. The reason is that there is more to the semantics of contexts than the particular objects they designate, which turn out to be irrelevant (and could just as well been made non-rigid, writing ${{c}^{{\cS }{c}}_{1}}$, with notational cost and no semantic gain). The only characteristic of ${{c}^{\cS }_{}}$ that has semantic significance, is in fact context-relative, see definition (20). Meanwhile, no syntax objects in $\cA$, $\cF$, or $\cP$ need be rigid, nor, as it turns out, do the syntax objects in $\cL$.

The expression ${\cC}^{\cS }$ stands for the collection of all ${{c}^{\cS }_{}}$, ${\cF}^{{\cS }{c}}$ stands for all ${{f}^{{\cS }{c}}_{}}$, ${\cP}^{{\cS }{c}}$ stands for all ${{P}^{{\cS }{c}}_{}}$, and ${\cA}^{{\cS }{c}}$ stands for all ${{a}^{{\cS }{c}}_{}}$. Furthermore, ${\cF}^{{\cS }{}}$ is the union of all ${\cF}^{{\cS }{c}}$, ${\cP}^{{\cS }{}}$ is the union of all ${\cP}^{{\cS }{c}}$, and ${\cA}^{{\cS }{}}$ is the union of all ${\cA}^{{\cS }{c}}$.

The semantics of the logical connectives based on a classical first-order structure are in effect for each $c$. If $P$ is in $\cP$, we write

$$\Miff {\Ent{{\cS }{c}}{}{P(a_1,\cdots,a_n)} } {\In {\Tup... ...dots,{{a}^{{\cS }{c}}_{n}}}} {{{P}^{{\cS }{c}}_{}}} } \comma$$ (11)

and for constructs $\phi$ and $\psi$,

$$\Miff {\Ent{{\cS }{c}}{}{\Land{\phi}{\psi}}} {\Mand {\Ent{{\cS }{c}}{}{\phi}} {\Ent{{\cS }{c}}{}{\psi}} } \comma$$ (12)

$$\Miff {\Ent{{\cS }{c}}{}{\Lor{\phi}{\psi}}} {\Mor {\Ent{{\cS }{c}}{}{\phi}} {\Ent{{\cS }{c}}{}{\psi}} } \comma$$ (13)

and,

$$\Miff {\Ent{{\cS }{c}}{}{\Lnot{\phi}}} {{} \nentsymb_{{\cS }{c}} {\phi}} \period$$ (14)

If $\Ent{{\cS }{c}}{}{\phi}$ for every structure $\cS$, then

$${\Ent{c}{}{\phi}} \period$$ (15)

If $\Ent{c}{}{\phi}$ for every context $c$, then

$${\Ent{}{}{\phi}} \period$$ (16)

Quantification

With $\phi[a]$ denoting $a$ occurring free in $\phi$, and $\phi[a_1/a]$ denoting $\phi$ with $a_1$ replacing $a$, we define

$$\begin{array}{c} \Miff {\Ent{{\cS }{c}}{}{\forall_{\mbox{{\... ...} {\Ent{{\cS }{c}}{}{\phi[{b}_{}/a]} } \comma } \end{array}$$ (17)

and similarly for ${\forall_{\mbox{{\scriptsize\texttt{C}}}}{}{}}$, $\exists_{\mbox{{\scriptsize\texttt{C}}}}{}{}$, $\forall_{\mbox{{\scriptsize\texttt{L}}}}{}{}$, and $\exists_{\mbox{{\scriptsize\texttt{L}}}}{}{}$. At ${{\cS }{c}}$, to each $c_1$ in $\cC$, the structure assigns an object ${\mbox{\texttt{U}}_{c_1}^{{{\cS }{c}}}}$, which is a set

$$\Subset {{\mbox{\texttt{U}}_{c_1}^{{{\cS }{c}}}}} {{{\cA }^{{\cS }{c}}_{}}} \period$$ (18)

Intuitively, ${\mbox{\texttt{U}}_{c_1}^{{{\cS }{c}}}}$ is the collection of items associated with the context $c_1$, as determined by the structure at ${{\cS }{c}}$. Note that a given item can be associated with multiple contexts. We define

$$\begin{array}{c} \Miff {\Ent{{\cS }{c}}{}{\forall_{{c_1}}{a... ...} {\Ent{{\cS }{c}}{}{\phi[{b}_{}/a]} } } \end{array}\period$$ (19)

Context-Relative Contexts

Possible Worlds

The structure $\cS$ includes a set of possible worlds $\cW$ (intended as the same abstract notion of possible worlds as used in modal logic semantics) and a ``consistency relation'' $\kappa_{}$, where

$$% \Subset {\kappa_{}} {(\TimesThree{{\cC}^{\cS }}{\cW }{{\cC}^{\cS }})} \period$$ (20)

Intuitively, we think of a context as a condition on possible worlds. Together, the contexts subsume, but do not necessarily partition, the collection of all possible worlds. Intuitively, the consistency relation $\kappa_{}$ specifies what possible worlds are associated with what contexts. However, each context is allowed to have its own specification, under the structure $\cS$, of which possible worlds are consistent with each context. Whatever these various relative constitutions of the contexts are, however, the set of syntactic context-objects for them is not context-variant, being given as part of the definition of $\cL$.

Intuitively, the expression

$$\kappa_{}({{c}^{\cS }_{1}},{w},{{c}^{\cS }_{2}})$$ (21)

indicates that according to the account of $c_1$, the possible world $w$ is consistent with context $c_2$. This level of generality is employed because we see no reason a priori to rule out the idea of context-dependent contexts, and this subsumes the case of context-independent contexts.

Examples

As an example of a context logic model, let contexts correspond to closed intervals of real time, and then the possible worlds consistent with a given context $t_1$ could be given as those worlds wherein the time falls within $t_1$. As another example, if we take contexts to be the logical closures $[\alpha]$ of assertions $\alpha$ about an arrangement of objects on a table, then the possible worlds consistent with $[\alpha]$ could be given as those worlds wherein $\alpha$ is satisfied, but where other aspects of the arrangement might vary.

Views and Truths

To say that truth is context-relative is meaningless without some way of comparing truths. One could devise an absolute framework within which relative truth is to be assessed; this is the case with the modal valuation function $v(\phi,w)$, which is a universal entity governing all world-relative truth.

But we shall not do this, and instead we leave it to each context to define its own framework within which to assess relative truth. For, ``who'' else is there to assess it? We are declining to require an absolute arbiter of either truth or relative truth, and yet there is no a priori reason to distinguish any one among the contexts themselves for this purpose. The result, of course, is that the assessment of relative truth is itself relative, with each context not only having its own account of what is true, but also a view on what truth means for each among the collection of contexts. Thus, every context can be an arbiter of relative truth, each in its own relative way.

So, for each $c$, the structure $\cS$ assigns an object ${\mbox{\texttt{T}}_{}^{{{\cS }{c}}}}$, which is a set

$$\Subset {{\mbox{\texttt{T}}_{}^{{{\cS }{c}}}}} {(\Times {\cW } {{{\cL }^{{\cS }{c}}_{}}} )} \period$$ (22)

Intuitively, ${\mbox{\texttt{T}}_{}^{{{\cS }{c}}}}$ can be thought of as giving what ``true'' means according to the account of $c$.

For each $c$, the structure $\cS$ assigns an object ${\texttt{V}_{}^{{{\cS }{c}}}}$, which is a set

$$\Subset {{\texttt{V}_{}^{{{\cS }{c}}}}} {(\TimesThree {\c... ...{{\cC }^{{\cS }{}}_{}}} {{{\cL }^{{\cS }{c}}_{}}} )} \period$$ (23)

Intuitively, ${\texttt{V}_{}^{{{\cS }{c}}}}$ can be thought of as giving context $c$'s view of what ``true in a context'' means, for each among the collection of contexts.

Self-Interpreting Structures

The semantics of context logic employ self-interpreting structures, that is, ones where the semantic objects in the range of the structure $\cS$ will themselves have interpretations assigned to them by $\cS$. This will prove useful in handling arbitrarily nested $ist$s (among other things), by offering a kind of internal self-reference at the semantic level, rather than a language that is expressive enough to represent its own syntax and allow the construction of self-referential sentences.

Moreover, we are not aware of any a priori reason to rule out the idea of self-interpreting semantic structures. Our model-theoretic structures have both domains and ranges consisting of abstract objects, so it's not difficult to imagine the domain subsuming the range, resulting in self-interpretation. If interpretation under $\cS$ is idempotent, the resulting structure will likely be simpler, but this is not a requirement of the model theory.

$ist$ Constructs

For each context $c$, the structure $\cS$ assigns to each atomic construct

$$% P(\Dots{a_1}{a_k})$$ (24)

an object which is a tuple from the cartesian product

$${\cA}^{{\cS }{c}} \times \cdots \times {\cA}^{{\cS }{c}} \times \{{{P}^{{\cS }{c}}_{}}\} \comma$$ (25)

where ${{\cA}^{{\cS }{c}}_{}}{}$ occurs $k$ times, and $\{{{P}^{{\cS }{c}}_{}}\}$ is a singleton set containing ${{P}^{{\cS }{c}}_{}}$, and so

$$\DefineEq {{{[P(\Dots{a_1}{a_k})]}^{{\cS }{c}}_{}}} {\Tupl... ... {{{a}^{{\cS }{c}}_{k}}}, {{P}^{{\cS }{c}}_{}} } } \period$$ (26)

Note that this should not be confused with the definition of $\Ent{{\cS }{c}}{}{P(\Dots{a_1}{a_k})}$, which is given as a condition on objects in the range of the structure $\cS$, but rather is a mapping of first-order atomic constructs to objects in the range of $\cS$. By definition,

$$\Mifflnln {\left[\Mforallln {\cW } {w} {\Mimplies {\kap... ...c}}_{}}}} } {{{({{P}^{{\cS }{c_1}}_{}})}^{{\cS }{c}}_{}}} }$$ (27)

and

$$\Mifflnln {\left[\Mforallln {\cW } {w} {\Mimplies {\kap... ... } {{{({{P}^{{\cS }{c_1}}_{}})}^{{\cS }{c_1}}_{}}} } \period$$ (28)

If $\phi$ is a first-order atomic construct like (24), then we define, for each $c, c_1$ in $\cC$,

$$% \Mifflnln {\Ent{{\cS }{c}}{}{\Ist{}{c_1}{\phi}} } { {\... ...}_{}^{{\cS }{{c}_{1}}}}} } } \right)} \right]} } } \period$$ (29)

Moreover, this same definition holds for non-atomic $\phi$, via the following compositional rules. For every $c, c_1$ in $\cC$ and $w$ in $\cW$, we have,
for $\land$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...x{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } } \comma \end{array}$$ (30)

for $\lor$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...x{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } } \comma \end{array}$$ (31)

for $\lnot$,

$$% \begin{array}{c} \Miff { {\In {\Tuple{w, {{c}^{\cS }_{1}... ...mbox{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma \end{array}$$ (32)

for ${\forall_{\mbox{{\scriptsize\texttt{C}}}}{}{}}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (33)

for $\exists_{\mbox{{\scriptsize\texttt{C}}}}{}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (34)

for $\forall_{\mbox{{\scriptsize\texttt{A}}}}{}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (35)

for $\exists_{\mbox{{\scriptsize\texttt{A}}}}{}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (36)

for $\forall_{\mbox{{\scriptsize\texttt{L}}}}{}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (37)

for $\exists_{\mbox{{\scriptsize\texttt{L}}}}{}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (38)

for each $\ \forall_{{c}}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \comma } \end{array}$$ (39)

and for each $\ \exists_{{c}}{}$,

$$% \begin{array}{c} \Miffln { {\In {\Tuple{w, {{c}^{\cS }_{... ...\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } \period } \end{array}$$ (40)

Nested $ist$

If $\cP$ includes $\Istsymb{}$, so that $ist$ can nest, we address the issue of defining

$$\Ent{{\cS }{c}}{}{\Ist{}{c_2}{\Ist{}{c_1}{\phi}}}$$ (41)

as follows. Following the form of definition (29), we use the condition,

$$% { {\Mforallln {\cW } {w} {\left[\Mandlnln {\left(\Mi... ...}_{}^{{\cS }{{c}_{2}}}}} } } \right)} \right]} } } \period$$ (42)

Referring to (42), we see we will need semantic definitions for the consequents of each of the implications in the brackets. We define

$$\Miff {\In {\Tuple{w, {{c}^{\cS }_{2}}, {{[\Ist{}{c_1}{\ph... ...c}}_{}}}} {{\texttt{V}_{}^{{{\cS }{c}}}}} } \right]} \comma$$ (43)

and

$$\Miff {\In {\Tuple{w, {{[\Ist{}{c_1}{\phi}]}^{{\cS }{c_2}}... ...} {{\mbox{\texttt{T}}_{}^{{\cS }{c_1}}}} } \right]} \period$$ (44)

This completes the semantics for nested $ist$s. Note that further nesting of $ist$ does not compound matters further - the self-interpreting structure $\cS$ provides interpretation for arbitrary nesting depths.

Our First Theorems

Distributivity of $ist$ over Conjunction

One intuitively desirable property of contexts is that two propositions each hold separately in a context if and only if their conjunction holds there as well 9 (9); 1 (1); 2 (2); 7 (7). Requiring more, such as the disjunctive analog, would not be in accordance with certain intuitive conceptions of context that humans may use. For example, using time intervals as contexts as mentioned earlier, while it should be the case that

$$\Ist {} {t_1} {\Lor {Asleep(Saul)} {\Lnot{Asleep(Saul)}} } \comma$$ (45)

that is, at any moment during $t_1$ either Saul is asleep or Saul is awake, it need not be the case that

$$\Lor {\Ist {} {t_1} {Asleep(Saul)} } {\Ist {} {t_1} {\lnot Asleep(Saul)} } \comma$$ (46)

that is, Saul is either asleep during the entire interval, or awake during it.

As it turns out, for the conjunctive version of this property, the choice is made for us, as the conjunctive condition always holds.

Theorem 4.1   At ${{\cS }{c}}$, for any $c_1$ in $\cC$, we have

$$% \Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{\Land{\phi}{\psi}}} {[\Land {\Ist{}{c_1}{\phi}} {\Ist{}{c_1}{\psi}} ]} }$$ (47)

Distributivity of $ist$ over Universal Quantification

Theorem 4.2   At ${{\cS }{c}}$, for any $c_1$ in $\cC$, with $\cA$ nonempty, we have

$$% \Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{\forall_{\mbox{{\scr... ...{\scriptsize\texttt{A}}}}{a}{\Ist{}{c_1}{\phi[a]}}} } \period$$ (48)

Note that this is not the analog of the Barcan formula and its converse. The treatment of the Barcan analogs involves analogs of the necessary and possible operators, described in terms of the collection of contexts, and will be addressed in a future work.

Theorem 4.3   At ${{\cS }{c}}$, for any $c_1$ in $\cC$, with $\cC$ nonempty, we have

$$\Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{{\forall_{\mbox{{\scri... ...iptsize\texttt{C}}}}{c_0}{\Ist{}{c_1}{\phi[c_0]}}}} } \period$$ (49)

Theorem 4.4   At ${{\cS }{c}}$, for any $c_1$ in $\cC$, with $\cL$ nonempty, we have

$$\Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{\forall_{\mbox{{\scrip... ...ize\texttt{C}}}}{(\psi)}{\Ist{}{c_1}{\phi[\psi]}}}} } \period$$ (50)

Theorem 4.5   At ${{\cS }{c}}$, for any $c_1$ in $\cC$, if ${\mbox{\texttt{U}}_{c_2}^{{{\cS }{c}}}}$ in nonempty, we have

$$\Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{\forall_{{c_2}}{a}{\phi[a]}}} {\forall_{{c_2}}{a}{\Ist{}{c_1}{\phi[c_2]}}} } \period$$ (51)

These all have proofs analogous to that of (56).

Contextualization of Truth and Falsehood

Theorem 4.6   With $\True$ representing the empty conjunction, and $\False$ the empty disjunction, neither of

$$\begin{array}{c} {\forall_{\mbox{{\scriptsize\texttt{C}}}}{}... ...}{(c)}}{(\Equal{\Ist{}{c}{\False}}{\False})} \comma \end{array}$$ (52)

are required to hold in context logic models in general, nor are their negations.

Remark

As a result of the two previous theorems in this section, we have, for $n \ge 1$,

$$% \Ent{{\cS }{c}}{}{\Liff {\Ist{}{c_1}{\LandDots{\phi_1}{\p... ...\LandDots {\Ist{}{c_1}{\phi_1}} {\Ist{}{c_1}{\phi_n}} ]} }$$ (53)

with the case of $n=1$ being trivial, and the case of $n \ge 2$ resulting inductively from (47) and associativity of conjunction; however, the result does not hold for $n=0$. That is, it is not always the case that $\Ent{{\cS }{c}}{}{\Liff{\Ist{}{c}{\True}}{\True}}$, even though a cursory inspection of (70) might incline one to think that it is. Yet there is no contradiction here, for we are dealing with a system where the $n$-way combination in (70) has in fact been proven for $n \ge 1$, and has in fact been dis-proven for $n=0$. So despite an intuitive reflex to set $n$ to $0$ in (70), it is not logically justified to do so.

This turns out to be a feature, not a bug, because, for example, in a context logic language $\cL$ where $ist$ does happen to distribute over disjunction, the analogous result would be ${\Ist{}{c_1}{\LorDots{\phi_1}{\phi_n}}}$ $\liff$ ${[\LorDots{\Ist{}{c_1}{\phi_1}}{\Ist{}{c_1}{\phi_n}}]}$ for $n \ge 1$. If setting $n$ to $0$ were an option in this case (which it obviously isn't), then we would then require that always $\Ent{{\cS }{c}}{}{\Liff{\Ist{}{c}{\False}}{\False}}$.

And while that might initially might seem a natural-enough looking thing, it is in fact completely counter-intuitive, for it requires, for such a language, that if a contradiction arises in some context - let us take the particular context in which Fred is in both Denmark and New Zealand at the same time - then a contradiction must exist outside of that context. Thus, by not insisting that the $n$-way combination in (70) holds for $n=0$, the machinery of context logic appears to be intrinsically protecting the integrity of the intuitive notion of context.

Definition 4.7 (Homogeneity)   A context logic model is ``homogeneous'' if, intuitively speaking, all contexts agree on what each of the contexts consists of. Formally, the condition is that

$$\MforallTwoln {{\cC}^{\cS }} {{{c}^{\cS }_{}},{{c}^{\cS }_... ... {\kappa_{}({{c}^{\cS }_{2}},{w},{{c}^{\cS }_{}})} } \period$$ (54)

Definition 4.8 (Coherence)   A context logic model is ``coherent'' if, intuitively speaking, any context's view any other context's notion of truth coincides with that context's notion of truth. Metaphorically speaking this means, ``we all agree what everyone thinks'', even if we differ otherwise in the things we think. Formally, the condition is that

$$\MforallThreeln {{\cC}^{\cS }} {{{c}^{\cS }_{}},{{c}^{\cS ... ...x{\texttt{T}}_{}^{{\cS }{{c}_{1}}}}} } } } \right)} \period$$ (55)

Definition 4.9 (Context-wise consensus)   A context logic model has ``consensus with respect to context $c$'' if, intuitively, by the account of $c$, any pair of overlapping contexts $c_1$ and $c_2$ are in agreement regarding any proposition $\phi$, where they overlap. Formally, the condition is that

$$\MforallThreeln {{\cC}^{\cS }} {{{c}^{\cS }_{}},{{c}^{\cS ... ..._{}^{{\cS }{{c}_{2}}}}} } } } \right)} \right]} } \period$$ (56)

Definition 4.10 (Consensus)   A context logic model has ``consensus'' if it has context-wise consensus with respect to every context in $\cC$.

Definition 4.11 (Global Relative Truth)   A context logic model has ``global relative truth'' if

$$\Mforallln {{\cC}^{\cS }} {{{c}^{\cS }_{1}},{{c}^{\cS }_{2... ..._{}^{{\cS }{c_1}}}} {{\texttt{V}_{}^{{\cS }{c_2}}}} } \comma$$ (57)

in which case we may write ${\texttt{V}_{}^{\cS }}$.

Context-Relative $ist$

We add the constructor $\istsymb_{\circ}^{}{}$ to those of the language $\cL$. If $c_1$ and $c_2$ are in $\cC$ and $\phi$ is in $\cL$, then

$$\istsymb_{\circ}({c_2},{c_1},{\phi})$$ (58)

is in $\cL$. This construct will henceforth be abbreviated

$$% \Ist{c_2}{c_1}{\phi} \period$$ (59)

Intuitively, this gives $c_2$'s context-relative account of $ist$.

Views and Truths Redux

For each $c_2$, the structure assigns at ${{\cS }{c}}$ an object ${\mbox{\texttt{T}}_{c_2}^{{{\cS }{c}}}}$, which is a set

$$\Subset {{\mbox{\texttt{T}}_{c_2}^{{{\cS }{c}}}}} {(\Times {\cW } {{{\cL }^{{\cS }{c}}_{}}} )} \comma$$ (60)

and an object ${\texttt{V}_{c_2}^{{{\cS }{c}}}}$, which is a set

$$\Subset {{\texttt{V}_{c_2}^{{{\cS }{c}}}}} {(\TimesThree ... ...{{\cC }^{{\cS }{}}_{}}} {{{\cL }^{{\cS }{c}}_{}}} )} \period$$ (61)

Semantically, we define

$$\Mifflnln {\Ent{{\cS }{c}}{}{\Ist{c_2}{c_1}{\phi}} } {\Mf... ...exttt{T}}_{c_2}^{{\cS }{{c}_{1}}}}} } }} \right]} } \period$$ (62)

Note that the semantics of $\Ist{c_2}{c_1}{\phi}$ are different from those of $\Ist{}{c_2}{\Ist{}{c_1}{\phi}}$, which are

$$\Mifflnln {\Ent{{\cS }{c}}{}{\Ist{}{c_2}{\Ist{}{c_1}{\phi}}... ...exttt{T}}_{}^{{\cS }{{c}_{2}}}}} } } \right)} \right]} } }$$ (63)

Semantics for Nested Context-Relative $ist$

By definition,

$$\Miff {\In {\Tuple{w, {{c}^{\cS }_{2}}, {{[\Ist{c_3}{c_1}{... ..._{}}}} {{\texttt{V}_{c_3}^{{{\cS }{c}}}}} } \right]} \comma$$ (64)

and

$$\Miff {\In {\Tuple{w, {{[\Ist{c_3}{c_1}{\phi}]}^{{\cS }{c_... ...{{\mbox{\texttt{T}}_{c_3}^{{\cS }{c_1}}}} } \right]} \period$$ (65)

Related Work

Early Treatment of Context Semantics

[Still need to add Guha's work...]

Propositional Logic of Contexts

Also related is Buvac's 10 (10) treatment of the semantics of propositional context logic. Interestingly, we find in that work, something like a propositional precursor of the concept of the consistency relation:

``Naively, a context is modelled by a set of truth assignments, that describe the possible states of affairs of that context. Thus a model will associate a set of truth assignments with every context. These truth assignments reflect the state of affairs which are possible in a context. For a proposition to be true in a context it has to be satisfied by all the truth assignments associated with that context.''

We can identify truth assignments with possible worlds, and note that a set of these is associated with each context. The concept of the consistency relation $\kappa_{}$, of course, does not assume that possible worlds are truth-assignments - any notion of possible world is admitted as the worlds are abstract. However, the choice of truth-assignments was of course the only available one in the case of propositional logic, since there are no terms available by which possible worlds could be parameterized.

.

[Rolf Nossum stuff]

Local Models Semantics

[...] the work of the Trento group, in particular the work of Chiara Ghidini on distributed first-order logics, which offers a kind of semantics for contexts. We note the following properties of their semantic approach.

LMS appears to assume that all contexts agree on what ``possible situations'' comprise each context. Thus, the contexts are required to be independent of context. This is a restriction that McCarthy, the author of the seminal work on contexts, has specifically said 7 (7) he would not choose to impose. This is an optional constraint (``homogeneity'') in the semantics presented here, and upon which our model-theoretic machinery does not rely.

LMS appears to assume that all contexts agree on what propositions hold in what contexts. Note of course that the contexts are free to make conflicting claims about propositions, but they are all still required to be in agreement on who claims what. This is another optional constraint (``coherence'') upon which our model-theoretic machinery does not rely.

LMS appears to assume that where the set of ``possible situations'' of two given contexts overlap, the contexts agree on the values of propositions in that overlap - in fact, this assumption seems to be built-in to the very relations that define ``context''. Again we treat this is an optional constraint (``consensus'').

LMS appears to assume an at-most countable, extensionally-defined, collection of contexts. This is a reasonable approach for tasks such as treating a distributed team of N autonomous agents, which seems to be an important type of motivating example for their work, but is not applicable to modelling any notion of context defined over continuous sets. The approach defined in the current work can use any set of contexts, extensional or intensional, of any cardinality.

In LMS a single set of truth conditions governs all the contexts, thereby in effect requiring a context-independent notion of $ist$. Again this is an optional constraint in our semantics.

We have not been able to identify something corresponding to the nesting of $ist$ in LMS, or to quantification over propositions.

[need citations]

Hybrid Logics

[yada]

.

10 Comparison with other logics of context The propositional logic of ist(c; Ã) is investigated in (Buva.c et al. 1995), and augmented with first-order quantification in (Buva.c 1996). These are axiomatic systems for reasoning with ist-formulas asserted in given contexts. The syntax for asserting Á in context c is c : Á, and a central motivation for these logics is the ability to enter a given context, perform some reasoning there according to facts that hold in that context, and exit with the results so obtained. In general, this gives rise 16 to a stack c of contexts having been entered into and not exited from, and these are the deduction rules governing entry into and exit from contexts: Enter: ` c : ist(c; Ã) ` cc : à Exit: ` cc : à ` c : ist(c; Ã) The Enter rule is not listed in the axiomatic presentation of (Buva.c et al. 1995), and it is subsumed by other axioms and rules of the logic. It is included here for symmetry. The semantics of (Buva.c 1996) does not distinguish between ist(c; ist(d; Á)) and ist(d; Á), which appears anomalous at first blush. The rules for entering and exiting contexts are correspondingly constrained: Enter: ` x : ist(c; Ã) ` c : à Exit: ` c : à ` x : ist(c; Ã) The logic remembers only the last context that has been entered into. This phenomenon, called flatness, is not unavoidable however, and as discussed below, (Nossum 2002) generalizes the propositional logic of ist(c; Á) to an algebraically generated spectrum of context logics where flat contexts are only a special case. We may compare our Á¡± à with 8c : ist(c; Á ! Ã) of (Buva.c 1996). The latter formula can be taken as rephrasing our semantical clause for the former. If the two are accepted as variants of each other, then Buva.c’s system is seen to be strictly more expressive than the one presented here, because it has full first-order quantification, over context variables as well as other variables. But as usual expressivity comes at a price: the system of (Buva.c 1996) is not decidable. To further illuminate the trade-o® that a®orded us decidability in the present logic, let us point out our axiom A2, which may be taken to express that each individual context is a logically coherent and complete entity. That is a stricter assumption than in most other logics of context, including other logics studied by this author (Nossum 2002), (Nossum and Serafini 2002), (Gabbay and Nossum 2000). 17 van Benthem (van Benthem 1996) finds that the term ’context’ denotes a convenient methodological fiction, rather than a well-defined ontological category. His proposal is for an indexing scheme, where each language element can be decorated with an index specifying an intended context for evaluation. This results in a logic where transition between contexts has a natural expression. Giunchiglia, Serafini et.al. have also developed logical systems of context where transition between contexts is the main concern (Serafini and Giunchiglia 2001). Each context is modelled by a separate natural deductive system, and there are special rules for inter-context deduction. However, there is no direct provision for nesting of contexts, as in ist(c; ist(d; Á)), although the natural deduction system allows for convenient passage between c and d. Nossum and Serafini have developed natural-deductive systems of context where context combination is catered for through an algebraic component (Nossum and Serafini 2002). Sequential composition of contexts, e.g. c; d; e; : : :, is represented associatively by algebraic terms, e.g. c © d © e : : :, and there is provision for algebraic equations on context terms, thus spanning a variety of natural-deductive logics of context including flat contexts, context sets, context multisets, and context sequences. (Nossum 2002) expands on the idea of algebraic context augmentation in the framework of an axiomatic ist-logic in the style of (Buva.c et al. 1995). This time, context terms like c©d©e are introduced into the syntax of the language, as are algebraic equations on ground context terms. The equational varieties within the scope of this approach are the same as in (Nossum and Serafini 2002), including flat contexts, context sets, context multisets, and context sequences. Augmenting a context w with another one, c, to form a composite context w © c, is analogous to going from possible world w to possible world w?c in the logic of the present paper. Ongoing work aims to generalize (Nossum 2002) to wider equational varieties and quasi-varieties, as well as to quantificational logic. In (Gabbay and Nossum 2000) a quantificational system similar to Buva.c’s is obtained by self fibring of predicate logics, and decidability is shown in a special case. They also develop a multi-modal logic for ist(Á; Ã), which is as expressive as the present logic for Á¡± Ã, but they do not prove decidability for it. 18 11 Conclusion We depart from the notation ist(c; Ã) which originates with (Guha 1991), preferring c¡± à and generalizing to Á¡± Ã. Our system harnesses generalization over contexts in a two-layered multi-modal system, the semantics of one modality quantifying over a set of simpler modalities. This results in a simple, decidable, sound, and complete axiomatic presentation.

Conclusion

Just as modal logic was inspired by the desire to model certain aspects of human cognition and communication richer than those expressible in first-order logic, such as the use of tenses and propositional attitudes, context logic was offered to model perhaps deeper aspects of human cognition and communication which may be key to obtaining human-level AI. We hope that this formal model theory for context logic will be of use in working toward that goal.

Bibliography

S. Buvac, V. Buvac, and I. Mason.

Metamathematics of contexts.
Fundamenta Informaticae, 23(2/3/4):263-301, 1995.

Ramanathan V. Guha.

Contexts: a formalization and some applications.
Technical Report STAN-CS-91-1399, Stanford CS Dept., Stanford, CA, 1991.

R.V. Guha.

Context dependence of representations in cyc.
In Colloque ICO '93, 1993.

J. McCarthy.

Notes on formalizing context.
In Proceedings of the thirteenth international joint conference on artificial intelligence, 1993.

John McCarthy.

Towards a mathematical science of computation.
In C. M. Popplewell, editor, Proceedings of IFIP Congress, pages 21-28. North-Holland, 1962.

Karl Heuer.

Personal communication.

John McCarthy.

Personal communication.

John McCarthy.

Generality in artificial intelligence.
Comm. of ACM, 30(12):1030-1035, 1987.

Rolf Nossum.

Propositional Logic for Ground Semigroups of Context.
Logic Journal of the IGPL, 10(3):273-297, 2002.

I. Mason S. Buvac, V. Buvac.

The semantics of propositional contexts.
In Proceedings of the 8th International Symposium on Methodologies for Intelligent Systems, pages 468-477. 1994.

About this document ...

A Model Theory for a
Quantified Generalized Logic of Contexts


[$Working$ $draft$ $Revision: 1.34$ - $please$ $do$ $not$ $distribute$]

This document was generated using the LaTeX2HTML translator Version 2002-2 (1.70)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html context-semantics

The translation was initiated by selene on 2005-06-02