A Strongly-Local Contextual Logic

1 Introduction

Formalising the role of context in symbolic reasoning was proposed by John McCarthy as a means of dealing with the problem of generality when representing common-sense knowledge [McCarthy, 1987]. Any proposition P, say "John is in the office", has a certain meaning that depends on the assumptions made when formalising P . With a different set of assumptions, P will quite possibly have a different meaning. By formalising the context in which they apply, the assumptions can be made explicit, thereby allowing different theories to both be represented at an appropriate level of generality and yet still be used together.

A number of symbolic formalisms have been developed in which context is treated explicitly. These can be broadly classified depending on their conceptualisation and implementation of context, either as multi-context systems if having a coarse-grained, 'compose-and-conquer" approach or as logics of context, if having a fine-grained, "divide-and-conquer" approach, each with certain strengths and weaknesses [Serafini and Bouquet, 2004]. The contextual system developed here occupies a middle-ground between the two, combining strengths of each, resulting in a formalism that should prove to be more suitable for some applications, in particular for cognitive robotics.

In multi-context systems, introduced by [Giunchiglia and Serafini, 1994], contexts are represented by individual logistic systems, each with their own languages, knowledge bases and possibly with different inference systems. Knowledge is related between contexts using a set of bridge rules, rules of inference defined at the meta-level that translate between the contexts. In these systems, reasoning within a context is enforced to be local-only. They are generally used for applications such as agent belief-desire-intention (BDI) models [Sabater et al., 2002], or for modelling multi-agent systems [De Saeger and Shimojima, 2007], where the contextual system (the sets of contexts and bridge rules) is in practice likely to be static.

For logics of context such as [Guha, 1995], contexts are represented as partitions of a knowledge base, with each context being a subset of a complete theory. All share the same language and machinery of inference, and contexts are usually reified, being represented as objects in the language. Contexts are related using lifting rules, sentences that are defined in the object language. Reasoning typically remains global, shifting a weak focus from one context to another via a pair of rules of inference; enter and exit. This light-weight approach derives fromMcCarthy's original proposal and is used in applications such as managing conflicting knowledge on the Semantic Web [Bao et al., 2010] or integrating theories in very large knowledge bases [Guha, 1995], where the contexts and relations between them may evolve.

While both approaches to formal context have useful applications, neither provide a good fit for the reasoning abilities of an individual agent in cognitive robotics. Such systems require a "logic of mental stuff", capable of representing the agent's knowledge of the world, supporting life-long learning as the agent interacts with its environment over time, and reasoning in real-time with limited physical resources. On the one hand, the locality of reasoning found in multi-context systems would benefit an agent with limited resources and a very large knowledge base by allowing it to focus only on the knowledge relevant to a problem. On the other, using contexts to shift focus between short-lived reasoning tasks suggests a more dynamic approach, and being able to introspect context is essential for such an agent reasoning about its own knowledge, and perhaps also for learning. These desiderata sketch out the objectives of the logic presented here; being a single logic, with deductively distinct contexts that are used to represent partial theories and that relate contexts at the object level. While sharing features of both approaches, it is possibly best described as being a "strongly-local" logic of context.

The rest of this paper proceeds as follows. Section 2 defines syntax and semantics. Section 3 defines a strongly-local contextual deductive system. Some properties of the system are introduced in Section 4. Section 5 sets out sketches of the soundness and completeness results and Section 6 closes with a discussion and future work.

2 Syntax and Semantics

The logic is based on the classical first-order predicate calculus. The classical syntax is extended with contextual constructs, and similarly the classical semantics are extended using possible worlds for contextual entailment.

2.1 Syntax

The logic adds a number of contextual logic symbols to the classical syntax; a set of quantifiers and a binary logical connective ':' named "is-true". For example, an intuitive reading of the statement t1 : Clean(room1) is "In the context t1, the formula Clean(room1) is true." This binary infix connective has the same meaning as the distinguished predicate ist [McCarthy, 1993], common in other logics of context. While it appears here as an operator for brevity, this also implies that is-true can nest, a case which must be carefully handled.

