# Argument for physician assisted suicide in Canada

Use AnnotateIt.org

Throughout this argument, S, NS, AS, PAS abbreviate 'suicide', 'no suicide', 'assisted suicide', 'physician-assisted suicide'

This is an argument for favouring the introduction of legislation that founds an administrative system (here broadly-defined) for granting Canadians access to physician-assisted suicide in limited cases. Before getting into the specifics, I want to discuss some important differences between this argument and (purely) natural language, non-deductive arguments also in favour of physician-assisted suicide (PAS).

The conclusion of this argument is weaker than the conclusions of the non-deductive arguments. In particular, the advocated (underspecified) PAS system is under-inclusive: it would not grant access to all people who I (or almost any proponent of physician-assisted suicide) think should have access. I am prepared to argue, informally, that this --and by "this" I mean under-inclusiveness in general, not the particular kind/degree of under-inclusive that the system involved here has-- that this is a necessary feature of any sufficiently-rigorous argument that does not make stronger assumptions than this one. More specifically, for any argument

• whose assumptions do not preclude the possibility of regrettable uses of physician-assisted suicide (see ‹regrettable PAS›), and
• that does not make strong assumptions along the lines of "regrettable assisted suicides aren't that bad", and
• whose assumptions do not guarantee that the advocated administrative system for PAS will have access to additional information about applicants,

there will be applicants who should, in a subjective moral sense according to proponents like me, have access to PAS, but who are indistinguishable from (hypothetical) applicants whose assisted suicide would be regrettable.

Even so, one could argue that this system is especially or unnecessarily under-inclusive, and that I won't dispute. This argument should be taken as a proof-of-concept. A more-serious attempt would have to involve much more research about this particular issue (e.g. data from the history of the systems in places like the Netherlands and Oregon) than I can afford to do for my thesis. A recent source of such information and much more is Quebec's Committee report on dying with dignity.

At this point I could enumerate the ways that existing non-deductive/natural language arguments use stronger assumptions than those employed here. But here is a method that you can use to collect most of those ways yourself: for each Assumption and Simplifying Assumption, consider how one could use natural language to hide the details of the problem that the assumption addresses. For example, I will spend a surprising amount of time delineating the things that I consider possibly-pertinent to the decision of whether or not to support the legislation. I have never seen this done in such a clear and explicit way in informal arguments; often the best one can hope for is that it can be unambiguously gleaned from reading nearly the entire text of the argument (which is book-length in some cases, e.g. the committee report linked to in the previous paragraph). Another example is the unusually-specific weighing of the (sometimes theoretical) pros and cons of such legislation; in this argument I go a level deeper than any natural language argument I have seen in the justification for the main required subjective proposition ✓Lemma 74.

