Leibniz' Project

Presentation

The present article formalizes the fact that, the more you’re ethical, the less room to maneuver you have and the less easy it is to reach your goals.

One relies on this article and this article.

Throughout this page, let \(T\) be the time, \(S\) the set of states, \(A\) the set of actions and \(pt\) the physical theory we adopt. \(\mathbf{Definition}\) Let \(SD = T \times S\) be the set of states in a dynamic environment. For \(sd = (t, s) \in SD\), let \(sd_T(sd) = t\) and \(sd_S(sd) = s\). \(\mathbf{Definition}\) Let \(E = {\{⊥ ,⊤\}}^{SD × A}\) be the set of ethics (let \(S = SD\) in this article). \(\mathbf{Definition}\) Let \(H = (S \times A)^T\) be the set of histories (let \(S = S \times A\) in this article). For \(t \in T\) and \(h(t) = (s, a)\), let \(h_S(t) = s\) and \(h_A(t) = a\). \(\mathbf{Definition}\) Let \(G = {\{⊥ ,⊤\}}^H\) be the set of goals (which are events in this article with \(S = S \times A\)).

	
		Context {Time : Type}.
Context {State : Type}.
Context {Action : Type}.
Context {physical_theory : @PhysicalTheory Time (State * Action)}.

Definition State_dynamic : Type := Time * State.

Definition get_time (state : State_dynamic) : Time :=
  fst state.

Definition get_state (state : State_dynamic) : State :=
  snd state.

Definition state_dynamic (t : Time) (state : State) : State_dynamic :=
  (t, state).

Ethics can’t help to achieve goals

\(\mathbf{Definition}\) An ethic \(e \in E\) is followed in a history \(h \in H\) at time \(t \in T\) if \(e((t, h_S(t)), h_A(t)) = ⊤\). An ethic \(e \in E\) is always followed in a history \(h \in H\) if \(\forall t \in T, e((t, h_S(t)), h_A(t)) = ⊤\). \(\mathbf{Definition}\) A \(g \in G\) may be achieved ethically with \(e \in E\) if there is a history compatible with the laws of physics in which \(g\) happens and \(e\) is always followed.

	
		Definition follows_its_ethic (history : @History Time (State * Action))
(ethic : @Ethic State_dynamic Action) (t : Time) : Prop :=
  ethic (
    (t, fst (history t))
  ) (
    snd (history t)
  ).

Definition always_follows_its_ethic (history : @History Time (State * Action))
(ethic :@Ethic State_dynamic Action) : Prop :=
  forall (t : Time), follows_its_ethic history ethic t.

Definition may_achieve_ethically (goal : @Event Time (State * Action))
(ethic : @Ethic State_dynamic Action) : Prop :=
  exists (history : @History Time (State * Action)),
    satisfies history physical_theory /\
    goal history = true /\
    always_follows_its_ethic history ethic.

If you may achieve a goal with your ethic, you may without as well.

\(\mathbf{Lemma}\) Let \(g \in G\) a goal and \(e \in E\) an ethic. If \(g\) may be achieved ethically with \(e\), then \(g\) may be achieved. \(\mathbf{proof:}\) Obvious: the history given by the ethical achievement also works for the ethicless achievement. ■

	
		Lemma ethics_cant_help_goal_achieving
(goal : @Event Time (State * Action)) (ethic : @Ethic State_dynamic Action) :
  may_achieve_ethically goal ethic ->
  @is_possible Time (State * Action) goal physical_theory.
Proof.
  intros.
  unfold may_achieve_ethically in H. unfold is_possible.
  destruct H as [history]. exists history.
  tauto.
Qed.

Restrictiveness and goal achieving

An ethic is more restrictive than an other if all the actions it allows are also allowed by the other, whatever the moment and the situation.

\(\mathbf{Definition}\) An ethic \(e_1 \in E\) is said more restrictive than \(e_2 \in E\) in a state \(s \in S\) if \(\forall t \in T, s \in S, e_1\) is more restrictive than \(e_2\) at time \(t\) and state \(s\) (see this article). And \(e_1\) is said strictly more restrictive than \(e_2\) if \(e_1\) is more restrictive than \(e_2\) and \(\exists t \in T, s \in S e_1(s, a) = ⊥\) and \(e_2(s, a) = ⊤\).

	
		Definition more_restrictive_dynamic (e1 e2 : @Ethic State_dynamic Action) : Prop :=
  forall (t : Time) (state : State), more_restrictive e1 e2 (
    state_dynamic t state
  ).

Definition strictly_more_restrictive_dynamic
(e1 e2 : @Ethic State_dynamic Action) : Prop :=
  more_restrictive_dynamic e1 e2 /\
  exists (t : Time) (state : State) (action : Action),
    e1 (state_dynamic t state) action = false /\
    e2 (state_dynamic t state) action = true.

If you may achieve a goal with your ethic, you may with a less restrictive one as well.

\(\mathbf{Lemma}\) Let \(g \in G\) a goal and \(e_1, e_2 \in E\) ethics such that \(e_1\) is more restrictive than \(e_2\). If \(g\) may be achieved ethically with \(e_1\), then \(g\) may be achieved ethically with \(e_2\). \(\mathbf{proof:}\) As \(g\) may be achieved ethically with \(e_1\), let \(h\) a history compatible with the laws of physics in which \(g\) happens and \(e_1\) is always followed. It suffices to show that \(e_2\) is always followed in \(h\), which is true because \(e_1\) is more restrictive than \(e_2\). ■

	
		Lemma ethic_restricts_goal_achieving (goal : @Event Time (State * Action))
(e1 e2 : @Ethic State_dynamic Action) :
  more_restrictive_dynamic e1 e2 ->
  may_achieve_ethically goal e1 ->
  may_achieve_ethically goal e2.
Proof.
  unfold may_achieve_ethically. intros.
  destruct H0 as [history]. exists history.
  destruct H0. destruct H1.
  split.
  { exact H0. }
  split.
  { exact H1. }
  {
    unfold more_restrictive_dynamic in H. unfold more_restrictive in H.
    unfold always_follows_its_ethic in *.
    intro. specialize (H2 t). specialize (H t).
    unfold follows_its_ethic in *.
    specialize (H (history t).1).
    specialize (H (history t).2).
    tauto.
  }
Qed.

If a goal may be achieved, it may be achieved with a void ethic (that is an ethic which allows everything).

\(\mathbf{Lemma}\) Let \(g \in G\) a goal which may be achieved. Then it may be achieved with the void ethic (see this article). \(\mathbf{proof:}\) As \(g\) may be achieved, let \(h\) a history compatible with the laws of physics in which \(g\) happens. Then the void ethic is satisfied by every history, so by \(h\) in particular. ■

	
		Lemma ethic_strictly_restricts_goal_achieving
(goal : @Event Time (State * Action)) :
  @is_possible Time (State * Action) goal physical_theory ->
  may_achieve_ethically goal ethicless.
Proof.
  intro.
  destruct H as [history]. destruct H.
  unfold may_achieve_ethically. exists history.
  split.
  { exact H. }
  split.
  { exact H0. }
  {
    unfold always_follows_its_ethic. intro.
    unfold follows_its_ethic.
    reflexivity.
  }
Qed.

The proofs' code is currently in . To switch to , click on the following icon:

You can check the Rocq code there and the Lean4 code there.