Model Theory: Local Models Semantics
The starting point in the definition of a MultiContext Logic is a family of logical languages {Li}i in I defined over a set of indexes I (in the following we drop the index "i in I"). Intuitively, each Li is the (formal) language used to describe what is true in a context. For the purpose of our work we suppose that I is (at most) countable. We restrict also ourselves to to (classes of) first order languages as this is the case we studied most, but the same ideas apply to different logical languages as well.
Notationally, let us write i:A to mean A and that A is a formula of Li. We say that A is an Li-formula, and that i:A is a formula or, also, a labelled Li-formula. This notation and terminology allows us to keep track of the context we are talking about.
The definition of a model for the family of languages {Li} is composed of two steps and is illustrated in Figure 1 in the case of a family of three languages {L1, L2, L3}.
Local Semantics
The first step is to associate a local semantics to each
language in the family {Li}. In order to do
that we associate a pair < Mi,
|=cl>, where
- Mi is the class of models for
Li
- |=cl is the (classical) satisfiability
relation between formulae in Li and models in
Mi
We call each model m in Mi a local model, and the satisfiability relation |=cl local satisfiability.
Semantics
The second step is to put together local models which
are ``mutually compatible", consistently with the
situation we are describing, and to define a model for the
whole family of languages {Li}. In order to do
that we define a compatibility sequence c (for
{Li}) as a sequence
A compatibility relation C (for {Li}) is a set C = {c} of compatibility sequences c.
A model (for {Li}) is a compatibility relation C which contains at least a sequence and does not contain the sequence of empty sets, that is,
- 1.
- C is not empty;
- 2.
- the sequence < ø, ø, ..., ø, ...> does not belong to C.
Conditions 1. and 2. eliminate meaningless compatibility relations and sequences, namely totally inconsistent context structures. In the following we write C to mean either a compatibility relation or a model, the context always makes clear what we mean.
Given a family of languages {Li}, different subclasses of models may be defined, depending on the definition of compatibility relation. For instance, a model C is a chain model if all the c in C are chains, that is compatibility sequences such that |ci| = 1 for all i in I. A model C is a weak chain model if all the c in C are weak chains, that is compatibility sequences such that |ci| < 2 for all i in I.
Let C = {c} be a model for {Li} and i:A be a formula. C satisfies i:A, in symbols C |= i:A, if for all c in C
Intuitively: an Li-formula is satisfied by a model C if all the local models in each i-th context satisfy it. A model C satisfies a set of formulae B, in symbols C |= B if it satisfies satisfies every formula in B.
A formula i:A is valid, in symbols |= i:A, if all models satisfy it.
What is more interesting is the notion of logical consequence which must take into account the fact that assumptions and conclusion may belong to distinct languages. Given a set of labelled formulae B, Bj denotes the set of Lj-formulae in B.
A formula i:A is a logical consequence of a set of
formulae B w.r.t. a model C, in symbols B |= i:A,
if every sequence c in C satisfies:
Intuitively: take a model C and a formula i:A. Take a set of assumptions B and, among them, isolate the set of assumptions Bj with j different from i. Take all the sequences in C whose local models in cj satisfy Bj (and throw away all the others). Consider now the local models in ci of the remaining sequences. B |= i:A if in these remaining local models all the local models which satisfy Bi locally satisfy A. Essentially, the intuition is that the formulae in Bj prune away compatibility sequences, while the formulae in Bi prune away local models in ci.