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.
Require Import Bool.Bool.
Require Import Relations.Relation_Definitions.
Require Import Arith.PeanoNat.
From mathcomp Require Import all_ssreflect.
Require Import ethics_first_steps.
Definition State : Type := ethics_first_steps.State.
Definition Action : eqType := ethics_first_steps.Action.
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 : State) : Prop :=
forall (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) : 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\).
Definition total {T : Type} (R : relation T) := forall (x y : T), R x y \/ R y x.
Definition transitive {T : Type} (R : relation T) := forall (x y z : T),
R x y -> R y z -> R x z.
Definition preference_order {T : Type} (R : relation T) :=
transitive R /\ total R.
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.
Structure PreferenceSpace : Type := {
carrier :> Type ;
order : relation carrier ;
is_preference_order: preference_order order
}.
Definition get_carrier : PreferenceSpace -> Type:=
fun (ps : PreferenceSpace) => ps.(carrier).
Definition get_preference_order (ps : PreferenceSpace) : relation (get_carrier ps) :=
ps.(order).
Definition UtilityFunction {ps : PreferenceSpace} : Type := State -> Action -> ps.
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) (uf : @UtilityFunction ps) : Prop :=
forall (state : State) (action : Action),
Is_true (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) : Prop :=
exists (ps : PreferenceSpace) (uf : UtilityFunction), @maximizes 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 -> nat :=
fun state => (fun action => if ethic state action then 0 else 1).
Lemma le_transitive : transitive le.
Proof.
intros n m o Hnm Hmo.
induction Hmo.
- apply Hnm.
- apply le_S. apply IHHmo.
Qed.
Lemma le_total : total le.
Proof.
intros n m.
assert (le n m \/ gt n m).
{ apply Nat.le_gt_cases. }
destruct H.
- left. tauto.
- right. unfold gt in H. apply Nat.lt_le_incl. tauto.
Qed.
Lemma le_preference_order : preference_order le.
Proof.
unfold preference_order. split.
- apply le_transitive.
- apply le_total.
Qed.
Definition associatedPreferenceSpace (ethic : Ethic) : PreferenceSpace := {|
carrier := nat ;
order := le ;
is_preference_order := 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), without_dead_end ethic -> is_utilitarian ethic.
Proof.
intros. unfold is_utilitarian.
exists (associatedPreferenceSpace ethic). 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.