Proof Theory: MultiContext Systems
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.
Given our family of languages {Li} over I, a
MultiContext system (MC system) MS is a pair
where:
- for each i in I,
is an axiomatic formal system where Li is the
language, 
is the set of axioms, and 
is the set of inference rules;
is a set of inference rules with premises and
conclusions in different languages.
An MC system is essentially a set of logical theories,
plus a set of inference rules which allow for the
propagation of consequences among theories.
MC systems are a generalization of Natural Deduction
(ND) systems [prawitz1]. The generalization
amounts to using formulae tagged with the language they
belong to. This allows for the effective use of the
multiple languages. The deduction machinery of an MC
system is composed of two kinds of inference rules: the
inference rules in each ,
called internal rules,
and the inference rules in ,
called bridge
rules. Internal rules are inference rules with
premises and conclusions in the same language, while
bridge rules are inference rules with premises and
conclusions belonging to different
languages. Notationally, inference rules are written as
follows:
![\begin{displaymath}
\begin{array}{c@{\hspace{3 cm}}c}
\infer[ir]
{i\hspace{-0.1c...
...s \quad i_n\hspace{-0.1cm}:\hspace{-0.05cm}\phi_n }
\end{array}\end{displaymath}](images/img7.1.gif)
where ir is an internal rule, while br is a bridge
rule. Internal rules allow us to draw consequences inside a
theory, while bridge rules allow us
to export results from one theory to another. Indeed
ir allows us to derive the formula C from the
formulae A1, ..., An in the theory
tagged with i, while br allows us to export the
formula C to the theory
tagged with j because of the fact that all the
A1, ..., An are derivable in the
theories tagged with i1, ..., in,
respectively.
.
is the deduction machinery of MS. Using ND and
following [prawitz1] in the notation and
terminology, the deduction machinery of MS
contains also inference rules which discharge assumptions,
written as:
![\begin{displaymath}
\infer[dr]
{j\hspace{-0.1cm}:\hspace{-0.05cm}\psi }
{i_1\hsp...
...i_{m+n}}
{[k_{m}\hspace{-0.1cm}:\hspace{-0.05cm}\gamma_{m}]}
}
\end{displaymath}](images/img13.1.gif)
dr represents an inference rule which allow to infer j:C from A1, ..., An discharging the assumptions D1, ..., Dm
Figure 2 illustrates the contruction of a MC system with three languages and four bridge rules. We start from different languages, e.g., L1, L2, and L3. Then, we associate each of them with a logical theory Ti. Finally, we connect different logical theories with bridge rules, e.g., br1, br2, br3, and br4. The final result is an MC system.
Deductions in MC systems are trees of formulae built starting from a finite number of assumptions and axioms, possibly belonging to distinct languages, and by applying a finite number of inference rules. A formula i:A is derivable from a set of formulae B in a MC system MS, in symbols |-MS, if there is a deduction with bottom formula i:A whose un-discharged assumptions are in B. A formula i:A is a theorem in MS, in symbols |-MS if it is derivable from the empty set. Notice that a deduction in an MC system can be seen as composed of sub-deductions in distinct languages, obtained by repeated applications of internal rules, any two or more sub-deductions being concatenated by one or more applications of bridge rules.