Formally, the language is composed of both logical symbols and sets of application-specific symbols. The logical symbols include the set of standard first-order logical symbols: ∧, ¬ and ∀A, where the latter is equivalent to the classical universal quantifier. The symbols ∨, →, ↔ and ∃A may be defined as the usual abbreviations. These are extended with the following contextual logical symbols:

• The contextual connective is-true ":".
• The local universal quantification symbol "∀c", having the domain of discourse of context c as its domain, abbreviated to "∀" when c is the same context in which the symbol was defined.
• Additional global universal quantification symbols "∀C" and "∀L", having respectively as domains: the set of all contexts, and the set of all contextual well-formed formulas (defined below).

Existential equivalents of these universal quantifiers may be defined as the usual abbreviations. Also included are an infinite set of variables a, b, c, . . .

The application-specific sets of non-logical symbols include the classical denumerable sets P: predicate symbols of some arity n ≥ 0, F: function symbols of some arity n ≥ 0 and A: being domain constants; the global domain of discourse. These are augmented with C, a countably infinite set of context symbols.

Definition 1 (Terms). A (constant) term is defined inductively as usual:

where va is a variable bound under either ∀c or ∀A, where a ∈ A and f ∈ F, and ⃗ ta represents a list of zero or more terms.

A context term is defined as:

where vc is a variable bound under ∀C and c ∈ C.

A language term is defined as:

where vL is a variable bound under ∀L and φ is a cwff , as defined below.

Definition 2 (Well-formed formulae). As usual, a wellformed formula (wff ) is defined inductively:

This is extended to the contextual case by inductively defining a contextual well-formed formula (cwff ) as:

The notation "φ[x]" denotes a wff φ containing variable x free in φ and "φ[a/x]" is used to denote the wff obtained by replacing all free occurrences of variable x in φ with a. Finally, "∀[c]" denotes the context name c as being optional.

2.2 Semantics

The semantics presented are a modified version of the "Quantified Generalized Logic of Contexts" (GLC) [Makarios, 2006]. GLC, a model-theoretic account of logics of context, uses a combination of endomorphic (that is, self-interpreting) structures and possible worlds. The semantics appearing here by comparison features strengthened contextual entailment and is simplified, using solely context-relative interpretations of possible worlds.

At an individual context, the entailment relation is equivalent to classical entailment for non-contextual formulae. For the contextual case, it is extended such that a contextual formula is entailed just in case there is agreement that all possible worlds associated with the context are consistent with the formula being true.

The semantic structure S

A model of the logic is defined to be, per GLC, a contextual logic structure S, which is composed of a set of semantic context objects C S , a set of possible worlds W, and a consonance relation κ:

Each context object cS ∈ C S is a semantic object assigned for each context symbol c ∈ C and each w ∈ W is a Kripkeesque possible world. The consonance relation is defined over these sets:

The role of the possible worlds is to provide context-relative semantics - that is, they provide a basis for specifying what is true in each context. The consonance relation κ states the possible words that one context "understands" 1 as being consistent with another: If 〈cS1 , w1, cS2 〉 ∈ κ, intuitively then, context cS1 understands that context cS2 is consistent with possible world w1 and hence is licensed in part to entail contextrelative statements about cS2 which are consistent with w1.

1 The term "understands" is used loosely in preference to alternatives such as "believes" since they may carry connotations that are best not implicated here.

Definition 3 (Entailment). Entailment is defined as a relation between a model at a specific context and a cwff . If the cwff φ is entailed by S at context c ("is true at Sc") then:

Definition 4 (Validity). If cwff φ is entailed by S for any context c, it is valid for S:

If φ is entailed at context c for any structure S, it is valid for c:

If φ is entailed by any structure S and any context c, then it is (globally) valid:

Non-contextual entailment

Entailment of a formula that does not contain any contextual logical symbols is equivalent to classical first-order logic.

At each cS ∈ C S , an object P Sc is assigned for each P ∈ P, an object f Sc is assigned for each f ∈ F, and an object aSc is assigned for each a ∈ A. These sets of semantic objects are denoted as P Sc , F Sc , and ASc , respectively.

