
## 2 The Causal Explanation Formalism 2.1 Preliminaries

For simplicity, we fully present the propositional version only. The full formalism, with predicates (without functions) and with an elementary "ontology" has been described in [3, 4]. The extension from the propositional case to the general case is not difficult, as will be explained in §**3.5. We distinguish** various types of statements in our formal system:
C**: A theory expressing causal statements.**
E.g. On alarm causes Heard bell or Flu causes F ever **T emperature**.

O: An ontology in the form of a set of IS-A **links between two items which**
can appear in a causal statement.

E.g., T emperature 39 →IS−A F ever **T emperature**,
T emperature 41 →IS−A F ever **T emperature**, Heard loud bell →IS−A Heard **bell**, Heard sof t bell →IS−A Heard **bell**.

W: A classical propositional theory expressing truths (incompatible **facts,**
co-occurring facts, . . .). E.g., Heard sof t bell → ¬Heard loud **bell**.

Intuitively, propositional symbols denote elementary properties describing states of affairs, which can be facts or *events* such as F ever **T emperature**,
On alarm, Heard bell**. The causal statements express causal relations between facts or events expressed by these propositional symbols.**
Some care is necessary when providing these causal and ontological atoms.

If "Flu causes F ever T emperature", we will conclude Flu *explains* T emperature 39 from T emperature 39 →IS−A F ever T emperature**, but we**
cannot state Flu causes T emperature 39: we require that the causal information is provided "on the right level" and in this case, T emperature **39 is**
not on the right level, since "T emperature **39" is too norrow with respect to**
our knowledge about flu and temperatures.

The formal system is meant to infer, from such premises C ∪ O ∪ W,
formulas denoting explanations. This inference will be denoted ⊢C**. The**
ontological atoms express some common sense knowledge which is necessary to infer these "explanations". Notice that a feature of our formalism is that standard implication alone cannot help to infer explanations [3, 4].