Counterfactual Conditionals in Quantified Modal Logic
Naveen Sundar Govindarajulu and Selmer Bringsjord

arXiv:1710.04161v2 [cs.AI] 2 Nov 2017

Rensselaer Polytechnic Institute, Troy, NY
{naveensundarg,selmer.bringsjord}@gmail.com

Abstract
We present a novel formalization of counterfactual conditionals in a quantified modal logic. Counterfactual conditionals
play a vital role in ethical and moral reasoning. Prior work
has shown that moral reasoning systems (and more generally, theory-of-mind reasoning systems) should be at least
as expressive as first-order (quantified) modal logic (QML)
to be well-behaved. While existing work on moral reasoning
has focused on counterfactual-free QML moral reasoning, we
present a fully specified and implemented formal system that
includes counterfactual conditionals. We validate our model
with two projects. In the first project, we demonstrate that our
system can be used to model a complex moral principle, the
doctrine of double effect. In the second project, we use the
system to build a data-set with true and false counterfactuals
as licensed by our theory, which we believe can be useful for
other researchers. This project also shows that our model can
be computationally feasible.

Introduction
Natural-language counterfactual conditionals (or simply
counterfactuals) are statements that have two parts (semantically, and sometimes syntactically): an antecedent and a
consequent. Counterfactual conditionals differ from standard material conditionals in that the mere falsity of the antecedent does not lead to the conditional being true. For example, the sentence “If John had gone to the doctor, John
would not be sick now” is considered a counterfactual as
it is usually uttered when “John has not gone to the doctor”. Note that the surface syntactic form of such conditionals might not be an explicit conditional such as “If X then
Y”; for example: “John going to the doctor would have prevented John being sick now”. Material conditionals in classical logic fail when used to model such sentences. Counterfactuals occur in certain ethical principles and are often
associated with moral reasoning. We present a formal computational model for such conditionals.
The plan for the paper is as follows. We give a brief
overview of how counterfactuals are used, focusing on moral
reasoning. Then we briefly discuss prior art in modeling
counterfactuals, including computational studies of counterfactuals. We then present our formal system, used as a founCopyright c 2018, Association for the Advancement of Artificial
Intelligence (www.aaai.org). All rights reserved.

dation for building our model of counterfactual conditionals. After this, we present the model itself and prove some
general properties of the system. We end by discussing two
projects to demonstrate how the formal model can be used.

Use of Counterfactual Conditionals
Counterfactual reasoning plays a vital role in human moral
reasoning. For instance, the doctrine of double effect
(DDE) requires counterfactual statements in its full formalization. DDE is an attractive target for building ethical
machines, as numerous empirical studies have shown that
human behavior in moral dilemmas is in accordance with
what the doctrine (or modified versions of it) predict.1 Another reason for considering DDE is that many legal systems use the doctrine for defining criminality. We briefly
state the doctrine below. Assume that we have an ethical hierarchy of actions as in the deontological case (e.g. forbidden, morally neutral, obligatory); see (McNamara 2010).2
We also assume that we have a utility or goodness function
for states of the world or effects, as in the consequentialist
case. Given an agent a, an action α in a situation σ at time
t is said to be DDE-compliant iff (the clauses are verbatim
from (Govindarajulu and Bringsjord 2017a)):
DDE Informal
C1 the action is not forbidden
C2 the net utility or goodness of the action is greater than
some positive amount γ;
C3a the agent performing the action intends only the good
effects;
C3b the agent does not intend any of the bad effects;
C4 the bad effects are not used as a means to obtain the good
effects; and
C5 if there are bad effects, the agent would rather the situation be different and the agent not have to perform the
action. That is, the action is unavoidable.

Note that while (Govindarajulu and Bringsjord 2017a)
present a formalization and corresponding implementation
1

Moral dilemmas are situations in which all available actions
have large positive and negative effects.
2
There are also exist in the literature more fine-grained hierarchies(Bringsjord 2015).

and “stopwatch” test of the first four clauses above, there
is no formalization of C5 . Work presented here will enable
such a formalization. The last clause has been rewritten below to make explicit its counterfactual nature.
C5 Broken Up
C5a The agent desires that the current situation be different.
C5b The agent believes that if the agent itself were in a different situation, the agent would not perform the action α.

Separately, (Migliore et al. 2014) have an empirical study
in which they elicit subjects to produce counterfactual answers to questions in a mix of situations with and without
moral content. Their answers have the form of C5a and C5b .
Their study shows with statistical significance that humans
spent more time responding to situations that had moral content. This suggests the presence of non-trivial counterfactual
reasoning in morally-charged situations.
Counterfactual reasoning also plays an important role in
the intelligence community in counterfactual forecasting
(Lehner 2017). In counterfacutal forecasting, analysts try to
forecast what would have happened if the situation in the
past was different than what we know, and as Lehner states
there is a need for formal/automated tools for counterfactual
reasoning.

Prior Art
Most formal modeling of counterfactuals has been in work
on subjunctive conditionals. While there are varying definitions of what a subjunctive conditional is, the hallmark of
such conditionals is that the antecedent, while not necessarily contrary to established facts (as is the case in counterfactuals), does speak of what could hold even if it presently
doesn’t; and then the consequent expresses that which would
(at least supposedly) hold were this antecedent to obtain.3
Hence, to ease exposition herein, we simply note that (i)
subjunctives are assuredly non-truth-functional conditionals, and (ii) we can take subjunctive conditionals to be a superclass of counterfactual conditionals. A lively overview of
formal systems for modeling subjunctive conditionals can
be found in (Nute 1984). Roughly, prior work can be divided into cotenability theories versus possible-worlds theories. In cotenability theories, a subjunctive φ > ψ holds
iff (C + φ) → ψ holds. Here C is taken to be a set
of laws (logical/physical/legal) cotenable with φ. One major issue with many theories of cotenability is that they
at least have the appearance of circularly defining cotenability in terms of cotenability. In possible-worlds theories,
semantics of subjunctive conditionals are defined in terms
of possible worlds.4 While conceptually attractive to a degree, such approaches are problematic. For example, many
3