Non-contextual entailment is thus inductively defined as:

Contextual entailment

For each context c ∈ C, additional sets of semantic objects are defined at Sc to support contextual entailment.

Definition 5. A propositional object is a tuple assigned for a variable-free predicate instance P(⃗a), for some P ∈ P and for some ⃗a ∈ (A× ... ×A) such that |⃗a| ≥ 0:

The set LSc = {〈aSc 1 , ..., aSc n , P Sc 〉 | for all aSc i ∈ ASc , for all P Sc ∈ P Sc and n = 0, 1, 2, . . . } contains a propositional object φSc for all possible variable-free propositions.

The set T Sc ⊆ (W ×LSc ) is a context's understanding of what is true. It can be thought of as a context-local valuation function, similar in purpose to the global valuation function V (w, φ) in modal logics. If 〈w, φSc 〉 ∈ T Sc then at Sc the propositional object φSc is understood to be true at possible world w. This may or may not be consistent with that which is classically entailed at Sc.

The set V Sc ⊆ (C S ×W×LSc ) is a context's understanding of truth in other contexts. If 〈cS1 ,w, φSc 〉 ∈ V Sc then at Sc the propositional object φSc is understood to be true at w for c1. This may be self-referential, that is defining the understanding of truth at Sc for c, which may or may not be consistent with both T Sc and classical entailment.

The sets U Sc ci ⊆ ASc , ∀ci ∈ C is a context's understanding of the local domain of discourse of all contexts c1 ∈ C, including c itself. If aSc ∈ U Sc c1 , then at Sc, the domain constant object aSc is understood to be a member of the local domain of discourse of c1.

Definition 6. The function Wκ : (C S × C S ) ↦→ 2W is defined as the set of worlds that according to κ, one context understands as being consistent with another:

The entailment relation can now be extended for the contextual cases as follows, with Wκ(cS , cS1 ) non-empty:

Note in (6), if the local context c1 is omitted, it defaults to the context in which the cwff was defined: c.

When an is-true expression has a non-atomic RHS, membership of V Sc and T Sc1 is defined by composition:

• For negation:

• For conjunction:

• For nested is-true expressions, with Wκ(cS1 , cS2 ) nonempty:

Where Sc is the context of the innermost is-true expression in which c1 : c2 : φ appears, or else the context of entailment.

• For local domain constant quantification:

If the local context d is omitted, it defaults to the context in which the cwff was defined: c

• For global contextual quantification:

And similarly substituting members of C S for ∀C cwff s and LSc for ∀L.

3 A Strongly-Local Deductive System

To define a system of contextual inference, the classical system is extended by defining a notion of local derivability and introducing rules of inference for the additional contextual logic symbols.

Definition 7 (Knowledge base). A contextual knowledge base K is a set of named contexts:

With each context Cci being a set of statements, cwff s that are true at ci:

A knowledge base may contain a countably infinite set of contexts, and each context may contain a countably infinite number of statements. The set C is given by the set of all context names in K:

Definition 8. The local language of a context Cc is the tuple:

Where Pc is the set of local predicate symbols for c, Fc the set of local function symbols, Cc the set of local context symbols and Ac the set of local constant symbols; being the local domain of discourse.

Definition 9. The global language of a contextual knowledge base is the tuple:

Where the set of global predicates P for knowledge base K is defined as the union of all sets of local predicates: P = ⋃ Pc, ∀c ∈ C, likewise for F, the set of global function symbols and A, the global domain of discourse.

A contextual system consists of discrete context-local derivations instead of the global derivations usually found in classical systems. A local derivation provides a means of deduction with respect to a single context, such that inference is restricted to the local premises, language, and domain of discourse of the context.

Definition 10 (Local derivation). A local derivation for context c is a sequence of one or more cwff s:

Where each φi ∈ Dc is a theorem, derived from applying a rule of inference to one or more of the previous theorems φ1, ..., φi-1, axioms valid in S for c, or premises φ ∈ Cc.

Definition 11 (Derivability). A cwff φ is locally derivable at context c ("is provable in c") if there exists a derivation Dc in which φ appears as a theorem:

A cwff φ is globally derivable if it is locally derivable for all contexts:

Derivability in this system is corresponds to that of classical systems when there is only a single context, since in this case there is only one context derivations may be made with respect to.

The classical propositional rules of inference are taken as globally sound, including Modus Ponens:

For contextual quantification, rules equivalent to those for classical quantification are defined, with some additions to the classical provisos to account for context-local restrictions.

The notation "∀λ" stands for any of the contextual quantifiers ∀[c], ∀A, ∀C and ∀L, while "tλ" and "vλ" stands for the appropriate term and variable type for each, respectively.

If tλ is a constant, it must be drawn from the domain of the quantifier: Ac for ∀[c], A for ∀A, C for ∀C and Lc for ∀L. If tλ is a variable, it must as usual appear free in φ[tλ/x] in every place that x appears free in φ[x].

As usual, the variable vλ must not occur free in ∀λx.φ or previously in the derivation Dc.

Rules may also be provided for existential quantification, with an additional proviso for local domain quantification.

If tλ is a domain constant a and a ∈ Ac, then the inferred quantifier ∃λ may be the local domain quantifier ∃[c], otherwise it must be ∃A. If tλ is a variable, it must as usual appear free in φ[tλ/x] in every place that x appears free in φ[tλ].

The variable vλ must as usual either be new in Dc, or must not occur free in φ[x] and not appear in any conclusion drawn from φ[vλ/x].

4 Properties

Due to the restriction of derivations to a specific context, context-relative theorems in this contextual system of inference can only be proven using other contexts via the system's axioms. These are obtained from properties of its models, in much the same way as modal systems are augmented with axioms arising from conditions on a model's accessibility relation R.

Several properties exist for all models of these semantics, without any assumptions needed about a particular S. Some examples are examined.

Property 1. Distributivity of conjunction and universal quantification across is-true.

The following are valid axiom schemata:

Proofs of validity are presented in GLC and they remain sound in the more strict semantics presented here.

Property 2. Weak distributivity of negation across is-true.

Negation distributes across is-true, in one direction only:

The proof initially runs similarly for (D.I.), demonstrating for arbitrary model S at context c and cwff φ, that distribution outwards holds. Running the proof in reverse, it is discovered that distribution inwards does not hold.

To provide some intuition for this, consider a context that understands c : ¬A to be true. It should not also understand paradoxically that c : A is true and this is affirmed when distributing the negation outwards to obtain ¬c : A. Further, if the context does understand ¬c : A to true, this simply reflects that it has no understanding of the truth of A at c, and hence it should not also be assumed that it understands ¬A at c without further justification.

The same property gives a result similar to the modal axiom K:

The proof for this is equivalent to that presented in GLC and holds in the strengthened semantics presented here.

It should then be no surprise this property also applies to disjunction and each of the existential quantifiers.

5 Formal Results

5.1 Soundness

A contextual system of inference is locally sound for any model at context c iff for any cwff φ:

A system is globally sound iff it is locally sound for all contexts:

Semantic arguments show both the classical and contextual rules of inference are locally valid for arbitrary model S at arbitrary context c.

Theorem 1. The contextual system of inference is locally sound.

Since the rules of inference are sound and assuming the premises are valid in model S, the proof proceeds as usual by strong induction on the number of theorems in a local derivation Dc for otherwise arbitrary S at arbitrary c.

Theorem 2. The contextual system of inference is globally sound.

This result follows immediately from Theorem 1, since local soundness was proven for arbitrary model S at arbitrary context c.

5.2 Completeness

A contextual system is locally complete for any model at context c iff for any cwff φ:

A system is globally complete iff it is locally complete for all contexts:

An extension of the standard Henkin construction [LeBlanc et al., 1991] is used to demonstrate local completeness, which is then extended to the global case. A proof outline only is presented due to space constraints. As usual, some preliminaries are required.

Definition 12 (Context-relative sets). A set T of cwff at context c1 generates a context-relative set T c1 c2 such that φ ∈ T c1 c2 iff c2 : φ ∈ T.

