Leibniz' Project
In a society composed of at least two individuals, it is proved here with given definitions that even if every individual is altruist, conflicts still happen.
One relies on this article.
Throughout this page, let \(I\) be the finite set of individuals of a society containing at least two of them, \(S\) be the set of states, \(A\) be the set of actions, \(SubjStates = S × I\) be the set of individual states and \(E = \{⊤, ⊥\}^{SubjStates \times A}\) the set of ethics. \(feasible: S × A^I -> \{⊤, ⊥\}\) is the function of practical feasibility.
Context {State : Type}. Context {Action : eqType}. Context {Individual : finType}. Context {feasible : State -> @ActionPerIndividual Action Individual -> bool}.
We define altruism of an individual \(i\) as the fact that if everyone did like \(i\), there would be no conflict. This is not the usual definition of altruism. If you have a better name for this concept, propose it in Github.
\(\mathbf{Definition}\)
Generalizing an individual ethic \(e\) to the whole society is the fact
to consider that every individual has ethic \(e\).
\(\mathbf{Definition}\)
An ethic \(e\) is said altruist
in \(s\) if \(\exists (a_i) \in A^I\) such that
there is no conflict if \(e\) is
generalized to the whole society.
Definition generalized_whole_society (e : @IndividualEthic State Action Individual) : EthicalProfile := fun (i : Individual) => e. Definition altruist (e : @IndividualEthic State Action Individual) (state : State) : Prop := exists (ap : @ActionPerIndividual Action Individual), @no_conflict State Action Individual feasible ( generalized_whole_society e ) ap state.
If there is an altruist ethic, then no one is in an ethical dead end (as everyone can follow this altruist ethic)
\(\mathbf{Lemma}\)
Let \(e \in E\) be an altruist
ethic in \(s \in S\). Then no
individual is in a dead end.
\(\mathbf{proof:}\)
Let \((a_i) \in A^I\) such that
there is no conflict if \(e\). We
conclude with Lemma
2 in this article.
■
Lemma no_dead_end_if_altruist (e : @IndividualEthic State Action Individual) (state : State) : altruist e state -> forall (i : Individual), ~ dead_end e (get_SubjectiveState state i). Proof. intros. unfold altruist in H. destruct H as [ap]. unfold generalized_whole_society in H. assert (~ dead_end ((fun (i : Individual) => e) i) (get_SubjectiveState state i)). { apply (@no_dead_end_if_no_conflict State Action Individual feasible ( fun (i : Individual) => e ) ap state). exact H. } simpl in H0. exact H0. Qed.
A bipartite contest is a situation where two individuals can do two conflictual actions (regardless of how act the other individuals) but things can work out if one of them gives up his action. For example, two individuals may want to seat on a chair in a public garden; this creates a conflict, unless one of them lets the chair to the other one.
\(\mathbf{Definition}\)
Let \(s\) be a state and \(i \neq j\) two individuals. There’s a
bipartite contest between \(i\)
and \(j\) over actions \(a_i, a_j\) with possible
renunciations \(b_i, b_j\) if
\[\begin{cases*}
\forall (ap_k) \in A^I \text{ such that } ap_i = a_i \text{ and
} ap_j = a_j \text{, we have } \neg feasible(s, (ap_k)) \\
\exists (ap_k) \in A^I \text{ such that } ap_i = a_i, ap_j = b_j
\text{ and } feasible(s, (ap_k)) \quad \text{(case $j$ gives up)}
\\
\exists (ap_k) \in A^I \text{ such that } ap_i = b_i, ap_j = a_j
\text{ and } feasible(s, (ap_k)) \quad \text{(case $i$ gives up)}
\end{cases*}\]
Definition bipartite_contest (state : State) (i j : Individual) (a_i a_j b_i b_j : Action) : Prop := i <> j /\ ( forall (ap : @ActionPerIndividual Action Individual), ap i = a_i -> ap j = a_j -> feasible state ap = false ) /\ ( exists (ap : @ActionPerIndividual Action Individual), ap i = a_i /\ ap j = b_j /\ feasible state ap = true ) /\ ( exists (ap : @ActionPerIndividual Action Individual), ap i = b_i /\ ap j = a_j /\ feasible state ap = true ).
In our example of bipartite contest, the first individual may think something like “the oldest should be given the seat” and the second one something like “first come first served”. Both opinions permit to avoid conflicts if everyone shares them, but there is still a conflict if the first individual is older than the second one.
\(\mathbf{Proposition}\)
In a state \(s\), if there a
bipartite contest between individuals \(i\) and \(j\) over actions \(a_i, a_j\) with possible
renunciations \(b_i, b_j\), then
there exists \((e_k) \in E^I, (ap_k) \in
A^I\) such that \[\begin{cases*}
\forall k \in I,e_k \text{ is altruist} \\
\text{ there is a conflict }
\end{cases*}\]
\(\mathbf{proof:}\)
Let \((e_k) \in E^I\) defined by
\[\begin{cases*}
e_i((s, i), a_i) = ⊤, e_i((s, i), b_i) = ⊤ \text { and } e_i((s,
i), a) = ⊥ \text{ for all other actions } a \\
e_i((s, j), b_j) = ⊤ \text { and } e_i((s, j), a) = ⊥ \text{ for
all other actions } a \\
e_i((s, k), a) = ⊤ \text{ for other } k \text{'s and all
actions } a \\
\text{ if } k \neq i, \\
e_k((s, j), a_j) = ⊤, e_k((s, j), b_j) = ⊤ \text { and } e_k((s,
j), a) = ⊥ \text{ for all other actions } a \\
e_k((s, i), b_i) = ⊤ \text { and } e_k((s, i), a) = ⊥ \text{ for
all other actions } a \\
e_k((s, l), a) = ⊤ \text{ for other } l \text{'s and all
actions } a
\end{cases*}\] Let \((ap_k) \in
A^I\) defined by \[\begin{cases*}
ap_i = a_i \\
ap_k = a_j \text{ for other } k \text{'s}
\end{cases*}\] - Let’s prove firstly that there is a
conflict. The unfeasability comes from the definitions of \((ap_k)\) and bipartite conflict (the
first of the three assertions). The fact that everyone follows its
ethic flows directly from the definitions of \((e_k)\) and \((ap_k)\).
- Let’s now conclude by proving that every individual is
altruist.
\(\quad\) For individual \(i\), the following action profile
\((api_k)\) permits to avoid a
conflict: \[\begin{cases*}
api_i = a_i \\
api_j = b_j \\
api_k \text{ is given by the definition of bipartite contest
(the second of the three assertions) }
\end{cases*}\] \(\quad\) For other individuals, the
following action profile \((apl_k)\) permits to avoid a
conflict: \[\begin{cases*}
api_i = b_i \\
api_j = a_j \\
api_k \text{ is given by the definition of bipartite contest
(the third of the three assertions) }
\end{cases*}\] ■
Proposition unanimous_altruism_not_enough_to_avoid_conflicts (state : State) : ( exists (i j : Individual) (a_i a_j b_i b_j : Action), bipartite_contest state i j a_i a_j b_i b_j ) -> ( exists (ep : EthicalProfile) (ap : @ActionPerIndividual Action Individual), @conflict State Action Individual feasible ep ap state /\ forall (k : Individual), altruist (ep k) state ). Proof. intro. destruct H as [i]. destruct H as [j]. destruct H as [a_i]. destruct H as [a_j]. destruct H as [b_i]. destruct H as [b_j]. exists ( fun (k : Individual) => fun (subj_state : SubjectiveState) => fun (action : Action) => if (k == i) then ( if (subj_state.(individual) == i) then ( if (action == a_i) then true else if (action == b_i) then true else false ) else if (subj_state.(individual) == j) then ( if (action == b_j) then true else false ) else true ) else ( if (subj_state.(individual) == j) then ( if (action == a_j) then true else if (action == b_j) then true else false ) else if (subj_state.(individual) == i) then ( if (action == b_i) then true else false ) else true ) ). exists ( fun (k : Individual) => if (k == i) then a_i else a_j ). split. { unfold conflict. split. { unfold bipartite_contest in H. destruct H. unfold not in H. assert ((i == j) = false). { by apply/eqP. } destruct H0. apply H0. { rewrite eq_refl. reflexivity. } { rewrite eq_sym. rewrite H1. reflexivity. } } { unfold everyone_follows_its_ethic. intro. destruct (i0 == i) eqn:Di0i. { rewrite Di0i. rewrite eq_refl. reflexivity. } { rewrite Di0i. rewrite eq_refl. rewrite proj_individual_SubjectiveState. destruct (i0 == j) eqn:Di0j ; reflexivity. } } } { intro. unfold altruist. unfold bipartite_contest in H. destruct H. destruct H0. destruct H1. destruct (k == i) eqn:Dki. { destruct H1 as [ap]. exists ( fun (k : Individual) => if (k == i) then a_i else if (k == j) then b_j else ap k ). unfold no_conflict. destruct H1. destruct H3. split. { rewrite <- H1. rewrite <- H3. assert ( (fun k0 : Individual => if k0 == i then ap i else if k0 == j then ap j else ap k0) = ap ). { apply functional_extensionality. intro. destruct (x == i) eqn:Dxi. { assert (x = i). { by apply/eqP. } rewrite H5. reflexivity. } { destruct (x == j) eqn:Dxj. { assert (x = j). { by apply/eqP. } rewrite H5. reflexivity. } reflexivity. } } rewrite H5. apply H4. } { unfold everyone_follows_its_ethic. intro. unfold generalized_whole_society. rewrite proj_individual_SubjectiveState. destruct (i0 == i) eqn: Di0i. { rewrite eq_refl. reflexivity. } { destruct (i0 == j) eqn: Di0j. { rewrite eq_refl. reflexivity. } { reflexivity. } } } } { destruct H2 as [ap]. exists ( fun (k : Individual) => if (k == i) then b_i else if (k == j) then a_j else ap k ). unfold no_conflict. destruct H2. destruct H3. split. { rewrite <- H2. rewrite <- H3. assert ( (fun k0 : Individual => if k0 == i then ap i else if k0 == j then ap j else ap k0) = ap ). { apply functional_extensionality. intro. destruct (x == i) eqn:Dxi. { assert (x = i). { by apply/eqP. } rewrite H5. reflexivity. } { destruct (x == j) eqn:Dxj. { assert (x = j). { by apply/eqP. } rewrite H5. reflexivity. } reflexivity. } } rewrite H5. apply H4. } { unfold everyone_follows_its_ethic. intro. unfold generalized_whole_society. rewrite proj_individual_SubjectiveState. destruct (i0 == i) eqn: Di0i. { rewrite eq_refl. destruct (i0 == j) eqn: Di0j. { assert (i0 = i). { by apply/eqP. } assert (i0 = j). { by apply/eqP. } assert (i = j). { rewrite <- H5. rewrite <- H6. reflexivity. } exfalso. apply H in H7. inversion H7. } { reflexivity. } } { destruct (i0 == j) eqn: Di0j. { rewrite eq_refl. reflexivity. } { reflexivity. } } } } } Qed.
