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.
Require Import Logic.Classical_Pred_Type.
Require Import Logic.FunctionalExtensionality.
From mathcomp Require Import all_ssreflect.
Require Import ethics_first_steps.
Require Import objective_ethics_no_disapproval_iff_same_ethic.
Require Import more_resrtictive_ethics_diminish_conflicts.
Definition Action : eqType := ethics_first_steps.Action.
Definition Individual : finType :=
more_resrtictive_ethics_diminish_conflicts.Individual.
Definition feasible : State -> ActionProfile -> bool :=
more_resrtictive_ethics_diminish_conflicts.feasible.
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) : EthicalProfile :=
fun (i : Individual) => e.
Definition altruist (e : IndividualEthic) (state : State) : Prop :=
exists (ap : ActionProfile), no_conflict (generalized_whole_society e) ap state.
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 : ActionProfile),
ap i = a_i ->
ap j = a_j ->
feasible state ap = false
) /\ (
exists (ap : ActionProfile),
ap i = a_i /\
ap j = b_j /\
feasible state ap = true
) /\ (
exists (ap : ActionProfile),
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 : ActionProfile),
conflict 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 ; rewrite 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 Di0i.
rewrite eq_refl.
reflexivity.
}
{
rewrite Di0i.
destruct (i0 == j) eqn: Di0j.
{
rewrite Di0j.
rewrite eq_refl.
reflexivity.
}
{
rewrite Di0j.
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 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.
}
{
rewrite Di0j.
reflexivity.
}
}
{
rewrite Di0i.
destruct (i0 == j) eqn: Di0j.
{
rewrite Di0j.
rewrite eq_refl.
reflexivity.
}
{
rewrite Di0j.
reflexivity.
}
}
}
}
}
Qed.