Theory AllgemeinesGesetz

theory AllgemeinesGesetz
imports Gesetz Maxime
begin

section‹Experimental: Moralisch Gesetzs Ableiten›
subsection‹Allgemeines Gesetz Ableiten›

text‹Wir wollen implementieren:

∗‹„Handle nur nach derjenigen Maxime, durch die du zugleich wollen kannst,
   dass sie ein ❙‹allgemeines Gesetz› werde.“›

Für eine gebene Welt haben wir schon eine Handlung nach einer Maxime untersucht:
\<^term>‹moralisch::'welt ⇒ ('person, 'welt) maxime ⇒ ('person, 'welt) handlungsabsicht ⇒ bool›

Das Ergebnis sagt uns ob diese Handlung gut oder schlecht ist.
Basierend darauf müssen wir nun ein allgemeines Gesetz ableiten.

Ich habe keine Ahnung wie das genau funktionieren soll, deswegen schreibe ich
einfach nur in einer Typsignatur auf, was zu tun ist:

Gegeben:
  ▪ \<^typ>‹'welt handlung›: Die Handlung
  ▪ \<^typ>‹sollensanordnung›: Das Ergebnis der moralischen Bewertung, ob die Handlung gut/schlecht.

Gesucht:
  ▪ \<^typ>‹('a, 'b) rechtsnorm›: ein allgemeines Gesetz
›

type_synonym ('welt, 'a, 'b) allgemeines_gesetz_ableiten =
  ‹'welt handlung ⇒ sollensanordnung ⇒ ('a, 'b) rechtsnorm›

text‹
Soviel vorweg:
Nur aus einer von außen betrachteten Handlung
und einer Entscheidung ob diese Handlung ausgeführt werden soll
wird es schwer ein allgemeines Gesetz abzuleiten.
›
(*TODO: waere hier ('person, 'welt) handlungsabsicht anstatt 'welt handlung besser?*)

subsection‹Implementierung Moralisch ein Allgemeines Gesetz Ableiten›
(*TODO: unterstütze viele Maximen, wobei manche nicht zutreffen können?*)
text‹Und nun werfen wir alles zusammen:

∗‹„Handle nur nach derjenigen Maxime, durch die du zugleich wollen kannst,
   dass sie ein allgemeines Gesetz werde.“›


Eingabe:
 ▪ \<^typ>‹'person›: handelnde Person
 ▪ \<^typ>‹'welt›: Die Welt in ihrem aktuellen Zustand
 ▪ \<^typ>‹('person, 'welt) handlungsabsicht›: Eine mögliche Handlung,
    über die wir entscheiden wollen ob wir sie ausführen sollten.
 ▪ \<^typ>‹('person, 'welt) maxime›: Persönliche Ethik.
 ▪ \<^typ>‹('welt, 'a, 'b) allgemeines_gesetz_ableiten›:
    wenn man keinen Plan hat wie man sowas implementiert, einfach als Eingabe annehmen.
 ▪ \<^typ>‹(nat, 'a, 'b) gesetz›: Initiales allgemeines Gesetz (normalerweise am Anfang leer).

Ausgabe:
   \<^typ>‹sollensanordnung›: Sollen wir die Handlung ausführen?
   \<^typ>‹(nat, 'a, 'b) gesetz›: Soll das allgemeine Gesetz entsprechend angepasst werden?
›
  (*TODO: Wenn unsere Maximen perfekt und die Maximen aller Menschen konsisten sind,
        soll das Gesetz nur erweitert werden.*)
(*
  -- Es fehlt: ich muss nach allgemeinem Gesetz handeln.
  --           Wenn das Gesetz meinen Fall nicht abdeckt,
  --           dann muss meine Maxime zum Gesetz erhoben werden.
  -- Es fehlt: "Wollen"
  -- TODO: Wir unterstützen nur Erlaubnis/Verbot.
*)

definition moarlisch_gesetz_ableiten ::
  ‹'person ⇒
   'welt ⇒
   ('person, 'welt) maxime ⇒
   ('person, 'welt) handlungsabsicht ⇒
   ('welt, 'a, 'b) allgemeines_gesetz_ableiten ⇒
   (nat, 'a, 'b) gesetz
  ⇒ (sollensanordnung × (nat, 'a, 'b) gesetz)›
where
  ‹moarlisch_gesetz_ableiten ich welt maxime handlungsabsicht gesetz_ableiten gesetz ≡
    let soll_handeln = if moralisch welt maxime handlungsabsicht
                       then
                         Erlaubnis
                       else
                         Verbot in
      (
        soll_handeln,
        hinzufuegen (gesetz_ableiten (handeln ich welt handlungsabsicht) soll_handeln) gesetz
      )›

text‹Das ganze \<^const>‹moarlisch_gesetz_ableiten› dient mehr dem Debugging, ...›


end