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, \(SubjStates = \{{s, i)\}_{s \in S, i \in I}\) be the set of individual states and \(E = \{⊤, ⊥\}^{SubjStates \times A}\) the set of ethics.
Require Import Bool.Bool.
Import BoolNotations.
From mathcomp Require Import all_ssreflect.
Require Import objective_ethics_no_disapproval_iff_same_ethic.
Definition Individual : finType :=
objective_ethics_no_disapproval_iff_same_ethic.Individual.
An ethic is more restrictive than another if it allows fewer actions.
\(\mathbf{Definition}\)
Let \(e_1, e_2\) be individual
ethics. \(e_1\) is said more
restrictive than \(e_2\) in state
\((s, k)\) if \(\forall a \in A, e_1((s, k), a) \implies
e_2((s, k), a)\).
Definition more_restrictive (e1 e2 : IndividualEthic)
(subj_state : SubjectiveState) : Prop :=
forall (action : Action),
e1 subj_state action = true -> e2 subj_state action = true.
An ethic is strictly more restrictive than another if it allows strictly fewer actions.
\(\mathbf{Definition}\)
Let \(e_1, e_2\) be individual
ethics. \(e_1\) is said strictly
more restrictive than \(e_2\) in
state \((s, k)\) if it’s more
restrictive, \(\exists a \in A, e_1((s,
k), a) = ⊥\) and \(e_2((s, k), a)
= ⊤\).
Definition strictly_more_restrictive (e1 e2 : IndividualEthic)
(subj_state : SubjectiveState) : Prop :=
more_restrictive e1 e2 subj_state /\
exists (action : Action),
e1 subj_state action = false /\ e2 subj_state action = true.
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}\)
\(feasible\) is said to involve
constraints in \(s\) if \(\exists (a_i) \in A^I, \neg feasible(s,
(a_i))\).
Definition ActionProfile : Type := Individual -> Action.
Context {feasible : State -> ActionProfile -> bool}.
Definition with_constraints (feasible : State -> ActionProfile -> bool)
(state : State) : Prop :=
exists (ap : ActionProfile), feasible state ap = false.
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\). We say that everyone follows its ethic if \(\forall i \in I, e_i((s, i),
a_i)\).
\(\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*}\]
Definition everyone_follows_its_ethic (ep : EthicalProfile) (ap : ActionProfile)
(state : State) : Prop :=
forall (i : Individual), ep i (get_SubjectiveState state i) (ap i) = true.
Definition conflict (ep : EthicalProfile) (ap : ActionProfile)
(state : State) : Prop :=
feasible state ap = false /\
everyone_follows_its_ethic ep ap state.
Definition no_conflict (ep : EthicalProfile) (ap : ActionProfile)
(state : State) : Prop :=
feasible state ap = true /\
everyone_follows_its_ethic ep ap state.
\(\mathbf{Definition}\)
Let \(s(e_i) \in E^I, e \in E\).
For some \(j \in I\), replacing
\(e_j\) with \(e\) in \((e_i)\) results in \((e_i)_{j/e}\).
Definition replace_individual_ethic (ep : EthicalProfile) (i : Individual)
(ethic : IndividualEthic) : EthicalProfile :=
fun (j : Individual) => if j == i then ethic else ep j.
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) (i : Individual) (ethic : IndividualEthic) (state : State) :
more_restrictive (ep i) ethic (get_SubjectiveState state i) ->
conflict ep ap state ->
conflict (replace_individual_ethic ep i ethic) ap state.
Proof.
intros. unfold conflict in *.
destruct H0. split.
{ apply H0. }
intro. unfold replace_individual_ethic.
destruct (i0 == i) eqn:H2.
2: { apply H1. }
assert (i0 = i).
{ by apply/eqP. }
rewrite H3.
unfold more_restrictive in H. pose proof (H (ap i)).
apply H4.
apply H1.
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
SubjStates, 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 SubjStates, 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) (ep : EthicalProfile) (ethic : IndividualEthic),
more_restrictive (ep i) ethic (get_SubjectiveState state i) /\
~ conflict ep ap state /\
conflict (replace_individual_ethic 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
).
repeat split.
{
unfold conflict.
intro. destruct H0. pose proof (H1 i).
rewrite eq_refl in H2. inversion H2.
}
{ tauto. }
{
intro.
unfold replace_individual_ethic.
destruct (i0 == i) ; reflexivity.
}
Qed.