Leibniz' Project
Here is formalized the concept of power of an individual in a society.
One relies mostly on this article and this one.
Throughout this page, let \(T\) be the set of instants in the
unfolding of time. If \(t, t' \in
T\), \(t \le t'\)
means that the instant \(t\) is
before (or simultaneous with) \(t'\).
Let \(I\) the finite set of
individuals of a society, \(S\)
be the set of states and \(A\)
the set of actions an individual can do.
Context {Time : Type}. Context {State : Type}. Context {Action : Type}. Context {Individual : finType}. Context {Before : TotalOrder Time}.
An individual policy is the line of conduct of an individual: what the individual does depending on the situation.
\(\mathbf{Definition}\)
Let \(h\) be a history and \(\sigma\) a permutation of \(S_I\).
Then the history \(h_\sigma\) is
defined as: \[\begin{align*}
T &\to \mathbb S × A^I\\
t &\mapsto h(t)_\sigma
\end{align*}\]
\(\mathbf{Definition}\)
Let \(e\) be an event and \(\sigma\) a permutation of \(S_I\).
Then the event \(e_\sigma\) is
defined as: \[\begin{align*}
H = (S × A^I)^T &\to \mathbb \{⊤, ⊥\}\\
h &\mapsto e(h_\sigma)
\end{align*}\]
\(\mathbf{Definition}\)
The set \(P\) of individual
policies is the set of functions from histories (before some
instant) to actions.
\(\mathbf{Definition}\)
An individual \(i \in I\) is said
to follow a policy in a history if at each instant its action is
the one given by the policy.
Definition permutation_History (ipos : @IndividualsPermutationsActingOnStates State Individual) (h : @History Time (State * @Profile Individual Action)) (σ : {perm Individual}) : @History Time (State * @Profile Individual Action) := fun (t : Time) => ( @permutation_State State Individual ipos (h t).1 σ, fun i : Individual => (h t).2 (σ i) ). Definition permutation_Event (ipos : @IndividualsPermutationsActingOnStates State Individual) (event : @Event Time (State * @Profile Individual Action)) (σ : {perm Individual}) : @Event Time (State * @Profile Individual Action) := fun (h : @History Time (State * @Profile Individual Action)) => event (permutation_History ipos h σ). Definition IndividualPolicy : Type := forall (t0 : Time), @HistoryBefore Time (State * @Profile Individual Action) Before t0 -> Action. Definition individual_follows_policy (i : Individual) (h : @History Time (State * @Profile Individual Action)) (policy : IndividualPolicy) : Prop := forall (t : Time), snd (h t) i = policy t ( @History_restriction_Before Time ( State * @Profile Individual Action ) Before t h ).
An individual is more powerful than another it can achieve every single goal the other can.
\(\mathbf{Definition}\)
A goal is said fulfilled by an individual in a history by a policy
if it happens while the policy is followed.
Definition individual_fulfills_goal (i : Individual) (h : @History Time (State * @Profile Individual Action)) (policy : IndividualPolicy) (goal : @Event Time (State * @Profile Individual Action)) : Prop := individual_follows_policy i h policy /\ @happens_in Time (State * @Profile Individual Action) goal h.
\(\mathbf{Definition}\)
An individual may achieve a goal under a scientific theory if
there is an individual policy and a history satisfying the
scientific theory in which the goal is fulfilled by the individual
by the policy.
Definition individual_may_achieve (i : Individual) (goal : @Event Time (State * @Profile Individual Action)) (st : @ScientificTheory Time (State * @Profile Individual Action)) : Prop := exists (h : @History Time (State * @Profile Individual Action)) (policy : IndividualPolicy), individual_fulfills_goal i h policy goal /\ @satisfies Time (State * @Profile Individual Action) h st.
\(\mathbf{Definition}\)
An individual \(i \in I\) is said
more powerful than another individual \(j \in I\) in a state \(s \in S\) under a scientific theory
\(st\) if for all goal \(g\) \[j
\text{ may achieve } g \text{ under } st \Rightarrow i \text{ may
achieve } g_\sigma \text{ under } st\] And an individual
\(i \in I\) is said strictly more
powerful than another individual \(j \in
I\) in a state \(s \in S\)
under a scientific theory \(st\)
if it’s more powerful and there is a goal achievable by \(i\) but not by \(j\).
Definition more_powerful (ipos : @IndividualsPermutationsActingOnStates State Individual) (st : @ScientificTheory Time (State * @Profile Individual Action)) (i j : Individual) (state : State) : Prop := forall (goal : @Event Time (State * @Profile Individual Action)), individual_may_achieve j goal st -> individual_may_achieve i ( permutation_Event ipos goal (tperm i j) ) st. Definition strictly_more_powerful (ipos : @IndividualsPermutationsActingOnStates State Individual) (st : @ScientificTheory Time (State * @Profile Individual Action)) (i j : Individual) (state : State) : Prop := more_powerful ipos st i j state /\ exists (goal : @Event Time (State * @Profile Individual Action)), ~ individual_may_achieve j goal st /\ individual_may_achieve i ( permutation_Event ipos goal (tperm i j) ) st.
