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 win conflicts.

Throughout this page, let \(T\) be the time, \(S\) the set of states, \(A\) the set of actions, \(I\) the set of individuals in the society and \(pt\) the physical theory we adopt. \(\mathbf{Definition}\) Let \(H = (S \times A^I)^T\) be the set of histories (let \(S = S \times A^I\) in this article). For \(t \in T, ap \in A^I\) and \(h(t) = (s, ap)\), let \(h_S(t) = s\) and \(h_{AP}(t) = ap\). \(\mathbf{Definition}\) Let \(G = {\{⊥ ,⊤\}}^H\) be the set of goals (which are events in this article with \(S = S \times A^I\)).

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

Conflicts

A goal profile is given by a goal for each individual.

\(\mathbf{Definition}\) The set \(GP\) of action profiles is \(G^I\).

	
		Definition GoalProfile : Type :=
  @Profile Individual (@Event Time (State * @Profile Individual Action)).

A conflict arises when not everyone may achieve its goal.

\(\mathbf{Definition}\) All the goals of \(gp \in GP\) may be achieved if \(\exists h \in H\) compatible with the laws of physics in which all the individual goals of \(gp\) are achieved.

	
		Definition may_achieve_all (goals : GoalProfile) :
Prop :=
  exists (history : @History Time (State * @Profile Individual Action)),
    satisfies history physical_theory /\
    forall (i : Individual), goals i history.

Someone wins a conflict when its goal is achieved. There may be more than one individual who achieves its goal.

\(\mathbf{Definition}\) An individual \(i \in I\) may win a conflict relative to goals \(gp \in GP\) if all the goals of \(gp\) may not be achieved but \(i\)’s goal \(gp(i)\) may be. An individual \(i \in I\) may not win a conflict relative to goals \(gp \in GP\) if all the goals of \(gp\) may not be achieved and \(i\)’s goal \(gp(i)\) may not either.

	
		Definition may_win_conflict (i : Individual) (goals : GoalProfile) :
Prop :=
  ~ may_achieve_all goals /\
  @is_possible Time (
    State * @Profile Individual Action
  ) (goals i)  physical_theory.

Definition may_not_win_conflict (i : Individual) (goals : GoalProfile) :
Prop :=
  ~ may_achieve_all goals /\
  @is_possible Time (State * @Profile Individual Action) (goals i) physical_theory.

Following one’s ethic

\(\mathbf{Definition}\) Everyone follows its ethic in a history \(h \in H\) for an ehtical profile \(ep\) at time \(t\) if \(\forall i \in I, ep(i)\) is followed by \(i\) in \(h\) at time \(t\). And everyone always follows its ethic in \(h\) for \(ep\) if \(\forall t \in T\) everyone follows its ethic in \(h\) for \(ep\) at time \(t\).

	
		Definition state_dynamic_to_subjective (state_d : @State_dynamic Time State)
(i : Individual) : @SubjectiveState (Time * State) Individual :=
  get_SubjectiveState (get_time state_d, get_state state_d) i.

Definition ethic_subjective_to_dynamic
(ethic_subj : @Ethic (@SubjectiveState (Time * State) Individual) Action)
(i : Individual) :
@Ethic (@State_dynamic Time State) (@Profile Individual Action) :=
  fun (state_d : @State_dynamic Time State) =>
  fun (action_profile : @Profile Individual Action) =>
  ethic_subj (
    state_dynamic_to_subjective state_d i
  ) (
    action_profile i
  ).

Definition everyone_follows_its_ethic_dynamic
(history : @History Time (State * @Profile Individual Action))
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual))
(t : Time) :
Prop :=
  forall (i : Individual),
    follows_its_ethic history (
      ethic_subjective_to_dynamic (ethical_profile i) i
    ) t.

Definition everyone_always_follows_its_ethic_dynamic
(history : @History Time (State * @Profile Individual Action))
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual)) :
Prop :=
  forall (i : Individual), always_follows_its_ethic history (
    ethic_subjective_to_dynamic (ethical_profile i) i
  ).

\mathbf{Definition}\) All the goals of \(gp \in GP\) may be achieved according to \(ep \in EP\) if there is a history \(h \in H\) compatible with the laws of physics in which: - \(\forall i \in I, gp(i)\) happens in \(h\) - Everyone always follows its ethic in \(h\) for \(ep

	
		Definition may_all_achieve_ethically (goals : GoalProfile)
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual)) :
Prop :=
  exists (history : @History Time (State * @Profile Individual Action)),
    satisfies history physical_theory /\
    forall (i : Individual), happens_in (goals i) history /\
    everyone_always_follows_its_ethic_dynamic history ethical_profile.

\mathbf{Definition}\) An individual \(i \in I\) may achieve a goal \(g \in G\) according to \(ep \in EP\) if there is a history \(h \in H\) compatible with the laws of physics in which: - \(gp(i)\) happens in \(h\) - Everyone always follows its ethic in \(h\) for \(ep

	
		Definition may_achieve_with_ethics (i : Individual)
(goal : @Event Time (State * @Profile Individual Action))
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual)) :
Prop :=
  exists (history : @History Time (State * @Profile Individual Action)),
    satisfies history physical_theory /\
    happens_in goal history /\
    everyone_always_follows_its_ethic_dynamic history ethical_profile.

Restrictiveness and conflict achieving

Winning a conflict ethically means here winning a conflict while everyone follows its own ethic.

\(\mathbf{Definition}\) An individual \(i \in I\) may win a conflict relative to goals \(gp \in GP\) according to \(ep \in EP\) if not all the goals of \(gp\) may be achieved according to \(ep\) but \(i\) may achieve its goal \(gp(i)\) according to \(ep\). And it may not win a conflict relative to goals \(gp \in GP\) according to \(ep \in EP\) if not all the goals of \(gp\) may be achieved according to \(ep\) and \(i\) may not achieve its goal \(gp(i)\) according to \(ep\).

	
		Definition may_win_conflict_with_ethics (i : Individual)
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual))
(goals : GoalProfile) :
Prop :=
  ~ may_all_achieve_ethically goals ethical_profile /\
  may_achieve_with_ethics i (goals i) ethical_profile.

Definition may_not_win_conflict_with_ethics (i : Individual)
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual))
(goals : GoalProfile) :
Prop :=
  ~ may_all_achieve_ethically goals ethical_profile /\
  ~ may_achieve_with_ethics i (goals i) ethical_profile.

Winning a conflict ethically means here winning a conflict while everyone follows its own ethic.

\(\mathbf{Lemma}\) Let \(i \in I\) an individual, \(goals \in GP\) a goal profile, \(ep \in EP\) an ethical profile and \(e\) an ethic such that \(ep(i)\) is more restrictive than \(e\). If \(i\) may achieve \(gp(i)\) according to \(ep\), \(i\) may still achieve \(gp(i)\) replacing its ethic \(ep(i)\) with \(e\). \(\mathbf{proof:}\) Let \(h\) a history \(h \in H\) compatible with the laws of physics in which: - \(gp(i)\) happens in \(h\) - Everyone always follows its ethic in \(h\) for \(ep\) It suffices to show that everyone always follows its ethic in \(h\) for \(ep_{i/e}\). All the individuals but \(i\) definitely do so as their ethic is unchanged. And so does \(i\) because \(ep(i)\) is more restrictive than \(e\). ■

	
		Lemma ethic_restricts_goal_achieving_with_ethics (i : Individual)
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual))
(relaxed_ethic : @Ethic (@SubjectiveState (Time * State) Individual) Action)
(goals : GoalProfile) :
  @more_restrictive_dynamic Time State (@Profile Individual Action) (
    ethic_subjective_to_dynamic (ethical_profile i) i
  ) (
    ethic_subjective_to_dynamic relaxed_ethic i
  ) ->
  may_achieve_with_ethics i (goals i) ethical_profile ->
  may_achieve_with_ethics i (goals i) (
    replace ethical_profile i (
      relaxed_ethic
    )
  ).
Proof.
  unfold may_achieve_with_ethics.
  intros.
  destruct H0 as [history]. destruct H0. destruct H1.
  exists history.
  split.
  { exact H0. }
  split.
  { exact H1. }
  {
    unfold everyone_always_follows_its_ethic_dynamic in *.
    intro.
    unfold always_follows_its_ethic in *.
    intro.
    generalize dependent H2. intro.
    unfold follows_its_ethic in *.
    unfold more_restrictive_dynamic in H.
    specialize (H t). specialize (H (history t).1).
    unfold more_restrictive in H.
    specialize (H (history t).2).
    assert (i0 = i \/ i0 <> i). { apply classic. }
    destruct H3.
    {
      rewrite H3.
      rewrite replace_changes.
      apply H.
      specialize (H2 i t).
      exact H2.
    }
    {
      rewrite replace_unchanges.
      2: { intro. rewrite H4 in H3. apply H3. reflexivity. }
      specialize (H2 i0). specialize (H2 t).
      exact H2.
    }
  }
Qed.

Winning a conflict ethically means here winning a conflict while everyone follows its own ethic.

\(\mathbf{Corollary}\) Let \(i \in I\) an individual, \(goals \in GP\) a goal profile, \(ep \in EP\) an ethical profile and \(e\) an ethic such that \(ep(i)\) is more restrictive than \(e\). If \(i\) may win a conflict relative to goals \(gp \in GP\) according to \(ep\), \(i\) still may achieve \(gp(i)\) replacing its ethic \(ep(i)\) with \(e\). \(\mathbf{proof:}\) By definition of winning a conflict, we have \(i\) who may achieve its goal \(gp(i)\) according to \(ep\). Then we just have to apply the previous lemma. ■

	
		Lemma ethic_restricts_conflict_winning (i : Individual)
(ethical_profile : @Profile Individual (@IndividualEthic (Time * State) Action Individual))
(relaxed_ethic : @Ethic (@SubjectiveState (Time * State) Individual) Action)
(goals : GoalProfile) :
  @more_restrictive_dynamic Time State (@Profile Individual Action) (
    ethic_subjective_to_dynamic (ethical_profile i) i
  ) (
    ethic_subjective_to_dynamic relaxed_ethic i
  ) ->
  may_win_conflict_with_ethics i ethical_profile goals ->
  may_achieve_with_ethics i (goals i) (
    replace ethical_profile i (
      relaxed_ethic
    )
  ).
Proof.
  intros.
  unfold may_win_conflict_with_ethics in H0.
  destruct H0.
  apply ethic_restricts_goal_achieving_with_ethics ; try tauto.
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.