(a) If α and β are classical atoms, then α causes β is a **causal atom**.

(b) A causal formula **is a Boolean combination of classical or causal**
atoms.

## 3. **Ontological Atoms**

If a and b are constant symbols, then a →IS−A b **is an ontological atom.**
Since we want our "predicate" system to encompass the preceding **"propositional" system, we must also consider ontological links between two**
propositional symbols: if P0 and Q0 **are two propositional symbols, then**
P0 →IS−A Q0 **is an ontological atom.**
4. A causal theory consists of a set W **of classical formulas, a set** C of causal formulas and a set O **of ontological atoms.**
5. Explanation atoms **From a given causal theory, some** *explanation atoms* will be derived. An *explanation atom* is α explains β because *possible* Φ
where α and β **are classical atoms and Φ is a set of classical atoms. It** reads "α explains β **because the set Φ is possible".**
Basically, the derivation of the explanation atoms is as given in the propositional case, thus now we can introduce directly the **formal proof system**.

## 3.3 Formal Proof System Of The Formalism With Predicates 1. **Property Of The Causal Atoms: Entailing Implication**

(a) (**α causes β**) → (α → β)

## 2. **Ontological Atoms**

The easiest way to present the rules in the predicate case is to augment the ontology by introducing ontological links between ground atoms:

## (A) **Deriving An Augmented Ontological Relation**

i. If α = P0 and β = Q0 **are propositional atoms, then**
P0 →IS−A(aug.) Q0 **whenever** P0 →IS−A Q0.

ii. Let Pall,one, ,··· denote some predicate of arity n**, essentially universal with respect to its first parameter and essentially existential with respect to its second parameter (other parameters not**
concerned here, clearly the first or the second parameter could similarly by the i th parameter for any i ∈ {1, · · · , n}**). Then**
Pall,one, ,···(a1, b2, a3, · · · , an) →IS−A(aug.) Pone(a1, a2, a3, · · · , an)
whenever a2 →IS−A b2**, and**
Pall,one, ,···(a1, a2, a3, · · · , an) →IS−A(aug.) Pone(b1, a2, a3, · · · , an)
whenever a1 →IS−A b1.