Home » Ethics » Formal Applications » Slaughtering Animals

Slaughtering Animals

The following is a formal demonstration that under some circumstances it is morally permissible to slaughter animals for food, leather, fur, etc.

Notation

  • Note: For notation not defined here see the rigorous theory of ethics.
  • Agents
    • a – an animal raised and then slaughtered
    • b – the farmer raising and slaughtering the animal
  • Times
    • t0 – the birth of the animal
    • ts – the slaughter of the animal
    • tn – the natural death of the animal in the wild
  •  Actions
    • CC = <a,C,t0,ts,b> – the act of raising the animal in captivity
    • SS = <a,S,ts,ts,b> – the act of slaughtering the animal and selling its parts
  • Other
    • $c – cost rate to the farmer while raising the animal in captivity
    • $S – total net benefit to the farmer from the slaughter

Situational Assumptions

  • Quantitative General
    1. t0 < ts < tn
    2. SB = {CC,SS}
    3. Eff({CC,SS} ) = {a,b}  – See the first bullet under Qualitative below
    4. ∀SC[ SC∈BAS & (CC∈SC || SS∈SC) ⇒ SC=SB ]
  • Quantitative BAS Requirements
    1. dNPWB( {a,b}, t0) † {CC} > 0  – Pertains to CC
    2. dNPWB( {a,b}, ts) † {SS} > 0  – Pertains to SS
    3. dNPWB(a,t0) † {CC, SS} > 0  – Pertains to a
    4. dNPWB(b,t0) † {CC, SS} > 0  – Pertains to b
  • Qualitative
    1. Only a & b are affected by CC or SS.  In reality, SS will affect anyone who uses the animal parts.  However, I will ignore these benefits to anyone other than the farmer, by assuming that the benefit to them ≈ price paid.  Thus, the farmer gets all the benefits from the price he receives.  This is not really true, but it simplifies things and does not affect the overall outcome.
    2. Treat captivity as a single action.  In reality, each action done during captivity is separate, but the affects of these accrue as time goes on, and they can be treated without any change in results as if they were a single action.
    3. Similarly, treat slaughter as a single action.  This is actually multiple actions, but none of them in themselves accrues enough of a benefit to form a BAS with CC.

Descriptions of Impacts

  • Specific Impacts
    1. dNPWB(a,t0) † CC  – Benefit to the animal from being in captivity
    2. -dNPWB(b,t0) † CC  – Cost to the farmer of caring for the animal
    3. -dNPWB(a,ts) † SS  – Cost to the animal of being slaughtered = the NPWB of the animal at the time of slaughter were the animal allowed to live out its life in the wild
    4. dNPWB(b,ts) † SS  – Benefit to the farmer from the animal parts
  • BAS Requirements
    1. dNPWB( {a,b}, t0 ) † CC > 0  – Benefit to the animal from being in captivity > Cost to the farmer of caring for the animal
    2. dNPWB( {a,b}, ts ) † SS > 0  –  Benefit to the farmer from the animal parts > Cost to the animal of being slaughtered
    3. dNPWB(a,t0) † CC + dNPWB(a,ts) † SS > 0  – Benefit to the animal from being in captivity > Cost to the animal of being slaughtered
    4. dNPWB(b,t0) † CC + dNPWB(b,ts) † SS > 0  – Benefit to the farmer from the animal parts > Cost to the farmer of caring for the animal

