The original proposals for context, [McC87b, McC93], have influenced a number of researchers to develop logics of context; these include [Sho91, Guh91, GSGF93, Nay94, AS95, BBM95, Buv96a]. We proceed with a short description of the logical properties of contexts and contextual reasoning.
1. Contexts are treated as formal objects, i.e. objects in the semantics which can be denoted by constants in the language and over which variables can range. Treating contexts as formal objects allows us to state relations between contexts in the same way we state relations between any other objects in the logic. For example, we can define a relation Specializes(c1,c2) which holds when context c2 is a specialization of context c1.
2. We introduce a new modality ist which is pronounced ``is true''.
Formulas of the form
are to be taken as assertions that the proposition p is true in context c.
This allows us to express that, for example, John McCarthy is a professor in the
context of Stanford University: 
. Note that sentences of the form ist(c,p) can
themselves be true in contexts, e.g. we can have ist(c1,ist(c,p)). The
ist modality also allows us to state lifting axioms--axioms relating
what is true in one context based on what is true in another context. Lifting
axioms are central for reasoning with multiple contexts; we will give examples
of lifting axioms throughout the following sections.
3. All formulas are stated in some context, so we write 
when
formula 
is given in context c. There is no outermost context; it is
always possible to transcend the outermost context so far referred to.
Transcendence is discussed in [McC93].
4. In order to capture the intuitive patterns of contextual reasoning, the formal system needs to contain rules for entering and exiting a context. For example, suppose we have the formula c0:ist(c,p). We can then enter the context c and infer the formula c:p. Conversely, if we have the formula c:p we can infer c0:ist(c,p) by exiting the context c.
5. Besides propositions being true in contexts, we also need the ability to
talk about a value of a term t in context c, which we will write as
Value(c,t). For example, we may need 
, when c
is a context that has a time, e.g. a context usable for making assertions about
a particular situation. In [MB94], we show how formulas
containing the Value function can be treated as abbreviations of formulas
containing ist.