E.g., “If you were to practice every day, your serve would be
reliable” is a subjunctive conditional. It might not be the the case
that you’re not already practicing hard. However, “If you had practiced hard, your serve would have been reliable” is a counterfactual
(because, as it’s said in the literature, the antecedent is “contrary to
fact”).
4
E.g., (Lewis 1973) famously aligns each possible world with
an order of relative similarity among worlds, and is thereby able

possible-worlds accounts are vulnerable to proofs that certain conceptions of possible worlds are provably inconsistent (e.g. see (Bringsjord 1985)). For detailed argumentation
against possible-world semantics for counterfactual conditionals, see (Ellis, Jackson, and Pargetter 1977).
Relevance logics strive to fix issues such as explosion and
non-relevance of antecedents and consequents in material
conditionals; see (Mares 2014) for a wide-ranging overview.
The main concern in relevance logics, as the name implies, is to ensure that there is some amount of relevance
between an antecedent and a consequent of a conditional,
and between the assumptions in a proof and its conclusions. Our model does not reflect this concern, as common notions of relevance such as variable/expression sharing become muddled when the system includes equality, and
become even more muddled when intensionality is added.
Most systems of relevance logic are primarily possibleworlds-based and share some of the same concerns we have
discussed above. For example, (Mares and Fuhrmann 1995;
Mares 2004) discuss relevance logics that can handle counterfactual conditionals but are all based on possible-worlds
semantics, and the formulae are only extensional in nature.5
Work in (Pereira and Saptawijaya 2016) falls under extensional systems, and as we explain below, is not sufficient for
our modeling requirements.
Differently, recent work in natural language processing
by (Son et al. 2017) focuses on detecting counterfactuals in
social-media updates. Due to the low base rate of counterfactual statements, they use a combined rule-based and statistical method for detecting counterfactuals. Their work is
on detecting (and not evaluating, analyzing further, or reasoning over) counterfactual conditionals and other counterfactual statements.

Needed Expressivity
Our modeling goals require a formal system F of adequate expressivity to be used in moral and other theoryof-mind reasoning tasks. F should be free of any consistency or soundness issues. In particular, F needs to avoid
inconsistencies such as the one demonstrated below, modified from (Govindarajulu and Bringsjord 2017a). In the inference chain below, we have an agent a who knows that the
murderer is the person who owns the gun. Agent a does not
know that agent m is the murderer, but it’s true that m is the
owner of the gun. If the knowledge operator K is a simple
first-order logic predicate, we get the proof shown below,
which produces a contradiction from sound premises.
to capture in clever fashion the idea that a counterfactual φ > ψ
holds just in case the possible world satisfying φ that is the most
similar to the actual world also satisfies ψ. While as is plain we are
not fans of possible-worlds semantics, those attracted to such an
approach to counterfactuals would do well in our opinion to survey
(Fritz and Goodman 2017).
5
By extensional logics, we refer broadly to non-modal logics
such as propositional logic, first-order logic, second-order logic etc.
By intensional logics, we refer to modal logics. Note that this is
different from intentions which can be represented by intensional
operators, just as knowledge, belief, desires etc can be represented
by intensional operators. See (Zalta 1988) for an overview.

Modeling Knowlege (or any Intension) in First-order Logic
1 K (a, Murderer (owner (gun))) ; given
2 ¬K (a, Murderer (m)) ; given
3 m = owner (gun) ; given
4 K (a, Murderer (m)) ; first-order inference from 3 and 1
5 ⊥ ; first-order inference from 4 and 2

Even more robust representation schemes can
still result in such inconsistencies, or at least unsoundness, if the scheme is extensional in nature
(Bringsjord and Govindarajulu 2012). Issues such as
this arise due to uniform handling of terms that refer to
the same object in all contexts. This is prevented if the
formal system F is a quantified modal logic (and other
sufficiently expressive intensional systems). We present
one such quantified modal logic below.

Background: Formal System

reasoning can be easly switched out in-place of the event
calculus.
The modal operators present in the calculus include the
standard operators for knowledge K, belief B, desire D, intention I, etc. The general format of an intensional operator
is K (a, t, φ), which says that agent a knows at time t the
proposition φ. Here φ can in turn be any arbitrary formula.
Also, note the following modal operators: P for perceiving a
state, C for common knowledge, S for agent-to-agent communication and public announcements, B for belief, D for
desire, I for intention, and finally and crucially, a dyadic deontic operator O that states when an action is obligatory or
forbidden for agents. It should be noted that DCEC is one
specimen in a family of easily extensible cognitive calculi.
The calculus also includes a dyadic (arity = 2) deontic
operator O. It is well known that the unary ought in standard
deontic logic lead to contradictions. Our dyadic version of
the operator blocks the standard list of such contradictions,
and beyond.7
Syntax
S ::= Agent | ActionType | Action ⊑ Event | Moment | Fluent

action : Agent × ActionType → Action