Proofs of Lemmas

  • (A) Proof that u0-min( {CC,SS} ) = t0
    1. {u0: ∃b∃A∃u1∃x1∃x2…∃xN[ <b,A,u0,u1,x1,x2…xN> ∈ {CC,SS} ]} = {t0, ts} — Def. of CC & Def. of SS
    2. t0 < ts — Quantitative General Assumption #1
    3. min( {t0, ts} ) = t0 — (2) & Def. of min()
    4. u0-min( {CC,SS} ) = t0 — (1), (3) & Def. of u0-min
    5. Q.E.D.
  • (B) Proof that ∀X[ X ∈ {CC,SS} ⇒ dNPWBT( Eff( {CC,SS} ), u0-min(X) ) † {X} > 0
    1. dNPWB( {a,b}, t0 ) † {CC} > 0  — Quantitative BAS Requirement #1
    2. dNPWB( Eff( {CC,SS} ), t0 ) † {CC} > 0  — (1) & Quantitative General #3
    3. dNPWB( Eff( {CC,SS} ), u0-min( {CC} ) ) †  {CC}  — (2), Def. of CC & Def. of u0-min
    4. dNPWB( {a,b}, t0 ) † {SS} > 0  — Quantitative BAS Requirements #2
    5. dNPWB( Eff( {CC,SS} ), t0 † {SS} > 0  — (4) & Quantitative General #3
    6. dNPWB( Eff( {CC,SS} ), u0-min(SS) † {SS} > 0  — (5), Def. of SS, & Def. of u0-min
    7. ∀X[ X ∈ {CC,SS} ⇒ dNPWBT( Eff( {CC,SS} ), u0-min(X) ) † {X} ]  > 0 — (3) & (6)
    8. Q.E.D.
  • (C) Proof that ∀d[ d∈Eff( {CC,SS} ) ⇒ dNPWB(d, u0-min( {CC,SS} )) † {CC,SS} > 0 ]
    1. dNPWB(a,t0) † {CC, SS} > 0 — Quantitative BAS Requirements Assumption #3
    2. dNPWB(a, u0-min( {CC,SS} )) † {CC,SS}  — (1) & Lemma (A)
    3. dNPWB(b,t0) † {CC, SS} > 0 — Quantitative BAS Requirements Assumption #4
    4. dNPWB(a, u0-min( {CC,SS} )) † {CC,SS}  — (3) & Lemma (A)
    5. ∀d[ d∈{a,b} ) ⇒ dNPWB(d, u0-min( {CC,SS} )) † {CC,SS} > 0  — (2) & (4)
    6. ∀d[ d∈Eff( {CC,SS} ) ⇒ dNPWB(d, u0-min( {CC,SS} )) † {CC,SS} > 0  — (5) & Quantitative General #3
    7. Q.E.D.
  • (D) Proof that SB∈BAS
    1. CC∈SB  — Quantitative General Assumption #2
    2. SS∈SB  — Quantitative General Assumption #2
    3. t0 < ts  — Quantitative General Assumption #1
    4. CC ≠ SS  — (3) & Definition of CC & SS
    5. ∃X∃Y[ X∈SB & Y∈SB & X≠Y ]  — (1),(2), & (4)
    6. ∀X[ X ∈ {CC,SS} ⇒ dNPWBT( Eff( {CC,SS} ), u0-min(X) ) † {X} > 0  — Lemma (B)
    7. ∀d[ d∈Eff( {CC,SS} ) ⇒ dNPWB(d, u0-min( {CC,SS} )) † {CC,SS} > 0 ]  — Lemma (C)
    8. SB∈SBAS  — (5), (6), (7), & Def. of SBAS
    9. {CC} ∉ SBAS  — Definition of SBAS (members must have at least 2 elements)
    10. {SS} ∉ SBAS  — Definition of SBAS
    11. ¬∃SA[ SA∈SBAS & SA⊂SB & SA≠{} ]  — (9), (10), & Def. of SB
    12. SB∈BAS  — (8), (11), & Def. of BAS
    13. Q.E.D.
  • (E) Proof that SB∈BASO(ts)
    1. SB∈BAS  — Lemma (D)
    2. SS∈SB  — Quantitative General Assumption #2
    3. SS∉Ex(SB,ts) — (2), Def. of SS, & Def. of Ex() — (i.e., because ts≥ts)
    4. ∃X[ X∈SB & X∉Ex(SB,ts) ]  — (2) & (3)
    5. ¬∀X[ X∈SB ⇒ X∈Ex(SB,ts) ]  — (4) & Logic
    6. SB∉BASC(ts)  — (5) & Def. of BASC
    7. SB∈BASO(ts)  — Lemma D, (6) & Def. of BASO
    8. Q.E.D.
  • (F) Proof that ∀X{ X∈SB ⇒ ¬∃SC[ X∈SC & SC∈BASC(ts) ] }
    1. ∀SC[ SC∈BAS & (CC∈SC † SS∈SC) ⇒ SC=SB ]  — Quantitative General Assumption #4
    2. ¬∃SC[ (SC∈BAS & (CC∈SC † SS∈SC) & SC≠SB ] — (1) & Logical
    3. X=CC † X=SS  — Assumption
    4. ¬∃SC[ SC∈BAS & X∈SC & SC≠SB ]  — (2) & (3)
    5. ¬∃SC[ SC∈BASC(ts) & X∈SC & SC≠SB ] — (4) & Def. of BASC
    6. SB∈BASO(ts)  — Lemma (E)
    7. ∀SC[ SC=SB ⇒ SC∈BASO(ts) ]  — (6) & Logic
    8. ∀SC[ SC=SB ⇒ SC∉BASC(ts) ]  — (7) & Def. of BASO
    9.  ¬∃SC[ SC∈BASC(ts) & SC=SB ]   — (8) & Logic
    10. ¬∃SC[ SC∈BASC(ts) & X∈SC & & SC=SB ]   — (9) & Logic
    11. ¬∃SC[ SC∈BASC(ts) & X∈SC ]  — (5) & (10)
    12. ∀X{ (X=CC || X=SS) ⇒ ¬∃SC[ SC∈ & SC∈BASC(ts) ] }  — (3) & (11)
    13. ∀X[ X∈SB ⇔ (X=CC || X=SS) ]   — Quantitative General Assumption #2
    14. ∀X{ X∈SB ⇒ ¬∃SC[ SC∈ & SC∈BASC(ts) ] }  — (12) & (13)
    15. Q.E.D.

Proof that SS ∈ MRLprm(b,ts)

  1. SB ∈ BASO(ts)  — Lemma (E)
  2. ∀X{ X∈SB ⇒ ¬∃SC[ X∈SC & SC∈BASC(ts) ] }  — Lemma (F)
  3. SB ∈ BASA(ts)  — (1), (2), & Def. BASA
  4. SS ∈ SB  — Quantitative General Assumption #2
  5. ∃SB[ SS∈SB & SB∈BASA(ts) ]   — (3) & (4)
  6. SS ∉ ActP(b,ts)  — (5) & Def. of ActP
  7. SS ∈ MRLprm(b,ts)  — (6) & Def. of MRLprm
  8. Q.E.D.

November, 2013


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: