Leibniz' Project
In a society composed of ndividuals, each of them being objective in his ethic, it is proved here that it’s not possible that an individual disapproves an action by another individual if and only if all the individuals have the same ethic.
One relies on this article.
Throughout this page, let \(I\) the finite set of individuals of a society, \(S\) be the set of states and \(A\) the set of actions.
Require Import Logic.FunctionalExtensionality.
From mathcomp Require Import all_ssreflect fintype fingroup perm seq.
Require Import ethics_first_steps.
Definition State : Type := ethics_first_steps.State.
Definition Action : eqType := ethics_first_steps.Action.
Context {Individual : finType}.
A subjective state is a situation seen in a specific individual’s perspective.
\(\mathbf{Definition}\)
A subjective state is a pair \((s,
i)\), where \(s \in S\),
\(i \in I\).
Structure SubjectiveState : Type := {
state : State ;
individual : Individual
}.
Definition get_SubjectiveState (state : State) (i : Individual) :
SubjectiveState := {|
state := state ;
individual := i
|}.
Lemma proj_individual_SubjectiveState (state : State) (i : Individual) :
individual (get_SubjectiveState state i) = i.
Proof.
auto.
Qed.
Lemma proj_state_SubjectiveState (s : State) (i : Individual) :
state (get_SubjectiveState s i) = s.
Proof.
auto.
Qed.
An individual ethic tells for each subjective state if a given action is “right” or “wrong”. As a subjective state can put anyone’s shoes, so can an individual ethic.
\(\mathbf{Definition}\)
An individual ethic is a function which at each subjective state
and action associates \(⊥\) if
the action is considered ethically right and \(⊤\) if it’s considered wrong.
Definition IndividualEthic : Type := SubjectiveState -> Action -> bool.
An individual profile gives the ethic of each individual.
\(\mathbf{Definition}\)
An ethical profile is a function which at each individual \(i \in I\) associates an individual
ethic.
Definition EthicalProfile : Type := Individual -> IndividualEthic.
Definition everyone_same_ethic
(ethical_profile : EthicalProfile) (subjective_state : SubjectiveState) : Prop :=
forall (i j : Individual),
ethical_profile i subjective_state =
ethical_profile j subjective_state.
Definition everyone_always_same_ethic (ethical_profile : EthicalProfile) : Prop :=
forall (subjective_state : SubjectiveState),
everyone_same_ethic ethical_profile subjective_state.
Permuting two individuals in a state consists in exchanging their roles. For example, if a state is described by “Alice is in jail and Bob is free”, permuting Alice and Bob gives “Bob is in jail and Alice is free”.
\(\mathbf{Definition}\)
Let \(s\) be a state of \(S\) and \(\sigma\) a permutation of \(S_I\). Then \(s_\sigma\) is the state obtained by
permuting individuals according to \(\sigma\) in \(s\).
\(\mathbf{Definition}\)
Let \((s, i)\) be an individual
state and \(\sigma\) a
permutation of \(S_I\). Then
\((s, i)_\sigma\) is defined as
\((s_\sigma, \sigma (i))\).
Definition PermutationOnIndividuals : Type := {perm Individual}.
Definition identity_permutation : {perm Individual} := 1.
Definition identity : PermutationOnIndividuals := identity_permutation.
Definition composition :
PermutationOnIndividuals -> PermutationOnIndividuals -> PermutationOnIndividuals :=
fun σ => fun τ => mulg σ τ.
Notation " σ ∘ τ " := (composition σ τ) (at level 40, no associativity).
Definition IndividualsPermutationOnStates : Type := {
permutation : State -> PermutationOnIndividuals -> State |
forall (state : State),
permutation state identity = state /\
forall (σ τ : PermutationOnIndividuals),
permutation (permutation state σ) τ = permutation state (σ ∘ τ)
}.
Definition permutation_subjective_state (ipos : IndividualsPermutationOnStates) :
SubjectiveState -> PermutationOnIndividuals -> SubjectiveState :=
fun subjective_state => fun σ => get_SubjectiveState (
proj1_sig ipos (state subjective_state) σ
) (σ (individual subjective_state)).
Notation " ipos , subjective_state ⋅ σ " := (
permutation_subjective_state ipos subjective_state σ
) (at level 100, no associativity).
An individual ethic is said objective if it does not depend on persons (only on states). To be more concrete, if the state is “Alice is in jail and Bob is free” and if one’s ethic specifies that someone in jail should be able to have a job, this ethical rule must apply whether it’s Alice or Bob who’s in jail. An objective ethic requires in some way an equality of rights, but an objective ethic can include something like “the richest one can do whatever (s)he wants”, provided it applies whoever is the richest one.
\(\mathbf{Definition}\)
An individual ethic \(e\) is said
objective if \[\forall state \in S, i
\in I, \sigma \in S_I, a \in A, e((s, i)_\sigma, a) = e((s, i),
a)\]
Definition objective (ethic : IndividualEthic)
(ipos : IndividualsPermutationOnStates) : Prop :=
forall (state : State) (individual : Individual) (σ : PermutationOnIndividuals),
ethic ( ipos , (
get_SubjectiveState state individual
) ⋅ σ ) = ethic (get_SubjectiveState state individual).
Definition everyone_is_objective (ethical_profile : EthicalProfile)
(ipos : IndividualsPermutationOnStates) :=
forall (i : Individual), objective (ethical_profile i) ipos.
An individual \(i\) may disapprove another individual \(j\) if there’s an action which: - \(j\)’s ethic allows him in his position - \(i\)’s ethic wouldn’t allow him if he was in \(j\)’s position
\(\mathbf{Definition}\)
Let \(i, j\) be two individuals,
with respective ethics \(e_i,
e_j\). \(i\) may
disapprove \(j\) in state \(s\) if \[\exists a \in A, e_j((s, j), a) = ⊤ \text{
and } e_j((s, i), a) = ⊥\]
Definition may_disapprove (ethical_profile : EthicalProfile) (i j : Individual)
(state : State) : Prop :=
exists (action : Action),
ethical_profile j (get_SubjectiveState state j) action = true /\
ethical_profile i (get_SubjectiveState state j) action = false.
Definition may_never_disapprove (ethical_profile : EthicalProfile)
(i j : Individual) : Prop :=
forall (state : State), ~ may_disapprove ethical_profile i j state.
Definition nobody_may_disapprove (ethical_profile : EthicalProfile)
(state : State) : Prop :=
forall (i j : Individual), ~ may_disapprove ethical_profile i j state.
Definition nobody_may_ever_disapprove (ethical_profile : EthicalProfile) : Prop :=
forall (state : State), nobody_may_disapprove ethical_profile state.
Two individuals having the same ethic may not disapprove one another.
\(\mathbf{Lemma}\)
If two individual ethics \(e_i,
e_j\) are identical in a state \(s\) seen by \(j\), then \(i\) may not disapprove \(j\) in this state.
\(\mathbf{proof:}\)
Let \(a\) be an action.
As \(e_i((s, j), a) = e_j((s, j),
a)\), it’s not possible that \(e_j((s, j), a) = ⊤\) and \(e_i((s, j), a) = ⊥\), which prevents
a disapproval.
■
Lemma same_ethic_implies_may_not_disapprove (ethical_profile : EthicalProfile)
(i j : Individual) (state : State) :
ethical_profile i (get_SubjectiveState state j) =
ethical_profile j (get_SubjectiveState state j) ->
~ may_disapprove ethical_profile i j state.
Proof.
intros. unfold not. intros.
unfold may_disapprove in H0. destruct H0 as [action]. destruct H0.
rewrite H in H1.
rewrite H0 in H1. inversion H1.
Qed.
If two individuals are objective and may not disapprove with one another, then they have the same ethic.
\(\mathbf{Proposition}\)
Let \(i, j\) be two individuals
with respective objective ethics \(e_i,
e_j\). If \(i\) and \(j\) may disapprove one another in no
state, then \(e_i = e_j\).
\(\mathbf{proof:}\)
Let’s suppose by contradiction that \(e_i \neq e_j\).
Then there are a subjective states \((s,
k)\) and an action \(a\)
such that \(e_i((s, k), a) \neq e_j((s,
k), a)\).
Let’s suppose for example that \(e_i((s,
k), a) = ⊤\) and \(e_j((s, k), a)
= ⊥\) (the other case \(e_i((s,
k), a) = ⊥\) and \(e_j((s, k), a)
= ⊤\) is analogous).
Let’s denote \((i, k)\) the
permutation swapping \(j\) and
\(k\), and letting the other
individuals unchanged.
By objectivity of \(i\), \(e_i((s, k), a)_{(i, k)} = e_i((s, k),
a)\).
And by definition of permutations on states, \(e_i((s, k), a)_{(i, k)} = e_i((s_{(i, k)},
(i, k)(k)), a) = e_i((s_{(i, k)}, i), a)\) (this remains
true if \(k\) equals \(i\) or \(j\), provided that \((i,i) = id\)).
Which gives us \[\begin{equation}
\tag{1}
e_i((s_{(i, k)}, i), a) = ⊤
\end{equation}\] On \(e_j\)’s side, by objectivity of \(j\), \(e_j((s, k), a)_{(i, k)} = e_j((s, k),
a)\).
And by definition of permutations on states, \(e_j((s, k), a)_{(i, k)} = e_j((s_{(i, k)},
(i, k)(k)), a) = e_j((s_{(i, k)}, i), a)\).
Which gives us \(e_j((s_{(i, k)}, i), a)
= ⊥\).
Together with \((1)\), this gives
that \(j\) may disapprove \(i\), which is in contradiction with a
hypothesis.
■
Proposition objective_ethics_may_never_disapprove_implies_same_ethic
(ipos : IndividualsPermutationOnStates) (ethical_profile : EthicalProfile)
(i j : Individual) :
objective (ethical_profile i) ipos ->
objective (ethical_profile j) ipos ->
may_never_disapprove ethical_profile i j ->
may_never_disapprove ethical_profile j i ->
ethical_profile i = ethical_profile j.
Proof.
intros.
apply functional_extensionality. intro.
apply functional_extensionality. intro.
destruct (ethical_profile i x x0) eqn:H3.
{
destruct (ethical_profile j x x0) eqn:H4.
{ reflexivity. }
destruct x.
pose proof (H state0 individual0 (tperm i individual0)).
unfold get_SubjectiveState in H5.
assert ( forall (action : Action),
ethical_profile i (
ipos, {| state := state0; individual := individual0 |} ⋅ tperm i individual0
) action =
ethical_profile i {| state := state0; individual := individual0 |} action
).
{ intro. rewrite H5. reflexivity. }
pose proof (H6 x0).
rewrite H3 in H7.
unfold permutation_subjective_state in H7.
rewrite proj_individual_SubjectiveState in H7.
rewrite proj_state_SubjectiveState in H7.
rewrite tpermR in H7.
pose proof (H0 state0 individual0 (tperm i individual0)).
unfold get_SubjectiveState in H8.
assert ( forall (action : Action),
ethical_profile j (
ipos, {| state := state0; individual := individual0 |} ⋅ tperm i individual0
) action =
ethical_profile j {| state := state0; individual := individual0 |} action
).
{ intro. rewrite H8. reflexivity. }
pose proof (H9 x0).
rewrite H4 in H10.
unfold permutation_subjective_state in H10.
rewrite proj_individual_SubjectiveState in H10.
rewrite proj_state_SubjectiveState in H10.
rewrite tpermR in H10.
pose proof (H2 (proj1_sig ipos state0 (tperm i individual0))).
exfalso. apply H11. exists x0. split ; tauto.
}
{
destruct (ethical_profile j x x0) eqn:H4.
2: { reflexivity. }
destruct x.
pose proof (H state0 individual0 (tperm j individual0)).
unfold get_SubjectiveState in H5.
assert ( forall (action : Action),
ethical_profile i (
ipos, {| state := state0; individual := individual0 |} ⋅ tperm j individual0
) action =
ethical_profile i {| state := state0; individual := individual0 |} action
).
{ intro. rewrite H5. reflexivity. }
pose proof (H6 x0).
rewrite H3 in H7.
unfold permutation_subjective_state in H7.
rewrite proj_individual_SubjectiveState in H7.
rewrite proj_state_SubjectiveState in H7.
rewrite tpermR in H7.
pose proof (H0 state0 individual0 (tperm j individual0)).
unfold get_SubjectiveState in H8.
assert ( forall (action : Action),
ethical_profile j (
ipos, {| state := state0; individual := individual0 |} ⋅ tperm j individual0
) action =
ethical_profile j {| state := state0; individual := individual0 |} action
).
{ intro. rewrite H8. reflexivity. }
pose proof (H9 x0).
rewrite H4 in H10.
unfold permutation_subjective_state in H10.
rewrite proj_individual_SubjectiveState in H10.
rewrite proj_state_SubjectiveState in H10.
rewrite tpermR in H10.
pose proof (H1 (proj1_sig ipos state0 (tperm j individual0))).
exfalso. apply H11. exists x0. split ; tauto.
}
Qed.
Overall, in a society where everyone is objective in his ethic, there is no possible disapproval if and only everyone has the same ethic.
\(\mathbf{Corollary}\)
If \(\forall i \in I,\) \(e_i\) is objective, \[\forall i,j \in I, i \text{ may not
disapprove } j \iff \forall i,j \in I, e_i = e_j\]
\(\mathbf{proof:}\)
\(\Rightarrow\) is a
straightforward consequence of the previous proposition.
\(\Leftarrow\) is obtained by
generalizing the last lemma on all individuals and states.
■
Corollary objective_ethics_no_disapproval_iff_same_ethic
(ipos : IndividualsPermutationOnStates) (ethical_profile : EthicalProfile) :
everyone_is_objective ethical_profile ipos ->
(
nobody_may_ever_disapprove ethical_profile <->
everyone_always_same_ethic ethical_profile
).
Proof.
intro. split.
- intro.
unfold everyone_always_same_ethic. intro.
unfold everyone_same_ethic. intros.
assert (ethical_profile i = ethical_profile j).
2 : { rewrite H1. reflexivity. }
unfold everyone_is_objective in H.
unfold nobody_may_ever_disapprove in H0. unfold nobody_may_disapprove in H0.
apply objective_ethics_may_never_disapprove_implies_same_ethic with (ipos:=ipos).
+ apply H.
+ apply H.
+ unfold may_never_disapprove. intro. apply H0.
+ unfold may_never_disapprove. intro. apply H0.
- intro.
unfold nobody_may_ever_disapprove. intro.
unfold nobody_may_disapprove. intros.
apply same_ethic_implies_may_not_disapprove.
unfold everyone_always_same_ethic in H0. unfold everyone_same_ethic in H0.
apply H0 with (subjective_state:=(get_SubjectiveState state0 j)).
Qed.