initially
: Fluent → Formula





 Holds : Fluent × Moment → Formula





 happens : Event × Moment → Formula
f ::=


clipped : Moment × Fluent × Moment → Formula





 initiates : Event × Fluent × Moment → Formula






terminates : Event × Fluent × Moment → Formula




prior : Moment × Moment → Formula

In this section, we present the formal system in which we
model counterfactual conditionals. The formal system we
use is deontic cognitive event calculus (DCEC). Arkoudas
and Bringsjord (2008) introduced, for their modeling of the
false-belief task, the general family of cognitive event calculi to which DCEC belongs. DCEC has been used to formalize and automate highly intensional moral reasoning processes and principles, such as akrasia (giving in to temptation that violates moral principles) (Bringsjord et al. 2014).
and the doctrine of double effect described above.6
Briefly, DCEC is a sorted (i.e. typed) quantified modal
logic (also known as sorted first-order modal logic). The
calculus has a well-defined syntax and proof calculus; outlined below. The proof calculus is based on natural deduction (Gentzen 1935), commonly used by practicing mathematicians and logicians, as well as to teach logic; the proof
calculus includes all the standard introduction and elimination rules for first-order logic, as well as inference schemata
for the modal operators and related structures.

t ::= x : S | c : S | f (t1 , . . . , tn )

q : Formula | ¬φ | φ ∧ ψ | φ ∨ ψ | ∀x : φ(x) |






 P(a, t, φ) | K(a, t, φ) |


φ ::=
C(t, φ) | S(a, b, t, φ) | S(a, t, φ) | B(a, t, φ)





D(a,
t, φ) | I(a, t, φ)




O(a, t, φ, (¬)happens(action(a∗ , α), t′ ))

Inference Schemata
Syntax
DCEC is a sorted calculus. A sorted system can be regarded
analogous to a typed single-inheritance programming language. We show below some of the important sorts used in
DCEC. Among these, the Agent, Action, and ActionType
sorts are not native to the event calculus.
The syntax can be thought of as having two components:
a first-order core and a modal system that builds upon this
first-order core. The figures below show the syntax and inference schemata of DCEC. The syntax is quantified modal
logic. The first-order core of DCEC is the event calculus
(Mueller 2006). Commonly used function and relation symbols of the event calculus are included. Other calculi (e.g. the
situation calculus) for modeling commonsense and physical
6
The description of DCE C here is mostly a subset of the discussion in (Govindarajulu and Bringsjord 2017a) relevant for us.

The figure below shows a fragment of the inference
schemata for DCEC. First-order natural deduction introduction and elimination rules are not shown. Inference schemata
RK and RB let us model idealized systems that have their
knowledge and beliefs closed under the DCEC proof theory.
While humans are not dedcutively closed, these two rules
lets us model more closely how more deliberate agents such
as organizations, nations and more strategic actors reason.
(Some dialects of cognitive calculi restrict the number of
iterations on intensional operators.) R4 states that knowledge of a proposition implies that the proposition holds R13
ties intentions directly to perceptions (This model does not
take into account agents that could fail to carry out their intentions). R14 dictates how obligations get translated into
known intentions.
7

A overview of this list is given lucidly in (McNamara 2010).

On Using the Material Conditional

Inference Schemata (Fragment)

K(a, t1 , Γ), Γ ⊢ φ, t1 ≤ t2
K(a, t2 , φ)
B(a, t1 , Γ), Γ ⊢ φ, t1 ≤ t2
B(a, t2 , φ)
K(a, t, φ)
φ

[RK ]
[RB ]

t < t′ , I(a, t, ψ)
[R4 ]

If we are considering a simple material conditional φ → ψ,
then if Γ ⊢ ¬φ, then trivially Γ ⊢ φ → ψ, if the proof
calculus subsumes standard propositional logic ⊢Prop , as is is
the case with logics used in moral reasoning. Another issue
is that whether Γ ⊢ (φ ֒→ ψ) holds is not simply a function
of whether Γ ⊢ φ holds and Γ ⊢ ψ holds, that is ֒→ is not a
truth-functional connective, unlike the material conditional
→.

P(a, t′ , ψ)

[R13 ]

B(a, t, φ) B(a, t, O(a, t, φ, χ)) O(a, t, φ, χ)
[R14 ]

K(a, t, I(a, t, χ))

Semantics
The semantics for the first-order fragment is the standard first-order semantics. The truth-functional connectives ∧, ∨, →, ¬ and quantifiers ∀, ∃ for pure first-order
formulae all have the standard first-order semantics. The
semantics of the modal operators differs from what is
available in the so-called Belief-Desire-Intention (BDI)
logics (Rao and Georgeff 1991) in many important ways.
For example, DCEC explicitly rejects possible-worlds semantics and model-based reasoning, instead opting for
a proof-theoretic semantics and the associated type of
reasoning commonly referred to as natural deduction
(Gentzen 1935; Francez and Dyckhoff 2010). Briefly, in this
approach, meanings of modal operators are defined via arbitrary computations over proofs, as we will see for the counterfactual conditional below.

Reasoning is performed through the first-order
modal
logic
theorem
prover,
ShadowProver
(Govindarajulu and Bringsjord 2017a). While we use
the prover in our simulations, describing the prover in more
detail is out of scope for the present paper.8

