Theory BeispielSteuern
theory BeispielSteuern
imports Zahlenwelt Maxime Steuern Aenderung KategorischerImperativ
begin
section‹Beispiel: Steuern›
text‹In diesem Abschnitt kombinieren wir das vorhergehende Modell der Einkommensteuergesetzgebung
mit dem kategorischen Imperativ um ein Beispiel über moralische Aussagen über Steuern zu schaffen.›
text‹Wir nehmen eine einfach Welt an, in der jeder Person ihr Einkommen zugeordnet wird.
Achtung: Im Unterschied zum BeispielZahlenwelt.thy modellieren wir hier nicht den Gesamtbesitz,
sondern das Jahreseinkommen. Besitz wird ignoriert.
›
datatype steuerwelt = Steuerwelt
(get_einkommen: ‹person ⇒ int›)
fun steuerwps :: ‹person ⇒ person ⇒ steuerwelt ⇒ steuerwelt› where
‹steuerwps p1 p2 (Steuerwelt besitz) = Steuerwelt (swap p1 p2 besitz)›
text‹Die Steuerlast sagt, wie viel Steuern gezahlt werden.›
fun steuerlast :: ‹person ⇒ steuerwelt handlung ⇒ int› where
‹steuerlast p (Handlung vor nach) = ((get_einkommen vor) p) - ((get_einkommen nach) p)›
text‹Das Einkommen vor Steuer wird brutto genannt.›
fun brutto :: ‹person ⇒ steuerwelt handlung ⇒ int› where
‹brutto p (Handlung vor nach) = (get_einkommen vor) p›
text‹Das Einkommen nach Steuer wird netto genannt.›
fun netto :: ‹person ⇒ steuerwelt handlung ⇒ int› where
‹netto p (Handlung vor nach) = (get_einkommen nach) p›
text‹Beispiele›
beispiel ‹steuerlast Alice (Handlung (Steuerwelt (€(Alice:=8))) (Steuerwelt (€(Alice:=5)))) = 3›
by eval
beispiel ‹steuerlast Alice (Handlung (Steuerwelt (€(Alice:=8))) (Steuerwelt (€(Alice:=0)))) = 8›
by eval
beispiel ‹steuerlast Bob (Handlung (Steuerwelt (€(Alice:=8))) (Steuerwelt (€(Alice:=5)))) = 0›
by eval
beispiel ‹steuerlast Alice (Handlung (Steuerwelt (€(Alice:=-3))) (Steuerwelt (€(Alice:=-4)))) = 1›
by eval
beispiel ‹steuerlast Alice (Handlung (Steuerwelt (€(Alice:=1))) (Steuerwelt (€(Alice:=-1)))) = 2›
by eval
text‹Folgende Menge beinhaltet alle Personen die mehr verdienen als ich.›
fun mehrverdiener :: ‹person ⇒ steuerwelt handlung ⇒ person set› where
‹mehrverdiener ich (Handlung vor nach) = {p. (get_einkommen vor) p ≥ (get_einkommen vor) ich}›
beispiel ‹mehrverdiener Alice
(Handlung (Steuerwelt (€(Alice:=8, Bob:=12, Eve:=7))) (Steuerwelt (€(Alice:=5))))
= {Alice, Bob}› by eval
lemma mehrverdiener_betrachtet_nur_ausgangszustand:
‹mehrverdiener p (handeln p' welt h) = mehrverdiener p (Handlung welt welt)›
by (metis handlung.collapse mehrverdiener.simps vorher_handeln)
text‹Folgende Maxime versucht Steuergerechtigkeit festzuschreiben:›
definition maxime_steuern :: ‹(person, steuerwelt) maxime› where
‹maxime_steuern ≡ Maxime
(λich handlung.
(∀p∈mehrverdiener ich handlung.
steuerlast ich handlung ≤ steuerlast p handlung)
∧ (∀p∈mehrverdiener ich handlung.
netto ich handlung ≤ netto p handlung)
)›
fun delta_steuerwelt :: ‹(steuerwelt, person, int) delta› where
‹delta_steuerwelt (Handlung vor nach) =
Aenderung.delta_num_fun (Handlung (get_einkommen vor) (get_einkommen nach))›
lemma ‹wpsm_kommutiert (Maxime
(λich handlung.
(∀p∈mehrverdiener ich handlung.
steuerlast ich handlung ≤ steuerlast p handlung))) steuerwps welt›
oops
lemma wfh_steuerberechnung_jeder_zahlt_int:
‹ha = Handlungsabsicht (λich w. Some (Steuerwelt ((λe. e - steuerberechnung e) ∘ (get_einkommen w))))
⟹ wohlgeformte_handlungsabsicht steuerwps welt ha›
apply(cases ‹welt›, rename_tac eink, simp)
apply(simp add: wohlgeformte_handlungsabsicht.simps comp_def fun_eq_iff)
apply(safe)
apply(rename_tac eink p1 p2 p)
by(rule swap_cases, simp_all add: swap_a swap_b swap_nothing)
text‹Wenn die Steuerfunktion monoton ist,
dann können wir auch einen sehr eingeschränkten kategorischen Imperativ zeigen.›
lemma katimp_auf_handlungsabsicht_monoton:
‹(⋀e1 e2. e1 ≤ e2 ⟹ steuerberechnung e1 ≤ steuerberechnung e2) ⟹
ha = Handlungsabsicht
(λich w. Some (Steuerwelt ((λe. e - steuerberechnung e) ∘ (get_einkommen w)))) ⟹
kategorischer_imperativ_auf ha welt
(Maxime
(λich handlung.
(∀p∈mehrverdiener ich handlung.
steuerlast ich handlung ≤ steuerlast p handlung)))›
apply(cases ‹welt›, rename_tac eink, simp)
apply(rule kategorischer_imperativ_aufI, rename_tac eink ich p1 p2)
apply(simp add: handeln_def nachher_handeln.simps)
done
subsection‹Beispiel: Keiner Zahlt Steuern›
text‹Die Maxime ist im Beispiel erfüllt, da wir immer nur kleiner-gleich fordern!›
beispiel ‹moralisch (Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5)))
maxime_steuern (Handlungsabsicht (λich welt. Some welt))› by eval
subsection‹Beispiel: Ich zahle 1 Steuer›
text‹Das funktioniert nicht:›
definition ‹ich_zahle_1_steuer ich welt ≡
Some (Steuerwelt ⟦(get_einkommen welt)(ich -= 1)⟧)›
beispiel ‹¬ moralisch (Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5)))
maxime_steuern (Handlungsabsicht ich_zahle_1_steuer)› by eval
text‹Denn jeder muss Steuer zahlen!
Ich finde es super spannend, dass hier faktisch ein Gleichbehandlungsgrundsatz rausfällt,
ohne dass wir so Etwas jemals explizit gefordert haben.
›
subsection‹Beiepiel: Jeder zahle 1 Steuer›
text‹Jeder muss steuern zahlen: funktioniert.
Das \<^term>‹ich› wird gar nicht verwendet, da jeder Steuern zahlt.›
definition ‹jeder_zahle_1_steuer ich welt ≡
Some (Steuerwelt ((λe. e - 1) ∘ (get_einkommen welt)))›
beispiel ‹moralisch (Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5)))
maxime_steuern (Handlungsabsicht jeder_zahle_1_steuer)› by eval
subsection‹Beispiel: Vereinfachtes Deutsches Steuersystem›
text‹Jetzt kommt die Steuern.thy ins Spiel.›
definition jeder_zahlt :: ‹(nat ⇒ nat) ⇒ 'a ⇒ steuerwelt ⇒ steuerwelt› where
‹jeder_zahlt steuerberechnung ich welt ≡
Steuerwelt ((λe. e - steuerberechnung e) ∘ nat ∘ (get_einkommen welt))›
lemma jeder_zahlt_ignoriert_person:
‹jeder_zahlt steuersystem_impl p w = jeder_zahlt steuersystem_impl p' w›
by(simp add: jeder_zahlt_def)
definition ‹jeder_zahlt_einkommenssteuer p w ≡ Some (jeder_zahlt einkommenssteuer p w)›
text‹Bei dem geringen Einkommen der \<^term>‹Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5))› zahlt keiner Steuern.›
beispiel ‹ist_noop
(handeln Alice(Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5)))
(Handlungsabsicht jeder_zahlt_einkommenssteuer))› by eval
beispiel ‹moralisch (Steuerwelt (€(Alice:=8, Bob:=3, Eve:= 5)))
maxime_steuern (Handlungsabsicht jeder_zahlt_einkommenssteuer)› by eval
text‹Für höhere Einkommen erhalten wir plausible Werte und niemand rutscht ins negative:›
beispiel ‹delta_steuerwelt
(handeln
Alice (Steuerwelt (€(Alice:=10000, Bob:=14000, Eve:= 20000)))
(Handlungsabsicht jeder_zahlt_einkommenssteuer))
= [Verliert Bob 511, Verliert Eve 1857]› by eval
beispiel ‹moralisch
(Steuerwelt (€(Alice:=10000, Bob:=14000, Eve:= 20000)))
maxime_steuern
(Handlungsabsicht jeder_zahlt_einkommenssteuer)› by eval
text‹Unser Beispiel erfüllt auch den kategorischen Imperativ.›
beispiel ‹erzeuge_beispiel
steuerwps (Steuerwelt (€(Alice:=10000, Bob:=14000, Eve:= 20000)))
[Handlungsabsicht jeder_zahlt_einkommenssteuer]
maxime_steuern
=
Some
⦇
bsp_erfuellte_maxime = True,
bsp_erlaubte_handlungen = [Handlungsabsicht jeder_zahlt_einkommenssteuer],
bsp_verbotene_handlungen = [],
bsp_uneindeutige_handlungen = []
⦈›
by beispiel_tac
subsection‹Vereinfachtes Deutsches Steuersystem vs. die Steuermaxime›
text‹Die Anforderungen für ein \<^locale>‹steuersystem› und die \<^const>‹maxime_steuern› sind vereinbar.›
lemma steuersystem_imp_maxime:
‹steuersystem steuersystem_impl ⟹
(∀welt. moralisch welt
maxime_steuern
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w))))›
apply(simp add: maxime_steuern_def moralisch_unfold handeln_def nachher_handeln.simps)
apply(simp add: jeder_zahlt_def bevoelkerung_def)
apply(intro allI impI conjI)
apply(rename_tac welt p1 p2)
thm steuersystem.wer_hat_der_gibt
apply(drule_tac
einkommen_b=‹nat (get_einkommen welt p1)› and
einkommen_a=‹nat (get_einkommen welt p2)› in steuersystem.wer_hat_der_gibt)
apply(simp; fail)
apply(simp; fail)
apply(rename_tac welt p1 p2)
apply(drule_tac
einkommen_b=‹nat (get_einkommen welt p1)› and
einkommen_a=‹nat (get_einkommen welt p2)› in steuersystem.leistung_lohnt_sich)
apply(simp; fail)
by (simp add: steuer_defs.netto_def)
text‹Danke ihr nats. Macht also keinen Sinn das als Annahme in die Maxime zu packen....›
lemma steuern_kleiner_einkommen_nat:
‹steuerlast ich (Handlung welt (jeder_zahlt steuersystem_impl ich welt))
≤ brutto ich (Handlung welt (jeder_zahlt steuersystem_impl ich welt))›
apply(simp del: steuerlast.simps)
apply(subst steuerlast.simps)
apply(simp add: jeder_zahlt_def)
done
text‹Mit genug zusätzlichen Annahmen gilt auch die Rückrichtung:›
lemma maxime_imp_steuersystem:
‹∀einkommen. steuersystem_impl einkommen ≤ einkommen ⟹
∀einkommen. einkommen ≤ 9888 ⟶ steuersystem_impl einkommen = 0 ⟹
∀welt. moralisch welt maxime_steuern
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w)))
⟹ steuersystem steuersystem_impl›
proof
fix einkommen_b einkommen_a :: ‹nat›
assume m: ‹∀welt. moralisch welt maxime_steuern
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w)))›
and a: ‹einkommen_b ≤ einkommen_a›
and bezahlbar: ‹∀einkommen. steuersystem_impl einkommen ≤ einkommen›
from m have m':
‹get_einkommen welt pA ≤ get_einkommen welt pB ⟹
get_einkommen welt pA -
int (nat (get_einkommen welt pA) - steuersystem_impl (nat (get_einkommen welt pA)))
≤ get_einkommen welt pB -
int (nat (get_einkommen welt pB) - steuersystem_impl (nat (get_einkommen welt pB)))›
for welt :: ‹steuerwelt› and pA pB :: ‹person›
by(simp add: handeln_def nachher_handeln.simps
maxime_steuern_def moralisch_unfold jeder_zahlt_def bevoelkerung_def)
from m'[where welt=‹Steuerwelt (λp. if p = Bob then einkommen_b else einkommen_a)›
and pA=‹Bob› and pB=‹Alice›] a
have almost:
‹int einkommen_b - int (einkommen_b - steuersystem_impl einkommen_b)
≤ int einkommen_a - int (einkommen_a - steuersystem_impl einkommen_a)›
by simp
from bezahlbar have ‹steuersystem_impl einkommen_b ≤ einkommen_b› by simp
from this almost show ‹steuersystem_impl einkommen_b ≤ steuersystem_impl einkommen_a›
by simp
next
fix einkommen_b einkommen_a :: ‹nat›
assume m: ‹∀welt. moralisch welt maxime_steuern
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w)))›
and a: ‹einkommen_b ≤ einkommen_a›
from m have m':
‹get_einkommen welt pA ≤ get_einkommen welt pB ⟹
nat (get_einkommen welt pA) - steuersystem_impl (nat (get_einkommen welt pA))
≤ nat (get_einkommen welt pB) - steuersystem_impl (nat (get_einkommen welt pB))›
for welt :: ‹steuerwelt› and pA pB :: ‹person›
by(simp add: handeln_def nachher_handeln.simps maxime_steuern_def moralisch_unfold
jeder_zahlt_def bevoelkerung_def)
from m'[where welt=‹Steuerwelt (λp. if p = Bob then einkommen_b else einkommen_a)›
and pA=‹Bob› and pB=‹Alice›] a
have ‹einkommen_b - steuersystem_impl einkommen_b ≤ einkommen_a - steuersystem_impl einkommen_a›
by simp
from this show
‹steuer_defs.netto steuersystem_impl einkommen_b
≤ steuer_defs.netto steuersystem_impl einkommen_a›
by(simp add: steuer_defs.netto_def)
next
fix einkommen
show ‹∀einkommen≤9888. steuersystem_impl einkommen = 0
⟹ einkommen ≤ 9888 ⟹ steuersystem_impl einkommen = 0›
by simp
qed
text‹
Dass die eine Richtung gilt (Maxime impliziert \<^const>‹steuersystem›),
die andere Richtung (\<^const>‹steuersystem› impliziert Maxime) jedoch nicht ohne weiter Annahmen,
stimmt auch mit Russels Beobachtung überein:
"Kants Maxime [das allgemeine Konzept, nicht meine Implementierung]
scheint tatsächlich ein notwendiges, jedoch nicht ∗‹ausreichendes› Kriterium der Tugend zu geben"
@{cite russellphi}.
Insbesondere Russels Folgesatz freut mich, da er mir bestätigt, dass unsere extensionale
Betrachtung von Handlungen vielversprechend ist:
"Um ein ausreichendes Kriterium zu gewinnen, müßten wir Kants rein formalen Standpunkt aufgeben
und die Wirkung der Handlungen in Betracht ziehen" @{cite russellphi}.
›
text‹
Für jedes \<^term_type>‹steuersystem_impl :: nat ⇒ nat›,
mit zwei weiteren Annahmen
gilt, dass \<^locale>‹steuersystem› und \<^const>‹maxime_steuern› in der \<^const>‹jeder_zahlt› Implementierung
äquivalent sind.›
theorem
fixes steuersystem_impl :: ‹nat ⇒ nat›
assumes steuer_kleiner_einkommen: ‹∀einkommen. steuersystem_impl einkommen ≤ einkommen›
and existenzminimum: ‹∀einkommen. einkommen ≤ 9888 ⟶ steuersystem_impl einkommen = 0›
shows
‹(∀welt. moralisch welt maxime_steuern
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w))))
⟷
steuersystem steuersystem_impl›
using steuersystem_imp_maxime maxime_imp_steuersystem
using assms by blast
text‹Da jede Steuersystemimplementierung welche \<^locale>‹steuersystem› erfüllt auch
moralisch ist (lemma @{thm [source] steuersystem_imp_maxime}),
erfüllt damit auch jedes solche System den kategorischen Imperativ.›
corollary steuersystem_imp_kaptimp:
‹steuersystem steuersystem_impl ⟹
kategorischer_imperativ_auf
(Handlungsabsicht (λp w. Some (jeder_zahlt steuersystem_impl p w)))
welt
maxime_steuern›
apply(drule steuersystem_imp_maxime)
by (simp add: kategorischer_imperativ_auf_def)
text‹Und daraus folgt, dass auch \<^const>‹jeder_zahlt_einkommenssteuer›
den kategorischen Imperativ erfüllt.›
corollary
‹steuersystem steuersystem_impl ⟹
kategorischer_imperativ_auf
(Handlungsabsicht jeder_zahlt_einkommenssteuer)
welt
maxime_steuern›
unfolding jeder_zahlt_einkommenssteuer_def
apply(rule steuersystem_imp_kaptimp)
by (simp add: steuersystem_axioms)
end