This is an argument for granting the right to assisted suicide to a particular individual, as opposed to an argument for an assisted suicide policy, as found in several countries in Europe and a couple American states, and which would provide access to assisted suicide to any Canadian who meets certain requirements. I will adopt a narrative where the party criticizing this proof is the supreme court justices who voted to deny Sue Rodriguez's petition [see full text decision or official summary]. Exactly the same argument works for the more-recent case of Gloria Taylor, who won her case for access to assisted suicide at the British Columbia Supreme Court in 2012, and lost at the B.C. Court of Appeal in 2013). In Sue Rodriguez's particular case, no major party to the argument argued that the government would be doing her harm by making assisted suicide legal for her (this is Assumption 7). Thus, the argument comes down to whether allowing Sue Rodriguez (S.R.) access to assisted suicide would have a negative effect of some sort (against other people - see Assumption 5; or abstract principles - see Assumption 4 and Assumption 6) that rivals the negative effect of denying her access. The main goals of this argument are:
  1. To clarify the qualitative cost to S.R. of denying her access to legal assisted suicide.
  2. To more-precisely state the position that (1) exceeds any cost incurred if the Supreme Court were to grant her access. Or rather, that no such cost has been presented, and because of that she should have been granted access.

One major difference between this formal argument and informal, natural language arguments about assisted suicide cases (those that I've encountered) is the careful distinguishing between

  • actions that individuals can do
  • states of affairs that individuals want to achieve, which are achievable by their taking certain actions
  • states of affairs that we try to prevent by criminalizing certain actions
The primitive symbols of the language of this proof only speak directly about criminalizing actions (sort Actions). The language speaks indirectly about criminalizing states of affairs (sort Propositions) via the defined predicate ‹Justifies criminalizing satisfaction of›; we can say that the law criminalizes a state of affairs if it criminalizes every action that can achieve that state of affairs. As an example, in many jurisdictions the law indirectly criminalizes any state of affairs ψ in which a young person is high on crack cocaine (). Suppose I want to justify that law, but without taking a moral stance on whether it is fundamentally wrong to use crack cocaine. Instead, I'll justify it in terms of the desired state of affairs δ that no young person is at risk of becoming addicted to crack cocaine. Then I must do two things:
  1. Argue that the only actions that can achieve ψ would falsify δ.
  2. Argue, or assert, the subjective position that the satisfaction of δ is more important than the satisfaction of ψ.
It is important to make these distinctions for this ethical issue for two reasons:

First, because it allows two people to disagree on part of the law while agreeing on a subjective moral position such as (2). For example, it is conceivable that in the future a drug is invented that somehow counteracts the addictive properties of crack cocaine. In such a future, (1) is much easier to reject, and if I reject it then I can argue that δ does not justify criminalizing ψ while still agreeing with (2). In more detail, imagine such an anti-addiction drug is invented, a combination of it and crack cocaine is manufactured, and the combination drug has the property that it is more costly to separate its two component parts than it is to make crack cocaine from scratch. An action a involving the manufacturing and selling of the combination drug is sufficient to attain ψ, but arguably does not risk falsifying δ. In the language of this argument: a‹actions sufficient for›(ψ) ∧ ¬Conflicts(a,δ).

Second, because it prevents one side of the argument from misrepresenting the opinion of the other side. In this example, it prevents supporters of the current law from misrepresenting the opinion of opponents as (being close to) fundamentally favouring the falsifying of δ (likely leading to addictions), and it prevents opponents of the current law from misrepresenting the opinion of supporters as (being close to) fundamentally favouring the impermissibility of ψ (that being high on crack cocaine is fundamentally wrong). Such misrepresentation happens often in informal argumentation, even sometimes unintentionally!

For the argument below about S.R.'s case, «SueR request» has the role of ψ. Note that its description does not explicitly mention assisted suicide. The conjunction of the elements of sc-concerns has the role of δ. As in the previous paragraph, this prevents misrepresentation of the opinions of the two sides of the issue: The justices who voted against S.R. were not arguing that assisting the suicide of another person is fundamentally wrong/impermissible, and the justices who voted in favour of S.R. were not arguing that all people have a fundamental right to choose when they will die. However, since I am arguing that the court ruled incorrectly, I must connect «SueR request» to the issue of assisted suicide. That is the purpose of ✓Lemma 1; it says that the only actions S.R. can take that achieve «SueR request» are ones that involve a physician giving her access to lethal drugs (defined by ‹assisted suicide actions for SueR›).

Let's next focus on the goal sentence ✓Goal of this argument (the final sentence derived from the axioms and lemmas):

¬‹Justifies criminalizing satisfaction of›(sc-concerns,«SueR request»)
sc-concerns is a set of four propositions that were raised by the justices in the majority opinion as desirably-satisfied propositions that might be falsified if they rule in favour of S.R. (). The goal sentence says that those concerns are not enough to justify criminalizing the satisfaction of «SueR request» (by criminalizing every action that can achieve «SueR request»).

We need a principle of law/morality that connects ¬‹Justifies criminalizing satisfaction of›(sc-concerns,«SueR request») and the rest of the proof. This is the predicate ‹Reach of law limit› (← hover cursor to see definition, which will be discussed shortly). I've made it a predicate instead of an axiom to avoid having to posit that the principle holds generally. Instead it is only assumed for one instance, by Assumption 1. That said, I do accept the principle generally with some additional qualification. See the end of the criticism section at the bottom of this page for the improved version ‹Reach of law limit 2› with additional qualification.

You might think that the defining formula for ‹Reach of law limit› is surprisingly complicated. There is a simpler, but stronger principle (see definition of ‹Reach of law limit› for discussion of its weakness), that also suffices to derive ✓Goal. It says a set of concerns Δ does not justify criminalizing an action a if that action can accomplish a proposition ψ such that for each of the concerns δ, either a does not conflict with δ, or δ is not more important than ψ. I'll now explain why I am reluctant to use this simpler principle. The problem is that ψ is not adequately constrained by a. Consider the contrapositive: If the concerns Δ justify criminalizing an action a, then for every proposition ψ that a accomplishes, there must be a concern δΔ such that a conflicts with δ and δ is more important than ψ. That consequent is too strong a requirement in some cases! Suppose we want to justify the criminalizing of an action that accomplishes something very good while unnecessarily accomplishing something bad. I'll use an example based on one given by Paul McNamara in a slightly different deontic logic context. We want to argue that it should be criminal to perform the action a of intentionally and unnecessarily breaking a person Timmy's fingers even if it is done while saving Timmy from a fire. The simpler-but-stronger principle that I am reluctant to use says that if we believe that (*) := "Timmy is saved and his fingers are broken" is more important than "Timmy's fingers are not broken", then we cannot consistently justify illegalizing a using just Timmy's desire δ to not have broken fingers. In contrast, with ‹Reach of law limit› we may consistently criminalize a and believe (*), under the reasonable assumption that it is possible to save Timmy without breaking his fingers.

Intended audience of critics

The intended audience for this interpreted formal proof consists of the Supreme Court justices who ruled against Sue Rodriguez, and anyone who agrees with their decision for the same reasons.


Sort op Set - Powerset of the given sort.
Sort Actions
Potential concrete actions of individuals. A set each element of which is a concrete/unrepeatable, potential action. By "concrete/unrepeatable", I mean that each action has a definite location (resp. interval of time) where (resp. when) it would hypothetically occur (). Also, each element of this set can be associated with a unique person who performs the action.
Sort Propositions
Propositions about the real world; things that will turn out true or false. Each will be satisfied or not in every model, but it is nonetheless important that they are distinct from 0-ary predicate symbols, as we will have functions with domain Propositions.
Sort People
The set of residents of Canada who are alive sometime during 1993 (the year of S.R.'s supreme court hearing) or later.
Variables δ, ψ, ψ₁, ψ₂, ψ₃, ψ₄ are reserved for sort Propositions.
Variables Δ, Δ′ are reserved for sort Set(Propositions).
Variable a is reserved for sort Actions.
Variables X, Y, Z, Y₁, Y₂, Y₃ are reserved for sort Set(Actions).
Variable p is reserved for sort People.

Performed : Actions → 𝔹 - The potential actions that are actually performed.
Satisfied : Propositions → 𝔹 - The propositions that turn out true.
S.R. : People - Sue Rodriguez
«S.R. facts» : Propositions
The conjunction of the following list of facts (satisfied propositions) about Sue Rodriguez:
  1. S.R. has ALS, a usually fatal disease, and multiple doctors have given their opinion that her life expectancy is short.
  2. In the late stages of the disease, S.R.'s movement will be greatly restricted. If she wishes to live until then (and she does), she will not be able to take her own life without assistance.
  3. There is no dispute about whether assisted suicide is truly what S.R. wants, as evidenced, for example, by the testimony of her friends and family, lack of contradicting testimony from anyone, and her involvement in the Death with Dignity movement.
  4. And many more. If some of the assumptions below are expanded into proved lemmas, more facts will be added to this list, and at some point it may be prudent to break this constant up into a number of constants, or a constant of type List(Propositions), so that the individual facts can be referred to and criticized more formally.
«SueR request» : Propositions
Satisfied iff Sue Rodriguez becomes confident that she will be able to take some action (in Actions) such that each of the following hold:
  1. After completion of the action, she has no further severe pain or indignity caused by her illness.
  2. The action, during its execution, does not cause pain or unusual physical or psychological discomfort.
  3. Her doing the action does not put any friend or loved one at risk of being convicted of a criminal offence.
  4. She does not need to leave Canada permanently in order to do the action.
  5. If the action causes permanent loss of consciousness, then it does not occur until a time when she believes she is no longer able to enjoy life (which she expected would be after losing most of her mobility).
‹assisted suicide actions for SueR› : Set(Actions)
The set of actions in which Sue Rodriguez, while in Canada, legally obtains, for the purpose of ending her life, a lethal dose of barbiturates, morphine, or any other drug that is reliably painless, and reliably induces sleeping before it induces loss of consciousness and then death.
$a_{SR}$ : Actions
Any element of ‹assisted suicide actions for SueR›. It may be necessary to make it more specific if Assumption 7 is criticized.
‹actions sufficient for› : PropositionsSet(Actions)
The set of all actions that are feasible and can be expected to result in the given proposition being satisfied.
‹More important than› : Propositions × Propositions → 𝔹
A vague (but sufficiently precisifiable) and highly subjective partial order. Example that everyone in the intended audience of this argument should agree on: specific propositions corresponding to instances of "the right to not be murdered" are typically more important than specific propositions corresponding to instances of "the right to free speech".
Conflicts : Actions × Propositions → 𝔹
If the relation holds for (a,ψ) then a conflicts with ψ in the sense that if a is performed then (causally, directly or indirectly) ψ cannot be satisfied.
not : PropositionsPropositions
The proposition that is satisfied iff the given proposition is not satisfied.
‹regrettable legal assisted suicide› : People → 𝔹
‹regrettable legal assisted suicide›(p) is the proposition that is satisfied iff:
  1. p dies by a legally-sanctioned use of assisted suicide.
  2. There is some information about p, which was unknown at the time when their application for assisted suicide was approved, that, if it had been known, would have caused a significant proportion (say, 5%) of people who would have supported p's application to resolutely change their mind. Here "resolutely" means that no further information about p would again change the minds of those 5% of people. We more simply (but slightly more vaguely) say that at least 5% of p's supporters, if given "perfect" information about p, would change their minds,
«avoid judicial overreach» : Propositions
The ruling of the supreme court justices on Sue Rodriguez's case does not constitute "judicial overreach".
«avoid legal precedent causing slippery slope» : Propositions
Satisfied if «SueR request» is not satisfied, or if «SueR request» is satisfied and a certain kind of "slippery slope" is blocked; in particular, permitting S.R.'s assisted suicide request does not "lead to" the Supreme Court or a lower court permitting a regrettable (see ‹regrettable legal assisted suicide›) instance of assisted suicide.
Defn~ «no regrettable legal assisted suicide for S.R.» : Propositions - The proposition that is satisfied iff ‹regrettable legal assisted suicide›(S.R.) is not satisfied.
Satisfied(«no regrettable legal assisted suicide for S.R.») ⇔ ¬‹regrettable legal assisted suicide›(S.R.)
«consistency with maj opinion» : Propositions
The proposition that is satisfied iff the decision made by the Supreme Court is "in agreement with the majority opinion" of Canadian citizens on whether S.R. should be granted an exception to the criminal code.
Defn sc-concerns : Set(Propositions) - "sc" for Supreme Court. Some of the concerns of opponents of assisted suicide, formulated as propositions that they want to be true. Specifically, they are the concerns mentioned in the majority opinion for the actual Supreme Court decision.
sc-concerns = {«avoid judicial overreach», «avoid legal precedent causing slippery slope», «no regrettable legal assisted suicide for S.R.», «consistency with maj opinion»}
‹Justifies criminalizing› : Set(Propositions) × Set(Actions) → 𝔹
The desirability of satisfying the given propositions justifies criminalizing the given actions.
Defn ‹Justifies criminalizing satisfaction of›(Δ, ψ) : Set(Propositions) × Propositions → 𝔹 - The desirability of satisfying the given propositions Δ justifies criminalizing the satisfaction of ψ.
Δ,ψ. ‹Justifies criminalizing satisfaction of›(Δ, ψ) ⇔ ‹Justifies criminalizing›(Δ, ‹actions sufficient for›(ψ))

Defn ‹Reach of law limit› : Set(Propositions) × Propositions → 𝔹 - The defining formula of this predicate is a general, but weak, principle of liberalism, which we will use one instance of (Assumption 1). It only requires justification for laws that criminalize all possible ways of accomplishing a proposition ψ, saying nothing about laws that criminalize, without justification, some but not all actions than can accomplish ψ.
It says that the set of (ostensibly desired) propositions Δ does not justify criminalizing the satisfaction of the proposition ψ (by criminalizing all the actions that can accomplish ψ) if there is an action that can accomplish ψ such that, for each of the desired propositions δ Δ, either δ is not more important than ψ, or the action does not conflict with δ.
Contrapositive: Suppose that a set of (ostensibly desired) propositions Δ justifies criminalizing the set of all actions that can accomplish another proposition ψ. Intuitively, this means Δ justifies criminalizing the satisfaction of ψ. Then, it must be that for each of those actions a that can achieve ψ, there is a proposition δ Δ that both conflicts with a and is more important than ψ.
Δ. ∀ψ. ‹Reach of law limit›(Δ, ψ) ⇔ ((∃a ‹actions sufficient for›(ψ). ∀δ Δ. ¬‹More important than›(δ, ψ) ∨ ¬Conflicts(a, δ)) ⇒ ¬‹Justifies criminalizing satisfaction of›(Δ, ψ))

✓Goal: The specific set of concerns sc-concerns does not justify criminalyzing the satisfaction of «SueR request».
¬‹Justifies criminalizing satisfaction of›(sc-concerns, «SueR request»)

The theorem is a logical consequence of the following axioms; the code that generates this HTML file also generates first-order validity problems, which were solved by CVC4 and Vampire via System on TPTP. Each axiom can be disputed, and some, with more work, can be made into lemmas, proved from more-basic assumptions and simplifying assumptions. Each axiom is informally labeled an Assumption or Assertion. The Assertions are intended to be uncontroversial.

Assumption 1: Suppose there is some action a that S.R. can take to achieve «SueR request» such that, for any concern ψ sc-concerns that is not strictly less important than «SueR request», the action a does not actually conflict with ψ. Then sc-concerns does not justify criminalizing the set of all actions that can achieve «SueR request».
‹Reach of law limit›(sc-concerns, «SueR request»)
✓Lemma 1: There are no actions that can achieve S.R.'s request other than the ones described above in ‹assisted suicide actions for SueR› (all of which involve her use of assisted suicide).
‹assisted suicide actions for SueR› = ‹actions sufficient for›(«SueR request»)
Argument sketch: I claim that there are three broad categories of actions that might plausibly be able to achieve the satisfaction of «SueR request»: (1) treatment, (2) suicide, or (3) palliative sedation (aka terminal sedation). In Rodriguez's and Taylor's cases, there are no sufficient treatments for ALS and there is no hope for the discovery and availability of a new one before their death, so (1) is out. To dismiss (3) one must do some reading, e.g. Palliative Sedation: It’s Not a Panacea; in short, the ideal of terminal sedation, in which a dying patient's life is not shortened, but all their suffering is medicated away, is far from achieved in practice. If it was ideal, we would include in ‹actions sufficient for›(«SueR request») actions by which a patient is guaranteed access to terminal sedation (there is currently no general way of getting such a guarantee in Canada; one has to just get lucky to end up with a doctor who is willing to do it).
$A_t, A_s, A_{ps}$ : Set(Actions)
Actions that could plausibly achieve, respectively, a treatment/cure, suicide (including assisted suicide), or palliative sedation, for S.R.
Assertion 1: Every action that can achieve S.R.'s request is one involving a treatment/cure of her condition, some form of suicide, or some form of palliative sedation.
‹actions sufficient for›(«SueR request») $A_t$ $A_s$ $A_{ps}$
Argument sketch: I claim that there are three broad categories of actions that might plausibly be able to achieve the satisfaction of «SueR request»: (1) treatments/cures, (2) suicide, or (3) palliative sedation (aka terminal sedation). I don't anticipate that this would be disputed.
Assertion 2: Treatment/cure-seeking actions cannot achieve S.R.'s request.
‹actions sufficient for›(«SueR request») $A_t$ =
Argument sketch: While ALS could be effectively treated or cured some day, «SueR request» would require the discovery and minimal testing of such a treatment within a year or two, and there is negligible hope within the medical community for that.
Assumption 2: Palliative sedation cannot achieve S.R.'s request.
‹actions sufficient for›(«SueR request») $A_{ps}$ =
Argument sketch: See Palliative Sedation: It’s Not a Panacea; in short, the ideal of terminal sedation, in which a dying patient's life is not shortened, but all their suffering is medicated away, is far from achieved in practice. If it was ideal, we would need to include, in ‹actions sufficient for›(«SueR request»), actions through which a patient becomes guaranteed access to terminal sedation. However, there is currently no general way of getting such a guarantee in Canada; one has to just get lucky to end up with a doctor who is willing to do it.
Assumption 3: Among the possible ways that S.R. could end her own life, only those in ‹assisted suicide actions for SueR› satisfy the criteria of «SueR request».
‹actions sufficient for›(«SueR request») $A_s$ = ‹assisted suicide actions for SueR›
Argument sketch: Proving this involves a morose consideration of all the known methods of suicide, observing that each of them, besides the use of legally-prescribed sedatives, violates at least one of the conditions of «SueR request».
Assertion 3: The uncontroversial assertion that the actions described in ‹assisted suicide actions for SueR› would suffice to meet S.R.'s desired condition «SueR request».
‹assisted suicide actions for SueR› ‹actions sufficient for›(«SueR request»)
Assertion 4: The specific action $a_{SR}$ is in ‹assisted suicide actions for SueR› (informally "by definition").
$a_{SR}$ ‹assisted suicide actions for SueR›
Assumption 4: The judges' necessary involvement in making it legal for S.R. to obtain lethal prescription drugs need not constititue judicial overreach.
¬Conflicts($a_{SR}$, «avoid judicial overreach»)
Argument sketch: Claim that a suspended annulment, with a period of at least one year, plus a special waiver for one person, is never judicial overreach. In a suspended annulment, a law is declared unconstitutional, but it is allowed to remain in effect for a period of time, to give the legislative branch the opportunity to replace it with a new, constitutional law. Reading: Myth of Judicial Overreach
Assumption 5: The judges' necessary involvement in making it legal for S.R. to obtain lethal prescription drugs need not create a legal precedent that leads to a "slippery slope".
¬Conflicts($a_{SR}$, «avoid legal precedent causing slippery slope»)
Argument sketch: Though the justices may not be able to artificially specify that their ruling in favour of S.R. should not be used as precedent, they can certainly restrict the extent of the precedent, by specifying only that the law is unconstitutional for any citzen satisfying «S.R. facts». A citizen petitioning a lower court for access to assisted suicide, who does not satisfy all of «S.R. facts», would be neither helped nor hindered by the ruling in favour of S.R. Given that consideration, we can use the same argument that we use for Assumption 7 to justify this assumption (since in that argument «S.R. facts» are the only facts we use about S.R.).
Assumption 6: S.R.'s claim for «SueR request» trumps her opponents' claim for Supreme Court decisions to be consistent with the majority opinion (among Canadian citizens).
¬‹More important than›(«consistency with maj opinion», «SueR request»)
Argument sketch: The goal of protection against tyranny of the majority is precisely what makes the constitution special, compared to other laws. My opinion is that «consistency with maj opinion» should be given very small (if not zero) weight when assessing whether a part of the law should be repealed on constitutional grounds. To replace this assumption with a high-level proof...
Assumption 7: The particular assisted suicide acton $a_{SR}$ that we chose does not conflict with the desire to avoid S.R. being the victim of a ‹regrettable legal assisted suicide›.
¬Conflicts($a_{SR}$, «no regrettable legal assisted suicide for S.R.»)
Argument sketch: This is easily argued by reference to «S.R. facts».

Criticizing the argument

The justices that ruled against Sue Rodriguez (hereafter called "the majority", as in the decision itself) and wrote the majority opinion in the Rodriguez ruling implicitly criticized Assumption 4, Assumption 5, and Assumption 6, but not Assumption 7. Their arguments did not significantly touch on the details considered in ✓Lemma 1, which is not surprising as they did not attempt to reason with non-trivial precision about the costs and benefits for Sue Rodriguez.

Take Assumption 6 for example. The authors of the majority opinion write: "the issue before the Court was whether a criminal prohibition on assisting suicide in situations where a person is terminally ill and mentally competent but unable to commit suicide by him or herself, is contrary to the principles of fundamental justice. What are principles of fundamental justice? Mr. Justice Sopinka noted that determining these principles can be an onerous task. Such principles, he pointed out, are those for which there is some consensus among reasonable people as to their importance to our societal concept of justice."

From that statement, we can see that the majority rather flatly disagree with the opinion I express in the prose below the statement of Assumption 6. So how to proceed after that? I could dispute their claim about the consensus of the Canadian public (probably hard, but that situation is slowly improving in favour of assisted suicide), or I could look for other cases that demonstrate the justices informally contradicting their allegiance to the principle expressed in the above quote (probably easy), or I could take this as a fundamental source of subjective disagreement. For the last option, I would move on to their criticisms of the other assumptions, and try to refute them (by demonstrating informal inconsistency), so that we are left with only one source of fundamental disagreement.

Another possible criticism is that sc-concerns is too small a set. A critic may wish to add an entirely new Propositions constant to sc-concerns, or perhaps the conjunction of two or more of the current elements of sc-concerns. An addition of the latter type could conceivably have a significant effect if combined with an addition of the first type, since Assumption 1 considers the elements of the first argument to ‹Reach of law limit› separately (an addition of the first type would be necessary to really force me to respond in a challenging way, since currently only one of the 4 primitive concerns are compared to «SueR request» with ‹More important than›). In any case, a language modification and extension that makes ‹Reach of law limit› respect conjunctions of elements of sc-concerns is as follows:

and : Set(Propositions) → Propositions - Conjunction of the given set of propositions.
: Set(Propositions) × Set(Propositions) → 𝔹 - Subset
\ : Set(Propositions) × Set(Propositions) → Set(Propositions) - Set difference
Defn ‹Reach of law limit 2› : Set(Propositions) × Propositions → 𝔹 - ‹Reach of law limit 2›(Δ,ψ) asserts the following statement, which is an implication. If Δ can be partitioned into two sets Δ' and Δ\Δ' such that
  • the conjunction of the concerns Δ' is not more important than ψ, and
  • there is an action a that can accomplish ψ such that none of the concerns in Δ\Δ' actually conflict with a
then Δ does not justify criminalizing all the actions that can accomplish ψ.
Δ,ψ. ‹Reach of law limit 2›(Δ, ψ) ⇔ ((∃Δ′ Δ. ¬‹More important than›(and(Δ′), ψ) ∧ (∃a ‹actions sufficient for›(ψ). ∀δ Δ\Δ′. ¬Conflicts(a, δ))) ⇒ ¬‹Justifies criminalizing satisfaction of›(Δ, ψ))