The Formal Problem
At a time point t, we are given a set of sentences Γ describing
what the system (or agent at hand) is working with. This set
of sentences can be taken to describe the current state of
the world at t; state of the world before t, up-to to some
horizon h in the past; and also desires and beliefs about the
future. We are given a counterfactual conditional φ ֒→ ψ
with possibly (but not always) Γ ⊢ ¬φ. We require that our
formal model provide us with the following:
Required Conditions
1. Given a set of formulae Γ, and a sentence of the form φ ֒→
ψ, we should be able to tell whether or not Γ ⊢ φ ֒→ ψ.
2. Given a set of formulae Γ, and a sentence of the form
Θ(a, t, φ ֒→ ψ), we should be able to tell whether or not
Γ ⊢ Θ(a, t, φ ֒→ ψ), here Θ is either B, K or D.
first-order

Extensional Context
Rcf 1 ֒→ Introduction



′

 [I1 ] Γ ⊆ Γ
Γ ⊢ φ ֒→ ψ ⇔¬Cons[{φ}] ∨ ∃Γ′
[I2 ] Con[Γ′ + φ]


[I3 ] (Γ′ + φ) ⊢ ψ


The elimination rule for ֒→ is much simpler and resembles
the rule for the material conditional →.
Rcf 2 ֒→ Elimination

Reasoner (Theorem Prover)

8
The
underlying
(Stickel et al. 1994).

Modeling Counterfactual Conditionals
The general intuition is that given φ ֒→ ψ, one has to drop
some of the formulae in Γ arriving at Γ′ and then if (Γ+φ) ⊢
ψ, we can conclude that φ ֒→ ψ. More precisely, φ ֒→ ψ
can be proven from Γ iff there is a subset Γ′ of Γ consistent
with φ such that (Γ′ + φ) ⊢ ψ. Since we are using a natural
deduction proof calculus, we need to specify introduction
and elimination rules for ֒→. Let Cons[Φ] denote that a set
of formulae Φ is consistent.

prover

is

SNARK

Γ + {φ, φ ֒→ ψ} ⊢ ψ

Intensional Context
The inference schema given below apply to the presence of
the counterfactual in any arbitrary context Υ. The context
for a formula is defined as below. Let hi denote the empty
list and let ⊕ denote list concatentation.
֒→ Definition of Υ

hi if the top connective in φ is not modal



 hK, a, ti, ⊕Υ[ψ], if φ ≡ K(a, t, ψ)
Υ[φ] =
 hB, a, ti, ⊕Υ[ψ], if φ ≡ B(a, t, ψ)



hD, a, ti, ⊕Υ[ψ], if φ ≡ D(a, t, ψ)

For example, Υ[B(a, t1 , K(b, t2 , P ))] = hB, a, t1 , K, b, t2 i
With the context defined as above, inference schemata for
֒→ occurring within a modal context is given below.
We also use the following shorthands in the two rules
given below:
(i)Υ[φ] denotes that formula φ has context Υ.
(ii)Υ[Γ] denotes the subset of Γ with context Υ.

Rcf 3 ֒→ Introduction

Property 2; R2 in (Pollock 1976)


′

 [I1 ] Γ ⊆ Υ[Γ]

′
Γ ⊢ Υ [φ ֒→ ψ] ⇔ ¬Cons[{φ}] ∨ ∃Γ
[I2 ] Con[Γ′ + φ]


[I3 ] (Γ′ + φ) ⊢ ψ

The elimination rule for ֒→ under any arbitrary context is
given below.
Rcf 4 ֒→ Elimination
Γ + {Υ[φ], Υ[φ ֒→ ψ]} ⊢ Υ[ψ]

For a simple example of the above rules, see the experiments
sections below.

A Note on Implementing the Introduction Rules
There are two possible dynamic programming algorithms.
In the worst case, both the algorithms amount to searching
over all possible subsets of a given Γ. In the first algorithm,
we start from smaller subsets and compute whether (Γ′ +
φ) ⊢ ψ and Cons[Γ′ + φ]. For any larger sets Γ′′ , (Γ′′ +
φ) ⊢ ψ need not be computed. In the second algorithm, we
start with larger subsets and compute (Γ′′ + φ) ⊢ ψ and
Cons[Γ′′ + φ]. For any smaller sets Γ′ , Cons[Γ′ + φ] need
not be computed. If ⊢ is first-order and above, the second
algorithm is preferable. If ⊢ encompasses first-order logic,
then computing Cons[Φ] for any set is hard in the general
case. In our implementation, we approximate Cons[Φ] by
running querying a prover for Φ ⊢ ⊥ up to a time limit δ. As
δ increases, the approximation becomes better.

Properties of the System
Now we canvass some meta-theorems about the system. All
the four inference schemata given above, when added to a
monotonic proof theory, preserve monotonicity.
Theorem 1: Monotonicity Preservation
If ⊢ is monotonic, then ⊢ augmented with
Rcf 1 , Rcf 2 , Rcf 3 , and Rcf 4 is still monotonic.

Proof Sketch: Notice that the right-hand side of the condition for the introduction rules stay satisfied if we replace Γ
with a superset Φ. The elimination rules hold regardless of
Γ. 
We assume that ⊢ is monotonic. For monotonic systems,
for any Γ′ ⊆ Γ, Cons[Γ] ⇒ Cons[Γ′ ]. We show that some
desirable properties that hold for other systems in the literature hold for the system presented here.



{} ⊢ φ → ψ ⇒ {} ⊢ φ ֒→ ψ

Proof: Either ¬Cons[{φ}] or Cons[{φ}]. If the former holds,
we are done. If the latter holds, then take Γ′ = {} and we
have Cons[Γ′ + φ] and Γ′ + φ ⊢ ψ, satisfying all three conditions I1 , I2 , and I3 . ∴ letting us introduce φ ֒→ ψ. 
Property 3; R3 in (Pollock 1976)





