Leibniz' Project
In a society composed of individuals, 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.
Context {State : Type}. Context {Action : Type}. Context {Individual : finType}.
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 State Action Individual) (ipos : @IndividualsPermutationsActingOnStates State Individual) : Prop := forall (state : State) (individual : Individual) (σ : {perm Individual}), ethic ( @permutation_SubjectiveState State Individual ipos ( @get_SubjectiveState State Individual state individual ) σ ) = ethic ( @get_SubjectiveState State Individual state individual). Definition everyone_is_objective (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) (ipos : @IndividualsPermutationsActingOnStates State Individual) := 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 : @Profile Individual (@IndividualEthic State Action Individual)) (i j : Individual) (state : State) : Prop := exists (action : Action), ethical_profile j ( @get_SubjectiveState State Individual state j ) action = true /\ ethical_profile i ( @get_SubjectiveState State Individual state j ) action = false. Definition may_never_disapprove (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) (i j : Individual) : Prop := forall (state : State), ~ may_disapprove ethical_profile i j state. Definition nobody_may_disapprove (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) (state : State) : Prop := forall (i j : Individual), ~ may_disapprove ethical_profile i j state. Definition nobody_may_ever_disapprove (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) : 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 : @Profile Individual (@IndividualEthic State Action Individual)) (i j : Individual) (state : State) : ethical_profile i ( @get_SubjectiveState State Individual state j) = ethical_profile j ( @get_SubjectiveState State Individual 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 : @IndividualsPermutationsActingOnStates State Individual) (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) (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 state individual (tperm i individual)). unfold get_SubjectiveState in H5. assert ( forall (action : Action), ethical_profile i ( @permutation_SubjectiveState State Individual ipos {| state := state; individual := individual |} (tperm i individual) ) action = ethical_profile i {| state := state; individual := individual |} action ). { intro. rewrite H5. reflexivity. } pose proof (H6 x0). rewrite H3 in H7. unfold permutation_SubjectiveState in H7. rewrite proj_individual_SubjectiveState in H7. rewrite proj_state_SubjectiveState in H7. rewrite tpermR in H7. pose proof (H0 state individual (tperm i individual)). unfold get_SubjectiveState in H8. assert ( forall (action : Action), ethical_profile j ( @permutation_SubjectiveState State Individual ipos {| state := state; individual := individual |} (tperm i individual) ) action = ethical_profile j {| state := state; individual := individual |} action ). { intro. rewrite H8. reflexivity. } pose proof (H9 x0). rewrite H4 in H10. unfold permutation_SubjectiveState in H10. rewrite proj_individual_SubjectiveState in H10. rewrite proj_state_SubjectiveState in H10. rewrite tpermR in H10. pose proof (H2 (proj1_sig ipos state (tperm i individual))). exfalso. apply H11. exists x0. split ; tauto. } { destruct (ethical_profile j x x0) eqn:H4. 2: { reflexivity. } destruct x. pose proof (H state individual (tperm j individual)). unfold get_SubjectiveState in H5. assert ( forall (action : Action), ethical_profile i ( @permutation_SubjectiveState State Individual ipos {| state := state; individual := individual |} (tperm j individual) ) action = ethical_profile i {| state := state; individual := individual |} action ). { intro. rewrite H5. reflexivity. } pose proof (H6 x0). rewrite H3 in H7. unfold permutation_SubjectiveState in H7. rewrite proj_individual_SubjectiveState in H7. rewrite proj_state_SubjectiveState in H7. rewrite tpermR in H7. pose proof (H0 state individual (tperm j individual)). unfold get_SubjectiveState in H8. assert ( forall (action : Action), ethical_profile j ( @permutation_SubjectiveState State Individual ipos {| state := state; individual := individual |} (tperm j individual) ) action = ethical_profile j {| state := state; individual := individual |} action ). { intro. rewrite H8. reflexivity. } pose proof (H9 x0). rewrite H4 in H10. unfold permutation_SubjectiveState in H10. rewrite proj_individual_SubjectiveState in H10. rewrite proj_state_SubjectiveState in H10. rewrite tpermR in H10. pose proof (H1 (proj1_sig ipos state (tperm j individual))). 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 : @IndividualsPermutationsActingOnStates State Individual) (ethical_profile : @Profile Individual (@IndividualEthic State Action Individual)) : 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 state j)). Qed.
