Leibniz' Project
Some phenomenons uncovered by quantum physicists have not been found to be deterministic: leading the (at least seemingly) same experiment leads to different outcomes, which apparently follow a probability distribution. As the physical world was considered deterministic until there by classical physics, an interpretation was proposed to render the results of quantum mechanics in a deterministic frame: the many-wrolds interpretation. The idea is to claim something difficultly provable or refutable: the fact that each outcome possible according to our physical theory which does not happen in our world does indeed happen, but in another world.
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 \(W\) the set of worlds.
Some definitions in this article are used.
Context {Time : Type}. Context {Before : TotalOrder Time}. Context {State : Type}. Context {World : Type}.
According to our definition, we can conclude that a physical theory isn’t deterministic whenever two histories of events coinciding at a certain instant must coincide every time after.
\(\mathbf{Definition}\)
Let \(pt\) a physical theory in
\({\{⊥ ,⊤\}}^{S^T}\).
An indeterminism in \(pt\) is a
\((h_1, h_2, t_0, t) \in {S^T \times S^T
\times T \times T}\) such that: \[\begin{cases*}
t_0 \lt t \\
pt \text{ satisfies } h_1 \\
pt \text{ satisfies } h_2 \\
h_1(t_0) = h_2(t_0) \\
h_1(t) \neq h_2(t)
\end{cases*}\] Let \(I(pt)\) be the set of indeterminisms
of \(pt\).
And let \(W = {\{⊥
,⊤\}}^{I(pt)}\) be the set of worlds.
Definition Indeterminism (pt : @PhysicalTheory Time State) : Type := { h1h2t1t2 : ( @History Time State) * ( @History Time State) * Time * Time | @instance_indeterminism Time Before State pt ( fst (fst (fst h1h2t1t2)) ) ( snd (fst (fst h1h2t1t2)) ) (snd (fst h1h2t1t2)) (snd h1h2t1t2) }. Definition get_h1 {pt : @PhysicalTheory Time State} (ind : Indeterminism pt) : @History Time State := fst (fst (fst (proj1_sig ind))). Definition get_h2 {pt : @PhysicalTheory Time State} (ind : Indeterminism pt) : @History Time State := snd (fst (fst (proj1_sig ind))). Definition get_t1 {pt : @PhysicalTheory Time State} (ind : Indeterminism pt) : Time := snd (fst (proj1_sig ind)). Definition get_t2 {pt : @PhysicalTheory Time State} (ind : Indeterminism pt) : Time := snd (proj1_sig ind). Definition deterministic_World (pt : @PhysicalTheory Time State) : Type := Indeterminism pt -> bool.
\(\mathbf{Lemma}\)
A physical theory \(pt\) is
deterministic if and only if \(I(pt) =
\emptyset\).
\(\mathbf{proof:}\)
Direct application of the definitions of a deterministic physical
theory and of an indeterminism.
■
Lemma indeterministic_iff_any_indeterminism (pt : @PhysicalTheory Time State) : ~ @is_deterministic Time Before State pt <-> inhabited (Indeterminism pt). Proof. unfold is_deterministic. split. { intros. apply exists_to_inhabited_sig. apply not_all_ex_not in H. destruct H as [h1]. apply not_all_ex_not in H. destruct H as [h2]. apply imply_to_and in H. destruct H. apply imply_to_and in H0. destruct H0. apply not_all_ex_not in H1. destruct H1 as [t1]. apply imply_to_and in H1. destruct H1. apply not_all_ex_not in H2. destruct H2 as [t2]. apply imply_to_and in H2. destruct H2. assert ( @instance_indeterminism Time Before State pt h1 h2 t1 t2). { unfold instance_indeterminism. tauto. } exists ((h1, h2, t1, t2)). simpl. exact H4. } { intros. apply inhabited_sig_to_exists in H. destruct H as [h1h2t1t2]. unfold instance_indeterminism in H. apply ex_not_not_all. exists (h1h2t1t2.1.1.1). apply ex_not_not_all. exists (h1h2t1t2.1.1.2). intro. destruct H. destruct H1. destruct H2. destruct H3. specialize (H0 H1 H2 h1h2t1t2.1.2 H3 h1h2t1t2.2 H). apply H4. exact H0. } Qed. Lemma deterministic_iff_no_indeterminism (pt : @PhysicalTheory Time State) : @is_deterministic Time Before State pt <-> ~ inhabited (Indeterminism pt). Proof. pose proof (indeterministic_iff_any_indeterminism pt). tauto. Qed.
To get rid of indeterminisms of a physical theory, we define a world for each possible outcome in each instance of indeterminism.
\(\mathbf{Definition}\)
Let \(pt\) a physical theory in
\({\{⊥ ,⊤\}}^{S^T}\).
The many-worlds extension is the physical theory \(\bar pt \in {\{⊥ ,⊤\}}^{(S^W)^T}\)
defined below: \[\begin{align*}
(S^W)^T &\to \mathbb \{⊥ ,⊤\} \\
\bar h &\mapsto \begin{cases*}
⊥ \text{ if } \exists ind=(h_1, h_2, t_0, t) \in I(pt), w
\in W \text{ such that } (w(ind) \text{ and } \forall t' \in
T, \bar h(t')(w) = h_2(t')) \text{ or } (\neg w(ind)
\text{ and } \forall t' \in T, \bar h(t')(w) =
h_1(t')) \\
\forall w \in W, pt(t \mapsto \bar h(t)(w)) \text{
otherwise}
\end{cases*}
\end{align*}\]
Definition many_worlds_extension (pt : @PhysicalTheory Time State) : @PhysicalTheory Time (deterministic_World pt -> State) := fun (h' : @History Time (deterministic_World pt -> State)) => if `[< exists (ind : Indeterminism pt) (w : deterministic_World pt), (w ind /\ (fun t => h' t w) = get_h2 ind) \/ (~ w ind /\ (fun t => h' t w) = get_h1 ind) >] then False else ( forall (w : deterministic_World pt), pt (fun t => h' t w) ).
\(\mathbf{Lemma}\)
The many-worlds extension of any physical theory is
deterministic.
\(\mathbf{proof:}\)
Let \(pt\) a physical theory in
\({\{⊥ ,⊤\}}^{S^T}\) and \(\bar pt\) its many-worlds
extension.
Let’s reason by contradiction and suppose that:
\[\begin{cases*}
t_0 \lt t \\
\bar pt \text{ satisfies } \bar h_1 \\
\bar pt \text{ satisfies } \bar h_2 \\
\bar h_1(t_0) = \bar h_2(t_0) \\
\bar h_1(t) \neq \bar h_2(t)
\end{cases*}\] The two staisfiabilities and the definition
of \(\bar pt\) imply that \[\tag{1} \forall w \in W, ind=(h_1, h_2,
t_0, t) \in I(pt),
\begin{cases*}
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_1(t')(w) = h_2(t')) \text{ or } (\neg w(ind) \text{ and
} \forall t' \in T, \bar h_1(t')(w) = h_1(t'))) \\
\forall w \in W, pt(t' \mapsto \bar h_1(t')(w)) \\
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_2(t')(w) = h_2(t')) \text{ or } (\neg w(ind) \text{ and
} \forall t' \in T, \bar h_2(t')(w) = h_1(t'))) \\
\forall w \in W, pt(t' \mapsto \bar h_2(t')(w))
\end{cases*}\] As \(\bar h_1(t)
\neq \bar h_2(t)\), there is a \(w \in W\) such that \(\bar h_1(t)(w) \neq \bar h_2(t)(w)\).
And as \(\bar h_1(t_0) = \bar
h_2(t_0)\), we have \(\bar
h_1(t_0)(w) = \bar h_2(t_0)(w)\).
Moreover, equations 2 and 4 in \((1)\) imply that \(pt\) satisfies \(t' \mapsto \bar h_1(t')(w)\)
and \(t' \mapsto \bar
h_2(t')(w)\).
Thus we have an indeterminism \((t'
\mapsto \bar h_1(t')(w), t' \mapsto \bar h_2(t')(w),
t_0, t) \in I(pt)\).
Applying equations 1 and 3 in \((1)\) to \(w\) and this indeterminism gives
\[\begin{cases*}
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_1(t')(w) = (t' \mapsto \bar h_2(t')(w))(t'))
\text{ or } (\neg w(ind) \text{ and } \forall t' \in T, \bar
h_1(t')(w) = (t' \mapsto \bar h_1(t')(w))(t'))) \\
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_2(t')(w) = (t' \mapsto \bar h_2(t')(w)(t'))
\text{ or } (\neg w(ind) \text{ and } \forall t' \in T, \bar
h_2(t')(w) = (t' \mapsto \bar h_1(t')(w)))(t')))
\end{cases*}\] That is \[\begin{cases*}
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_1(t')(w) = \bar h_2(t')(w)) \text{ or } (\neg w(ind)
\text{ and } \forall t' \in T, \bar h_1(t')(w) = \bar
h_1(t')(w))) \\
\neg ((w(ind) \text{ and } \forall t' \in T, \bar
h_2(t')(w) = \bar h_2(t')(w)) \text{ or } (\neg w(ind)
\text{ and } \forall t' \in T, \bar h_2(t')(w) =
h_1(t')(w)))
\end{cases*}\] As \(\bar
h_1(t)(w) \neq \bar h_2(t)(w)\), this gives \[\begin{cases*}
\neg \neg w(ind) \\
\neg w(ind)
\end{cases*}\] and therefore a contradiction.
■
Lemma deterministic_many_worlds_interpretation (pt : @PhysicalTheory Time State) : @is_deterministic Time Before (deterministic_World pt -> State) ( many_worlds_extension pt ). Proof. unfold is_deterministic. unfold many_worlds_extension. unfold satisfies. unfold deterministic_World. intros. destruct ( `[< exists (ind : Indeterminism pt) (w : Indeterminism pt -> bool), w ind /\ h1^~ w = get_h2 ind \/ ~ w ind /\ h1^~ w = get_h1 ind >] ) eqn:dstrH1. { inversion H. } apply false_to_False in dstrH1. pose proof (not_ex_all_not (Indeterminism pt) ( fun (ind : Indeterminism pt) => exists (w : Indeterminism pt -> bool), w ind /\ h1^~ w = get_h2 ind \/ ~ w ind /\ h1^~ w = get_h1 ind ) dstrH1). simpl in H3. destruct ( `[< exists (ind : Indeterminism pt) (w : Indeterminism pt -> bool), w ind /\ h2^~ w = get_h2 ind \/ ~ w ind /\ h2^~ w = get_h1 ind >] ) eqn:dstrH2. { inversion H0. } apply false_to_False in dstrH2. pose proof (not_ex_all_not (Indeterminism pt) ( fun (ind : Indeterminism pt) => exists (w : Indeterminism pt -> bool), w ind /\ h2^~ w = get_h2 ind \/ ~ w ind /\ h2^~ w = get_h1 ind ) dstrH2). simpl in H4. rewrite <- notP. intro Hndet. pose proof (functional_extensionality (h1 t) (h2 t)). rewrite <- contrapositive in H5. 2: { unfold Decidable.decidable. tauto. } specialize (H5 Hndet). apply not_all_ex_not in H5. destruct H5 as [w Hneq]. apply equal_f with (x:=w) in H1. assert ( @instance_indeterminism Time Before State pt (h1^~ w) (h2^~ w) t0 t). { unfold instance_indeterminism. split. { exact H2. } split. { apply H. } split. { apply H0. } split. { rewrite H1. reflexivity. } { exact Hneq. } } set ( ind := exist ( fun h1h2t1t2 => @instance_indeterminism Time Before State pt ( fst (fst (fst h1h2t1t2)) ) ( snd (fst (fst h1h2t1t2)) ) (snd (fst h1h2t1t2)) (snd h1h2t1t2) ) (((h1^~ w), (h2^~ w), t0, t)) H5 ). specialize (H3 ind). specialize (H4 ind). pose proof (not_ex_all_not (Indeterminism pt -> bool) ( fun (w : Indeterminism pt -> bool) => w ind /\ h1^~ w = get_h2 ind \/ ~ w ind /\ h1^~ w = get_h1 ind ) H3). simpl in H6. specialize (H6 w). pose proof (not_ex_all_not (Indeterminism pt -> bool) ( fun (w : Indeterminism pt -> bool) => w ind /\ h2^~ w = get_h2 ind \/ ~ w ind /\ h2^~ w = get_h1 ind ) H4). simpl in H7. specialize (H7 w). tauto. Qed.