The set of context-relative sets T contains the contextrelative sets for all permutations of contexts in L:

It is constructed from set T at context c, such that if c1 : ψ ∈ T, then ψ ∈ T c c1 . If ψ is of form c2 : ξ, then ξ ∈ T c1 c2 , and recursively for ξ.

Definition 13 (Set consistency). A finite set T of cwff is consistent at context c iff there is no cwff φ ∈ Lc such that T ⊢c φ, and φ is inconsistent. An infinite set T of cwff is consistent at context c iff every finite subset of T is consistent at c. The set T of cwff is maximally consistent at context c iff it is consistent and for every φ ∈ Lc, if φ /∈ T , then T ∪ {φ} is inconsistent.

Definition 14 (Term-completeness). A set of cwff T is termcomplete iff for some formula ∀λx.φ[x] ∈ Lc, if ∀λx.φ[x] ∈ T then φ[oλ/x] ∈ T for all objects oλ in the quantifier's domain.

Lemma 1 (Lindenbaum). Any consistent set T of cwff φ ∈ Lc may be extended to a maximally consistent, term-complete set T ′ at c such that T ⊆ T ′ .

The extension of the Henkin construction sees two sequences of sets generated, the first being as usual T0 ⊆ T1 ⊆ . . . such that if T0 is consistent then each Ti is consistent, while additionally constructing a sequence T0, T1, . . . such that for (T cj ck )n being a member of Tn, (T cj ck )i-1 ⊆ (T cj ck )i for all cj, ck ∈ C and if (T cj ck )0 is consistent, then each (T cj ck )i is also consistent.

Proceeding by taking T as T0 and generating T0 from T, the denumerable cwff in Lc are enumerated in some ordered sequence φ1, φ2, . . . , φi, . . .. In the case of φi being of the form ¬∀λc.ψ[x], a witness is required of the form ¬ψ[ω/x], where ω is chosen as the first individual from some ordering of the domain of the quantifier such that Ti-1 ∪ {φi, ¬ψ[ω/x]} is consistent. For each φi, Ti is obtained from Ti-1 by taking the union of Ti-1 and φi if the union is consistent, ¬φi if it is not, and both φi and a witness if φi is a negated, universally quantified cwff . If φi is an is-true cwff , then it and any nested is-true expressions are recursively checked for consistency against Ti-1.

At the same time, Ti is constructed fromTi-1 by extending it with any is-true cwff added to Ti-1 when obtaining Ti. If a negated, quantified cwff is added to a context-relative set, a suitable witness is also added.

The resulting union T∞ = ⋃ Ti over all Ti is maximally consistent and term-complete [LeBlanc et al., 1991]. Similarly, the unions of all context relative sets (T cj ck )∞ = ⋃(T cj ck )i are maximally consistent and term-complete.

Thus any set of cwff T can be extended to a maximally consistent, term-complete set T ′ , with a set T′ of maximally consistent, term-complete context-relative sets.

Theorem 3. A maximally consistent, term-complete set T ′ with maximally consistent, term-complete context-relative sets T′ , derived from consistent set T at context c has a model.

To construct a model S of T ′ at c, begin by taking the set of context names C as the set of context objects C S . For each context-relative set T cj ck ∈ T′ , assign T cj ck as world w in W and both 〈cj , T cj ck , ck〉 and 〈ck, T cj ck , ck〉 to κ.

For all contexts ci ∈ C, at Sci assign a set P Sci for each P ∈ P and the set A as ASci , then construct LSci as usual. Let T Sci ⊆ (W ×LSci ) such that 〈w, φSci 〉 ∈ T Sci iff w ∈ Wκ(ci, ci) and for φSci = [P(⃗a)]Sci then P(⃗a) ∈ w. Similarly, let V Sci ⊆ (C ×W ×LSci ) such that 〈cj,w, φSci 〉 ∈ V Sci iff w ∈ Wκ(ci, cj) and for φSci = [P(⃗a)]Sci then P (⃗a) ∈ w.

Finally, at Sc assign a tuple 〈⃗aSc 〉 to each to each P Sc iff P(⃗a) ∈ T ′ . For each c1 ∈ C, let U Sc c1 = A.

