Leibniz' Project
It is proved here that every ethic without dead end is utlitarian, in the sense that it maximizes a utility function.
One relies on this article.
Throughout this page, let \(S\) be the set of states and \(A\) the set of actions.
Context {State : Type}. Context {Action : Type}.
variable {State : Type} variable {Action : Type}
A dead end is a situation in which the ethic allows no action.
\(\mathbf{Definition}\)
A dead end in an ethic \(e: S × A \to
\{⊥ ,⊤\}\) is a state \(s \in
S\) such that \(\forall a \in A,
e(s, a) = ⊥\).
Definition dead_end (ethic : @Ethic State Action) (state : State) : Prop := forall (action : Action), ethic state action = false.
def dead_end (ethic : @Ethic State Action) (state : State) : Prop := ∀ (action : Action), ethic state action = false
An ethic without dead end is an ethic for which no situation is a dead end. Note that this is not an assumption of hope: such a possible action can be “do nothing”. It seems possible to assume that every ethic has no dead end (or at least can be slightly modified to remove them, for example adding as ethical action “kill oneself” to situations having none).
\(\mathbf{Definition}\)
An ethic is without dead end if \(\forall s \in S\) \(s\) is not a dead end.
Definition without_dead_end (ethic : @Ethic State Action) : Prop := forall (state : State), ~ dead_end ethic state.
def without_dead_end (ethic : @Ethic State Action) : Prop := forall (state : State), ¬ dead_end ethic state
We may have in each situation a preference among all the alternatives of actions.
\(\mathbf{Definition}\)
A preference order is a total and transitive binary relation. We
will in this page denote with \(a_1 \ge
a_2\) the fact that the alternative \(a_1\) is preferable (or equally
preferable) to an alternative \(a_2\).
A utility function gives preferences among all possible alternatives. In our context, you may see this utility function as a measure of the “goodness” of actions.
\(\mathbf{Definition}\)
A utility function is a function from a set \(A\) of alternatives to a set \(U\) endowed with a preference order.
In our context, the alternatives are the possible actions in each
given situation, and a utility function is from \(S × A\) to \(U\). Strictly speaking, we have a
utility function for each state.
Note that the usual utility functions are given with \(U\) being the real numbers endowed with the usual \(\ge\) operator. We deal with (arguably) the most general definition.
Definition UtilityFunction {ps : PreferenceSpace} : Type := State -> Action -> ps.(carrier).
def UtilityFunction (ps : PreferenceSpace) : Type := State → Action → ps.carrier
An ethic is said to maximize a utility function if for each situation it imposes the action with the maximum goodness. There may be more than one such action.
\(\mathbf{Definition}\)
An ethic \(e\) maximizes a
utility function \(u\) if \[\forall s \in S,\ \forall a \in A,\ e(s,
a)=⊤ \iff \forall a' \in A,\ u(a) \ge u(a')\]
Definition can_be_obtained {ps : PreferenceSpace} (uf : UtilityFunction) (state : State) (utility : get_carrier ps) : Prop := exists (action : Action), utility = uf state action. Definition is_maximum {ps : PreferenceSpace} (uf : UtilityFunction) (state : State) (utility : get_carrier ps) : Prop := can_be_obtained uf state utility /\ forall (action : Action), get_preference_order ps utility (uf state action). Definition maximizes {ps : PreferenceSpace} (ethic : @Ethic State Action) (uf : @UtilityFunction ps) : Prop := forall (state : State) (action : Action), Is_true (ethic state action) <-> is_maximum uf state (uf state action).
def can_be_obtained {ps : PreferenceSpace} (uf : @UtilityFunction State Action ps) (state : State) (utility : get_carrier ps) : Prop := ∃ (action : Action), utility = uf state action def is_maximum {ps : PreferenceSpace} (uf : @UtilityFunction State Action ps) (state : State) (utility : get_carrier ps) : Prop := can_be_obtained uf state utility ∧ ∀ (action : Action), get_preference_order ps utility (uf state action) def maximizes {ps : PreferenceSpace} (ethic : @Ethic State Action) (uf : @UtilityFunction State Action ps) : Prop := forall (state : State) (action : Action), ethic state action ↔ is_maximum uf state (uf state action)
An ethic is said to be utilitarian if it maximizes a utility function.
\(\mathbf{Definition}\)
An ethic \(e\) is utilitarian if
there is a utility function \(u\)
such that \(e\) maximizes \(u\).
Definition is_utilitarian (ethic : @Ethic State Action) : Prop := exists (ps : PreferenceSpace) (uf : UtilityFunction), @maximizes ps ethic uf.
def is_utilitarian (ethic : @Ethic State Action) : Prop := ∃ (ps : PreferenceSpace) (uf : @UtilityFunction State Action ps), @maximizes State Action ps ethic uf
An ethic being given, we can for each situation assign the value \(1\) to the approved action(s) and \(0\) to the disapproved ones.
\(\mathbf{Definition}\)
An ethic \(e\) being given, its
associated utility is the following function: \[\begin{align*}
S × A &\to \mathbb R\\
(s, a) &\mapsto \begin{cases*}
1 \text{ if } e(s, a) = ⊤ \\
0 \text{ if } e(s, a) = ⊥
\end{cases*}
\end{align*}\]
Definition associated_utility (ethic : @Ethic State Action) : State -> Action -> nat := fun state => (fun action => if ethic state action then 0 else 1).
def associated_utility (ethic : @Ethic State Action) : State → Action → ℕ := fun state => (fun action => if ethic state action then 0 else 1) lemma le_preference_order : preference_order Nat.le := by unfold preference_order constructor · apply transitive_le · apply le_total def associatedPreferenceSpace : PreferenceSpace := @PreferenceSpace.mk ℕ Nat.le le_preference_order
If the ethic has no dead end, this gives a utility function it maximizes.
\(\mathbf{Proposition}\) Every ethic without dead end is utilitarian.
\(\mathbf{proof:}\)
Let \(e\) be an ethic without
dead end.
By definition of utilitarian, it suffices to show that \(e\) maximizes its associated utility
(which we note \(au\)), that
is:
\[\forall s \in S,\ \forall a \in A,\
e(s, a)=⊤ \iff \forall a' \in A,\ au(a) \ge
au(a')\] Let \(s \in
S\) and \(a \in A\).
As \(e\) has no dead end, by
definition of the associated utility, there is an action whose
image by \(au\) is \(1\), which is thus the maximum value
of \(au\) (because the other
possible value is \(0\)), that
is:
\[\forall a' \in A,\ au(a) \ge
au(a') \iff au(a) = 1\] And \(e(s, a)=⊤ \iff au(a) = 1\) results
from the definition of the associated utility
■
Proposition every_ethic_without_dead_end_is_utilitarian : forall (ethic : @Ethic State Action), without_dead_end ethic -> is_utilitarian ethic. Proof. intros. unfold is_utilitarian. exists associatedPreferenceSpace. exists (associated_utility ethic). unfold maximizes. intros. unfold is_maximum. split. - intro. destruct (ethic state action) eqn:H1. 2: { simpl in H0. inversion H0. } split. + unfold can_be_obtained. exists action. reflexivity. + unfold associated_utility. rewrite H1. intro. case (ethic state action0). reflexivity. apply le_S. apply le_n. - intro. destruct H0. destruct (ethic state action) eqn:H2. + reflexivity. + unfold associated_utility in H1. rewrite H2 in H1. unfold without_dead_end in H. pose proof (H state). unfold dead_end in H3. exfalso. apply H3. intro. pose proof (H1 action0). destruct (ethic state action0). { inversion H4. } { reflexivity. } Qed.
lemma every_ethic_without_dead_end_is_utilitarian2 : ∀ (ethic : @Ethic State Action), without_dead_end ethic → is_utilitarian ethic := by intro ethic intro h unfold is_utilitarian exists associatedPreferenceSpace exists (associated_utility ethic) unfold maximizes intro state action unfold is_maximum constructor · intro h0 constructor · unfold can_be_obtained exists action · unfold associated_utility rw [h0] simp intro action' match (ethic state action') with | true => simp unfold associatedPreferenceSpace unfold get_preference_order simp | false => simp unfold associatedPreferenceSpace unfold get_preference_order simp · intro h0 rcases h0 with ⟨h1, h2⟩ match h4 :(ethic state action) with | true => rfl | false => unfold associated_utility at h1 ; unfold without_dead_end at h ; specialize h state ; unfold dead_end at h ; exfalso ; apply h ; intro action' ; specialize h2 action' ; unfold associated_utility at h2 cases h3 : (ethic state action') · case false => rfl · case true => rw [h3] at h2 ; simp at h2 ; rw [h4] at h2 ; simp at h2 ; unfold associatedPreferenceSpace at h2 ; unfold get_preference_order at h2 ; simp at h2