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
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. (actually, they didn't argue this for the fourth one, «no regrettable legal assisted suicide for S.R.»; I include it because in most arguments about assisted suicide, where a policy is being considered as opposed to permission for one person, it is the concern that is given the most attention). 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.
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.