Leibniz' Project
Here is proposed a formalization of the concept of physical theory, and what it is to be deterministic.
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.
A history is a complete description of all what happened through time (successive states). A history until a certain instant is all what happened through time until this instant. A history extends a history until a certain instant if both coincide before that instant.
\(\mathbf{Definition}\)
The set \(H\) of histories is
\(S^T\).
The set \(H_{t_0}\) of histories
until \(t_0\) is \(S^{\{t \in T | t \le t_0\}}\) (where
\(t_0 \in T\)).
The set \(H_{<t_0}\) of
histories before \(t_0\) is \(S^{\{t \in T | t \lt t_0\}}\) (where
\(t_0 \in T\)).
\(\mathbf{Definition}\)
Let \(t_0 \in T\), \(h \in H\) and \({hu} \in H_{t_0}\).
\(h\) is said to extend \({hu}\) if \(\forall t \le t_0, h(t) =
{hu}(t)\).
Definition History : Type := Time -> State. Definition HistoryUntil (t0 : Time) : Type := { t : Time | non_strict Before t t0 } -> State. Definition HistoryBefore (t0 : Time) : Type := { t : Time | strict Before t t0 } -> State. Definition extends {t0 : Time} (h : History) (hu : HistoryUntil t0) : Prop := forall (t : { t : Time | non_strict Before t t0 }), non_strict Before (proj1_sig t) t0 -> h (proj1_sig t) = hu t.
As a history contains all the information, it can report which events happened and which didn’t.
\(\mathbf{Definition}\)
The set \(E\) of events is \({\{⊥, ⊤\}}^H\), provided \(e(h) = ⊤\) when the event \(e \in E\) happens in history \(h \in H\).
Definition Event : Type := pred History. Definition happens_in (e : Event) (h : History) : Prop := e h = true.
A physical theory comes down to the ability to determine whether a given history is physically possible or not (being given this ability, we may describe its behaviour in physical laws).
\(\mathbf{Definition}\)
The set \(PT\) of physical
theories is \({\{⊥
,⊤\}}^H\).
(it is equal to the set of events but its elements are interpreted
differently)
\(\mathbf{Definition}\)
A history \(h \in H\) is said to
satisfy a physical theory \(pt \in
PT\) if \(pt(h) = ⊤\)
Definition PhysicalTheory : Type := History -> Prop. Definition satisfies (h : History) (pt : PhysicalTheory) : Prop := pt h.
An event is possible if there exists a physically possible history in which it happens.
\(\mathbf{Definition}\)
An event \(e \in E\) is said
possible in a physical theory \(pt \in
PT\) if \(\exists h \in
H\) which satisfies \(pt\)
such that \(e(h)=⊤\).
Definition is_possible (event : Event) (pt : PhysicalTheory) : Prop := exists (h : History), satisfies h pt /\ event h = true.
A physical theory is deterministic when a given state at a given instant determines all the other states after that instant: if we know everything at the present moment, we can describe all that’s going to happen. For example, classical and relativistic mechanics are deterministic. See for example the page 12 of this article.
\(\mathbf{Definition}\)
A physical theory \(pt \in PT\)
is said deterministic if \(\forall h_1,
h_2 \in H\) which satisfy \(pt\) and such that \(h_1(t_0) = h_2(t_0)\) for a given
\(t_0 \in T\), then \(\forall t \gt t_0, h_1(t) =
h_2(t)\).
Definition is_deterministic (pt : PhysicalTheory) : Prop := forall (h1 h2 : History), satisfies h1 pt -> satisfies h2 pt -> forall (t0 : Time), ( h1 t0 = h2 t0 -> forall (t : Time), strict Before t0 t -> h1 t = h2 t ).
