Leibniz' Project
An ethic being said to leave no freedom when it allows a unique action, it is proved here that for every utlitarian ethic (that is every ethic without dead end according to this article, there is no freedom if and only if the maximum utility is reached for a unique action.
The context is the same as in 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.
From mathcomp Require Import all_ssreflect.
Require Import ethics_first_steps.
Require Import every_ethic_without_dead_end_is_utilitarian.
Definition State : Type := ethics_first_steps.State.
Definition Action : eqType := ethics_first_steps.Action.
In a given situation, an ethic is said to leave no freedom if allows a unique action.
\(\mathbf{Definition}\)
Let \(s\) in \(S\). An ethic \(e\) leaves no freedom in state \(s\) if \[\exists! a, e(s, a) = ⊤\]
Definition leaves_no_freedom (ethic: Ethic) (state: State) : Prop :=
exists! (action: Action), ethic state action = true.
An ethic is said to never leave freedom if it leaves no freedom in every situation.
\(\mathbf{Definition}\)
An ethic \(e\) never leaves
freedom if \(\forall s \in S\),
\(e\) leaves no freedom in \(s\).
Definition never_leaves_freedom (ethic: Ethic) : Prop :=
forall (state: State), leaves_no_freedom ethic state.
In a given situation, if an ethic leaves no freedom, then it still allows an action and therefore we are not in a dead end.
\(\mathbf{Lemma}\)
If an ethic \(e\) leaves no
freedom in a state \(s\), then
\(s\) is not a dead end for \(e\).
\(\mathbf{proof:}\)
Let \(e\) be an ethic and \(s\) be a state in which \(e\) leaves no freedom.
By definition, there is a unique action \(a\) allowed by \(e\) in \(s\).
Then this action \(a\) is allowed
by \(e\) in \(s\), which means that \(s\) is not a dead end
■
Lemma no_freedom_implies_no_dead_end (ethic: Ethic) (state: State) :
leaves_no_freedom ethic state -> ~ dead_end ethic state.
Proof.
intro. unfold leaves_no_freedom in H.
destruct H. unfold unique in H.
destruct H. unfold dead_end.
intro. pose proof (H1 x).
rewrite H in H2. inversion H2.
Qed.
Therefore, if an ethic never leaves freedom, then it is without dead end.
\(\mathbf{Corollary}\)
An ethic which never leaves freedom is without dead end.
\(\mathbf{proof:}\)
Let \(e\) be an ethic which never
leaves freedom.
By definition, \(\forall s \in
S\), \(e\) leaves no
freedom in \(s\).
By the previous lemma, \(\forall s \in
S\), \(s\) is not a dead
end for \(e\), which means it is
without dead end.
■
Corollary never_leaves_freedom_implies_never_has_dead_end (ethic: Ethic) :
never_leaves_freedom ethic -> without_dead_end ethic.
Proof.
unfold without_dead_end. unfold never_leaves_freedom. intro.
intro. apply no_freedom_implies_no_dead_end. apply H.
Qed.
\(\mathbf{Definition}\)
An utilitarian ethic \(e\)
(endowed with a utility function called \(uf\)) is said to have a unique action
\(a\) maximizing its utility if
\[\begin{cases*}
\forall a' \in A, uf(s, a') \le uf(s, a) \text{ (where
$\le$ designating the prefereence order associated with the
utility function)} \\
\forall a' \in A, uf(s, a') = uf(s, a) \implies a' =
a
\end{cases*}\]
Definition utilitarian_ethic_unique_maximum {ps : PreferenceSpace}
(ethic : Ethic) (uf : @UtilityFunction ps)
(ethic_maximizes_uf : maximizes ethic uf) (state : State) :=
exists! (action : Action), is_maximum uf state (uf state action).
\(\mathbf{Definition}\)
An utilitarian ethic \(e\) is
said to always have a unique action maximizing its utility if
\(\forall s \in S\), \(e\) has a unique maximum action
maximizing its utility
Definition utilitarian_ethic_always_unique_maximum {ps : PreferenceSpace}
(ethic : Ethic) (uf : @UtilityFunction ps) (ethic_maximizes_uf : maximizes ethic uf) :=
forall (state: State),
utilitarian_ethic_unique_maximum ethic uf ethic_maximizes_uf state.
\(\mathbf{Proposition}\)
A utilitarian ethic \(e\) has a
unique action maximizing its utility in a state \(s\) iff it leaves no freedom in \(s\).
\(\mathbf{proof:}\)
Let \(e\) be a utilitarian ethic,
\(uf\) its utility function and
\(s\) a state.
- if \(e\) has a unique action
\(a\) maximizing its utility in
\(s\), as an utilitarian ethic
requires to maximize its utility, the only allowed action is \(a\), which leaves no freedom.
- if \(e\) leaves no freedom in
\(s\), then the only allowed
action \(a\) must maximize the
utility function (by definition of utility function) and be the
only action to do so.
■
Proposition utilitarian_ethic_no_freedom_iff_maximum_for_unique_action
{ps : PreferenceSpace} :
forall (ethic: Ethic) (uf : UtilityFunction)
(ethic_maximizes_uf : maximizes ethic uf) (state: State),
@utilitarian_ethic_unique_maximum ps ethic uf ethic_maximizes_uf state <->
leaves_no_freedom ethic state.
Proof.
intros.
unfold maximizes in ethic_maximizes_uf.
split.
- intro. unfold leaves_no_freedom. unfold unique.
unfold utilitarian_ethic_unique_maximum in H.
destruct H. unfold unique in H. destruct H.
exists x. split.
+ pose proof (ethic_maximizes_uf state). pose proof (H1 x).
rewrite <- H2 in H. unfold Is_true in H.
destruct (ethic state x).
{ reflexivity. }
{ inversion H. }
+ intros.
pose proof (H0 x'). apply H2.
pose proof (ethic_maximizes_uf state). pose proof (H3 x').
rewrite <- H4. unfold Is_true.
rewrite H1. tauto.
- intro. unfold leaves_no_freedom in H. unfold unique in H.
unfold utilitarian_ethic_unique_maximum. unfold unique.
destruct H. destruct H.
pose proof (ethic_maximizes_uf state).
exists x. split.
+ pose proof (H1 x).
rewrite <- H2. rewrite H. easy.
+ intro. pose proof (H0 x'). intro.
rewrite <- H1 in H3. unfold Is_true in H3.
destruct (ethic state x').
{ apply H2. reflexivity. }
{ inversion H3. }
Qed.
\(\mathbf{Corollary}\)
A utilitarian ethic always has a unique action maximizing its
utility iff it never leaves freedom.
\(\mathbf{proof:}\)
Let \(e\) be a utilitarian ethic,
\(uf\) its utility
function.
\(e\) always has a unique action
maximizing its utility
\(\iff \forall s \in S\), \(e\) has a unique action maximizing
its utility in \(s\)
\(\iff \forall s \in S\), \(e\) leaves no freedom in \(s\)
\(\iff e\) never leaves
freedom
■
Corollary utilitarian_ethic_never_freedom_iff_always_maximum_for_unique_action
{ps : PreferenceSpace} :
forall (ethic: Ethic) (uf : UtilityFunction)
(ethic_maximizes_uf : maximizes ethic uf),
@utilitarian_ethic_always_unique_maximum ps ethic uf ethic_maximizes_uf <->
never_leaves_freedom ethic.
Proof.
intros. unfold utilitarian_ethic_always_unique_maximum. unfold never_leaves_freedom.
split ; intros; pose proof (H state) ;
apply @utilitarian_ethic_no_freedom_iff_maximum_for_unique_action with
(ps:=ps) (ethic:=ethic) (uf:=uf) (ethic_maximizes_uf:=ethic_maximizes_uf) ;
tauto.
Qed.