EPDL: A Logic for Causal Reasoning

1 Introduction

Causality plays a basic role in human reasoning. The philosophical study of causality dates back to the origin of the discipline. AI research in causality finds its impetus in considerations from commonsense reasoning, especially the ramification problem. It has been found that propagations of effects cannot be appropriately specified by domain constraints (a set of pure logical expressions) ([Lin 1995;McCain and Tuner 1995;Thielscher 1997]). Not only the causation between actions and fluents but also the causation between fluents has to be explicitly represented and specified. It is obvious that these two kinds of causation bear some essential similarities and so might be formalized with a similar logical structure. This is of importance not just in ontology. From the methodological point of view, we might take advantage of such a similarity to propose a provably correct theory of causality. We have both a good understanding of, and formalisms for the direct effects of actions. However, causal propagation is often confused with logical relevancy and persistence of fluents.

In this paper, we introduce a formalism for representing and specifying both the direct and indirect effects of actions in a unified logical structure. Our framework is based on dynamic logic. We do so not only because the dynamic logic is one of the typical formalisms for reasoning about action (c.f. the preface of [Harel 1979]) but also because the modal expression of causal relation is one of the main approaches to causation in philosophy ([Brand 1976]) and in AI ([McCain and Turner 1995;Giordano et al. 2000]).

In dynamic logic, causation between an action and its effects is expressed by the modal formula ✠ ✡ ☛ ✌ , where ✡ is a

(primitive or compound) action and ✌ is a property. For instance, ✠ ✎ ✏ ✒ ✒ ✕ ☛ ✘ ✚ ✜ ✣ ✤ ✥ is read as "the action ✎ ✏ ✒ ✒ ✕ causes a turkey to be dead". In many cases, the effects of an action can be further propagated through causal relations between fluents. For instance, if a turkey is shot down, its death will cause the turkey to be unable to walk: ✘ ✚ ✜ ✣ ✤ ✥ causes ✘ ✩ ✚ ✜ ✬ ✣ ✯ ✰ . However, this cannot be formally expressed in dynamic logic. Obviously it cannot simply written as either ✘ ✚ ✜ ✣ ✤ ✥ ✲ ✘ ✩ ✚ ✜ ✬ ✣ ✯ ✰ or ✠ ✘ ✚ ✜ ✣ ✤ ✥ ☛ ✘ ✩ ✚ ✜ ✬ ✣ ✯ ✰ . The first expression is obviously unsuitable because of the directionality of causation. The second one is not allowed in the syntax of dynamic logic. Therefore, our idea for expressing indirect effects of actions in dynamic logic is to extend the traditional dynamic logic language by allowing a proposition as a modality, say ✠ ✸ ☛ for proposition ✸ . If we allow a proposition as a modality 1 , we will have a way to unify the treatment of the causation between action and proposition and between propositions, likewise the treatment of direct and indirect effects of actions.

In this paper, we first present such an extended system of the propositional dynamic logic(✄ ✆ ✞ ). The system serves as a formal platform for causal reasoning on which a set of causal logics are constructed to show how to build a causal logic satisfying our intuitions of causal reasoning with different domains. An inference mechanism on action descriptions is introduced to facilitate reasoning with action laws and causal laws. Finally, an application of our approach to the ramification problem is briefly presented and the computational complexity of some causal logics is discussed.

2 Extended Propositional Dynamic Logic

In this section, we extend the ✄ ✆ ✞ by introducing propositional modalities, relative axioms and the intended semantics. The extended system is called ✂ ✄ ✆ ✞ .

2.1 Language of ✺ ✻ ✽ ✾

The alphabet of the language ❀ ❁ ❃ ❄ ❅ of the extended propositional dynamic logic consists of a countable set ❆ ❇ ❉ of fluent symbols and a countable set ❊ ❋ ● ❃ of primitive action symbols.

1 A similar approach has been used by [Ryan and Schobbens 1997] to model knowledge updates and counterfactuals. Besides the motivation, however, the semantics and deduction system are quite different from ours.

Propositions ( ✸ a0 ✁ ✄ ✆ ), formulas ( ✌ a0 ❆ ✞ ✠ ) and actions (✡ a0 ❊ ❋ ● ) are defined by the following BNF rules:

The intendedmeaning for ✠ ✡ ☛ ✌ is " ✡ (always) causes ✌ if ✡ is executable". The dual operator ✮ ✡ ✯ ✌ ✰ defined as usual, reads as "✡ is executable and possibly (or may) cause(s) ✌ ". For instance, ✮ ✎ ✱ ✣ ✯ ✯ ✘ ✜ ✒ ✚ ✴ ✥ ✴ says that "spinning a gun may cause it to be unloaded" ✷ ✮ ✡ ✯ ✹ means " ✡ is executable".

The formula ✠ ✸ ☛ ✌ ✰ where ✸ is a proposition, represents propositional causation, reading as " ✸ causes ✌ ". For example, ✠ ✼ ✏ ✒ ✽ ✕ - ✾ ✣ ✽ ✾ ❀ ✣ ✕ ☛ ✴ ✚ ❃ ✚ ✰ ✥ ✴ says that "a short-circuit causes the circuit to be damaged".