With a model S constructed, what remains is for any cwff φ ∈ Lc, that φ is entailed by S at c just in case it is a member of T ′ , thus demonstrating S is a model for T ′ .

This property holds for all non-contextual φ, as would be expected of a Henkin model: For atomic φ of the form P (⃗t ) it follows immediately by (1) and by the construction of S that:

For non-atomic φ, the proof proceeds by cases and induction on the length of the formula. Further, the property holds for cwff of the form ∀λx.ψ[x] in the same way as for classical quantification with a Henkin model.

For is-true cwff φ with form c1 : ψ, the proof is by cases and by induction on the depth of the nesting of is-true. For the base case where there is no nesting, i.e. neither ψ nor any component of it is an is-true expression, suppose c1 : ψ is not entailed. Then by (5) either Wκ(c, c1) = ∅, or for any w ∈ Wκ(c, c1), either w /∈ Wκ(c1, c1), or 〈c1,w, ψSc 〉 /∈ V Sc , or 〈w, ψSc1 〉 /∈ T Sc1 . These can all be falsified, leading to a contradiction. The inductive step proceeds almost identically. Further, the proof holds in both directions, giving:

Theorem 4. The contextual system of inference is locally complete.

Since T ′ is maximally consistent at c and every φ ∈ T ′ is entailed at Sc, S is a model of T ′ . Because T ⊆ T ′ , it follows that S is also a model of T. Thus the contextual system is locally complete.

Theorem 5. The contextual system of inference is globally complete.

The global case follows by creating a Henkin construction and model for each set Tc1 at other context c1, retaining however both the initially constructed set of maximally consistent sets T∞ and model S. If Tc1 is contextually consistent with T , then the resulting augmented model S′ will be a model of both T and Tc1 , and so on for the remaining contexts. Thus the contextual system is also globally complete.

6 Discussion and FutureWork

The logic presented here is strongly-local in that inference is restricted with respect to a specific context, yet remains a logic of context due to its shared model and object-level contextual relations. Compared to GLC, the semantics here offer both the simplification and the strengthening required to construct a sound and complete contextual deductive system. By comparison with other quantificational logics of context such as [Buvaˇc, 1996] and [Perrussel, 2002], it also provides a more general model and hence licenses more general inferences. A more recent example is [Klarman and Guti´errezBasulto, 2010], however being a description logic it is not clear if it would be well-suited for intended applications such as reasoning about action.

Having a number of similarities, there is an inevitable comparison with modal logics, and many logics of context do indeed rely on something similar to modal structures. The primary differences are the strongly-local nature of inference, the contextualisation of truth, and that contexts are conditions on multiple possible worlds. While it should be possible to define a modal logic using these semantics the reverse is not, and so the semantics here represent a generalisation of that of modal logics.

The most crucial aspect in defining the logic was perhaps unsurprisingly the definitions of entailment of is-true, especially in the nested case. While the base case seems to provide an intuitive notion, in the nested case the intuition itself is somewhat unclear and small changes to the definition can have a great effect on that which can be entailed by the system. This aspect certainly warrants further research.

The separation of classical first-order inference from contextual inference by overlaying possible worlds in the model works effectively to avoid paradoxical sentences, at a cost of a limited form of self-reference. This seems like a reasonable trade-off. While there is machinery in place to restrict sets of non-logical symbols (such as the domain of discourse) to finite sets locally, this is yet to be taken full advantage of in the system presented here. It is also essential to research further the properties of models of this logic, since local inference requires an axiomatic basis for reasoning about knowledge in related contexts.

In addition to examining the above there is interest in developing an automated contextual deductive system. Some ongoing research includes examining the use of a collection of Answer Set Programming [Baral, 2003] solver instances, one per local derivation. Restricting local derivations to finite sets of non-logical symbols should provide further benefits here. Another aim is to extend the logic to an action calculus aimed at reasoning about the effects of action with commonsense knowledge, which in conjunction with an automated reasoner should have strong payoffs for non-trivial cognitive robotics systems.