{} ⊢ φ → ψ ⇒ {} ⊢ (χ ֒→ φ) → (χ ֒→ ψ)

Proof: Assume {} ⊢ φ → ψ. We need to prove {χ ֒→ φ} ⊢
(χ ֒→ ψ). If ¬Cons[{χ ֒→ φ}], we succeed. Otherwise,
take Γ′ to be {χ ֒→ φ}. By the elimination rule we have
{χ ֒→ φ} + χ ⊢ φ, and using {} ⊢ φ → ψ, we have
{χ ֒→ φ} + χ ⊢ ψ, thus satisfying our conditions I1 , I2 , and
I3 to introduce χ ֒→ ψ. 
Property 4; A6 in (Pollock 1976), MP in (Nute 1984),
If Γ ⊢ φ ֒→ ψ, then Γ ⊢ φ → ψ

Proof: Γ ⊢ (φ ֒→ ψ), therefore Γ+{φ} ⊢ ψ using ֒→ -elim.
Using → -intro we have Γ ⊢ φ → ψ. 
Property 5; MOD in (Nute 1984)
If Γ ⊢ (¬ψ) ֒→ ψ, then Γ ⊢ φ → ψ

Proof: Given Γ ⊢ (¬ψ) ֒→ ψ, therefore using ֒→ -elim
Γ + ¬ψ ⊢ ψ, and using ¬-elim we have Γ ⊢ ψ, giving us
Γ ⊢ φ → ψ. 
Property 6
If Γ ⊢ (φ ֒→ ψ) ∧ (ψ ֒→ φ)
then Γ ⊢ (φ → χ) ⇔ Γ ⊢ (ψ → χ)

Proof: We prove the left-to-right direction of the biconditional
Γ ⊢ (φ → χ) ⇒ Γ ⊢ (ψ → χ)
Assume Γ ⊢ (φ → χ). We need to prove Γ ⊢ (ψ → χ).
Since we are given Γ ⊢ ψ ֒→ φ, either ¬Cons[{ψ}] or there
is a Γ′ ⊆ Γ such that Cons[Γ′ + ψ] and Γ′ + ψ ⊢ φ. If
the former holds, we are finished. If the latter holds, we then
have Γ + ψ ⊢ φ since ⊢ is monotonic. Using the given Γ ⊢
(φ → χ) and the → −elimination rule, we obtain Γ+ψ ⊢ χ.
Therefore, Γ ⊢ ψ → χ. 
Property 7; CSO in (Nute 1984)
If {} ⊢ (φ ֒→ ψ) ∧ (ψ ֒→ φ)
then Γ ⊢ (φ ֒→ χ) ⇔ Γ ⊢ (ψ ֒→ χ)

Property 1; ID in (Nute 1984)
{} ⊢ φ ֒→ φ

Proof: If ¬Cons[{φ}], we are done. Otherwise, since {φ} ⊢
φ, we can see that I1 , I2 , and I3 hold. 

Proof: We establish the left-to-right direction of the biconditional
Γ ⊢ (φ ֒→ χ) ⇒ Γ ⊢ (ψ ֒→ χ)
Assuming {} ⊢ (φ ֒→ ψ) ∧ (ψ ֒→ φ) and using Property
4 and ⊢Prop , we have {} ⊢ (φ → ψ) ∧ (ψ → φ); and using

⊢Prop again we obtain {} ⊢ φ ↔ ψ. Assume Γ ⊢ (φ ֒→
χ). We need to prove Γ ⊢ (ψ ֒→ χ). Since we assumed
Γ ⊢ φ ֒→ χ, either ¬Cons[{φ}] or there is a Γ′ ⊆ Γ such
that Cons[Γ′ + φ] and Γ′ + φ ⊢ χ. If the former holds we
are done because ¬Cons[{φ}] ⇒ ¬Cons[{ψ}]. If the latter
holds, we have Cons[Γ′ +ψ] and Γ′ +ψ ⊢ χ as {} ⊢ φ ↔ ψ.

Property 8
If {} ⊢ (φ ֒→ ψ) ∧ (ψ ֒→ φ)
then Γ ⊢ (χ ֒→ φ) ⇔ Γ ⊢ (χ ֒→ ψ)

Γ′ + (φ1 ∨ φ2 ) ⊢ ⊥ through ∨-elim, which overthrows
our assumption that Cons[Γ′ + (φ1 ∨ φ2 )]. So either
Cons[Γ′ + φ1 ] or Cons[Γ′ + φ2 ], then I2 is satisfied for
either φ1 ֒→ ψ or φ2 ֒→ ψ. Assume that it holds for the
former.
(3) I3 is satisfied as {φ1 } ⊢ φ1 ∨ φ2 and we have Γ′ + (φ1 ∨
φ2 ) ⊢ ψ; therefore Γ′ + φ1 ⊢ ψ. 
With stronger assumptions we can obtain a property that
directly resembles SDA.
Property 10

Proof: Similar to the previous proof, we prove the left-toqright direction of the biconditional

If



Γ ⊢ (φ1 ∨ φ2 ) ֒→ ψ
and Γ 6⊢ ¬φ1 and Γ 6⊢ ¬φ2



Γ ⊢ (φ ֒→ χ) ⇒ Γ ⊢ (ψ ֒→ χ)

then Γ ⊢ (φ1 ֒→ ψ) ∧ (φ1 ֒→ ψ)