Notice the difference between ✠ ✸ ☛ and ✠ ✸ ✬ ☛ . ✸ ✬ is an action, called test action, which can be compounded with other actions but ✸ can not be compoundedwith actions.

2.2 Semantics

The semantics for ✂ ✄ ✆ ✞ is the standard semantics for ✄ ✆ ✞ plus the interpretation of propositional causation.

As usual, a model for ✂ ✄ ✆ ✞ is a structure ❅ ✌ ❆ ❇ ✰ ❉ ✰ ● ❍ , where ❉ ✌ ❑ ▼ ◆ ☛ ✡ a0 ❊ ❋ ● ❖ ✩ ❑ ▼ ❙ ☛ ✸ a0 ✁ ✄ ✆ ❖ . The meanings of ❇ , ❑ ▼ ◆ ☛ ✡ a0 ❊ ❋ ● ❖ and ● are the same as the ones for a ✄ ✆ ✞ model. For any proposition ✸ , ▼ ❙ , similar to ▼ ◆ , is a binary relation on ❇ .

The satisfaction relation ❅ ✑ ✌ ❱ ✌ can be defined as usual. For instance:

❅ ✑ ✌ ❳ ✠ ❨ ☛ ✌ iff for any ❆ ✩ ✰ ✩ ❩ ❍ a0 ▼ ❪ , ❅ ✑ ✌ ❳ ❴ ✌ ✰ where ❨ a0 ❊ ❋ ● ✩ ✁ ✄ ✆ .

As in any modal logic, ✌ a0 ❆ ✞ ✠ is valid in ❅ , written as ❅ ✑ ✌ ✌ ✰ if ❅ ✑ ✌ ❳ ✌ for all ✩ a0 ❇ ✷ ✑ ✌ ✌ means that ✌ is valid in all models.

The conditions of standard models for program connectives are as usual. For instance, the condition for test action is: " ❆ ✩ ✰ ✩ ❍ a0 ▼ ❝ ❞ iff ❅ ✑ ✌ ❳ ✌ ".

The conditions of standard models for propositional causation are as follows:

• ❡ ❢ ❣ ✐ : If ❅ ✑ ✌ ❳ ✸ , then ❆ ✩ ✰ ✩ ❍ a0 ▼ ❙ ✷
• ❡ ❢ ❣ ❁ : If ✑ ✌ ✸ ✔ ❦ ✸ ✖ , then ▼ ❙ ❧ ✌ ▼ ❙ ♦ ✷

The condition ❢ ❣ ✐ is one half of the test action semantics. It implies ▼ ❙ ❞ a113 ▼ ❙ . So ✑ ✌ ✠ ✸ ☛ ✌ ✲ ✠ ✸ ✬ ☛ ✌ . Note that ✑ ✌ ✠ ✸ ✬ ☛ ✌ ❦ ❆ ✸ ✲ ✌ ❍ . Thus ✑ ✌ ✠ ✸ ☛ ✌ ✲ ❆ ✸ ✲ ✌ ❍ . This reflects the essential difference between the causal relation and the material implication. The difference between them is obvious. Semantically, to verify ✸ ✲ ✌ , we only need to check the truth-values of ✸ and ✌ in the current world whereas to verify ✠ ✸ ☛ ✌ , not only the current world but also other related worlds have to be considered. In other words, a causal relation is action-relevant in the way that it is sensitive to both the history and the future evolution of the system under consideration.

The condition ❢ ❣ ❁ shows that propositional causationswe consider are syntax-independent. Although it is not necessarily true in practical reasoning, it is certainly a way to make a causal theory simple.

2.3 Deductive system

The axiomatic system for ✂ ✄ ✆ ✞ consists of the following axiom schemes and inference rules:

• (1). Axiom schemes:
• ❡ all tautologies of propositional calculus.
• ❡ all axioms for compound programs 2 .
• ❡ ✂ a116 : ✉ ✠ ❨ ☛ ❆ ✌ ✲ ✈ ❍ ✲ ❆ ✠ ❨ ☛ ✌ ✲ ✠ ❨ ☛ ✈ ❍ (Extended a116 ❍
• ❡ ❢ ❇ : ✉ ✠ ✸ ☛ ✌ ✲ ✠ ✸ ✬ ☛ ✌ (Causal Weakening)
• (2). Inference rules:
• ❡ ❅ ✄ : From ✉ ✌ and ✉ ✌ ✲ ✈ , infer ✉ ✈ ✷ (Modus Ponens)
• ❡ ✂ ⑦ : From ✉ ✌ infer ✉ ✠ ❨ ☛ ✌ ✷ (Extended Necessitation)
• ❡ ❢ ✂ : From ✉ ✸ ❦ ⑨ infer ✉ ✠ ✸ ☛ ✌ ❦ ✠ ⑨ ☛ ✌ . (Cause Equivalence)

where ✸ ✰ ✸ ✔ ✰ ✸ ✖ a0 ✁ ✄ ✆ ✰ ✌ a0 ❆ ✞ ✠ ✰ ✡ a0 ❊ ❋ ● and ❨ a0 ✁ ✄ ✆ ✩ ❊ ❋ ● .

✂ a116 and ✂ ⑦ are the extensions of the Axiom a116 and Necessitation ⑦ of ✄ ✆ ✞ , respectively. They convey the message that propositional causation ✠ ✸ ☛ will be treated as the standard dynamic modality. The ✂ a116 specifies propagation of causations under logical implication. The inference rule ✂ ⑦ says that tautologies can always be caused.

The axiom ❢ ❇ and the inference rule ❢ ✂ are new, specifying propositional causation. ❢ ❇ corresponds to the semantic condition ❢ ❣ ✐ , which reflects the standard way to find and judge a causal relation. The rule ❢ ✂ (▼ ❢ ✂ ❢ in conditional logic ([Nute 1984])) exactly corresponds to the semantic condition ❢ ❣ ❁ .

Note that if we add an extra axiom " ✠ ✸ ✬ ☛ ✌ ✲ ✠ ✸ ☛ ✌ " into the deductive system, ✂ ✄ ✆ ✞ will collapse to ✄ ✆ ✞ (precisely, ✄ ✆ ✞ plus a duplicate of each test action, denoted by ✄ ✆ ✞ ❶ ). So the consistency of this axiomatic system is obvious.

Following the standard technique of using canonical models and filtration, we can prove that the deductive system for ✂ ✄ ✆ ✞ is sound and complete.

Theorem 1 ✉ ✌ if and only if ✑ ✌ ✌ .

✂ ✄ ✆ ✞ also preserves the finite model property, so it is decidable.

2.4 Reasoning with action descriptions

In reasoning about a dynamic system, we generally specify the system by a set of domain-dependent axioms to describe preconditions, qualifications and effects of actions, causal relations and other domain constraints. Such a set is called an action description or domain description, which can be any finite set of ✂ ✄ ✆ ✞ formulas.

Example 1 Consider the circuit of the following figure. Let ❆ ❇ ❉ ✌ ❑ ✼ ✩ ✔ , ✼ ✩ ✖ , ✜ ✣ ✰ ✏ ✕ ❖ and ❊ ❋ ● ❃ ✌ ❑ ❺ ✒ ✰ ✰ ✜ ✥ ✔ , ❺ ✒ ✰ ✰ ✜ ✥ ✖ ❖ . Then the circuit can be specified by the following action description:

➦

➨

2 See [Goldblatt 1987] or any other dynamic logic book.

The first two formulas describe the direct effects of action ❺ ✒ ✰ ✰ ✜ ✥ ✔ and ❺ ✒ ✰ ✰ ✜ ✥ ✖ . The middle two specify the causal relations among the fluents in the circuit. " ✮ ❺ ✒ ✰ ✰ ✜ ✥ a0 ✯ ✹ " means the action ❺ ✒ ✰ ✰ ✜ ✥ a0 is always executable. ✁

We can easily see that a formula in an action description is different from an ordinary formula. For instance, the sentence "✼ ✩ ✔ ✲ ✠ ❺ ✒ ✰ ✰ ✜ ✥ ✔ ☛ ✘ ✼ ✩ ✔ " in an action description means that "whenever switch 1 is on, toggling it will cause it to be off". In situation calculus language, it can be expressed as ✂ ✼ ❆ ✼ ✩ ✔ ❆ ✼ ❍ ✲ ✘ ✼ ✩ ✔ ❆ ✽ ✥ ✼ ❀ ✜ ✕ ❆ ❺ ✒ ✰ ✰ ✜ ✥ ✔ ✰ ✼ ❍ ❍ ❍ . A similar expression in dynamic logic is ✠ ✠ ✄ ✆ ☛ ❆ ✼ ✩ ✔ ✲ ✠ ❺ ✒ ✰ ✰ ✜ ✥ ✔ ☛ ✘ ✼ ✩ ✔ ❍ , where ✠ ✄ ✆ is a special action, meaning "any action". With the help of ✠ ✠ ✄ ✆ ☛ ✰ a sentence in an action description can be easily differentiated from an ordinary formula. In [Goranko and Passy 1992], it was shown that ✠ ✠ ✄ ✆ ☛ can be an ✎ ✞ - modality. Therefore, if we want to introduce ✠ ✄ ✆ formally as [Prendinger and Schurz 1996] and [Castilho et al. 1999] did, we must extend our system further by adding all the axioms of ✎ ✞ and an extra axiom " ✠ ✠ ✄ ✆ ☛ ✌ ✲ ✠ ✡ ☛ ✌ ", stating that ✠ ✄ ✆ is a universal action. 3 Instead of doing this, however, we prefer a simpler way to deal with action description by treating it as a set of extra axioms (domain axioms).

Definition 1 Let ☛ be an action description. A formula ✌ is ☛ -provable, written as ✉ ☞ ✌ , if it belongs to the smallest set of formulas which contains all the theorems of ✂ ✄ ✆ ✞ ✰ all the elements of ☛ ✰ and is closed under ❅ ✄ and ✂ ⑦ ✷ 4

Example 2 Consider the action description in Example 1. We can easily prove the following consequences:

1. ✉ ☞ ❆ ✼ ✩ ✔ ✌ ✼ ✩ ✖ ❍ ❦ ✜ ✣ ✰ ✏ ✕

The first expression shows that the causal laws " ✠ ✼ ✩ ✔ ✌ ✼ ✩ ✖ ☛ ✜ ✣ ✰ ✏ ✕ " and " ✠ ✘ ✼ ✩ ✔ ✏ ✘ ✼ ✩ ✖ ☛ ✘ ✜ ✣ ✰ ✏ ✕ " imply the domain constraint " ❆ ✼ ✩ ✔ ✌ ✼ ✩ ✖ ❍ ❦ ✜ ✣ ✰ ✏ ✕ ". The second inference relation reflects the propagation of effects of action ❺ ✒ ✰ ✰ ✜ ✥ ✔ through the causal law ✠ ✘ ✼ ✩ ✔ ✏ ✘ ✼ ✩ ✖ ☛ ✘ ✜ ✣ ✰ ✏ ✕ . ✁

Note that the action description ☛ is not complete. All the frame axioms were left out. For such an incomplete action description, a solution to the frame problem is necessary. Otherwise, we can not even derive the following very intuitive consequence:

We will not include a solution to the frame problem in this paper. A solution to the frame problem based on ✂ ✄ ✆ ✞ has been presented in a separated paper 5 There are also several other PDL-based solutions to the problem in the literature which can be easily embedded in ✂ ✄ ✆ ✞ ([Prendinger and Schurz 1996;Castilho et al. 1999]).

3 This process is not necessary if the underlying language is finite. Additionally, [Castilho et al. 1999] treated ➊ ✓ ✔ ✖ ➓ as ✗ ✘ -modality.

4 Note that we do not require that ❼ -provability is closed under ✙ ✚ . In fact, it is provable in the following sense:

If ✜ ✢ ✤ ✦ , then ✜ ★ ➊ ✦ ➓ ✩ ✤ ➊ ✢ ➓ ✩ .

5 The basic idea of that paper is postponing the listing of frame axioms till a query arises in order to reduce the requirement of frame axioms. We proved that the required frame axioms for answering a query only depend on the objects involved in the query and possibly some objects in action description. The manuscript of the paper is available at ftp://ftp.cse.unsw.edu.au/pub/users/ksg/Working/action3.zip.

A standard model ❅ is called a ☛ -model if ❅ ✑ ✌ ✈ for any ✈ a0 ☛ . ✌ is ☛ -valid, written by ✑ ✌ ☞ ✌ ✰ if it is valid in every ☛ -model. Then we have

Theorem 2 (Soundness and completeness of ☛ -provability)

3 Logics for Causal Propagation

✂ ✄ ✆ ✞ provides a unified syntax and inference mechanism for reasoning about both direct effects and indirect effects of actions. It is a minor extension of the classical propositional dynamic logic.

We did not endow ✂ ✄ ✆ ✞ with unlimited ability for causal reasoning. For instance, in Example 1, it is obvious that one of the switches being off will cause the light to be off. However, we cannot prove in ✂ ✄ ✆ ✞ that ✉ ☞ ✠ ✘ ✼ ✩ ✔ ☛ ✘ ✜ ✣ ✰ ✏ ✕ or ✉ ☞ ✠ ✘ ✼ ✩ ✖ ☛ ✘ ✜ ✣ ✰ ✏ ✕ . The reason for our decision is that causality is a relation sensitive to context, time, domains and so on. It seems impossible to have a universal causal logic to satisfy all kinds of applications. Instead, we introduce some optional inference laws for causality in order to form a flexible platform for causal reasoning.

Let us consider the following plausible laws of causality:

✌ ⑦ ✆ ☛

✬ ▼ ☛

✉ ✠ ✸ ☛ ✌ ✲ ✠ ✸ ✌ ⑨ ☛ ✌

✉ ✠ ✸ ☛ ✌ ✌ ✠ ⑨ ☛ ✌ ✲ ✠ ✸ ✏ ⑨ ☛ ✌

❢ ✏ ✯ ☛ ✉ ✠ ✸ ✌ ⑨ ☛ ✌ ✲ ✠ ✸ ☛ ✠ ⑨ ☛ ✌ (Chaining)

✄ ✼ ❢ ☛

✉ ✌ ✲ ✠ ✸ ☛ ✌ (Pseudo-Causation)

These laws are not hard to understand even though they are not necessarily widely acceptable. For instance, the first one says that if ✸ causes ✌ , then it still causes ✌ with any extra fact. The second one says that if individually ✸ and ⑨ cause ✌ , having one will cause ✌ .

Chn says that if ✸ and ⑨ are the causes of ✌ , then these causes can be chained into a nested causation. For instance, in the circuit of Example 1, we could say that the closing of switch 1 causes that the closing of switch 2 causes the light to be on.

PsC says that everything can cause a true statement.

We can easily find examples in everyday reasoning to verify or refute any of these laws . For instance, on one hand by ✌ ⑦ ✆ we can say that if ✽ ✚ ✣ ✯ ✣ ✯ ✰ causes ✩ ✥ ✕ , then ✽ ✚ ✣ ✯ ✣ ✯ ✰ and ✼ ✏ ✣ ✯ ✣ ✯ ✰ cause ✩ ✥ ✕ as well; on the other hand, ✌ ⑦ ✆ implies the following intuitive inference rule in the presence of ❢ ✂ :

This law, named as ▼ ❢ a116 in conditional logic, reflects the regularity of causal propagation through logical relevancy.

It can be proved in ✂ ✄ ✆ ✞ that ✄ ✼ ❢ implies the following law ☛

We call it the collapsing of cause-effect chain. Sometimes it is a good simplification for causal reasoning. However, it could be harmful if the cause-effect chain matters.

We can also find some pros and cons for the other laws. In fact, we do not intend to persuade people to believe in these laws but try to introduce a hierarchy of causal logics to meet different requirements of causal reasoning. We refer to these logics as:

✂ ✄ ✆ ✞ ✔ ✌ ✂ ✄ ✆ ✞ a0 ✌ ⑦ ✆ ✂ ✄ ✆ ✞ ✖ ✌ ✂ ✄ ✆ ✞ ✔ a0 ✬ ▼ ✂ ✄ ✆ ✞ ✁ ✌ ✂ ✄ ✆ ✞ ✖ a0 ❢ ✏ ✯ ✂ ✄ ✆ ✞ ✄ ✌ ✂ ✄ ✆ ✞ ✁ a0 ✄ ✼ ❢

Note that all the laws are independent. So we can combine them in any fashion. We suggest that in practice such laws should be recombined, or new axioms be introduced to form particular systems of causal reasoning for particular applications. 6

The following properties are the corresponding conditions on standard models for the associated laws:

❢ ❝ ✝ ❄ ☛ ▼ ❙ ✟ ✡ a113 ▼ ❙ ❢ ☛ ✌ ☛ ▼ ❙ ✎ ✡ a113 ▼ ❙ ✩ ▼ ✡ ✷ ❢ ❣ ✏ ✒ ☛ ▼ ❙ ✔ ▼ ✡ a113 ▼ ❙ ✟ ✡ ❢ ❃ ❱ ❣ ☛ ▼ ❙ a113 ▼ a0 ✘

where ▼ a0 ✘ is the identity relation.

Note that all conditions ❢ ❣ ❁ ✰ ❢ ❝ ✝ ❄ ✰ ❢ ☛ ✌ ✰ ❢ ❣ ✏ ✒ and ❢ ❃ ❱ ❣ together imply:

Therefore the conditions for ✂ ✄ ✆ ✞ ✄ models force the accessibility relations of propositional causation to be a Boolean lattice on the subsets of the identity relation. Fortunately, the gap between causation and implication (or test action) still exists. So ✂ ✄ ✆ ✞ ✄ does not collapse to ✄ ✆ ✞ ❶ .

Proof. Let ✣ be a language of ✚ ✤ ✦ ★ in which ✪ ✫ ✬ ❽ ✭ ✯ ➔ ➢ ✯ ↔ ✱ and ✳ ✴ ✵ ✶ ❽ ✭ ✱ . Let ✸ ❽ ✹ ✻ ➢ ✽ ➢ ✿ ❁ be a standard model of ✚ ✤ ✦ ★ , where ✻ ❽ ✭ ➆ ➢ ➆ ❄ ✱ ➢ ❅ ❇ ❧ ❽ ✭ ✹ ➆ ➢ ➆ ❁ ➢ ✹ ➆ ❄ ➢ ➆ ❄ ❁ ✱ , ❅ ❋ ❇ ❧ ❽ ✭ ✹ ➆ ➢ ➆ ❁ ✱ , ❅ ❇ ♦ ❽ ✭ ✹ ➆ ➢ ➆ ❁ ✱ , ❅ ❋ ❇ ♦ ❽ ✭ ✹ ➆ ➢ ➆ ❁ ➢ ✹ ➆ ❄ ➢ ➆ ❄ ❁ ✱ , ✿ ✹ ✯ ➔ ❁ ❽ ✭ ➆ ❄ ✱ , ✿ ✹ ✯ ↔ ❁ ❽ ✭ ➆ ✱ ■ Let ❅ ❏ ❑ ▲ ❽ ❅ ❏ ◆ ❅ ▲ and ❅ ❏ a80 ▲ ❽ ❅ ❏ ◗ ❅ ▲ . Then ✸ is an ✚ ✤ ✦ ★ ✘ model. We have ✸ ❙ ❽ ❯ ➊ ✯ ➔ ❱ ➓ ✯ ➔ , but ✸ ❳ ❙ ❽ ❯ ➊ ✯ ➔ ➓ ✯ ➔ .

Accessibility relation for ✠ ✎ ✔ ✬ ☛ . Accessibility relation for ✠ ✎ ✔ ☛ .

This proposition differentiates our approach to causality from the counterfactual-based approaches where SelfCausation is generally accepted.

The following theorem gives the soundness and completeness of each logic, where ✉ a0 ( ✑ ✌ a0 ) represents the syntactical (semantic) entailment in each logic.

Theorem 3 ✉ a0 ✌ if and only if ✑ ✌ a0 ✌ (✣ ✌ ❩ ✰ ❭ ❭ ❭ ✰ ❫ ).

Decidability of each logic can be also proved in a similar waywith ✂ ✄ ✆ ✞ . ☛ -provability is readily extended into each logic.

6 These logics form a chain between ✤ ✦ ★ and ✤ ✦ ★ ❴ : ✚ ✤ ✦ ★ ❛ ✚ ✤ ✦ ★ ➔ ❛ ✚ ✤ ✦ ★ ↔ ❛ ✚ ✤ ✦ ★ ❜ ❛ ✚ ✤ ✦ ★ ✘ ❛ ✤ ✦ ★ ❴ .

The ordering shows the degree of closeness between causation and implication in each logic.

4 Reasoning with Causal Laws

Two kinds of causal relations have been explicitly distinguished in the philosophy of causality: causal laws and causal instances. Roughly speaking, a causal relation is a causal law if it exists everywhere whereas a causal instance only exists in some particular worlds. Interestingly, most of our intuition about causal reasoning comes from reasoning with causal laws. For instance, Transitivity is generally accepted as a property of causal reasoning. However, if you are not an ✂ ✄ ✆ ✞ ✄ reasoner, it does not hold for causal instances. More precisely, ✠ ✸ ☛ ⑨ ✌ ✠ ⑨ ☛ ❝ ✲ ✠ ✸ ☛ ❝ is not a tautology in ✂ ✄ ✆ ✞ ✁ or lower. The reason is: even if ✸ can cause ⑨ to be true in any accessible worlds and ⑨ can cause ❝ to be true in any accessible world, ✸ does not necessarily cause ❝ to be true in all its accessible worlds because ⑨ does not necessarily cause ❝ in ✸ 's accessible worlds. However, if we express Transitivity in the following form:

"If ✠ ✸ ☛ ⑨ ✰ ✠ ⑨ ☛ ❢ a0 ☛ , then ✉ ☞ ✠ ✸ ☛ ❢ ",

it will be valid in any causal logic. This means that if both ✠ ✸ ☛ ⑨ and ✠ ⑨ ☛ ❢ are causal laws, ✠ ✸ ☛ ❢ will be a derived causal law.

We call a formula ✠ ✸ ☛ ⑨ a causal law if it is in an action description. A general question is: Given a set ☛ of causal laws, what other causal laws can be derived?, or formally, whether ✉ ☞ ✠ ✸ ☛ ⑨ ?

4.1 Properties of causal reasoning

Firstly, let's show some basic properties of causal reasoning with causal laws. The following theorem is a summary of properties of ✂ ✄ ✆ ✞ and its extensions.

Theorem 4 Let ☛ be any action description. Then

1. If ✜ ★ ➊ ✢ ➓ ✦ and ✜ ✦ ➈ ❤ , then ✜ ★ ➊ ✢ ➓
2. ❤ (Right Weakening). 2. If ✜ ★ ➊ ✢ ➓ ✦ and ✜ ★ ➊ ✦ ➓ ❤ , then ✜ ★ ➊ ✢ ➓ ❤ (Transitivity). 3. If ✜ ★ ➊ ✢ ➓ ✦ and ✜ ★ ➊ ✢ ➓ ❤ , then ✜ ★ ➊ ✢ ➓ ✹ ✦ → ❤ ❁ (Conjunction) 4. If ✜ ★ ➊ ✢ ➓ ❤ and ✜ ✢ ✤ ✦ , then ✜ ★ ➊ ✦ ➓ ❤ (Left Logical Equivalence). 5. If ✜ ★ ➊ ✢ ➓ ✦ and ✜ ★ ➊ ✢ ➓ ➊ ✦ ➓ ❤ , then ✜ ★ ➊ ✢ ➓ ❤ (Chain Effects). 6. If ✜ ★ ➔ ➊ ❤ ➓ ✦ and ✜ ✢ ➈ ❤ , then ✜ ★ ➔ ➊ ✢ ➓ ✦ (Left Strengthening). 7. If ✜ ★ ➔ ➊ ✢ ➜ ✦ ➓ ❤ , then ✜ ★ ➔ ➊ ✢ ➓ ❤ → ➊ ✦ ➓ ❤ (Disjunctive Antecedents). 8. If ✜ ★ ↔ ➊ ✢ ➓ ❤ and ✜ ★ ↔ ➊ ✦ ➓ ❤ , then ✜ ★ ↔ ➊ ✢ ➜ ✦ ➓ ❤ (Reasoning by Cases). 9. If ✜ ★ ❜ ➊ ✢ ➓ ✦ and ✜ ★ ❜ ➊ ✢ → ✦ ➓ ❤ , then ✜ ★ ❜ ➊ ✢ ➓ ❤ (Cumulative Transitivity).

10. If ✜ ★ ✘ ➊ ✢ → ✦ ➓ ❤ , then ✜ ★ ✘ ➊ ✢ ➓ ❤ ➜ ➊ ✦ ➓ ❤ (Conjunctive Antecedents).

Note that the majority of acceptable properties of causal reasoning have been exhibited by ✂ ✄ ✆ ✞ . Some properties, for instance, Conjunctive Antecedents, are not desirable for all situations. This implies that not all the causal logics are applicable to any domain. Nevertheless, the list of properties gives us criteria for selecting the best suitable causal logic for reasoning about particular systems. We could also use them to compare the logics we presented in the paper and other causal theories 7 . For instance, [McCain and Tuner 1995]'s causal theory is different from all the causal logics we consider because it does not satisfy Reasoning by Cases

7 [Schwind 1999] provided a comparative tableaux showing some of these properties satisfied by the main formalisms of causality in AI, which could be helpful for such a comparison.

(see [Giordano et al. 2000]) but satisfies Cumulative Transitivity. Those universal causal theories [Geffner 1992;Turner 1999;Giordano et al. 2000](basically using ✸ ✲ a0 ⑨ to express causation between ✸ and ⑨ ) satisfy almost all the properties except Chain Effects or Pseudo-Causation 8 . On the other hand, if we take McCain and Turner's causal explanation ([McCain and Turner 1997]) as semantics for causal relation, causal reasoning in ✂ ✄ ✆ ✞ and its extensions is sound in the following sense:

Let ☛ ✫ a0 ✌ ❑ ✠ ❢ ☛ ❝ ☛ ✉ ☞ a0 ✠ ❢ ☛ ❝ ❖ (✣ ✌ ❩ ✰ ❭ ❭ ❭ ✰ ❫ ). It can be proved that if ✁ is causally explained according to ☛ , then it is causally explained according to ☛ ✫ a0 for any ✣ . In other words, ☛ ✫ a0 is a conservative expansion of ☛ with respect to the causal explanation semantics.

Some properties are not expected for causal reasoning. Besides the Self-Causation (Proposition 1), Contraposition is generally not acceptable for causal reasoning([Mackie 1974]). For instance, ✠ ✘ ✚ ✜ ✣ ✤ ✥ ☛ ✘ ✩ ✚ ✜ ✬ ✣ ✯ ✰ does not imply ✠ ✩ ✚ ✜ ✬ ✣ ✯ ✰ ☛ ✚ ✜ ✣ ✤ ✥ . The following example shows that even in ✂ ✄ ✆ ✞ ✄ , contraposition is not valid.

Example 3 Let ☛ ✌ ❑ ✠ ✘ ✎ ✔ ☛ ✎ ✖ ❖ . Based on the proof of Proposition 1 we have ✜ ✑ ✌ ☞ ✄ ✠ ✘ ✎ ✖ ☛ ✎ ✔ . ✁

Nonmonotonicity sometimes is an attractive property of reasoning. Unfortunately (or fortunately), ✂ ✄ ✆ ✞ and its extensions are monotonic in both the following senses:

We do not think that nonmonotonicity is essential to causal reasoning. We can use causal logic in the meta-level to build monotonic or nonmonotomic systems for satisfying various applications. Nevertheless, it is still interesting to investigate nonmonotonic extensions of ✂ ✄ ✆ ✞ . For instance, the following axiom from conditional logic could be a promising substitute for ✌ ⑦ ✆ 9 ☛

4.2 Application to the ramification problem

Before we present some further properties of ✂ ✄ ✆ ✞ , let us consider an application of the logic. [Foo and Zhang 2001] presented a unified solution to the ramification problem. The main idea is the following. Suppose that we are given the

initial state ✎ ✟ of a dynamic system, which is a maximal consistent set of fluent literals. A possible next state ✎ of the system after performed an action should consist of three parts: the direct effects ✂ , the unchanged part ✡ and the indirect effects ✁ .

According to the causation-based idea to the ramification problem, the indirect effects ✁ should be caused by the direct effects ✂ and the unchanged part ✡ . 10 This idea can be formalized in our terminology as ✉ ☞ ✠ ✂ ✩ ✡ ☛ ✁ , where ☛ consists of all the causal laws about the system 11 . Therefore, a state ✎ is a possible next state of the initial state ✎ ✟ if and only if ✉ ☞ ✠ ✂ ✩ ✡ ☛ ✁ , where ✡ ✌ ✎ ✟ ✚ ✎ and ✁ ✌ ✎ ✓ ❆ ✂ ✩ ✡ ❍ .

8 Conjunctive Antecedents is always satisfied by such a logic but it is not acceptable for most cases of causal reasoning.

9 If we conceive the causal relation ➊ ✢ ➓ ✦ as a nonmonotonic inference relation ✢ ❙ ☛ ✦ , then ✩ ✌ ✦ will be Monotonicity and ✙ ✿ will be Rational Monotonicity[Kraus et al. 1990] (One might have found some similarities between the logics ✚ ✤ ✦ ★ ➇ and the logics in [Kraus et al. 1990]). Note that a significant difference between causal reasoning and nonmonotonic reasoning is that causal reasoning is not necessarily reflexive.

This provides a unified approach to the ramification problem. We can choose different causal logics (not just the ones we presented here) to satisfy different applications against criteria of, for instance, inferential strength, expressive power, computational complexity and so on. This motivated us to provide a set of causal logics rather than a single one.

The results in the following section show that such a choice could be important at least for the solution to the ramification problem.

4.3 Characteristic theorem and complexity of reasoning with causal laws

A common misunderstanding in AI seems to be that an action theory in dynamic logic is prohibitively expensive in computation because the complexity of theorem proving of propositional dynamic logic is exponential. However, dynamic logic is highly expressive. It can express any complicated program. Therefore decidability may be the best result we can expect. The extended propositional dynamic logic for action and causation preserves decidability. With the same expressive power, however, the other formalisms of action may need second-order logic.

In this subsection, we argue that if we focus on causal reasoning with causal laws, the computational complexity in some causal logics can be lowered. First, we give a characterization theorem for ✂ ✄ ✆ ✞ and some of its extensions. This theorem shows that causal reasoning in these logics can be transformed into the classical propositional logic.

Theorem 5 Let ☛ be a set of causal laws and ✆ ❆ ☛ ❍ ✌ ❑ ✸ ✲ ⑨ ☛ ✠ ✸ ☛ ⑨ a0 ☛ ❖ . Then

The results in the theorem are a little bit complicated but still quite intuitive. ✆ ❆ ☛ ❍ can be read as the domain constraints implied by the causal laws ☛ . Take ✂ ✄ ✆ ✞ ✔ as an example. Theorem 5 shows that given a set of causal laws ☛ , a causal law ✠ ✸ ☛ ⑨ is derivable if ✸ logically implies some causeswhose effects logically imply ⑨ under the domain constraints. It is easy to see that the computational complexity of causal reasoning with causal laws in these three logics is in ✄ ✝ ❃ , so it is significantly lower than the complexity of ✄ ✆ ✞ .

The characterization theorems for ✂ ✄ ✆ ✞ ✁ and ✂ ✄ ✆ ✞ ✄ are still open problem. The one for ✂ ✄ ✆ ✞ ✁ could be fairly complicated. Relatively, the one for ✂ ✄ ✆ ✞ ✄ might be simpler because we can transform a causal law into a normal form.

10 Note that the unchanged part should be considered as the causes of indirect effects because making something unchanged is also a kind of effect of actions.

11 We overloaded the set of literals to the conjunction of the set.

Example 4 Consider the circuit in Example 1. The causal relation in this circuit can be described by the following causal laws:

Suppose that the initial state ✎ ✟ is ❑ ✘ ✼ ✩ ✔ , ✼ ✩ ✖ , ✘ ✜ ✣ ✰ ✏ ✕ ❖ . Since ✜ ✉ ☞ ✔ ✠ ✼ ✩ ✔ ✌ ✘ ✜ ✣ ✰ ✏ ✕ ☛ ✘ ✼ ✩ ✖ , the only possible next state is ✎ ✌ ❑ ✼ ✩ ✔ , ✼ ✩ ✖ , ✜ ✣ ✰ ✏ ✕ ❖ after performed an action ❺ ✒ ✰ ✰ ✜ ✥ ✔ if we use ✂ ✄ ✆ ✞ ✔ as the meta-logic for reasoning. Note that ✂ ✄ ✆ ✞ ✔ is enough for this example becausewe need not consider the disjunctive or nested causal laws here. ✁

[Foo and Zhang 2001] provided a more general approach to deal with more complicated domains, which can also be applied in this framework.

5 Conclusion

We have presented an extended system ✂ ✄ ✆ ✞ of propositional dynamic logic for reasoning about causality. The extended propositional dynamic logic provides a unified formalism for reasoning about (direct and indirect) effect of actions. The extension is so slight that only two axioms and two inference rules were added. It has been shown that the resultant system captures the basic properties of causal reasoning. Such simplicity may reflect the essential similarity between direct and indirect effect of actions.

✂ ✄ ✆ ✞ was then extended with a set of extra axioms on causal propagation. A series of causal logics were designed and the properties of these logics in causal reasoning with causal instances and causal laws are discussed, respectively. However, presenting these logics is not the main purpose of the work. We aimed to show in this paper how to construct causal logics for satisfying different applications in different domains. We believe that the representation of causation in dynamic logic affords the flexibility to accommodate different varieties of causal reasoning while retaining a core that captures their uncontroversial aspects.

There is a lot of work left for the future. Besides the nonmonotonic extensions, characterization theorems for ✂ ✄ ✆ ✞ ✁ and ✂ ✄ ✆ ✞ ✄ , and complexityanalysis of causal reasoning, a comprehensive comparison needs to be done with other formalisms of causality in AI and philosophy.