There may already exist a natural language argument about PAS that is every bit as fair and disciplined as the one I give here (the best concise argument I've read was written by the supreme court justices in the minority opinion for the Sue Rodriguez case). A similar thing can be said for any proposed prescription or standard; always there are actors in the scope of the prescription that have come to comply with it on their own. In the case of maximally fair/disciplined argumentation, like in the case of prescriptions for limiting pollution, or the protection of human rights, etc, those actors should be applauded, but their existence should not detract from the importance of the prescription unless they are sufficiently common (where "sufficiently common" is relative: we would need them to be very common in the case of pollution, or universal in the case of human rights).

## Some features of the administrative system

First, a person must opt-in before being diagnosed with their terminal illness. The purpose of this feature is to lower the (already low) incidence of some forms of difficult instances of regrettable assisted suicides (‹difficult-regrettable PAS›), which are regrettable assisted suicides in which

1. The applicant is correctly diagnosed; or the applicant is incorrectly diagnosed, but nonetheless suffers from an illness that is terminal without treatment, and all methods of diagnosis have been exhausted (see ‹PAS with wrong and substandard diagnosis›).
2. The person who uses the lethal drugs is the person who applied for them (see ‹PAS of wrong person›).
3. The applicant uses the drugs with the intention of dying.
4. The applicant was not actively coerced into applying for and/or taking the drugs (see ‹coerced suicide›).

Second, a person must take the drugs in the presence of their physician. This is not ideal, and is not required in Oregon, for example, but it is useful for justifying the assumption that with very high probability, the negations of items 2 and 3 above never happen.

Third, there is a fixed list of eligible terminal diseases, which includes only those for which it can be established with "high" probability that a person has the disease and will "very likely" not live for more than X months. Each of "high", "very likely" and X can differ for different patients; the first two only need to be high enough and the third small enough that the patient is unwilling to try to beat the doctors' reported odds.

Fourth, in some parts of Canada, prosecution for illegal assisted suicide is rare relative to its incidence. This must remain the case even after a PAS law is passed. This is to justify the assumption that ‹S, NS because of incr fear of prosecution› happens to no one with high probability (in Assumption 2). In particular, a person answering a request to assist another person in dying, where the second person is ineligible for legal PAS, should not be, or perceive to be, at increased risk of prosecution, compared to the risk before the law is passed.

Fifth, to justify the assumption that ‹NS, NS & worse palliative care› happens to no one with high probability (in Assumption 2), the government will monitor private donations towards palliative care and research on palliative care, and if the appropriately-adjusted funds per person drops below what it was before the PAS law was passed, the government will increase public funding to compensate.

Sixth, to support all of Assumption 2 through Assumption 6, since all can be broken by incompetence, the government will adopt one of the provisions from Quebec's bill 52, which they summarize as follows:

A commission on end-of-life care is established under the name “Commission sur les soins de fin de vie”, as well as rules with respect to its composition and operations. The mandate of the Commission is to examine all matters relating to end-of-life care and to oversee the application of specific requirements relating to medical aid in dying.

## High-level features of the argument

I refer to the things that the axioms assume are pertinent to comparing the two outcomes (legislation passed, or not) as individual-future relations (sort IFR). They are essentially just relations on the lives of people (sort People) in a given possible future (sort ◊Future).

### Classifying the differences of a person's life between two possible futures

We are going to be reasoning about the costs and benefits to people of the proposed legislation in terms of some of the qualitative effects, for each person, of "moving" from a possible future without PAS (status-quo future) to one with PAS (assisted suicide future). To that end, we categorize people using individual-future-difference relation (sort Δ), which are relations about the features of their lives in a given pair of possible futures (sort ◊FuturePair). Usually, a Δ is determined by a pair of IFR's; the people satisfying such a Δ satisfy the first IFR in the status-quo future and the second IFR in the assisted suicide future. Some Δ's can't easily be represented as a product of two IFR's. An example is ‹NS, NS & worse palliative care›, which means:
The person's death is not a suicide in the status-quo future or the assisted suicide future, and the quality of palliative care available to them is worse in the assisted suicide future compared to in the status-quo future.
The problem is that worse palliative care depends on both of the futures. Such a Δ could be defined by a family of IFR-pairs, but that would appear to require quantifying the quality of palliative care, which is difficult to do right (in a way that is satisfactory to everyone), and even if done right introduces an unnecessary abstract entity into the argument (namely the partially-ordered set of quantities).

### Distributions over possible futures

Our uncertainty about how the future will turn out, with or without new legislation for PAS, is modelled by a Bayesian probability distribution 𝒟 over pairs of possible futures, where the first (resp. second) element of a pair is a possible future in which the proposed legislation is not (resp. is) passed. To be accurate, the distribution is over equivalence classes of pairs of possible futures (sort ◊FuturePairEC), where two pairs are in the same class if they agree on δ(p,·) for every individual future difference relation δ and every person p (see definition of ec). That is just so that our interpretations of 𝒟 can be finite (since we define only finitely-many Δ's), to assuage any discomfort about measures over possible futures.

### Two typical futures

The language of Bayesian reasoning isn't used in informal debates about PAS, and it won't be used much here either. Instead, we will define two "typical" possible futures, according to whether or not the legislation is passed. In this introduction I will call them ASF (assisted suicide future) and SQF (status-quo future), though in the proof they are always paired together as $\vec{F}_{\text{typical}}$. Assumption 1 is the axiom that says the goal ‹should pass› is implied by a statement about $\vec{F}_{\text{typical}}$, so it is the assumption a critic should reject if they have a problem with passing from Bayesian distributions to the typical future pair, or a more-fundamental problem with the use of a Bayesian distribution at all. For δ an individual-future-difference relation, and ${\vec{F}}$ a pair of possible futures, let #(δ, ${\vec{F}}$) be the number of people p such that δ(p) holds in ${\vec{F}}$ (written δ(p, ${\vec{F}}$) in the proof). Let Exp#(δ, ${\vec{F}}$) be the expected value of #(δ, ${\vec{F}}$) when ${\vec{F}}$ is sampled from 𝒟. Then in the definition of $\vec{F}_{\text{typical}}$, SQF and ASF are partially defined() in such a way that:
• extremely unlikely Δ's don't happen to anyone.
• there are slightly-pessimistic counts (for proponent of PAS), relative to the expected values determined by 𝒟, for Δ's that are favourable for ASF.
• there are slightly-optimistic counts (for opponents of PAS), relative to the expected values determined by 𝒟, for Δ's that are favourable for SQF.

### Argument in steps

Most of the main tasks of the argument are as follows:
1. Semantically define a number of IFR's (i.e. introduce them as primitive symbols, with language interpretation guide entries).
2. State uncontroversial axioms about relations between the IFR's.
3. Syntactically define a number of Δ's in terms of IFR's, and semantically define a few more.
4. Derive some statements relating the Δ's (using relations between IFR's), and assume some others as uncontroversial axioms.
5. Define the pair of typical futures $\vec{F}_{\text{typical}}$ = ‹SQF, ASF› as discussed above.
6. Syntactically define sets of people P₁,…,Pₙ in terms of satisfying various Δ's with respect to $\vec{F}_{\text{typical}}$.
7. Derive some subset, disjointness and emptiness relations between the Pᵢs (from relations between the Δ's). Also make assumptions, some of them controversial, about relations between some of the other Pᵢs.
8. Make subjective, controversial assumptions of this form: "The change in moving from SQF to ASF in the quality-of-life for the people in Pᵢ (considered as a group- not individually) is worse/better/approximately the same as the change for the people in Pⱼ."
9. State easily-agreed-upon axioms that suffice to derive, from the other axioms and lemmas, that the change in moving from SQF to ASF in the quality of life for the set of ‹all people› is positive overall.
Note that the form of the final conclusion in item 9 is the same as the form of the subjective assumptions in item 8. This may lead one to wonder what we gain from all this work. Here is part of the answer: the item 8 (and item 7) assumptions are much more specific than the item 9 conclusion, and because of this you learn a lot more about my opinions than you would from my simply asserting the item 9 conclusion. That is a good thing on its own, but it also makes the task of criticizing my opinions much more feasible.

Sort People
The set of residents of Canada. For concreteness, let's say the residents who are alive sometime during 1993 (the year of Sue Rodriguez's supreme court hearing) or later.
Sort ◊Future
Conceivable possible futures. This set is loosely defined. The main requirement, implicitly imposed by RelAppIFR and RelAppΔ, is that each element is defined precisely enough that any IFR relation can be evaluated on it (and similarly for Δ relations).
Sort IFR
Individual-Future Relation. An element is a relation on People × ◊Future.
Sort ◊FuturePair - This is ◊Future × ◊Future.
Sort Δ
Individual-future-difference relation. An element is just a relation on People × ◊FuturePair = People × ◊Future × ◊Future, which is accessed via RelAppΔ.
Sort ◊FuturePairEC
Equivalence classes of ◊Future pairs. Effectively defined by ec and rep.
Sort FinSet(People)
Sort MultiSet(Delta)
Sort Distr(FPairEC)

‹should pass› : → 𝔹
True if you think that legislation should be passed that introduces an administrative system for assisted suicide that is compliant with the description at the top of this argument.
RelAppIFR : IFR × People × ◊Future → 𝔹
When φ is an IFR relation, p is from People, and F is from ◊Future, then RelAppIFR(φ, p, F) means φ is true for p in F. The second order syntax φ(p, F) is used to display RelAppIFR(φ, p, F).
RelAppΔ : Δ × People × ◊FuturePair → 𝔹
When δ is a Δ relation, p is from People, and ${\vec{F}}$ is from ◊FuturePair, then RelAppΔ(δ, p, ${\vec{F}}$) means δ is true for p in ${\vec{F}}$. The second order syntax δ(p, ${\vec{F}}$) is used to display RelAppΔ(δ, p, ${\vec{F}}$).
Definitional Axiom 1: P₁,P₂. P₁ = P₂ ⇔ (∀p. p P₁p P₂)
Definitional Axiom 2: φ₁,φ₂. φ₁ = φ₂ ⇔ (∀p. ∀F. φ₁(p, F) ⇔ φ₂(p, F))
Definitional Axiom 3: δ₁,δ₂. δ₁ = δ₂ ⇔ (∀p,${\vec{F}}$. δ₁(p, ${\vec{F}}$) ⇔ δ₂(p, ${\vec{F}}$))
Δof : People × ◊FuturePairΔ
δ = Δof(p,${\vec{F}}$) is the unique most-specific/smallest δ:Δ such that δ(p,${\vec{F}}$). For a given ◊FuturePair ${\vec{F}}$, the differences (that you think are sufficiently-relevant to this debate) between a person p's experiences in the two futures -directed differences, the change from the first element of ${\vec{F}}$ to the second element of ${\vec{F}}$- are given by Δof(p,${\vec{F}}$).
ΔsOf : FinSet(People) × ◊FuturePairMultiSet(Δ)
If P is a set of People, then ΔsOf(P,${\vec{F}}$) is the multiset of the same size |P| obtained by applying ΔsOf(·,${\vec{F}}$) to P.
Δ : MultiSet(Δ) × MultiSet(Δ) → 𝔹
A subjective comparison relation. If Y₁ Δ Y₂ then you would rather have the life-experience changes Y₁ happen to |Y₁| random people than have the life-experience changes Y₂ happen to |Y₂| random people. Is a strict partial order.
: MultiSet(Δ) × MultiSet(Δ) → 𝔹
A subjective equivalence relation. If Y₁ Y₂ then you are impartial or cannot decide whether you would rather have the life-experience changes Y₁ happen to |Y₁| random people or the life-experience changes Y₂ happen to |Y₂| random people.
Defn Δ : MultiSet(Δ) × MultiSet(Δ) → 𝔹 - Y₁,Y₂. Y₁ Δ Y₂ ⇔ (Y₁ Δ Y₂Y₁ Y₂)
Defn~ ec : ◊FuturePair◊FuturePairEC - ${\vec{F}_{1}}$,${\vec{F}_{2}}$. ec(${\vec{F}_{1}}$) = ec(${\vec{F}_{2}}$) ⇔ (∀p,δ. δ(p, ${\vec{F}_{1}}$) ⇔ δ(p, ${\vec{F}_{2}}$)) - Equivalence class of the given ◊FuturePair. See description of ◊FuturePairEC.
Defn~ rep : ◊FuturePairEC◊FuturePair - E. ec(rep(E)) = E
A representative for the given equivalence class. rep(E) can be any ${\vec{F}}$:◊FuturePair such that ec(${\vec{F}}$) = E.
Defn swap : ◊FuturePair◊FuturePair - ${\vec{F}}$. swap(${\vec{F}}$) = ❬${\vec{F}}$[2],${\vec{F}}$[1]❭
Defn~ pairIFR : IFR × IFRΔ - p,${\vec{F}}$,φ,ψ. pairIFR(φ, ψ)(p, ${\vec{F}}$) ⇔ (φ(p, ${\vec{F}}$[1]) ∧ ψ(p, ${\vec{F}}$[2]))
The Δ relation obtained in the natural way from two IFR relations; the first (resp. second) IFR relation is applied to the first (resp. second) element of the given ◊FuturePair. Most elements of Δ can be defined in the way. An example of an exception is ‹S, NS & worse palliative care›, because worse palliative care'' depends on both elements of the ◊FuturePair. Such a Δ relation could be defined by a family of IFR-pairs, although that would appear to require quantifying the quality of palliative care, which, if done right (in a way that is satisfactory to everyone), introduces an unnecessary abstract entity into the argument, namely the partially-ordered set of quantities.
Defn~ peopleInIFR : IFR × ◊FutureFinSet(People) - φ,F,p. p peopleInIFR(φ, F) ⇔ φ(p, F)
Defn~ peopleInΔ : Δ × ◊FuturePairFinSet(People) - δ,${\vec{F}}$,p. p peopleInΔ(δ, ${\vec{F}}$) ⇔ δ(p, ${\vec{F}}$)
Defn~ 0 : MultiSet(Δ) - ${\vec{F}}$. 0 = ΔsOf(, ${\vec{F}}$)
Empty multiset that corresponds to a 'neutral' judgement; if ΔsOf(P,${\vec{F}}$) = 0, then for the set of people P, the pair of futures ${\vec{F}}$ are, overall, of equal value with respect to the Δ relations in use.
Defn~ ‹true› : IFR - F. ∀p. ‹true›(p, F) - Trivial IFR such that ‹true›(p,F) for all p,F.

‹S› : IFR - The person's death is a suicide.
Defn ‹NS› : IFR := co(‹S›) - The person's death is not a suicide.
Defn~ ‹PAS› : IFR - ‹PAS› ‹S› - The person ends their life via physician-assisted suicide
Defn ‹non-PA suicide› : IFR := ‹S› \ ‹PAS› - The person's death is a non-physician-assisted suicide.
Defn~ ‹regrettable PAS› : IFR - ‹regrettable PAS› ‹PAS›
A person p is in this IFR if they legally use physician-assisted suicide and if there is some information about p, which was unknown at the time when their application for PAS was approved, that, if it had been known, would have caused a significant proportion (say, 20%) 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 20% of people. A more concise but possibly more vague definition would be to say that at least 20% of p’s supporters, if given "perfect information" about p, would change their minds.
Defn ‹non-regrettable PAS› : IFR := ‹PAS› \ ‹regrettable PAS›
Defn~ ‹PAS with wrong and substandard diagnosis› : IFR - ‹PAS with wrong and substandard diagnosis› ‹regrettable PAS›
The person is incorrectly diagnosed with a soon-to-be-terminal condition when their real condition is presently treatable. For this argument, we will only allow PAS for conditions that can be diagnosed with very high accuracy. The other option one could take is to argue that a patient can still benefit from PAS even when they were wrongly diagnosed, provided at least that they had the best medical care available. The point is that, if all available evidence has been taken into account, including the probabilities of misleading and missing evidence, then the individual's decision indirectly expresses their utilities of living with suffering vs dying unnecessarily, and in that case we should use their utilities as opposed to an average.
Defn~ ‹coerced suicide› : IFR - ‹coerced suicide› ‹S›
The person was actively coerced into suicide (assisted or otherwise) by another person, where "actively coerced" means influenced by some means other than guilt, a sense of duty, etc. This is another logical possibility that is easy to "deal with" in this argument (where "deal with" does not mean prevent - see Assumption 4).
Defn ‹non-coerced suicide› : IFR := ‹S› \ ‹coerced suicide›
Defn~ ‹PAS of wrong person› : IFR - ‹PAS of wrong person› ‹regrettable PAS›
This could theoretically happen in Oregon, for example, since the prescribed lethal drugs don't need to be taken in the presence of a physician. To simplify this argument, we posit a stricter system in which the prescribed drugs must be taken in the presence of a physician.
Defn ‹coerced PAS› : IFR := ‹coerced suicide› ‹PAS›
Definitional Axiom 4: ‹coerced PAS› ‹regrettable PAS›
Defn ‹very bad PAS› : IFR := ‹PAS of wrong person› (‹coerced PAS› ‹PAS with wrong and substandard diagnosis›)
Union of some relations that, when true, constitute major failures of the safeguards of the assisted suicide system.
Defn ‹non-coerced PAS› : IFR := ‹PAS› \ ‹coerced PAS›
Defn ‹very bad non-coerced PAS› : IFR := ‹very bad PAS› ‹non-coerced PAS›
Defn ‹regrettable non-coerced PAS› : IFR := ‹regrettable PAS› ‹non-coerced PAS›
Defn ‹non-regrettable non-coerced PAS› : IFR := ‹non-regrettable PAS› ‹non-coerced PAS›
Defn ‹non-coerced non-PA suicide› : IFR := ‹non-coerced suicide› ‹non-PA suicide›
Defn ‹difficult-regrettable PAS› : IFR := ‹regrettable PAS› \ ‹very bad PAS›
The kinds of hypothetical regrettable uses of PAS that are hardest to prevent.
Defn ‹difficult-regrettable non-coerced PAS› : IFR := ‹difficult-regrettable PAS› ‹non-coerced PAS›
‹NS & worst-case denial of PAS› : IFR
These are the people who have a genuine self-centered desire for PAS and suffer most from not having the option of PAS. Includes at least each person who has an (eventually) physically and/or mentally painful condition and:
• Will not be physically capable of committing suicide without help, by the time they wish to. E.g. if their medical condition severely restricts their movement. And:
Doesn't know anyone who would be willing to assist them, or does know such a person but is unwilling to put them at risk of prosecution, or is unwilling to break the law.
Or:
• Would be physically capable, but
• Can't afford to travel to a place where PAS is legal.
• And:
• Is unwilling to end their life in a way that disfigures their body (e.g. for consideration of the person who finds them, or their family, or religious reasons).
‹NS & typical-case denial of PAS› : IFR
These are the people who have a genuine self-centered desire for PAS and don't suffer greatly from not having the option of PAS (i.e. not in ‹NS & worst-case denial of PAS›), but whose quality of life is still negatively affected.
‹NS & best-case denial of PAS› : IFR
These are the (possibly empty) set of people who have a genuine self-centered desire for PAS but nonetheless benefit, overall, from not having the option of PAS.
Defn~ ‹NS & desire for PAS› : IFR - DisjointUnion₃(‹NS & desire for PAS›, ‹NS & worst-case denial of PAS›, ‹NS & typical-case denial of PAS›, ‹NS & best-case denial of PAS›) ∧ ‹NS & desire for PAS› ‹NS› - Person wanted PAS but didn't receive it (for any reason).
Defn ‹NS & no desire for PAS› : IFR := ‹NS› \ ‹NS & desire for PAS›

‹true, NS & worse palliative care› : Δ
A genuine worry for some opponents of PAS is that a PAS policy could lead to decreased funding for palliative care. There are two ways one can address this concern: (1) use data from jurisdictions that have PAS to argue that it hasn't happened there, and postulate that Canada will be the same. (2) take extra, active measures to defend against this happening. I have only touched on (2); see note about this in introduction (starts "Fifth, to justify the assumption...")
Defn ‹S, NS & worse palliative care› : Δ := ‹true, NS & worse palliative care› ‹S,NS›
Defn ‹NS, NS & worse palliative care› : Δ := ‹true, NS & worse palliative care› ‹NS,NS›
The person's death is not a suicide in the status-quo future or the assisted suicide future, and the quality of palliative care available to them is worse in the assisted suicide future compared to in the status-quo future.
Defn~ ‹S, NS because of incr fear of prosecution› : Δ - ‹S, NS because of incr fear of prosecution› ‹S,NS›
There is a logical possibility that a person will choose to end their life via illegal non-physician-assisted suicide if legal PAS is not an option for anyone, but will choose not to if legal PAS is an option for some people but not for them. If the difference is because they have an increased fear that whoever helps them to die will be prosecuted, then they would be worse off in the assisted-suicide future (with a new law passed) than they would be in the status-quo future. We will specify that any PAS law that this argument endorses does not lead to increased prosecution for illegal assisted suicide.
‹NS, NS because of incr fear of prosecution› : Δ
Definitional Axiom 5: ‹NS, NS because of incr fear of prosecution› ‹NS,NS›
Defn ‹true, NS because of incr fear of prosecution› : Δ := ‹NS, NS because of incr fear of prosecution› ‹S, NS because of incr fear of prosecution›
Definitional Axiom 6: Disjoint(‹NS, NS because of incr fear of prosecution›, ‹S, NS because of incr fear of prosecution›)
Defn ‹NS, NS & same-or-better palliative care› : Δ := ‹NS,NS› \ ‹NS, NS & worse palliative care›
Defn ‹S, NS & same-or-better palliative care & no incr fear of prosecution› : Δ := (‹S,NS› \ ‹S, NS because of incr fear of prosecution›) \ ‹S, NS & worse palliative care›
‹NS, NS & same-or-better palliative care & exacerbated guilt› : Δ
A genuine worry for some opponents of assisted suicide is that, with physician-assisted suicide available, we will see a decrease in the quality of life of people who are eligible for it but do not want it, due to, for example, feelings of being a burden on their family and friends. We do not try to design an assisted suicide system that prevents this; instead we acknowledge it and postulate that it is compensated for by the benefits of an assisted suicide system.
‹NS, NS & same-or-better palliative care & no exacerbated guilt› : Δ
Definitional Axiom 7: DisjointUnion(‹NS, NS & same-or-better palliative care›, ‹NS, NS & same-or-better palliative care & no exacerbated guilt›, ‹NS, NS & same-or-better palliative care & exacerbated guilt›)
Defn EasierCases : Δ := (‹true, NS & worse palliative care› ‹true, NS because of incr fear of prosecution›) (pairIFR(‹true›, ‹very bad PAS›) ‹S,S›)
Defn ‹NS, coerced suicide› : Δ := pairIFR(‹NS›, ‹coerced suicide›) \ EasierCases
Defn ‹coerced suicide, NS› : Δ := pairIFR(‹coerced suicide›, ‹NS›) \ EasierCases
Defn ‹NS, non-PA suicide & non-coerced› : Δ := pairIFR(‹NS›, ‹non-PA suicide› ‹non-coerced suicide›) \ EasierCases
Defn ‹non-PA suicide & non-coerced, NS› : Δ := pairIFR(‹non-PA suicide› ‹non-coerced suicide›, ‹NS›) \ EasierCases
Defn ‹NS, difficult-regrettable PAS› : Δ := pairIFR(‹NS›, ‹difficult-regrettable PAS›) \ EasierCases
Defn ‹NS & typical-case denial of PAS, non-regrettable PAS› : Δ := pairIFR(‹NS & typical-case denial of PAS›, ‹non-regrettable PAS›) \ EasierCases
Defn ‹NS & worst-case denial of PAS, non-regrettable PAS› : Δ := pairIFR(‹NS & worst-case denial of PAS›, ‹non-regrettable PAS›) \ EasierCases
Defn ‹S, NS & no incr fear of prosecution› : Δ := ‹S,NS› \ ‹S, NS because of incr fear of prosecution›
Defn ‹S, NS & worse palliative care & no incr fear of prosecution› : Δ := ‹S, NS & worse palliative care› ‹S, NS & no incr fear of prosecution›

Note that, at the current level of detail of this proof, the next two symbols are only used in the semantic descriptions of other symbols - not in any axioms.

𝒟 : Distr(◊FuturePairEC) - A finite, subjective Bayesian probability distribution over ◊FuturePairEC
Exp# : Distr(◊FuturePairEC) × Δ≥0
Exp#(D,δ) is the expected value of |peopleInΔ(δ,rep(E))| when ◊FuturePairEC E is chosen at random from D
Defn~ ‹favourable for status quo› : Δ → 𝔹 - δ. ‹favourable for status quo›(δ) ⇔ 0 Δ ΔsOf(peopleInΔ(δ, $\vec{F}_{\text{typical}}$), $\vec{F}_{\text{typical}}$)
‹favourable for status quo›(δ) means that δ(·, $\vec{F}_{\text{typical}}$) represents a negative change (or equivalently, δ(·, swap($\vec{F}_{\text{typical}}$)) represents a positive change). This is more easily conveyed by examples: ‹favourable for status quo›(‹NS, coerced suicide›) holds because if ‹NS, coerced suicide›(p, $\vec{F}_{\text{typical}}$) then clearly something gets better for p when moving from the assisted suicide future (the second of the pair) to the status quo future (or worse when moving in the opposite direction).
$\vec{F}_{\text{typical}}$ : ◊FuturePair
A particular future pair whose equivalence class is "typical", in a certain sense, with respect to 𝒟. At a high level, we assume
• Extremely unlikely (w.r.t. 𝒟) Δs don't happen to anyone in $\vec{F}_{\text{typical}}$.
• The count of people who δ happens to is roughly the expected value of the corresponding counting random variable of 𝒟. We round up for the Δs that are favourable for the status-quo (SQ) futures, and down for the Δs that are neutral or favourable for the assisted suicide futures.
More precisely, there is a constant ε:≥0, which is a parameter of this argument, such that:
• |peopleInΔ(δ,$\vec{F}_{\text{typical}}$)| = 0 for all δ such that Exp#(δ,𝒟) < ε.
• |peopleInΔ(δ,$\vec{F}_{\text{typical}}$)| = ceil(x) for all δ such that Exp#(δ,𝒟) = x ≥ ε and ‹favourable for status quo›(δ).
• |peopleInΔ(δ,$\vec{F}_{\text{typical}}$)| = floor(x) for all δ such that Exp#(δ,𝒟) = x ≥ ε and ¬‹favourable for status quo›(δ).
Defn~ ‹all people› : FinSet(People) - p. p ‹all people›

Assumption 1: ΔsOf(‹all people›, $\vec{F}_{\text{typical}}$) Δ 0‹should pass›

Goal: ‹should pass›
Defn~ peopleIn$_{\text{IFR}}^{1,*}$ : IFRFinSet(People) - φ. ∀p. p peopleIn$_{\text{IFR}}^{1,*}$(φ) ⇔ φ(p, $\vec{F}_{\text{typical}}$[1])
Defn~ peopleIn$_{\text{IFR}}^{2,*}$ : IFRFinSet(People) - φ. ∀p. p peopleIn$_{\text{IFR}}^{2,*}$(φ) ⇔ φ(p, $\vec{F}_{\text{typical}}$[2])
Defn ṗeopleInΔ : ΔFinSet(People) - δ. ṗeopleInΔ(δ) = peopleInΔ(δ, $\vec{F}_{\text{typical}}$)
Definitional Axiom 14: P₁,P₂,${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) 0ΔsOf(P₂, ${\vec{F}}$) 0ΔsOf(P₁ P₂, ${\vec{F}}$) 0
Definitional Axiom 15: P₁,P₂. ∀${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ 0ΔsOf(P₂, ${\vec{F}}$) Δ 0ΔsOf(P₁ P₂, ${\vec{F}}$) Δ 0
Definitional Axiom 16: P₁,P₂. ∀${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ 0ΔsOf(P₂, ${\vec{F}}$) Δ 0ΔsOf(P₁ P₂, ${\vec{F}}$) Δ 0
Definitional Axiom 17: P₁,P₂. ∀${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) ΔsOf(P₂, swap(${\vec{F}}$)) ⇒ ΔsOf(P₁ P₂, ${\vec{F}}$) 0
Definitional Axiom 18: P₁,P₂. ∀${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ ΔsOf(P₂, swap(${\vec{F}}$)) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ 0ΔsOf(P₁ P₂, ${\vec{F}}$) Δ 0
Definitional Axiom 19: P₁,P₂. ∀${\vec{F}}$. Disjoint(P₁, P₂) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ ΔsOf(P₂, swap(${\vec{F}}$)) ∧ ΔsOf(P₁, ${\vec{F}}$) Δ 0ΔsOf(P₁ P₂, ${\vec{F}}$) Δ 0
Assumption 2: For each δ in {pairIFR(‹true›, ‹PAS of wrong person›), ‹S, NS because of incr fear of prosecution›, pairIFR(‹true›, ‹PAS with wrong and substandard diagnosis›), ‹NS, NS & worse palliative care›}: ṗeopleInΔ(δ) =
The proposed safeguards for the implementation make these Δs so unlikely that they do not apply to anyone in $\vec{F}_{\text{typical}}$.
Assumption 3: For each δ in {‹S,S›, pairIFR(‹NS & no desire for PAS›, ‹non-regrettable PAS›), ‹NS, NS & same-or-better palliative care & no exacerbated guilt›, ‹S, NS & same-or-better palliative care & no incr fear of prosecution›}: ΔsOf(ṗeopleInΔ(δ), $\vec{F}_{\text{typical}}$) Δ 0
The quality of life for these people is not significantly different between the two futures. We make the superficially-weaker assumption that their quality of life is not worse in the assisted-suicide future than it is in the status quo future.
Assumption 4: ΔsOf(ṗeopleInΔ(‹NS, coerced suicide›), $\vec{F}_{\text{typical}}$) ΔsOf(ṗeopleInΔ(‹coerced suicide, NS›), swap($\vec{F}_{\text{typical}}$))
Let P₁ be the people whose death is not a suicide in SQF and whose death is a coerced suicide in ASF. Let P₂ be the people whose death is a coerced suicide in SQF and not a suicide in ASF. Note that P₁ and P₂ are disjoint. When it comes to comparing SQF and ASF, the cost for the people in P₁ of moving from SQF to ASF is approximately equal to the cost for the people in P₂ of moving from ASF to SQF. In a more-detailed version of this argument, this assumption would be derived (by a single axiom) from two simpler ones:
• The size of P₁ is approximately equal to the size of P₂. This requires that passing of PAS legislation eliminates as many coerced suicides as it introduces (P₂ are eliminated, P₁ are introduced).
• You believe coerced suicide in ASF and coerced suicide in SQF are equally-bad fates.
Assumption 5: ΔsOf(ṗeopleInΔ(‹NS & typical-case denial of PAS, non-regrettable PAS›), $\vec{F}_{\text{typical}}$) Δ ΔsOf(ṗeopleInΔ(‹NS, NS & same-or-better palliative care & exacerbated guilt›), swap($\vec{F}_{\text{typical}}$))
Let P₁ be the people who satisfy ‹NS & typical-case denial of PAS› in SQF and ‹non-regrettable PAS› in SQF. Let P₂ be the people whose death is not a suicide in SQF who, in ASF, still do not die by suicide, and have equally-good access to palliative care, but also are tormented with guilt for not choosing PAS (and there was no such guilt for them SQF, because PAS was illegal). When it comes to comparing SQF and ASF, the cost to the people in P₁ of moving from ASF to SQF is at least as great as the cost to the people in P₂ of moving from SQF to ASF. In a more-detailed version of this argument, this assumption would be derived (by a single axiom) from two simpler ones:
• For some fraction n/m ≥ 1 (say, n=10 and m=1), (n/m)|P₁| < |P₂|. That is, you grant that P₂ is larger than P₁, but you posit that it is no more than (n/m) times larger.
• You believe it is at least as bad to move m people who satisfy ‹NS & typical-case denial of PAS, non-regrettable PAS› from ASF to SQF as it is to move n people who satisfy ‹NS, NS & same-or-better palliative care & exacerbated guilt› from SQF to ASF.
Assumption 6: ΔsOf(ṗeopleInΔ(‹NS & worst-case denial of PAS, non-regrettable PAS›), $\vec{F}_{\text{typical}}$) Δ ΔsOf(ṗeopleInΔ(‹NS, difficult-regrettable PAS›), swap($\vec{F}_{\text{typical}}$))
This assumption is similar to Assumption 5 in form (except for using Δ instead of Δ), but it concerns more-severe kinds of changes. This assumption is often the main explicit disagreement between non-religious proponents of PAS and (self-reported) non-religious opponents of PAS. So please read the informal description of Assumption 5 first. Like Assumption 5, in a more-detailed version of this argument, this assumption would be derived (by a single axiom) from two simpler ones, which are of the form in Assumption 5 except that one might argue the fraction n/m is < 1 if the safeguards of the PAS system are very good.
Assertion 1: ΔsOf(ṗeopleInΔ(‹NS & typical-case denial of PAS, non-regrettable PAS›), $\vec{F}_{\text{typical}}$) Δ 0
From ‹NS & typical-case denial of PAS› to ‹non-regrettable PAS› is a good change. Some self-reported religious people, who are not in the intended audience of this argument, will reject this assumption.
Assertion 2: ΔsOf(ṗeopleInΔ(‹NS & worst-case denial of PAS, non-regrettable PAS›), $\vec{F}_{\text{typical}}$) Δ 0
From ‹NS & worst-case denial of PAS› to ‹non-regrettable PAS› is a good change. Some religious people, who are not in the intended audience of this argument, will reject this assumption.
Simplifying Assumption 1: peopleIn$_{\text{IFR}}^{1,*}$(‹NS & desire for PAS›) = peopleIn$_{\text{IFR}}^{1,*}$(‹NS & typical-case denial of PAS›) peopleIn$_{\text{IFR}}^{1,*}$(‹NS & worst-case denial of PAS›)
From the proposition accompanying the introduction of ‹NS & desire for PAS›, this is equivalent to the assumption that there are no instances of ‹NS & best-case denial of PAS› in SQF. This assumption is disputable. It would be better to include the hypothetical set of people who satisfy ‹NS & best-case denial of PAS› in Assumption 5 or Assumption 6, which would amount to a strengthening of those assumptions.
✓Lemma 70: ΔsOf(‹all people›, $\vec{F}_{\text{typical}}$) Δ 0
Defn People1-5 : FinSet(People) := (((People₁ People₂) People₃) People₄) People₅
✓Lemma 71: ‹all people› = People1-5
Lemma 4: ‹all people› ((ṗeopleInΔ(‹S,S›) ṗeopleInΔ(‹S,NS›)) ṗeopleInΔ(‹NS,S›)) ṗeopleInΔ(‹NS,NS›)
The four sets on the right hand side are a partition of ‹all people› since ‹NS› is the complement of ‹S›.
Lemma 5: ṗeopleInΔ(‹S,S›) People1-5
Follows easily from basic set reasoning, Claim 22, and the definition of People1-5.
Claim 22: ṗeopleInΔ(‹S,S›) People₂
Lemma 6: ṗeopleInΔ(‹S,NS›) People1-5
Follows easily from basic set reasoning, Claim 23, and the definition of People1-5.
Claim 23: ṗeopleInΔ(‹S,NS›) People₁ People₂
Claim 24: ṗeopleInΔ(‹NS,S›) People1-5
Lemma 7: ṗeopleInΔ(‹NS,NS›) People1-5
Follows easily from basic set reasoning, Claim 25, and the definition of People1-5.
Claim 25: ṗeopleInΔ(‹NS,NS›) (People₁ People₂) People₄
✓Lemma 72: People1-5 ‹all people›
✓Lemma 73: ‹all people› People1-5
✓Lemma 74: ΔsOf(People1-5, $\vec{F}_{\text{typical}}$) Δ 0
✓Lemma 75: ΔsOf(People₅, $\vec{F}_{\text{typical}}$) Δ 0
✓Lemma 76: ΔsOf(((People₁ People₂) People₃) People₄, $\vec{F}_{\text{typical}}$) Δ 0
✓Lemma 77: ΔsOf(People₄, $\vec{F}_{\text{typical}}$) Δ 0
Claim 26: Disjoint(ṗeopleInΔ(‹NS, NS & same-or-better palliative care & exacerbated guilt›), ṗeopleInΔ(‹NS & typical-case denial of PAS, non-regrettable PAS›))
✓Lemma 78: ΔsOf((People₁ People₂) People₃, $\vec{F}_{\text{typical}}$) 0