Assuming {} ⊢ (φ ֒→ ψ) ∧ (ψ ֒→ φ) and using Property 4
and ⊢Prop , we deduce {} ⊢ (φ → ψ) ∧ (ψ → φ); and using
⊢Prop again we infer {} ⊢ φ ↔ ψ. Assume Γ ⊢ (χ ֒→ φ).
We need to show Γ ⊢ (χ ֒→ ψ). Since we assumed Γ ⊢
χ ֒→ φ, either ¬Cons[{χ}] or there is a Γ′ ⊆ Γ such that
Cons[Γ′ + χ] and Γ′ + χ ⊢ φ. If the former, we are done; if
the latter, we have Γ′ + χ ⊢ ψ. 
The next property states that if we are given φ ֒→ ψ1 and
φ ֒→ ψ2 , we can reach φ ֒→ ψ1 ∧ ψ2 . For instance, “If a
had gone to the doctor, a would not have been sick” and “If
a had gone to the doctor, a would be happy now” give us “If
a had gone to the doctor, a would not have been sick and a
would be happy now”.
One property which has been problematic for many previous formal systems is simplification of disjunctive antecedents (SDA). For instance, given “If a had gone to
the doctor or if a had taken medication, a would not be
sick now” should give us “If a had gone to the doctor, a would not be sick now, and if a had taken medication, a would not be sick now.” Logics based on possible worlds find it quite challenging to handle this property — yet it seems like a necessary property to secure
(Ellis, Jackson, and Pargetter 1977), though there are some
disagreements on this front (Loewer 1976). As a middle
ground we can prove “If a had gone to the doctor, a would
not be sick now, or if a had taken medication, a would not
be sick now.”

Proof: The proof is similar to the previous proof, needing
only minor modifications.

Property 9
If Γ ⊢ (φ1 ∨ φ2 ) ֒→ ψ then
Γ ⊢ (φ1 ֒→ ψ) ∨ (φ1 ֒→ ψ)

Proof: We need to either prove Γ ⊢ φ1 ֒→ ψ or Γ ⊢ φ1 ֒→ ψ
and use ∨−introduction to get Γ ⊢ (φ1 ֒→ ψ) ∨ (φ2 ֒→
ψ). If ¬Cons[φ1 ∨ φ2 ], we have ¬Cons[φ1 ] and ¬Cons[φ2 ],
we then reach our conclusion. Otherwise, if Cons[φ1 ∨ φ2 ],
then there is a Γφ1 ∨φ2 serving as Γ′ . We need to prove three
clauses:
(1) I1 is satisfied as Γ′ = Γφ1 ∨φ2 .
(2) I2 is satisfied because if Cons[Γ′ + φ1 ∨ φ2 ] then at
least one of Cons[Γ′ + φ1 ] or Cons[Γ′ + φ2 ]; otherwise if Γ′ + φ1 ⊢ ⊥ and Γ′ + φ2 ⊢ ⊥, giving us

Property 11, A4 in (Pollock 1976)
If Γ ⊢ (φ ֒→ ψ) and Γ ⊢ (φ ֒→ χ)
then Γ ⊢ (φ ∧ ψ) ֒→ χ

Proof: Since we have Γ ⊢ (φ ֒→ χ), either ¬Cons[{φ}] or
there is a Γ′ ⊆ Γ such that Cons[Γ′ + φ] ⊢ χ. If the former
holds, we have ¬Cons[{φ∧ψ}], giving us Γ ⊢ (φ∧ψ) ֒→ χ.
If the latter holds, we have Γ′ + (φ ∧ ψ) ⊢ χ. Assume that
¬Cons[Γ′ + (φ ∧ ψ)]; then we get Γ ∪ {φ, ψ} ⊢ ⊥, giving us Γ + φ ⊢ ¬ψ through ¬−introduction. With → −
introduction we get Γ ⊢ φ → ¬ψ, but using Property 4
and the given Γ ⊢ φ ֒→ ψ, we have Γ ⊢ φ → ψ. Therefore, Γ ⊢ ¬φ. This goes against Cons[Γ′ + φ], giving us that
Cons[Γ′ + (φ∧ψ)]. This satisfies I1 , I2 , and I3 which yields
Γ ⊢ (φ ∧ ψ) ֒→ χ. 
Finally, we have the following theorem, the proof of
which can be obtained by exploiting all the properties above.
Theorem 2
All the above properties hold if every counterfactual φ ֒→ ψ
is replaced by Υ[φ ֒→ ψ].

Given the above, we can prove the following, using rules
R4 and R14 . The following theorem gives an account of
how an agent might assert a counterfactual conditional in
a moral/ethical situation.
Theorem 3



Γ ⊢ B a, t, O(a, t, φ, χ) ∧ O(a, t, φ, χ)

⇒ Γ ⊢ B(a, t, φ) ֒→ χ

Experiments

We describe two experiments that demonstrate the model in
action, the first in moral dilemmas and the second in general
situations.9
9
Axioms for both the experiments, data and the reasoning system can be obtained here: https://goo.gl/nDZtWX

Counterfactual Conditionals in Moral Dilemmas
We
look
at
moral
dilemmas
used
in
(Govindarajulu and Bringsjord 2017a). Each dilemma
d has an axiomatization Γd . Two such dilemmas are axiomatized and studied in (Govindarajulu and Bringsjord 2017a).
Assume that an agent a is facing a given dilemma d. The
axiomatization Γd includes a’s knowledge and beliefs about
the dilemma. We show that for each d, we can get C5a and
C5b . Note that C5a and C5b talk about situations. Though
event calculus does not directly model situations, we can
use fluents to do so. A situation is formalized as an object
of sort Situation:
Situation ⊏ Object

