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.
Context {State : Type}. Context {Action : eqType}. Definition Ethic : Type := ethics_first_steps.Ethic State Action.
variable {State : Type} variable {Action : Type}
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.
def leaves_no_freedom (ethic: @Ethic State Action) (state: State) : Prop := ∃! (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.
def never_leaves_freedom (ethic: @Ethic State Action) : Prop := ∀ (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.
lemma no_freedom_implies_no_dead_end (ethic: @Ethic State Action) (state: State) : leaves_no_freedom ethic state -> ¬ dead_end ethic state := by intro h unfold leaves_no_freedom at h unfold ExistsUnique at h rcases h with ⟨action, h⟩ rcases h with ⟨x1, h2⟩ unfold dead_end intro h specialize h action rw [h] at x1 contradiction
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.
lemma never_leaves_freedom_implies_never_has_dead_end (ethic: @Ethic State Action) : never_leaves_freedom ethic → without_dead_end ethic := by unfold without_dead_end unfold never_leaves_freedom intro h intro state apply no_freedom_implies_no_dead_end apply h
\(\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} (uf : @UtilityFunction State Action ps) (state : State) : Prop := exists! (action : Action), is_maximum uf state (uf state action).
def utilitarian_ethic_unique_maximum {ps : PreferenceSpace} (uf : @UtilityFunction State Action ps) (state : State) : Prop := ∃! (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} (uf : @UtilityFunction State Action ps) : Prop := forall (state: State), utilitarian_ethic_unique_maximum uf state.
def utilitarian_ethic_always_unique_maximum {ps : PreferenceSpace} (uf : @UtilityFunction State Action ps) : Prop := ∀ (state: State), utilitarian_ethic_unique_maximum 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 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.
theorem utilitarian_ethic_no_freedom_iff_max_for_unique_action {ps : PreferenceSpace} : ∀ (ethic: @Ethic State Action) (uf : @UtilityFunction State Action ps) (_ethic_maximizes_uf : maximizes ethic uf) (state: State), utilitarian_ethic_unique_maximum uf state ↔ leaves_no_freedom ethic state := by intro ethic intro uf intro ethic_maximizes_uf intro state unfold maximizes at ethic_maximizes_uf constructor · intro h0 unfold leaves_no_freedom unfold ExistsUnique unfold utilitarian_ethic_unique_maximum at h0 unfold ExistsUnique at h0 rcases h0 with ⟨x, h0⟩ rcases h0 with ⟨h1, h2⟩ simp at h2 exists x constructor · simp specialize ethic_maximizes_uf state specialize ethic_maximizes_uf x rw [← ethic_maximizes_uf] at h1 exact h1 · simp intro y intro h3 specialize h2 y apply h2 specialize ethic_maximizes_uf state specialize ethic_maximizes_uf y rw [← ethic_maximizes_uf] exact h3 · intro h unfold leaves_no_freedom at h unfold ExistsUnique at h unfold utilitarian_ethic_unique_maximum unfold ExistsUnique rcases h with ⟨action, h⟩ rcases h with ⟨h1, h2⟩ specialize ethic_maximizes_uf state exists action simp constructor · specialize ethic_maximizes_uf action rw [← ethic_maximizes_uf] exact h1 · intro y simp at h2 specialize h2 y intro h3 rw [← ethic_maximizes_uf] at h3 apply h2 exact h3
\(\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 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) ; tauto. Qed.
lemma utilitarian_ethic_never_freedom_iff_always_maximum_for_unique_action {ps : PreferenceSpace} : ∀ (ethic: @Ethic State Action) (uf : @UtilityFunction State Action ps) (_ethic_maximizes_uf : maximizes ethic uf), utilitarian_ethic_always_unique_maximum uf ↔ never_leaves_freedom ethic := by intro ethic intro uf intro ethic_maximizes_uf unfold utilitarian_ethic_always_unique_maximum unfold never_leaves_freedom constructor · intro h intro state specialize h state rw [← utilitarian_ethic_no_freedom_iff_max_for_unique_action ethic uf] <;> tauto · intro h intro state specialize h state rw [utilitarian_ethic_no_freedom_iff_max_for_unique_action ethic uf] <;> tauto