Theory BeispielZahlenwelt
theory BeispielZahlenwelt
imports Zahlenwelt BeispielPerson KategorischerImperativ
begin
section‹Beispiel: Zahlenwelt\label{sec:bspzahlenwelt}›
text‹In diesem Abschnitt werden wir ein Beispiel sehen.›
text‹Wir nehmen an, die Welt lässt sich durch eine Zahl darstellen,
die den Besitz einer Person modelliert.
Der Besitz ist als ganze Zahl \<^typ>‹int› modelliert und kann auch beliebig negativ werden.›
datatype zahlenwelt = Zahlenwelt
‹person ⇒ int ›
definition ‹show_zahlenwelt w ≡ case w of Zahlenwelt besitz ⇒ show_num_fun besitz›
fun gesamtbesitz :: ‹zahlenwelt ⇒ int› where
‹gesamtbesitz (Zahlenwelt besitz) = aufsummieren besitz›
text‹Beispiel:›
beispiel ‹gesamtbesitz (Zahlenwelt (€(Alice := 4, Carol := 8))) = 12› by eval
beispiel ‹gesamtbesitz (Zahlenwelt (€(Alice := 4, Carol := 4))) = 8› by eval
text‹Mein persönlicher Besitz:›
fun meins :: ‹person ⇒ zahlenwelt ⇒ int› where
‹meins p (Zahlenwelt besitz) = besitz p›
text‹Beispiel:›
beispiel ‹meins Carol (Zahlenwelt (€(Alice := 8, Carol := 4))) = 4› by eval
text‹Um den 🗏‹SchleierNichtwissen.thy› zu implementieren:›
fun zahlenwps :: ‹person ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt› where
‹zahlenwps p1 p2 (Zahlenwelt besitz) = Zahlenwelt (swap p1 p2 besitz)›
text‹Beispiel:›
beispiel ‹zahlenwps Alice Carol (Zahlenwelt (€(Alice := 4, Bob := 6, Carol := 8)))
= (Zahlenwelt (€(Alice := 8, Bob := 6, Carol := 4)))›
by eval
lemma zahlenwps_sym:
‹zahlenwps p1 p2 welt = zahlenwps p2 p1 welt›
by(cases ‹welt›, simp add: swap_symmetric)
lemma zahlenwps_id: ‹zahlenwps p p w = w›
by(cases ‹w›, simp)
lemma zahlenwps_twice:
‹zahlenwps p1 p2 (zahlenwps p1 p2 welt) = welt›
‹zahlenwps p1 p2 (zahlenwps p2 p1 welt) = welt›
by(cases ‹welt›, simp)+
lemma gesamtbesitz_swap:
‹gesamtbesitz (zahlenwps p1 p2 welt) = gesamtbesitz welt›
by(cases ‹welt›, simp add: aufsummieren_swap)
lemma hlp1: ‹meins p1 (zahlenwps p1 p2 welt) = meins p2 welt›
by(cases ‹welt›, simp add: swap_def)
lemma hlp2: ‹meins p2 (zahlenwps p1 p2 welt) = meins p1 welt›
by(cases ‹welt›, simp add: swap_def)
lemma hlp3: ‹p1 ≠ p2 ⟹ p ≠ p1 ⟹ p ≠ p2 ⟹
meins p (zahlenwps p1 p2 welt) = meins p welt›
by(cases ‹welt›, simp add: swap_def)
text‹\<^const>‹Alice› hat Besitz, \<^const>‹Bob› ist reicher, \<^const>‹Carol› hat Schulden.›
definition ‹initialwelt ≡ Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3))›
subsection‹Ungültige Handlung›
text‹Sobald ich eine konkrete Person in einer Handlungsabsicht hardcode,
ist diese nicht mehr wohlgeformt.›
beispiel ‹¬wohlgeformte_handlungsabsicht
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
(Handlungsabsicht (λich w. if ich = Alice then Some w else Some (Zahlenwelt (λ_. 0))))›
apply(simp add: wohlgeformte_handlungsabsicht.simps swap_def)
apply(eval)
done
subsection‹Nicht-Wohlgeformte Handlungen›
fun stehlen_nichtwf :: ‹int ⇒ person ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹stehlen_nichtwf beute opfer dieb (Zahlenwelt besitz) =
Some (Zahlenwelt ⟦⟦besitz(opfer -= beute)⟧(dieb += beute)⟧)›
text‹Die Handlung \<^const>‹stehlen› diskriminiert und ist damit nicht wohlgeformt:›
lemma ‹wohlgeformte_handlungsabsicht_gegenbeispiel zahlenwps
(Zahlenwelt (λx. 0)) (Handlungsabsicht (stehlen_nichtwf 5 Bob))
Alice Bob›
by(eval)
text‹Wir versuchen, das Opfer nach Besitz auszuwählen, nicht nach Namen.
Nach unserer Definition ist der Besitz ein Merkmal, nach dem man diskriminieren darf.
Man darf nur nicht nach Eigenschaften der \<^typ>‹person› diskriminieren, sondern nur
nach Eigenschaften der \<^typ>‹zahlenwelt›.›
fun opfer_nach_besitz_auswaehlen :: ‹int ⇒ ('person ⇒ int) ⇒ 'person list ⇒ 'person option› where
‹opfer_nach_besitz_auswaehlen _ _ [] = None›
| ‹opfer_nach_besitz_auswaehlen b besitz (p#ps) =
(if besitz p = b then Some p else opfer_nach_besitz_auswaehlen b besitz ps)›
fun stehlen_nichtwf2 :: ‹int ⇒ int ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹stehlen_nichtwf2 beute opfer_nach_besitz dieb (Zahlenwelt besitz) =
(case opfer_nach_besitz_auswaehlen opfer_nach_besitz besitz Enum.enum
of None ⇒ None
| Some opfer ⇒ Some (Zahlenwelt ⟦⟦besitz(opfer -= beute)⟧(dieb += beute)⟧)
)›
text‹Leider ist diese Funktion auch diskriminierend:
Wenn es mehrere potenzielle Opfer mit dem gleichen Besitz gibt,
dann bestimmt die Reihenfolge in \<^term>‹Enum.enum› wer bestohlen wird.
Diese Reihenfolge ist wieder eine Eigenschaft von \<^typ>‹person› und nicht \<^typ>‹zahlenwelt›.›
beispiel‹handeln Alice (Zahlenwelt (€(Alice := 10, Bob := 10, Carol := -3)))
(Handlungsabsicht (stehlen_nichtwf2 5 10))
= Handlung (Zahlenwelt (€(Alice := 10, Bob := 10, Carol := - 3)))
(Zahlenwelt (€(Alice := 10, Bob := 10, Carol := - 3)))› by eval
beispiel‹handeln Bob (Zahlenwelt (€(Alice := 10, Bob := 10, Carol := -3)))
(Handlungsabsicht (stehlen_nichtwf2 5 10))
= Handlung (Zahlenwelt (€(Alice := 10, Bob := 10, Carol := - 3)))
(Zahlenwelt (€(Alice := 5, Bob := 15, Carol := - 3)))› by eval
beispiel ‹wohlgeformte_handlungsabsicht_gegenbeispiel
zahlenwps
(Zahlenwelt (€(Alice := 10, Bob := 10, Carol := -3))) (Handlungsabsicht (stehlen_nichtwf2 5 10))
Alice Bob›
by eval
fun schenken :: ‹int ⇒ person ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹schenken betrag empfaenger schenker (Zahlenwelt besitz) =
Some (Zahlenwelt ⟦⟦besitz(schenker -= betrag)⟧(empfaenger += betrag)⟧)›
text‹Da wir ganze Zahlen verwenden und der Besitz auch beliebig negativ werden kann,
ist Stehlen äquivalent dazu einen negativen Betrag zu verschenken:›
lemma stehlen_ist_schenken: ‹stehlen_nichtwf i = schenken (-i)›
apply(simp add: fun_eq_iff)
apply(intro allI, rename_tac p1 p2 welt, case_tac ‹welt›)
by auto
text‹Das Modell ist nicht ganz perfekt, .... Aber passt schon um damit zu spielen.›
subsection‹Wohlgeformte Handlungen›
text‹Die folgende Handlung erschafft neuen Besitz aus dem Nichts:›
fun erschaffen :: ‹nat ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹erschaffen i p (Zahlenwelt besitz) = Some (Zahlenwelt ⟦besitz(p += int i)⟧)›
lemma wohlgeformte_handlungsabsicht_erschaffen:
‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht (erschaffen n))›
apply(case_tac ‹welt›, simp add: wohlgeformte_handlungsabsicht.simps)
apply(simp add: swap_def Fun.swap_def)
done
text‹Wenn wir das Opfer eindeutig auswählen, ist die Handlungsabsicht "Stehlen" wohlgeformt.
Allerdings wird niemand bestohlen, wenn das Opfer nicht eindeutig ist.›
fun stehlen :: ‹int ⇒ int ⇒ person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹stehlen beute opfer_nach_besitz dieb (Zahlenwelt besitz) =
map_option Zahlenwelt (Zahlenwelt.stehlen beute opfer_nach_besitz dieb besitz)›
lemma wohlgeformte_handlungsabsicht_stehlen:
‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht (stehlen n p))›
apply(cases ‹welt›)
apply(rule wfh_generalize_world_ConstrI[OF wohlgeformte_handlungsabsicht_stehlen, where C=‹Zahlenwelt›])
by(auto)
text‹Reset versetzt die Welt wieder in den Ausgangszustand. Eine sehr destruktive Handlung.›
fun reset :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹reset ich (Zahlenwelt besitz) = Some (Zahlenwelt (λ _. 0))›
text‹Der \<^const>‹reset› ist im moralischen Sinne vermutlich keine gute Handlung,
dennoch ist es eine wohlgeformte Handlung, welche wir betrachten können:›
lemma wohlgeformte_handlungsabsicht_reset:
‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht reset)›
apply(simp add: wohlgeformte_handlungsabsicht.simps handeln_def nachher_handeln.simps)
by(case_tac ‹welt›, simp add: swap_def fun_eq_iff)
fun alles_kaputt_machen :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹alles_kaputt_machen ich (Zahlenwelt besitz) = Some (Zahlenwelt (λ _. Min (besitz ` UNIV) - 1))›
lemma alles_kaputt_machen_code[code]:
‹alles_kaputt_machen ich welt =
(case welt of Zahlenwelt besitz ⇒ Some (Zahlenwelt (λ_. min_list (map besitz enum_class.enum) -1)))›
apply(cases ‹welt›, simp add: alles_kaputt_machen_code_help)
done
lemma wohlgeformte_handlungsabsicht_alles_kaputt_machen:
‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht alles_kaputt_machen)›
apply(simp add: wohlgeformte_handlungsabsicht.simps)
apply(simp add: alles_kaputt_machen_code)
apply(case_tac ‹welt›, simp add: fun_eq_iff)
apply(simp add: min_list_swap_int_enum)
by (simp add: swap_def)
beispiel ‹alles_kaputt_machen Alice (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
= Some (Zahlenwelt (€(Alice := -4, Bob := -4, Carol := -4, Eve := -4)))›
by(code_simp)
text‹Auch die unmögliche (niemals ausführbare) Handlung lässt sich modellieren.›
fun unmoeglich :: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹unmoeglich _ _ = None›
text‹Die Beispielhandlungsabsichten, die wir betrachten wollen.›
definition ‹handlungsabsichten ≡ [
Handlungsabsicht (erschaffen 5),
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht reset,
Handlungsabsicht alles_kaputt_machen,
Handlungsabsicht unmoeglich
]›
lemma wfh_handlungsabsichten:
‹ha ∈ set handlungsabsichten ⟹ wohlgeformte_handlungsabsicht zahlenwps welt ha›
apply(simp add: handlungsabsichten_def)
apply(safe)
apply(simp_all add: wohlgeformte_handlungsabsicht_stehlen
wohlgeformte_handlungsabsicht_alles_kaputt_machen
wohlgeformte_handlungsabsicht_erschaffen
wohlgeformte_handlungsabsicht_reset)
apply(simp add: wohlgeformte_handlungsabsicht.simps)
done
subsection‹Maxime für individuellen Fortschritt›
text‹Wir definieren eine Maxime die besagt,
dass sich der Besitz einer Person nicht verringern darf:›
fun individueller_fortschritt :: ‹person ⇒ zahlenwelt handlung ⇒ bool› where
‹individueller_fortschritt p (Handlung vor nach) ⟷ (meins p vor) ≤ (meins p nach)›
definition maxime_zahlenfortschritt :: ‹(person, zahlenwelt) maxime› where
‹maxime_zahlenfortschritt ≡ Maxime (λich. individueller_fortschritt ich)›
lemma mhg_maxime_zahlenfortschritt_stehlen:
‹maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_zahlenfortschritt (Handlungsabsicht (stehlen 5 10)) p›
apply(simp add: maxime_und_handlungsabsicht_generalisieren_def
maxime_zahlenfortschritt_def, intro allI impI)
apply(case_tac ‹welt›, simp)
apply(simp add: Zahlenwelt.stehlen.simps handeln_def nachher_handeln.simps
opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem_enumall)
apply(auto intro: the_single_elem_exhaust)
done
text‹Die Eigenschaft \<^const>‹maxime_und_handlungsabsicht_generalisieren› wird von den meisten
Handlungsabsichten erfüllt.
Jedoch nicht von \<^const>‹reset›.
Das nicht-wohlgeformte \<^const>‹stehlen_nichtwf› erfüllt sie allerdings schon.›
lemma ‹ha ∈ {
Handlungsabsicht (erschaffen 5),
Handlungsabsicht (stehlen_nichtwf 5 Bob),
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht alles_kaputt_machen,
Handlungsabsicht unmoeglich
} ⟹ maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_zahlenfortschritt ha p›
apply(simp)
apply(safe)
apply(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def; fail)
apply(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def; fail)
subgoal using mhg_maxime_zahlenfortschritt_stehlen by simp
subgoal
by(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def, auto)
apply(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def; fail)
done
text‹Nicht alle Handlungen generalisieren, z.B. \<^const>‹reset› nicht:›
beispiel
‹¬ maxime_und_handlungsabsicht_generalisieren
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
maxime_zahlenfortschritt (Handlungsabsicht reset) Alice›
by eval
text‹Die \<^const>‹maxime_zahlenfortschritt› erfüllt allgemein ❙‹nicht›
den \<^const>‹kategorischer_imperativ›,
da \<^const>‹Alice› nach der Maxime z.B. \<^const>‹Bob› bestehlen dürfte.›
beispiel ‹kategorischer_imperativ_gegenbeispiel
zahlenwps initialwelt maxime_zahlenfortschritt
(Handlungsabsicht (stehlen 1 10))
Alice
Bob
Alice›
apply(simp add: kategorischer_imperativ_gegenbeispiel_def
wohlgeformte_handlungsabsicht_stehlen mhg_maxime_zahlenfortschritt_stehlen)
by(eval)
lemma ‹wpsm_kommutiert (maxime_zahlenfortschritt) zahlenwps welt›
by(simp add: maxime_zahlenfortschritt_def handeln_def
nachher_handeln.simps wpsm_kommutiert_def hlp1 hlp2 zahlenwps_sym)
text‹Folgendes Beispiel zeigt, dass die \<^const>‹maxime_zahlenfortschritt› den
kategorischen Imperativ auf unseren \<^const>‹handlungsabsichten› nicht erfüllt
(zu sehen an dem \<^const>‹False› im \<^const>‹bsp_erfuellte_maxime›.).
Die Handlungsabsichten \<^const>‹stehlen› als auch \<^const>‹reset› sind nicht mit der Maxime vereinbar.
Für die übrigen Handlungsabsichten ist das Ergebnis aber intuitiv:
▪ \<^const>‹erschaffen› ist erlaubt.
▪ da \<^const>‹unmoeglich› im Nichtstuen endet, ist dies auch erlaubt.
▪ \<^const>‹alles_kaputt_machen› ist verboten.
›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
handlungsabsichten
maxime_zahlenfortschritt =
Some
⦇
bsp_erfuellte_maxime = False,
bsp_erlaubte_handlungen = [
Handlungsabsicht (erschaffen 5),
Handlungsabsicht unmoeglich],
bsp_verbotene_handlungen = [Handlungsabsicht alles_kaputt_machen],
bsp_uneindeutige_handlungen = [
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht reset]⦈›
by beispiel_tac
subsubsection‹Einzelbeispiele›
text‹In jeder Welt ist die \<^term>‹Handlungsabsicht (erschaffen n)› \<^const>‹moralisch›:›
lemma ‹moralisch welt maxime_zahlenfortschritt (Handlungsabsicht (erschaffen n))›
apply(cases ‹welt›)
by(simp add: maxime_zahlenfortschritt_def moralisch_simp handeln_def nachher_handeln.simps)
text‹In kein Welt ist Stehlen \<^const>‹moralisch›:›
lemma ‹¬ moralisch welt maxime_zahlenfortschritt (Handlungsabsicht (stehlen_nichtwf 5 Bob))›
by(cases ‹welt›, auto simp add: maxime_zahlenfortschritt_def moralisch_simp handeln_def nachher_handeln.simps)
text‹In unserer \<^const>‹initialwelt› in der \<^const>‹Bob› als Opfer anhand seines Besitzes
als Opfer eines Diebstahls ausgewählt würde, ist stehlen dennoch nicht \<^const>‹moralisch›,
obwohl die Handlungsabsicht wohlgeformt ist:›
lemma ‹¬ moralisch initialwelt maxime_zahlenfortschritt (Handlungsabsicht (stehlen 5 10))›
by(eval)
text‹Da Schenken und Stehlen in dieser Welt equivalent ist, ist Schenken auch unmoralisch:›
lemma ‹¬ moralisch welt maxime_zahlenfortschritt (Handlungsabsicht (schenken 5 Bob))›
by(cases ‹welt›, auto simp add: maxime_zahlenfortschritt_def moralisch_simp handeln_def nachher_handeln.simps)
subsection‹Maxime für allgemeinen Fortschritt›
text‹Wir können die vorherige Maxime generalisieren, indem wir \<^const>‹individueller_fortschritt›
für jeden fordern.
Effektiv wird dabei das \<^term>‹ich::person› ignoriert.›
definition maxime_altruistischer_fortschritt :: ‹(person, zahlenwelt) maxime› where
‹maxime_altruistischer_fortschritt ≡ Maxime (λich h. ∀pX. individueller_fortschritt pX h)›
text‹Folgendes Beispiel zeigt, dass die \<^const>‹maxime_altruistischer_fortschritt›
den kategorischen Imperativ (für diese \<^const>‹initialwelt› und \<^const>‹handlungsabsichten›)
erfüllt; zu sehen an dem \<^const>‹True› im \<^const>‹bsp_erfuellte_maxime›.
Die Handlungsabsichten werden eingeordnet wie erwartet:
▪ \<^const>‹erschaffen› ist gut, \<^const>‹unmoeglich› (bedeutet: Nichtstun) ist auch okay.
▪ \<^const>‹stehlen›, \<^const>‹reset›, \<^const>‹alles_kaputt_machen› ist schlecht.
›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
handlungsabsichten
maxime_altruistischer_fortschritt =
Some
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = [
Handlungsabsicht (erschaffen 5),
Handlungsabsicht unmoeglich],
bsp_verbotene_handlungen = [
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht reset,
Handlungsabsicht alles_kaputt_machen],
bsp_uneindeutige_handlungen = []⦈›
by beispiel_tac
text‹Das ist ein sehr schönes Beispiel.›
lemma wpsm_kommutiert_altruistischer_fortschritt:
‹wpsm_kommutiert maxime_altruistischer_fortschritt zahlenwps welt›
apply(simp add: maxime_altruistischer_fortschritt_def wpsm_kommutiert_def handeln_def nachher_handeln.simps)
apply(safe)
apply(case_tac ‹p1 = p2›)
apply(simp add: zahlenwps_id; fail)
apply(case_tac ‹pX = p1›)
apply(simp)
apply (metis hlp1 zahlenwps_sym)
apply (metis hlp2 hlp3 zahlenwps_sym)
by (metis hlp2 hlp3 zahlenwps_id zahlenwps_sym)
lemma mhg_maxime_altruistischer_fortschritt_stehlen:
‹maxime_und_handlungsabsicht_generalisieren zahlenwps welt
maxime_altruistischer_fortschritt (Handlungsabsicht (stehlen 5 10)) p›
apply(simp add: maxime_altruistischer_fortschritt_def maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def handeln_def nachher_handeln.simps, intro allI impI)
apply(simp add: ausfuehrbar.simps)
apply(case_tac ‹welt›, simp)
apply(simp add: Zahlenwelt.stehlen.simps opfer_eindeutig_nach_besitz_auswaehlen_the_single_elem_enumall)
apply(simp add: ist_noop_def split: option.split option.split_asm)
by fastforce
lemma maxime_altruistischer_fortschritt_reset:
‹maxime_und_handlungsabsicht_generalisieren zahlenwps welt
maxime_altruistischer_fortschritt (Handlungsabsicht (reset)) p›
apply(simp add: maxime_altruistischer_fortschritt_def maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def handeln_def nachher_handeln.simps, intro allI impI)
apply(case_tac ‹welt›, simp)
apply(auto simp add: swap_def Fun.swap_def split: option.split option.split_asm)
done
lemma maxime_altruistischer_fortschritt_alles_kaputt_machen:
‹maxime_und_handlungsabsicht_generalisieren zahlenwps welt
maxime_altruistischer_fortschritt (Handlungsabsicht (alles_kaputt_machen)) p›
apply(simp add: maxime_altruistischer_fortschritt_def maxime_und_handlungsabsicht_generalisieren_def maxime_zahlenfortschritt_def handeln_def nachher_handeln.simps, intro allI impI)
apply(case_tac ‹welt›, simp)
apply(auto simp add: swap_def Fun.swap_def split: option.split option.split_asm)
done
lemma wfm_maxime_altruistischer_fortschritt:
‹wohlgeformte_maxime zahlenwps maxime_altruistischer_fortschritt›
apply(simp add: maxime_altruistischer_fortschritt_def wohlgeformte_maxime_def wohlgeformte_maxime_auf_def handeln_def nachher_handeln.simps, intro allI, rename_tac h p1 p2)
apply(case_tac ‹h›, rename_tac vor nach, simp)
apply(case_tac ‹vor›, case_tac ‹nach›, simp)
apply(simp add: swap_forall)
done
lemma individueller_fortschritt_map_handlung_zahlenwps:
‹individueller_fortschritt pX (map_handlung (zahlenwps p1 p2) ha)
= individueller_fortschritt (swap p1 p2 id pX) ha›
apply(cases ‹ha›, simp)
apply(cases ‹pX = p1›)
apply(simp add: hlp1 swap_a; fail)
apply(cases ‹pX = p2›)
apply(simp add: hlp2 swap_b; fail)
by (metis hlp3 id_apply swap_nothing zahlenwps_id)
lemma maxime_altruistischer_fortschritt_mhg_handlungsabsichten:
‹ha ∈ set handlungsabsichten ⟹
maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_altruistischer_fortschritt ha p›
apply(simp add: handlungsabsichten_def)
apply(safe)
apply(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_altruistischer_fortschritt_def; fail)
apply (simp add: mhg_maxime_altruistischer_fortschritt_stehlen; fail)
apply(simp add: maxime_altruistischer_fortschritt_reset; fail)
apply(simp add: maxime_altruistischer_fortschritt_alles_kaputt_machen; fail)
apply(case_tac ‹welt›, simp add: handeln_def nachher_handeln.simps maxime_und_handlungsabsicht_generalisieren_def maxime_altruistischer_fortschritt_def)
done
text‹Die Aussage, dass die \<^const>‹maxime_altruistischer_fortschritt› den kategorischen Imperativ
für bestimmte Handlungsabsichten und Welten erfüllt generalisiert noch weiter.
Für alle Welten und alle wohlgeformten Handlungsabsichten welche mit der Maxime generalisieren
erfüllt die Maxime den kategorischen Imperativ.›
theorem kapimp_maxime_altruistischer_fortschritt: ‹
∀p. maxime_und_handlungsabsicht_generalisieren zahlenwps welt maxime_altruistischer_fortschritt ha p ⟹
wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
kategorischer_imperativ_auf ha welt maxime_altruistischer_fortschritt›
unfolding maxime_altruistischer_fortschritt_def
apply(erule globale_maxime_katimp)
apply(cases ‹ha›, simp add: ist_noop_def handeln_def nachher_handeln.simps; fail)
apply(simp add: wpsm_kommutiert_altruistischer_fortschritt[simplified maxime_altruistischer_fortschritt_def]; fail)
apply (simp add: zahlenwps_sym; fail)
apply (simp add: zahlenwps_twice; fail)
by(simp; fail)
text‹Allgemein scheint dies eine sehr gute Maxime zu sein
(für dieses sehr beschränkte Weltenmodell).›
corollary ‹ha ∈ set handlungsabsichten ⟹
kategorischer_imperativ_auf ha welt maxime_altruistischer_fortschritt›
apply(rule kapimp_maxime_altruistischer_fortschritt)
using maxime_altruistischer_fortschritt_mhg_handlungsabsichten apply simp
using wfh_handlungsabsichten apply simp
done
lemma
‹okay maxime_altruistischer_fortschritt p1 (handeln p2 welt ha) ⟷
okay maxime_altruistischer_fortschritt p2 (map_handlung (zahlenwps p1 p2) (handeln p2 welt ha))›
using wfm_maxime_altruistischer_fortschritt
by (simp add: wohlgeformte_maxime_auf_def wohlgeformte_maxime_def)
beispiel ‹p ≠ p1 ⟹ p ≠ p2 ⟹
zahlenwps p2 p (zahlenwps p1 p2 (zahlenwps p1 p welt)) = zahlenwps p1 p2 welt›
apply(cases ‹welt›, simp add: swap_def)
by (metis swap_nilpotent swap_triple)
lemma zahlenwps_unrelated_im_kreis:
‹p ≠ p1 ⟹ p ≠ p2 ⟹
zahlenwps p2 p (zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt))) = welt›
by(cases ‹welt›, simp add: swap_unrelated_im_kreis)
lemma zahlenwps_unrelated_im_kreis_map_handlung_helper:
‹p ≠ p1 ⟹ p ≠ p2 ⟹
map_handlung (zahlenwps p1 p) (map_handlung (zahlenwps p2 p1) (map_handlung (zahlenwps p p2) h))
= map_handlung (zahlenwps p2 p1) h›
apply(cases ‹h›, rename_tac vor nach, simp)
apply(case_tac ‹vor›, case_tac ‹nach›, simp)
by (metis swap1 swap_unrelated_im_kreis)
lemma wfh_unrelated_pullout_wps:
‹p ≠ p1 ⟹ p ≠ p2 ⟹
∀welt. wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
handeln p (zahlenwps p1 p2 welt) ha
= map_handlung (zahlenwps p2 p1) (handeln p welt ha)›
thm wohlgeformte_handlungsabsicht_wpsid_wpssym_komm
thm wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p1 p2 welt› ‹ha›]
apply(subgoal_tac ‹handeln p (zahlenwps p1 p2 welt) ha =
map_handlung (zahlenwps p1 p) (handeln p1 (zahlenwps p p1 (zahlenwps p1 p2 welt)) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p1 p2 welt› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p (zahlenwps p1 p2 welt) ha = _›)
thm wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p p1 (zahlenwps p1 p2 welt)› ‹ha›]
apply(subgoal_tac ‹handeln p1 (zahlenwps p p1 (zahlenwps p1 p2 welt)) ha =
map_handlung (zahlenwps p2 p1) (handeln p2 (zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt))) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹(zahlenwps p p1 (zahlenwps p1 p2 welt))› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p1 _ ha = _›)
thm wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹(zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt)))› ‹ha›]
apply(subgoal_tac ‹handeln p2 (zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt))) ha =
map_handlung (zahlenwps p p2)
(handeln p (zahlenwps p2 p (zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt)))) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹(zahlenwps p1 p2 (zahlenwps p p1 (zahlenwps p1 p2 welt)))› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p2 _ ha = _›)
apply(simp add: zahlenwps_unrelated_im_kreis zahlenwps_unrelated_im_kreis_map_handlung_helper; fail)
done
lemma wohlgeformte_handlungsabsicht_zahlenwps_komm:
‹∀welt. wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
handeln p (zahlenwps p1 p2 welt) ha =
map_handlung (zahlenwps p1 p2) (handeln (swap p1 p2 id p) welt ha)›
apply(subgoal_tac ‹wohlgeformte_handlungsabsicht zahlenwps (zahlenwps p1 p2 welt) ha›)
prefer 2 apply blast
apply(drule wohlgeformte_handlungsabsicht_mit_wpsid)
subgoal by (simp add: wps_id_def zahlenwps_twice(2))
apply(case_tac ‹p=p1›)
apply(simp add: swap_a)
apply (metis handlung.collapse handlung.map_sel(1) handlung.map_sel(2) zahlenwps_sym zahlenwps_twice(1))
apply(case_tac ‹p=p2›)
apply(simp add: swap_b)
apply (metis zahlenwps_twice(2))
apply(simp add: swap_nothing)
apply(thin_tac ‹ ∀p1a p2a. _ p1a p2a›)
using wfh_unrelated_pullout_wps
by (metis zahlenwps_sym)
lemma ‹pX ≠ p1 ⟹ pX ≠ p2 ⟹ p1 ≠ p2 ⟹
zahlenwps pX p1 (zahlenwps pX p2 (zahlenwps p1 pX (zahlenwps p1 p2 welt))) = welt›
by(cases ‹welt›, simp add: swap_def Fun.swap_def)
lemma ‹pX ≠ p1 ⟹ pX ≠ p2 ⟹ p1 ≠ p2 ⟹
zahlenwps pX p2 (zahlenwps pX p1 (zahlenwps p2 pX (zahlenwps p1 p2 welt))) = welt›
by(cases ‹welt›, simp add: swap_def Fun.swap_def)
lemma zahlenwps_funny_permutation: ‹p ≠ p1 ⟹ p ≠ p2 ⟹
zahlenwps p2 p1 (zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt)))
= zahlenwps p p1 (zahlenwps p2 p welt)›
apply(cases ‹welt›, simp add: swap_def Fun.swap_def)
by auto
lemma zahlenwps_funny_permutation_map_handlung_helper:
‹p ≠ p1 ⟹ p ≠ p2 ⟹ p1 ≠ p2 ⟹
map_handlung (zahlenwps p p1) (map_handlung (zahlenwps p2 p) (map_handlung (zahlenwps p1 p2) h))
= map_handlung (zahlenwps p2 p) ( ( h))›
apply(cases ‹h›, rename_tac vor nach, simp)
apply(case_tac ‹vor›, case_tac ‹nach›, simp)
apply(simp add: swap_def Fun.swap_def)
by auto
lemma wfh_pullout_wps_helper_same:
‹p1 = p2 ⟹
handeln p1 (zahlenwps p1 p2 welt) ha = handeln p1 welt ha›
apply(simp add: zahlenwps_id)
done
text‹Umschreiben mit einem unrelated p. Bin mir noch nicht sicher, ob das was bringt.›
lemma wfh_pullout_wps_move_to_unrelated:
‹∀welt. wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
p ≠ p1 ⟹ p ≠ p2 ⟹ p1 ≠ p2 ⟹
handeln p1 (zahlenwps p1 p2 welt) ha
= map_handlung (zahlenwps p2 p) (handeln p1 (zahlenwps p p1 (zahlenwps p2 p welt)) ha)›
apply(subgoal_tac ‹handeln p1 (zahlenwps p1 p2 welt) ha =
map_handlung (zahlenwps p p1) (handeln p (zahlenwps p1 p (zahlenwps p1 p2 welt)) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p1 p2 welt› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p1 _ ha = _›)
thm wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p1 p (zahlenwps p1 p2 welt)› ‹ha›]
apply(subgoal_tac ‹handeln p (zahlenwps p1 p (zahlenwps p1 p2 welt)) ha =
map_handlung (zahlenwps p2 p) (handeln p2 (zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt))) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹(zahlenwps p1 p (zahlenwps p1 p2 welt))› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p _ ha = _›)
thm wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt))› ‹ha›]
apply(subgoal_tac ‹handeln p2 (zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt))) ha =
map_handlung (zahlenwps p1 p2)
(handeln p1 (zahlenwps p2 p1 (zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt)))) ha)›)
prefer 2
using wohlgeformte_handlungsabsicht_wpsid_simp[of ‹zahlenwps› ‹zahlenwps p p2 (zahlenwps p1 p (zahlenwps p1 p2 welt))› ‹ha›]
apply (simp add: wps_id_def zahlenwps_twice(2); fail)
apply(simp)
apply(thin_tac ‹handeln p2 _ ha = _›)
apply(simp add: zahlenwps_funny_permutation zahlenwps_funny_permutation_map_handlung_helper)
done
subsection‹Maxime für strikten individuellen Fortschritt›
text‹In der Maxime \<^const>‹individueller_fortschritt› hatten wir
\<^term>‹(meins p nach) ≥ (meins p vor)›.
Was wenn wir nun echten Fortschritt fordern:
\<^term>‹(meins p nach) > (meins p vor)›?›
fun individueller_strikter_fortschritt :: ‹person ⇒ zahlenwelt handlung ⇒ bool› where
‹individueller_strikter_fortschritt p (Handlung vor nach) ⟷ (meins p vor) < (meins p nach)›
text‹Folgendes ernüchterndes Beispiel zeigt,
die Maxime \<^const>‹individueller_strikter_fortschritt› erfüllt nicht den kategorischen Imperativ.
Entweder erlaubt die Maxime keine Assuage über eine Handlungsabsicht,
oder die Handlungsabsicht ist verboten.›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
handlungsabsichten
(Maxime individueller_strikter_fortschritt) =
Some
⦇
bsp_erfuellte_maxime = False,
bsp_erlaubte_handlungen = [],
bsp_verbotene_handlungen = [
Handlungsabsicht alles_kaputt_machen,
Handlungsabsicht unmoeglich],
bsp_uneindeutige_handlungen = [
Handlungsabsicht (erschaffen 5),
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht reset]
⦈›
by beispiel_tac
text‹In keiner Welt ist die Handlung \<^const>‹erschaffen› nun \<^const>‹moralisch›:›
lemma ‹¬ moralisch welt
(Maxime (λich. individueller_strikter_fortschritt ich)) (Handlungsabsicht (erschaffen 5))›
apply(cases ‹welt›)
by(auto simp add: maxime_zahlenfortschritt_def moralisch_simp handeln_def nachher_handeln.simps)
text‹ Der Grund ist, dass der Rest der Bevölkerung keine ∗‹strikte› Erhöhung des
eigenen Wohlstands erlebt.
Effektiv führt diese Maxime zu einem Gesetz, welches es einem Individuum nicht erlaubt
mehr Besitz zu erschaffen, obwohl niemand dadurch einen Nachteil hat.
Diese Maxime kann meiner Meinung nach nicht gewollt sein.
Beispielsweise ist \<^const>‹Bob› das Opfer wenn \<^const>‹Alice› sich 5 Wohlstand erschafft,
aber \<^const>‹Bob›'s Wohlstand sich dabei nicht erhöht:›
beispiel
‹⦇
dbg_opfer = Bob, dbg_taeter = Alice,
dbg_handlung = handeln Alice initialwelt (Handlungsabsicht (erschaffen 5))
⦈
∈ debug_maxime id initialwelt
(Maxime (λich. individueller_strikter_fortschritt ich)) (Handlungsabsicht (erschaffen 5)) ›
by eval
subsection‹Maxime für globales striktes Optimum›
text‹Wir bauen nun eine Maxime, die das Individuum vernachlässigt und nur nach dem
globalen Optimum strebt:›
fun globaler_strikter_fortschritt :: ‹zahlenwelt handlung ⇒ bool› where
‹globaler_strikter_fortschritt (Handlung vor nach) ⟷ (gesamtbesitz vor) < (gesamtbesitz nach)›
text‹Die Maxime ignoriert das \<^term>‹ich :: person› komplett.
Nun ist es \<^const>‹Alice› wieder erlaubt, Wohlstand für sich selbst zu erzeugen,
da sich dadurch auch der Gesamtwohlstand erhöht:›
beispiel ‹moralisch initialwelt
(Maxime (λich. globaler_strikter_fortschritt)) (Handlungsabsicht (erschaffen 5))›
by(eval)
text‹Allerdings ist auch diese Maxime auch sehr grausam, da sie Untätigkeit verbietet:›
beispiel ‹¬ moralisch initialwelt
(Maxime (λich. globaler_strikter_fortschritt)) (Handlungsabsicht (erschaffen 0))›
by(eval)
text‹Unsere initiale einfache \<^const>‹maxime_zahlenfortschritt› würde Untätigkeit hier erlauben:›
beispiel ‹moralisch initialwelt
maxime_zahlenfortschritt (Handlungsabsicht (erschaffen 0))›
by(eval)
text‹Folgendes Beispiel zeigt, dass die Maxime \<^const>‹globaler_strikter_fortschritt›
den kategorischen Imperativ erfüllen kann.
Die Handlungsabsichten sind fast intuitiv in erlaubt und verboten eingeordnet.
▪ \<^term>‹erschaffen 5› ist erlaubt.
▪ \<^const>‹stehlen›, \<^const>‹reset›, \<^const>‹alles_kaputt_machen› sind verboten.
Allerdings ist auch \<^const>‹unmoeglich› verboten, da die Maxime Untätigkeit verbietet.
Dieser letzte Fall ist unschön.
›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
handlungsabsichten
(Maxime (λich. globaler_strikter_fortschritt)) =
Some
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = [Handlungsabsicht (erschaffen 5)],
bsp_verbotene_handlungen = [
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht reset,
Handlungsabsicht alles_kaputt_machen,
Handlungsabsicht unmoeglich],
bsp_uneindeutige_handlungen = []⦈›
by beispiel_tac
subsection‹Maxime für globales Optimum›
text‹Wir können die Maxime für globalen Fortschritt etwas lockern.›
fun globaler_fortschritt :: ‹zahlenwelt handlung ⇒ bool› where
‹globaler_fortschritt (Handlung vor nach) ⟷ (gesamtbesitz vor) ≤ (gesamtbesitz nach)›
text‹Untätigkeit ist nun auch hier erlaubt:›
beispiel ‹moralisch initialwelt
(Maxime (λich. globaler_fortschritt)) (Handlungsabsicht (erschaffen 0))›
by(eval)
lemma globaler_fortschritt_kommutiert:
‹wpsm_kommutiert (Maxime (λich::person. globaler_fortschritt)) zahlenwps welt›
by(simp add: wpsm_kommutiert_def gesamtbesitz_swap zahlenwps_sym handeln_def nachher_handeln.simps)
text‹Allerdings ist auch Stehlen erlaubt, da global gesehen, kein Besitz vernichtet wird:›
beispiel ‹moralisch initialwelt
(Maxime (λich. globaler_fortschritt)) (Handlungsabsicht (stehlen_nichtwf 5 Bob))›
by(eval)
beispiel ‹moralisch initialwelt
(Maxime (λich. globaler_fortschritt)) (Handlungsabsicht (stehlen 5 10))›
by(eval)
text‹Folgendes Beispiel zeigt, dass die Maxime \<^const>‹globaler_fortschritt›
den kategorischen Imperativ erfüllen kann.
Die Handlungsabsichten sind meiner Meinung nach intuitiv
(basierend auf der globalen Betrachtung der Maxime) in erlaubt und verboten eingeordnet.
▪ \<^term>‹erschaffen› ist erlaubt.
Auch \<^const>‹stehlen› ist erlaubt, da dabei "doem Kollektiv" kein Besitz verloren geht.
Untätigkeit wird wieder über \<^const>‹unmoeglich› erlaubt.
▪ \<^const>‹reset› und \<^const>‹alles_kaputt_machen› sind verboten.
›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
handlungsabsichten
(Maxime (λich. globaler_fortschritt)) =
Some
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = [
Handlungsabsicht (erschaffen 5),
Handlungsabsicht (stehlen 5 10),
Handlungsabsicht unmoeglich],
bsp_verbotene_handlungen = [
Handlungsabsicht reset,
Handlungsabsicht alles_kaputt_machen],
bsp_uneindeutige_handlungen = []⦈›
by beispiel_tac
text‹Auch allgemein lässt ich beweisen,
dass diese Maxime für sehr viele Handlungsabsichten den kategorischen Imperativ erfüllt.›
theorem
‹∀p. maxime_und_handlungsabsicht_generalisieren zahlenwps welt
(Maxime (λich. globaler_fortschritt)) ha p ⟹
wohlgeformte_handlungsabsicht zahlenwps welt ha ⟹
kategorischer_imperativ_auf ha welt (Maxime (λich::person. globaler_fortschritt))›
apply(erule globale_maxime_katimp)
apply(cases ‹welt›, cases ‹ha›, simp add: ist_noop_def handeln_def nachher_handeln.simps; fail)
apply(simp add: globaler_fortschritt_kommutiert; fail)
apply(simp add: zahlenwps_sym)
apply (simp add: zahlenwps_twice; fail)
by(simp; fail)
text‹Sollte man das Kollektiv höher stellen als das Individuum
und damit effektiv das Recht auf Privateigentum ablehnen (was ich persönlich nicht unterstütze),
so ist \<^const>‹globaler_fortschritt› eine Maxime mit schönen Eigenschaften.›
subsection‹Ungültige Maxime›
text‹Es ist verboten, in einer Maxime eine spezielle Person hardzucoden.
Technisch könnte so eine Maxime den \<^const>‹kategorischer_imperativ_auf› erfüllen.
Dies wollen wir aber nicht, da dies gegen die Gleichbehandlung aller Menschen verstoßen würde.
Das Ergebnis wären verdrehte Moralbewertungen,
welche moralische Entscheidungen ausschließlich basierend auf egoistischen Bedürfnissen
der hardgecodeten Personen basieren.
Beispielsweise könnten wir \<^const>‹individueller_fortschritt› nicht mehr parametrisiert verwenden,
sondern einfach \<^const>‹Alice› reinschreiben:›
beispiel ‹individueller_fortschritt Alice
= (λh. case h of Handlung vor nach ⇒ (meins Alice vor) ≤ (meins Alice nach))›
apply(simp add: fun_eq_iff)
apply(intro allI, rename_tac h, case_tac ‹h›)
apply(simp)
done
text‹Solch eine Maxime ist allerdings nicht wohlgeformt.›
beispiel ‹¬ wohlgeformte_maxime_auf
(handeln Alice initialwelt (Handlungsabsicht (stehlen 5 10))) zahlenwps
(Maxime (λich. individueller_fortschritt Alice))›
apply(simp add: wohlgeformte_maxime_auf_def)
apply(rule_tac x=‹Alice› in exI)
apply(rule_tac x=‹Bob› in exI)
apply(code_simp)
done
text‹Sobald wir aufhören \<^const>‹Alice› hardzucoden, wird die Maxime wohlgeformt.›
beispiel ‹wohlgeformte_maxime_auf
(handeln Alice initialwelt (Handlungsabsicht (stehlen 5 10))) zahlenwps
(Maxime (λich. individueller_fortschritt ich))›
apply(simp add: wohlgeformte_maxime_auf_def)
apply(code_simp)
done
text‹Unser \<^const>‹erzeuge_beispiel› verweigert die Arbeit auf nicht-wohlgeformten Maximen.›
subsection‹Uneindeutige Handlungen›
text‹Bis jetzt haben wir den Schuldigen immer bei der Maxime gesucht,
wenn der kategorische Imperativ nicht erfüllt war und wir somit über bestimmte Handlungsabsichten
keine Aussage treffen konnten.
Gibt es jedoch auch Handlungsabsichten welche vermutlich unabhängig von jeder durchdachten Maxime
keine Bewertung im Sinne des kategorischen Imperativs erlauben?›
text‹Folgende Funktion ist inspiriert durch das 🌐‹https://de.wikipedia.org/wiki/Collatz-Problem›.›
fun collatz:: ‹int ⇒ int› where
‹collatz n = (if n mod 2 = 0 then n div 2 else 3*n + 1)›
beispiel ‹collatz 19 = 58› by eval
text‹Es folgt eine Handlungsabsicht, basierend auf dem Collatz-Problem.
Das eigentliche Collatz-Problem ist an dieser Stelle nicht relevant,
da wir nur eine Iteration machen.
Allerdings ist das eine spannende Handlungsabsicht,
da diese sowohl den Besitz erhöhen kann, aber auch verringern kann.›
fun collatzh:: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹collatzh ich (Zahlenwelt besitz) = Some (Zahlenwelt (besitz( ich := collatz (besitz ich))))›
text‹Die Handlungsabsicht \<^const>‹collatzh› ist tatsächlich immer wohlgeformt.›
lemma ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht collatzh)›
apply(simp add: wohlgeformte_handlungsabsicht.simps)
apply(case_tac ‹welt›, simp add: swap_def fun_eq_iff Fun.swap_def)+
done
text‹Die Handlungsabsicht \<^const>‹collatzh› generalisiert nicht mit der
\<^const>‹maxime_zahlenfortschritt›.
Dies ist keine große Überraschung, da \<^const>‹reset› auch nicht mit dieser Maxime generalisiert
hat und wir die Maxime auch für ungeeignet befunden haben.›
beispiel
‹¬ maxime_und_handlungsabsicht_generalisieren
zahlenwps (Zahlenwelt (€(Alice := 2, Bob := 3)))
maxime_zahlenfortschritt (Handlungsabsicht collatzh) Alice›
by eval
text ‹Für unsere hochgelobte \<^const>‹maxime_altruistischer_fortschritt› hingegen
haben wir noch kein Beispiel einer Handlungsabsicht gesehen,
welche nicht mit ihr generalisiert hat.
Dies wirft die Frage auf:
"gibt es überhaupt wohlgeformte Handlungsabsichten, welche nicht mit
\<^const>‹maxime_altruistischer_fortschritt› generalisieren?"
Die Antwort liefert \<^const>‹collatzh›.›
beispiel
‹¬ maxime_und_handlungsabsicht_generalisieren
zahlenwps (Zahlenwelt (€(Alice := 2, Bob := 3)))
maxime_altruistischer_fortschritt (Handlungsabsicht collatzh) Alice›
by eval
text‹Wir haben \<^const>‹collatzh› bis jetzt immer bei der Bewertung von Maximen ausgeschlossen.
Das Ergebnis vorweg:
Ein kategorischer Imperativ, egal welche vielversprechende Maxime,
gilt nicht für die Handlungsabsicht \<^const>‹collatzh›.›
beispiel
‹¬ kategorischer_imperativ_auf (Handlungsabsicht collatzh)
initialwelt maxime_zahlenfortschritt›
‹¬ kategorischer_imperativ_auf (Handlungsabsicht collatzh)
initialwelt maxime_altruistischer_fortschritt›
‹¬ kategorischer_imperativ_auf (Handlungsabsicht collatzh)
initialwelt (Maxime (λich. globaler_fortschritt))›
by(eval)+
text ‹
Der Grund ist, oberflächlich gesprochen, dass diese Handlungsabsicht
keinen eindeutigen Charakter hat.
Die Handlungsabsicht kann sowohl Besitz verringern als auch vermehren.
In vielen Welten wird es Leute geben, für die \<^const>‹collatzh› eine positive
Wirkung hat.
Jedoch ist \<^const>‹collatzh› wohl allgemein nicht \<^const>‹moralisch›,
da es normalerweise auch Leute gibt, für die \<^const>‹collatzh› eine
negative Auswirkung hat.
Daher kann eine Maxime \<^const>‹collatzh› nicht allgemein beurteilen.
Jedoch ist auch diese Meta-Aussage eine spannende Aussage:
Der kategorische Imperativ sagt (dadurch, dass er nicht erfüllt ist),
dass die Handlungsabsicht \<^const>‹collatz› nicht durch eine unserer Maximen
beurteilt werden sollte, bzw. sollten wir ein allgemeines Gesetz bauen wollen,
so können wir weder \<^const>‹collatzh› uneingeschränkt in die Liste erlaubter Handlungsabsichten
aufnehmen,
noch können wir uneingeschränkt \<^const>‹collatzh› uneingeschränkt in die Liste verbotener
Handlungsabsichten aufnehmen.
Oder anders ausgedrückt: können wir ein allgemeines Gesetz wollen,
welches eine Aussage über die Handlungsabsicht \<^const>‹collatzh› macht?
Ich argumentiere, dass wir solch ein Gesetz nicht wollen, da
▪ Würden wir nur die Auswirkung von \<^const>‹collatzh› betrachten,
(also die resultierende \<^typ>‹'welt handlung›,
nicht die \<^term_type>‹Handlungsabsicht collatzh›)
so kann diese Auswirkung durchweg positiv sein,
und wir möchten etwas positives nicht verbieten.
▪ Jedoch hat die Handlungsabsicht auch negative Charakterzüge,
da wir billigend in Kauf nehmen, dass Besitz vernichtet werden könnte.
Daher möchten wir diese Absicht auch nicht uneingeschränkt erlauben.
Besonders deutlich wird dies bei folgender zugespitzten Handlungsabsicht,
welche billigend die komplette Vernichtung allen Besitzes in Kauf nehmen würde.
›
definition uneindeutiger_charakter:: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹uneindeutiger_charakter ≡
(λich welt. if meins ich welt mod 2 = 0
then alles_kaputt_machen ich welt
else erschaffen 5 ich welt)›
lemma ‹wohlgeformte_handlungsabsicht zahlenwps welt (Handlungsabsicht uneindeutiger_charakter)›
unfolding uneindeutiger_charakter_def
apply(rule wohlgeformte_handlungsabsicht_ifI)
apply(simp add: wohlgeformte_handlungsabsicht_alles_kaputt_machen)
apply(simp add: wohlgeformte_handlungsabsicht_erschaffen)
apply(simp add: hlp1 hlp2)
done
beispiel
‹¬ kategorischer_imperativ_auf (Handlungsabsicht uneindeutiger_charakter)
initialwelt maxime_zahlenfortschritt›
‹¬ kategorischer_imperativ_auf (Handlungsabsicht uneindeutiger_charakter)
initialwelt maxime_altruistischer_fortschritt›
‹¬ kategorischer_imperativ_auf (Handlungsabsicht uneindeutiger_charakter)
initialwelt (Maxime (λich. globaler_fortschritt))›
by(eval)+
text‹Mir gefällt, dass der (extensionale) kategorische Imperativ prinzipiell sagt,
dass wir die Handlungsabsicht \<^const>‹uneindeutiger_charakter› nicht in einem allgemeinen
Gesetz behandeln können,
da die potenziellen positiven Auswirkungen im starken Gegensatz
zu der potenziell destruktiven zugrundeliegenden Absicht stehen.›
text‹Wenn wir allerdings ausnutzen, dass Handlungsabsichten partiell sein können,
und so den guten und den schlechten Charakter in eigenständige Handlungsabsichten separieren,
so können wir wieder allgemeines Aussage über die beiden Handlungsabsichten machen.›
definition partiell_guter_charakter:: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹partiell_guter_charakter ≡
(λich welt. if meins ich welt mod 2 = 0
then None
else erschaffen 5 ich welt)›
definition partiell_schlechter_charakter:: ‹person ⇒ zahlenwelt ⇒ zahlenwelt option› where
‹partiell_schlechter_charakter ≡
(λich welt. if meins ich welt mod 2 = 0
then alles_kaputt_machen ich welt
else None)›
beispiel ‹erzeuge_beispiel
zahlenwps (Zahlenwelt (€(Alice := 5, Bob := 10, Carol := -3)))
[Handlungsabsicht partiell_guter_charakter, Handlungsabsicht partiell_schlechter_charakter]
maxime_altruistischer_fortschritt
= Some
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = [Handlungsabsicht partiell_guter_charakter],
bsp_verbotene_handlungen = [Handlungsabsicht partiell_schlechter_charakter],
bsp_uneindeutige_handlungen = []
⦈›
by beispiel_tac
end