in : Agent × Situation → Fluent
Action : Agent × ActionType × Situation × Moment
→ Formula

We have the following axiom which states that the only actions that an agent can perform in a situation at a time are
those sanctioned by the Action predicate.
∀a : Agent, α : ActionType, t : Moment.


happens (action(a, α), t) →



∃σ : Situation. Holds(in(a, σ), t) ∧ Action(a, α, σ, t)

As a warmup to C5b , we state C5a below. Let the current
agent be I and time be denoted by t. The formula below
states that the agent believes it is in a situation σ ′ and desires to be in a situation σ ′ different from σ with at least one
action type α that is not forbidden and does not have any
negative effects.10 Here µ : Fluent → R denotes the total
utility of a fluent for all agents and all times.
Formalization of C5a

¬∃f [µ(f ) > 0] ∧ terminates(α, f, t)















Let αD be the DDE-complaint action that the agent is
saddled with in the current situation σ. Let Θ(σ, t) be the inner statement in the desires modal operator above. The statement below formalizes C5b and can be read as the agent believing that if the agent were in a different situation with at
least one action that is not forbidden and does not have any
negative effects, it would then not perform the action αD
required of it by DDE.
10




B I, t, Θ(σ, t) ֒→ ¬happens action(I, αD ), t + 1

!

We derive the above two conditions from: (1) axioms describing situations; and (2) common knowledge C(Φ) dictating that agents should only perform non-forbidden actions and in a non-dilemma situation will peform an action
with only positive effects. C5a takes around 780ms and C5b
takes around 8.378s.

Evaluation of the System

We have the following additional symbols that tell us when
an agent is in a situation and what actions are possible for an
agent in a situation at a given time:

B (I, t, Holds (in (I, σ))) ∧


Holds (in (I, σ)) ∧
  Action(I, α, ρ, t)∧



 

  ¬O(I, t, ρ, ¬happens (action(I, α), t)
I,
t,
∃ρ
D
 ∃α




  ¬∃f [µ(f ) < 0] ∧ initiates(α, f, t)


Formalization of C5b

Note that this is a mere first formulation of a complex mental
state and further refinements, simple and drastic, are possible and
expected.

We demonstrate the feasibility of our system by showing the
model working for a small dataset of representative problems. There are 16 problems each with its own set of assumptions Γ. For each problem Γ, we have a statement that
is provably counterfactual, that is Γ ⊢ ¬φ. Using this statement, we build three conditionals: (1) a counterfactual conditional φ ֒→ ψ; (2) an absurd material conditional φ → ⊥;
and (3) an absurd counterfactual φ ֒→ ⊥. The number of
premises range from 2 to 15. One simple problem is shown
below:
Γ=




∀x : Human(x) → Mortal (x) , Human(socrates)

Γ ⊢ ¬Mortal (socrates) ֒→ ¬Human(socrates)
Γ ⊢ ¬Mortal (socrates) → (P ∧ ¬P )
Γ 6⊢ ¬Mortal (socrates) ֒→ (P ∧ ¬P )

The table below shows how much time proving the true and
false counterfactuals takes when compared with proving the
absurd material conditional for the same problem. As expected, the counterfactual conditional takes more time than
the material conditional. The absurd counterfactual φ ֒→ ⊥
is merely intended as a sanity check and the large reasoning times are expected (mainly due to timeouts), and is not
expected to be a common use case.
Formula

Mean (s)

Min (s)

Max (s)

φ ֒→ ψ
φ→⊥
φ ֒→ ⊥

2.496
0.169
19.7

0.449
0.089
1.93

11.14
0.341
120.67

Conclusion & Future Work
We have presented a novel formal model for counterfactual conditionals. We have applied this model to complete
a formalization of an important ethical principle, the doctrine of double effect. We have also provided an implementation of a reasoning system and a dataset with counterfactual conditionals. There are three main threads for future work. First, the reasoning algorithm is quite simple
and can be improved by looking at either hand-built or
learned heuristics. Second, we hope to leverage recent work
in developing an uncertainty system for a cognitive calculus
(Govindarajulu and Bringsjord 2017b). Finally, we hope to
build a more robust and extensive dataset of counterfactual
reasoning validated by multiple judgements from humans.

References
[Arkoudas and Bringsjord 2008] Arkoudas,
K.,
and
Bringsjord, S. 2008. Toward Formalizing CommonSense Psychology: An Analysis of the False-Belief Task.
In Ho, T.-B., and Zhou, Z.-H., eds., Proceedings of the
Tenth Pacific Rim International Conference on Artificial
Intelligence (PRICAI 2008), number 5351 in Lecture Notes
in Artificial Intelligence (LNAI), 17–29. Springer-Verlag.
[Bringsjord and Govindarajulu 2012] Bringsjord, S., and
Govindarajulu, N. S. 2012. Given the Web, What is
Intelligence, Really? Metaphilosophy 43(4):361–532. This
URL is to a preprint of the paper.
[Bringsjord et al. 2014] Bringsjord, S.; Govindarajulu, N. S.;
Thero, D.; and Si, M. 2014. Akratic Robots and the
Computational Logic Thereof. In Proceedings of ETHICS
• 2014 (2014 IEEE Symposium on Ethics in Engineering,
Science, and Technology), 22–29. IEEE Catalog Number:
CFP14ETI-POD.
[Bringsjord 1985] Bringsjord, S. 1985. Are There SetTheoretic Worlds? Analysis 45(1):64.
[Bringsjord 2015] Bringsjord, S. 2015. A 21st-Century Ethical Hierarchy for Humans and Robots: EH. In Ferreira,
I.; Sequeira, J.; Tokhi, M.; Kadar, E.; and Virk, G., eds.,
A World With Robots: International Conference on Robot
Ethics (ICRE 2015). Berlin, Germany: Springer. 47–61.
[Ellis, Jackson, and Pargetter 1977] Ellis, B.; Jackson, F.;
and Pargetter, R. 1977. An Objection to Possible-world Semantics for Counterfactual logics. Journal of Philosophical
Logic 6(1):355–357.
[Francez and Dyckhoff 2010] Francez, N., and Dyckhoff, R.
2010. Proof-theoretic Semantics for a Natural Language
Fragment. Linguistics and Philosophy 33:447–477.
[Fritz and Goodman 2017] Fritz, P., and Goodman, J. 2017.
Counterfactuals and Propositional Contingentism. Review
of Symbolic Logic 10(3):509–529.
[Gentzen 1935] Gentzen, G. 1935. Investigations into Logical Deduction. In Szabo, M. E., ed., The Collected Papers
of Gerhard Gentzen. Amsterday, The Netherlands: NorthHolland. 68–131. This is an English version of the wellknown 1935 German version.
[Govindarajulu and Bringsjord 2017a] Govindarajulu, N. S.,
and Bringsjord, S. 2017a. On Automating the Doctrine
of Double Effect. In Sierra, C., ed., Proceedings of the
Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, 4722–4730. Preprint available at this
url: https://arxiv.org/abs/1703.08922.
[Govindarajulu and Bringsjord 2017b] Govindarajulu, N. S.,
and Bringsjord, S. 2017b. Strength Factors: An Uncertainty
System for a Quantified Modal Logic. Presented at Workshop on Logical Foundations for Uncertainty and Machine
Learning at IJCAI 2017, Melbourne, Australia.
[Lehner 2017] Lehner, P. 2017. Forecasting counterfactuals
in uncontrolled settings. webpage.
[Lewis 1973] Lewis, D. 1973. Counterfactuals. Oxford, UK:
Blackwell.

[Loewer 1976] Loewer, B. 1976. Counterfactuals with
disjunctive antecedents.
The Journal of Philosophy
73(16):531–537.
[Mares and Fuhrmann 1995] Mares, E. D., and Fuhrmann,
A. 1995. A relevant theory of conditionals. Journal of
Philosophical Logic 24(6):645–665.
[Mares 2004] Mares, E. D. 2004. Relevant Logic: A Philosophical Interpretation. Cambridge University Press.
[Mares 2014] Mares, E. 2014. Relevance logic. In Zalta,
E. N., ed., The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, spring 2014 edition.
[McNamara 2010] McNamara, P. 2010. Deontic Logic. In
Zalta, E., ed., The Stanford Encyclopedia of Philosophy.
McNamara’s (brief) note on a paradox arising from Kant’s
Law is given in an offshoot of the main entry.
[Migliore et al. 2014] Migliore, S.; Curcio, G.; Mancini, F.;
and Cappa, S. F. 2014. Counterfactual thinking in moral
judgment: An experimental study. Frontiers in Psychology
5.
[Mueller 2006] Mueller, E. 2006. Commonsense Reasoning:
An Event Calculus Based Approach. San Francisco, CA:
Morgan Kaufmann. This is the first edition of the book. The
second edition was published in 2014.
[Nute 1984] Nute, D. 1984. Conditional Logic. In Gabay, D.,
and Guenthner, F., eds., Handbook of Philosophical Logic
Volume II: Extensions of Classical Logic. Dordrecht, The
Netherlands: D. Reidel. 387–439.
[Pereira and Saptawijaya 2016] Pereira, L. M., and Saptawijaya, A. 2016. Counterfactuals, Logic Programming and
Agent Morality. In Rahman, S., and Redmond, J., eds.,
Logic, Argumentation and Reasoning. Springer. 85–99.
[Pollock 1976] Pollock, J. 1976. Subjunctive Reasoning.
Dordrecht, Holland & Boston, USA: D. Reidel.
[Rao and Georgeff 1991] Rao, A. S., and Georgeff, M. P.
1991. Modeling Rational Agents Within a BDI-architecture.
In Fikes, R., and Sandewall, E., eds., Proceedings of Knowledge Representation and Reasoning (KR&R-91), 473–484.
San Mateo, CA: Morgan Kaufmann.
[Son et al. 2017] Son, Y.; Buffone, A.; Raso, J.; Larche, A.;
Janocko, A.; Zembroski, K.; Schwartz, H. A.; and Ungar,
L. 2017. Recognizing Counterfactual Thinking in Social
Media Texts. In Proceedings of the 55th Annual Meeting
of the Association for Computational Linguistics (Volume 2:
Short Papers), volume 2, 654–658.
[Stickel et al. 1994] Stickel, M.; Waldinger, R.; Lowry, M.;
Pressburger, T.; and Underwood, I. 1994. Deductive Composition of Astronomical Software From Subroutine Libraries. In Proceedings of the Twelfth International Conference on Automated Deduction (CADE–12), 341–355.
SNARK can be obtained at the url provided here.
[Zalta 1988] Zalta, E. N. 1988. Intensional Logic and the
Metaphysics of Intentionality. Cambridge, MA: MIT Press.

