Leibniz' Project
There is some kind of existential issue in admitting that the physical rules of the world are deterministic: then, as we are part of this world, all of our actions and thoughts are (in theory) perfectly predictable and at least predetermined. But this removes our free will and can eventually be dangerous for the society, as it implies that no one is responsible for his actions.
Here is described a frame in which an individual sees the outer world as a deterministic one but his actions remain his.
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 \(S\) be the set of states
and \(A\) be the set of
actions.
Some definitions in this article are used.
Context {Time : Type}. Context {Before : TotalOrder Time}. Context {State : Type}. Context {Action : Type}.
If one takes the perspective of an individual, it perceives the world with its captors and acts by motions.
With this subjective approach, the rules of the world (as perceived by our individual) are deterministic if a given state at a given instant together with the following individual’s actions determine all the other states after that instant.
One can potentially assimilate our individual to mankind in order to be less subjective. Then the actions are the sum of actions of everyone and the single free will for mankind can be seen as the sum of all the free wills.
In our definition below, every action is considered feasible in every physical theory mostly by convenience, but it’s consistent with actions/movements fired by neural signals: the intended action may not happen but we have tried.
\(\mathbf{Definition}\)
A physical theory \(pt \in {\{⊥
,⊤\}}^{S^T}\) is said deterministic except for free will if
\[\forall h_1, h_2 \in (S \times A)^T
\text{ whose projections satisfy both } pt \text{ and such that }
h_1(t_0) = h_2(t_0) \text{ for a given } t_0 \in T, \forall t \gt
t_0, (\text{all the actions between } t_0 \text{ and } t \text{
are equal in } h_1 \text{ and } h_2 \Rightarrow h_1(t) =
h_2(t))\]
Definition ignore_actions (h : @History Time (State * Action)) : @History Time State := fun t => fst (h t). Definition get_action (h : @History Time (State * Action)) (t : Time) : Action := snd (h t). Definition is_deterministic_except_for_free_will (pt : @PhysicalTheory Time State) (a_def : Action) : Prop := forall (h1 h2 : @History Time (State * Action)), satisfies (ignore_actions h1) pt -> satisfies (ignore_actions h2) pt -> forall (t0 : Time), ( h1 t0 = h2 t0 -> forall (t2 : Time), strict Before t0 t2 -> ( forall (t1 : Time), strict Before t0 t1 -> non_strict Before t1 t2 -> get_action h1 t1 = get_action h2 t1 ) -> h1 t2 = h2 t2 ).
