Leibniz' Project
This page lays the foundations of ethics in a society composed of individuals.
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 action profile is given by the action of each individual.
\(\mathbf{Definition}\)
The set \(AP\) of action profiles
is \(A^I\).
Definition Profile (T : Type) : Type := Individual -> T.
A subjective state is a situation seen in a specific individual’s perspective.
\(\mathbf{Definition}\)
The set \(SubjS\) of subjective
states is \(S × 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.
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))\).
Open Scope group_scope. Notation " σ ∘ τ " := (σ * τ) (at level 40, no associativity). Definition identity : {perm Individual} := 1. Definition IndividualsPermutationsActingOnStates : Type := { permutation : State -> {perm Individual} -> State | forall (state : State), permutation state identity = state /\ forall (σ τ : {perm Individual}), permutation (permutation state σ) τ = permutation state (σ ∘ τ) }. Definition permutation_State (ipos : IndividualsPermutationsActingOnStates) : State -> {perm Individual} -> State := fun state => fun σ => proj1_sig ipos state σ. Definition permutation_SubjectiveState (ipos : IndividualsPermutationsActingOnStates) : SubjectiveState -> {perm Individual} -> SubjectiveState := fun subjective_state => fun σ => get_SubjectiveState ( proj1_sig ipos subjective_state.(state) σ ) (σ subjective_state.(individual)).
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}\)
The set \(IE\) of individual
ethics is \({\{⊥ ,⊤\}}^{SubjS ×
A}\).
Definition IndividualEthic : Type := @Ethic SubjectiveState Action.
An ethical profile gives the ethic of each individual.
\(\mathbf{Definition}\)
The set \(EP\) of ethical
profiles is \(IE^I\).
\(\mathbf{Definition}\)
Individuals \(i, j \in I\) of an
ethical profile \(ep\) are said
to have the same ethic in a subjective state \(subjS\) if \(\forall a \in A, ep(i)(SubjS, a) =
ep(j)(SubjS, a)\).
\(\mathbf{Definition}\)
Individuals \(i, j \in I\) of an
ethical profile \(ep\) are said
to always have the same ethic if \(\forall subjS \in SubjS,\) \(i\) and \(j\) have the same ethic in \(subjS\) .
Definition everyone_same_ethic (ethical_profile : Profile IndividualEthic) (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 : Profile IndividualEthic) : Prop := forall (subjective_state : SubjectiveState), everyone_same_ethic ethical_profile subjective_state.
