Theory Utilitarismus
theory Utilitarismus
imports Handlung "HOL-Library.Extended_Real" Maxime
begin
section‹Utilitarismus›
text‹
Wir betrachten hier primär einen einfachen Handlungsutilitarismus.
Frei nach Jeremy Bentham. Sehr frei. Also sehr viel persönliche Auslegung.
Eine Handlung ist genau dann moralisch richtig,
wenn sie den aggregierten Gesamtnutzen,
d.h. die Summe des Wohlergehens aller Betroffenen, maximiert wird.›
type_synonym 'welt glueck_messen = ‹'welt handlung ⇒ ereal›
text‹Wir messen Glück im Typen \<^typ>‹ereal›, also reelle Zahlen mit \<^term>‹∞::ereal›
und \<^term>‹-∞::ereal›, so dass auch "den höchsten Preis zahlen" modelliert werden kann.›
lemma ‹(λh::ereal handlung. case h of Handlung vor nach ⇒ nach - vor) (Handlung 3 5) = 2›
by simp
lemma ‹(λh::ereal handlung. case h of Handlung vor nach ⇒ nach - vor) (Handlung 3 ∞) = ∞›
by simp
lemma ‹(λh::ereal handlung. case h of Handlung vor nach ⇒ nach - vor) (Handlung 3 (-∞)) = -∞›
by simp
text‹Eine Handlung ist genau dann moralisch richtig,
wenn die Gesamtbilanz einen positiven Nutzen aufweist.›
definition moralisch_richtig :: ‹'welt glueck_messen ⇒ 'welt handlung ⇒ bool› where
‹moralisch_richtig glueck_messen handlung ≡ (glueck_messen handlung) ≥ 0›
subsection‹Goldene Regel und Utilitarismus im Einklang \label{sec:golregelutilkonsistent}›
text‹
In \S\ref{sec:gesinnungsverantwortungsethik} haben wir
Gesinnungsethik und Verantwortungsethik definiert.
In diesem kleinen Intermezzo werden wir zeigen, wie sich die Gesinnungsethik der goldenen Regel
in die Verantwortungsethik des Utilitarismus übersetzen lässt.
›
text‹Wir modellieren die goldene Regel als Gesinnungsethik.›
definition goldene_regel_als_gesinnungsethik
:: ‹('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ bool›
where
‹goldene_regel_als_gesinnungsethik maxime handlungsabsicht ≡
∀welt. moralisch welt maxime handlungsabsicht›
definition utilitarismus_als_verantwortungsethik
:: ‹'welt glueck_messen ⇒ 'welt handlung ⇒ bool›
where
‹utilitarismus_als_verantwortungsethik glueck_messen handlung ≡
moralisch_richtig glueck_messen handlung›
text‹
Eine Maxime ist immer aus Sicht einer bestimmten Person definiert.
Wir "neutralisieren" eine Maxime indem wir diese bestimmte Person entfernen
und die Maxime so allgemeingültiger machen.
Alle Personen müssen gleich behandelt werden.
Um die Maxime unabhängig von einer bestimmten Person zu machen,
fordern wir einfach, dass die Maxime für aller Personen erfüllt sein muss.›
fun maximeNeutralisieren :: ‹('person, 'welt) maxime ⇒ ('welt handlung ⇒ bool)› where
‹maximeNeutralisieren (Maxime m) = (λwelt. ∀p::'person. m p welt)›
text‹
Nun übersetzen wir eine Maxime in die \<^typ>‹'welt glueck_messen› Funktion des Utilitarismus.
Der Trick: eine verletzte Maxime wird als unendliches Leid übersetzt.›
definition maxime_als_nutzenkalkuel
:: ‹('person, 'welt) maxime ⇒ 'welt glueck_messen›
where
‹maxime_als_nutzenkalkuel maxime ≡
(λwelt. case (maximeNeutralisieren maxime) welt
of True ⇒ 1
| False ⇒ - ∞)›
lemma ereal_zero_geq_case:
‹((0::ereal) ≤ (case (∀p. f p) of True ⇒ 1 | False ⇒ - ∞)) ⟷ (∀p. f p)›
by (simp add: bool.split_sel)
text‹Für diese Übersetzung können wir beweisen,
dass die Gesinnungsethik der goldenen Regel und die utilitaristische Verantwortungsethik
konsistent sind:›
theorem ‹gesinnungsethik_verantwortungsethik_konsistent
(goldene_regel_als_gesinnungsethik maxime)
(utilitarismus_als_verantwortungsethik (maxime_als_nutzenkalkuel maxime))›
apply(cases ‹maxime›, rename_tac m, simp)
apply(simp add: gesinnungsethik_verantwortungsethik_konsistent_def
goldene_regel_als_gesinnungsethik_def utilitarismus_als_verantwortungsethik_def
moralisch_richtig_def maxime_als_nutzenkalkuel_def)
apply(intro allI)
apply(case_tac ‹handlungsabsicht›, rename_tac h, simp)
apply(simp add: moralisch_simp)
apply(simp add: ereal_zero_geq_case)
by blast
text‹Diese Konsistenz gilt nicht im allgemeinen,
sondern nur wenn Glück gemessen wird mit Hilfe der \<^const>‹maxime_als_nutzenkalkuel› Funktion.
Der Trick dabei ist nicht, dass wir einer verletzten Maxime \<^term>‹-∞::ereal› Nutzen zuordnen,
sondern der Trick besteht in \<^const>‹maximeNeutralisieren›, welche nicht erlaubt Glück
aufzuaddieren und mit Leid zu verrechnen, sondern dank des Allquantors dafür sorgt,
dass auch nur das kleinste Leid dazu führt, dass sofort \<^const>‹False› zurückgegebn wird.
Aber auch wenn wir ordentlich aufsummieren, jedoch einer verletzten Maxime \<^term>‹-∞::ereal›
Nutzen zuordnen und zusätzlich annehmen, dass die Bevölkerung endlich ist,
dann funktioniert das auch:
›
fun maxime_als_summe_wohlergehen
:: ‹('person, 'welt) maxime ⇒ 'welt glueck_messen›
where
‹maxime_als_summe_wohlergehen (Maxime m) =
(λwelt. ∑p∈bevoelkerung. (case m p welt
of True ⇒ 1
| False ⇒ - ∞))›
lemma sum_wohlergehen_simp:
‹(∑p∈B. case f p of True ⇒ 1 | False ⇒ - ∞) = (∑p∈B. if f p then 1 else - ∞)›
by (simp add: case_bool_if)
lemma ‹(∑p∈B. if f p then 1 else - ∞) < (∞::ereal)›
by (simp add: sum_Pinfty)
lemma helper_finite_wohlergehen_sum_cases:
‹finite B ⟹
(∑p∈B. if f p then 1 else - ∞) = (- ∞::ereal)
∨
((0::ereal) ≤ (∑p∈B. if f p then 1 else - ∞))›
apply(induction rule: finite.induct)
apply(simp; fail)
apply(simp add: sum.insert_if)
apply(intro allI impI conjI)
apply(elim disjE)
apply(simp)
apply(simp)
done
lemma helper_wohlergehen_sum_IH:
‹finite B ⟹ (0::ereal) ≤ (∑p∈insert b B. if f p then 1 else - ∞)
⟹ (0::ereal) ≤ (∑p∈B. if f p then 1 else - ∞)›
apply(frule helper_finite_wohlergehen_sum_cases[of _ ‹f›])
apply(elim disjE)
apply(simp add: sum.insert_if)
apply(case_tac ‹b ∈ B›)
apply(simp; fail)
apply(simp)
apply (metis (full_types) ereal_plus_1(3) not_MInfty_nonneg plus_ereal.simps(6))
apply (simp)
done
lemma helper_wohlergehen_sum_minfty:
‹(∑p∈B. if f p then 1 else - ∞) = (-∞::ereal) ⟹ ∃x∈B. ¬ f x›
by (metis (mono_tags, lifting) not_MInfty_nonneg sum_nonneg zero_less_one_ereal)
lemma helper_wohlergehen_sum_pos:
‹finite B ⟹ (0::ereal) ≤ (∑p∈B. if f p then 1 else - ∞) ⟹ ∀p∈B. f p›
apply(induction ‹B› rule: finite.induct)
apply(simp; fail)
apply(frule(1) helper_wohlergehen_sum_IH)
apply(simp)
apply(simp add: sum.insert_if)
apply(case_tac ‹a ∈ A›)
apply(simp; fail)
apply(simp)
apply(case_tac ‹f a›)
apply(simp; fail)
apply(simp)
by (metis MInfty_neq_PInfty(2) ereal_plus_eq_MInfty ereal_times(1) not_MInfty_nonneg sum_Pinfty)
lemma helper_wohlergehen_sum_iff:
‹finite B ⟹ (0::ereal) ≤ (∑p∈B. if f p then 1 else - ∞) ⟷ (∀p∈B. f p)›
apply(frule helper_finite_wohlergehen_sum_cases[of _ ‹f›])
apply(elim disjE)
apply(simp add: helper_wohlergehen_sum_minfty; fail)
apply(simp)
using helper_wohlergehen_sum_pos by blast
lemma helper_wohlergehen_sum_cases_iff:
‹finite (bevoelkerung::'person set) ⟹
(0::ereal) ≤ (∑p∈(bevoelkerung::'person set). case f p of True ⇒ 1 | False ⇒ - ∞)
⟷ (∀p∈bevoelkerung. f p)›
using helper_wohlergehen_sum_iff sum_wohlergehen_simp by metis
theorem
fixes maxime :: ‹('person, 'welt) maxime›
assumes ‹finite (bevoelkerung:: 'person set)›
shows
‹gesinnungsethik_verantwortungsethik_konsistent
(goldene_regel_als_gesinnungsethik maxime)
(utilitarismus_als_verantwortungsethik (maxime_als_summe_wohlergehen maxime))›
apply(cases ‹maxime›, rename_tac m, simp)
apply(simp add: gesinnungsethik_verantwortungsethik_konsistent_def
goldene_regel_als_gesinnungsethik_def utilitarismus_als_verantwortungsethik_def
moralisch_richtig_def)
apply(intro allI)
apply(case_tac ‹handlungsabsicht›, rename_tac h, simp)
apply(simp add: moralisch_simp)
apply(subst helper_wohlergehen_sum_cases_iff[OF ‹finite bevoelkerung›])
apply(auto simp add: bevoelkerung_def)
done
text‹
"Wie zu erwarten, will Kant nichts vom Utilitarismus oder sonstigen Lehren wissen,
die der Moral einen außerhalb ihrer selbst liegenden Zweck zuschreiben" @{cite russellphi}.
Die eben bewiesene Konsitenz von Gesinnungsethik und Verantwortungsethik zeigt,
das unsere Grunddefinitionen bereits eine Formalisierung des Kategorischen Imperativs
komplett im strengen Sinne Kants ausschließen.
Dennoch finde ich unsere Interpretation bis jetzt nicht abwegig.
Der große Trick besteht darin, dass wir eine \<^typ>‹('person, 'welt) handlungsabsicht›
sehr einfach in eine \<^typ>‹'welt handlung› in unserem theoretischen Modell überführen können.
Die widerspricht Kants Grundannahme, dass die Folgen einer Handlungsabsicht unvorhersehbar sind.
›
end