Leibniz' Project
In a society composed of individuals, it is proved here with given definitions that the more individuals have a restrictive in their personnal ethic, the less likely conflicts are.
One relies on this article.
Throughout this page, let \(I\) be the finite set of individuals of a society, \(S\) be the set of states, \(A\) be the set of actions, \(SubjS = S × I\) be the set of subjective states and \(E = \{⊤, ⊥\}^{SubjS \times A}\) the set of ethics.
Context {State : Type}. Context {Action : Type}. Context {Individual : finType}.
We introduce the notion of practical fesability. For example, it’s not possible that 30 persons simultaneously sit on a public bench.
\(\mathbf{Definition}\)
Let \(feasible\) be a function
which at each \(s \in S, (a_i) \in
A^I\) associates \(⊥\) if
it’s not concretely possible that each individuals \(i\) does the \(a_i\) action and \(⊤\) if it is.
\(\mathbf{Definition}\)
An action profile \((a_i) \in
A^I\) is said compatible in state \(s \in S\) if \(feasible(s, (a_i)) = ⊤\) and
incompatible if \(feasible(s, (a_i)) =
⊥\).
\(\mathbf{Definition}\)
\(feasible\) is said to involve
constraints in \(s\) if \(\exists (a_i) \in A^I, \neg feasible(s,
(a_i))\).
Context {feasible : State -> @ActionProfile Action Individual -> bool}. Definition compatible (ap : @ActionProfile Action Individual) (state : State) : Prop := feasible state ap = true. Definition incompatible (ap : @ActionProfile Action Individual) (state : State) : Prop := feasible state ap = false. Definition with_constraints (feasible : State -> @ActionProfile Action Individual -> bool) (state : State) : Prop := exists (ap : @ActionProfile Action Individual), incompatible ap state.
If everyone can follow its own ethic then no one is an ethical dead end.
\(\mathbf{Definition}\)
Let \(s \in S, (e_i) \in E^I, (a_i) \in
A^I\). We say that everyone follows its ethic if \(\forall i \in I, e_i((s, i),
a_i)\).
\(\mathbf{Lemma\text{
}1}\)
Let $s S, (e_i) E^I, (a_i) A^I. If every individual follows its
own ethic, then none of them is in an ethical dead end.
\(\mathbf{proof:}\)
Let \(s \in S\) and \(i \in I\).
As \(i\) follows its own ethic,
there is an \(a \in A\) such that
\(e_i((s, i), a_i)\), so \(i\) is not in an ethical dead
end.
■
Definition everyone_follows_its_ethic (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : Prop := forall (i : Individual), ep i (get_SubjectiveState state i) (ap i) = true. Lemma no_dead_end_if_everyone_follows_its_ethic (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : everyone_follows_its_ethic ep ap state -> forall (i : Individual), ~ dead_end (ep i) (get_SubjectiveState state i). Proof. unfold everyone_follows_its_ethic. intros. unfold dead_end. specialize (H i). apply ex_not_not_all. exists (ap i). rewrite H. intuition. Qed.
A conflict occurs when not every individual (following its own ethic) can do the action (s)he wants.
\(\mathbf{Definition}\)
Let \(s \in S, (e_i) \in E^I, (a_i) \in
A^I\). There is a conflict if \[\begin{cases*}
\neg feasible(s, (a_i)) \\
\text{ everyone follows its ethic }
\end{cases*}\] There is no conflict if \[\begin{cases*}
feasible(s, (a_i)) \\
\text{ everyone follows its ethic }
\end{cases*}\]
Definition conflict (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : Prop := feasible state ap = false /\ everyone_follows_its_ethic ep ap state. Definition no_conflict (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : Prop := feasible state ap = true /\ everyone_follows_its_ethic ep ap state.
Conflict (and the absence of conflict) presuppose that everyone follows its own ethic, which is possible only if no one is an ethical dead end.
\(\mathbf{Lemma\text{
}2}\)
If there is a conflict, then no individual is in an ethical dead
end.
If there is no conflict, then no individual is in an ethical dead
end.
\(\mathbf{proof:}\)
Let \(s \in S\) and \(i \in I\).
In both cases, everyone follows its own ethic by definition, and
we conclude with the previous lemma.
■
Definition no_dead_end_if_conflict (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : conflict ep ap state -> forall (i : Individual), ~ dead_end (ep i) (get_SubjectiveState state i). Proof. unfold conflict. intro. destruct H. apply no_dead_end_if_everyone_follows_its_ethic with (ap:=ap). exact H0. Qed. Definition no_dead_end_if_no_conflict (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (state : State) : no_conflict ep ap state -> forall (i : Individual), ~ dead_end (ep i) (get_SubjectiveState state i). Proof. unfold no_conflict. intro. destruct H. apply no_dead_end_if_everyone_follows_its_ethic with (ap:=ap). exact H0. Qed.
If an individual ethic is replaced with a more restrictive one, this can’t create a conflict.
\(\mathbf{Proposition}\)
Let \(s \in S, (e_i) \in E^I, (a_i) \in
A^I, j \in I, e \in E\). If \(e_j\) is more restrictive than \(e\) and \(s, (e_i), (a_i)\) conflict, then
\(s, (e_i)_{j/e}, (a_i)\)
conflict.
\(\mathbf{proof:}\)
As \(s, (e_i), (a_i)\) conflict,
we have \(\neg feasible(s,
(a_i))\) and \(\forall i \in I,
e_i((s, i), a_i)\) by definition.
As \(e_j\) is more restrictive
than \(e\), we have \(e((s, j), a_j)\).
We can cconclude that \(s, (e_i)_{j/e},
(a_i)\) conflict.
■
Proposition more_restrictive_ethic_diminishes_conflicts (ep : EthicalProfile) (ap : @ActionProfile Action Individual) (i : Individual) (ethic : @IndividualEthic State Action Individual) (state : State) : more_restrictive (ep i) ethic (get_SubjectiveState state i) -> conflict ep ap state -> conflict (replace ep i ethic) ap state. Proof. intros. unfold conflict in *. destruct H0. split. { apply H0. } intro. assert (i0 = i \/ i0 <> i). { apply classic. } destruct H2. { rewrite H2. unfold more_restrictive in H. pose proof (H (ap i)). rewrite replace_changes. apply H3. apply H1. } { rewrite replace_unchanges. { apply H1. } { intro. rewrite H3 in H2. apply H2. reflexivity. } } Qed.
And if not everything is feasible, one can create a conflict by unrestricting a single individual ethic.
\(\mathbf{Proposition}\)
Let \(j \in I\). If \(feasible\) involves constraints, then
\(\exists s \in S, (e_i) \in E^I, (a_i)
\in A^I, e \in E,\) such that \[\begin{cases*}
e_j \text{ is more restrictive than } e \text{ in subjective
state } (s, j) \\
(e_i), (a_i) \text{ don't conflict in } s \\
(e_i)_{j/e}, (a_i) \text{ conflict in } s
\end{cases*}\]
\(\mathbf{proof:}\)
Let \(s \in S, (a_i) \in A^I\)
unfeasible.
Let \((e_i) \in E^I\) defined in
\(s\) by (whatever state and
action) \[\begin{cases*}
⊥ \text{ if } i = j \\
⊤ \text{ otherwise }
\end{cases*}\] Then, as \(j\) doesn’t act accordingly to its
ethic, \((e_i), (a_i)\) don’t
conflict in \(s\).
Let \(e \in E\) defined by \(e((s, i), a) = ⊤ \text{ } \forall (s, i) \in
SubjS, a \in A\).
Then, as \(e\) allows everything,
\(e_j\) is more restrictive than
\(e\).
Now, \((e_i)_{j/e}((s, i), a) = ⊤ \text{
} \forall (s, i) \in SubjS, a \in A\), which creates a
conflict together with the fact that \(s, (a_i)\) is not feasible.
■
Proposition more_restrictive_ethic_strictly_diminishes_conflicts (state : State) (i : Individual) : with_constraints feasible state -> exists (ap : @ActionProfile Action Individual) (ep : EthicalProfile) (ethic : @IndividualEthic State Action Individual), strictly_more_restrictive (ep i) ethic (get_SubjectiveState state i) /\ ~ conflict ep ap state /\ conflict (replace ep i ethic) ap state. Proof. intro. unfold with_constraints in H. destruct H as [ap]. exists (ap). exists ( fun (j : Individual) => fun (subj_state : SubjectiveState) => fun (action : Action) => if j == i then false else true ). exists ( fun (subj_state : SubjectiveState) => fun (action : Action) => true ). split. { unfold strictly_more_restrictive. split. { unfold more_restrictive. intro. reflexivity. } { exists (ap i). split. { rewrite eq_refl. reflexivity. } { reflexivity. } } } unfold conflict. split. { intro. destruct H0. pose proof (H1 i). rewrite eq_refl in H2. inversion H2. } split. { tauto. } { intro. assert (i0 = i \/ i0 <> i). { apply classic. } destruct H0. { rewrite H0. rewrite replace_changes. reflexivity. } { rewrite replace_unchanges. { assert (i0 == i = false). { by apply/eqP. } rewrite H1. reflexivity. } { intro. rewrite H1 in H0. apply H0. reflexivity. } } } Qed.
