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.
Context {Time : Type}. Context {Before : TotalOrder Time}. Context {State : Type}. Context {offset : Time -> Time -> Time}.
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 := @ScientificTheory Time State.
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 (in theory) 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 Time State), satisfies h1 pt -> satisfies h2 pt -> forall (t0 : Time), ( h1 t0 = h2 t0 -> forall (t : Time), strict Before t0 t -> h1 t = h2 t ). Definition instance_indeterminism (pt : PhysicalTheory) (h1 h2 : @History Time State) (t1 t2 : Time) : Prop := strict Before t1 t2 /\ satisfies h1 pt /\ satisfies h2 pt /\ h1 t1 = h2 t1 /\ h1 t2 <> h2 t2.
A physical theory is said to respect time-translation symmetry if shifting the time by a given amount does not change satisfiability.
\(\mathbf{Definition}\)
Let \(h \in H\) and \(\delta\) an amount of time.
\(h_\delta\) is defined as the
history \(t \mapsto h(t +
\delta)\).
\(\mathbf{Definition}\)
\(pt \in PT\) is said to respect
time-translation symmetry if \(\forall
\delta\) amount of time and \(\forall h \in H\), \(h\) satisfies \(pt\) if and only if \(h_\delta\) satisfies \(pt\).
Definition History_offset (h : @History Time State) (delta_t : Time) : @History Time State := fun t => h (offset delta_t t). Definition time_translation_symmetry (pt : PhysicalTheory) : Prop := forall (delta_t : Time) (h : @History Time State), satisfies h pt <-> satisfies (History_offset h delta_t) pt.
