Leibniz' Project
Here is formalized the deduction of a scientific theory from a record of all what happened.
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 {State : Type}. Context {Before : TotalOrder Time}.
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)\).
Let \(t_0 \in T\), \(h \in H\) and \({hb} \in H_{<t_0}\).
\(h\) is said to extend \({hb}\) if \(\forall t \lt t_0, h(t) =
{hb}(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_until {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. Definition extends_before {t0 : Time} (h : History) (hu : HistoryBefore t0) : Prop := forall (t : { t : Time | strict Before t t0 }), strict Before (proj1_sig t) t0 -> h (proj1_sig t) = hu t. Definition History_restriction_Before (t : Time) (h : History) : HistoryBefore t := fun (t0 : { t0 : Time | strict Before t0 t }) => h (proj1_sig t0). Definition HistoryUntil_restriction {t1 t2 : Time} (le : non_strict Before t1 t2) (h2 : HistoryUntil t2) : HistoryUntil t1. Proof. unfold HistoryUntil in *. intros [t Ht]. apply h2. apply exist with (x:=t). unfold TotalOrder in Before. destruct Before. unfold total_order in *. simpl in le. simpl in Ht. simpl. destruct t0. destruct o. unfold Relation_Definitions.transitive in ord_trans. apply ord_trans with (y:=t1); tauto. Defined. Definition HistoryBefore_restriction {t1 t2 : Time} (le : non_strict Before t1 t2) (h2 : HistoryBefore t2) : HistoryBefore t1. Proof. unfold HistoryBefore in *. intros [t Ht]. apply h2. apply exist with (x:=t). apply strict_non_strict_transitive with (b:=t1); tauto. Defined.
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. Definition happened_before {t0 : Time} (e : Event) (h0 : HistoryBefore t0) : Prop := forall (h : History), extends_before h h0 -> happens_in e h.
Looking at the history, you may recognize patterns giving indications about how the environment works. Elaborating a scientific theory amounts to compiling such patterns in a way consistent with the history (and with itself).
\(\mathbf{Definition}\)
The set \(ST\) of scientific
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 scientific theory \(pt \in
PT\) if \(pt(h) = ⊤\).
\(\mathbf{Definition}\)
A history \(h_{t_0} \in H_{t_0}\)
is said to satisfy a scientific theory \(st \in ST\) until \(t_0 \in T\) if \(\exists h \in H\) extending \(h_{t_0}\) such that \(st(h) = ⊤\). A history \(h_{<t_0} \in H_{<t_0}\) is said
to satisfy a scientific theory \(st \in
ST\) before \(t_0 \in T\)
if \(\exists h \in H\) extending
\(h_{<t_0}\) such that \(st(h) = ⊤\).
Definition ScientificTheory : Type := History -> Prop. Definition satisfies (h : History) (st : ScientificTheory) : Prop := st h. Definition satisfies_until {t0 : Time} (h0 : HistoryUntil t0) (st : ScientificTheory) : Prop := exists (h : History), st h /\ extends_until h h0. Definition satisfies_before {t0 : Time} (h0 : HistoryBefore t0) (st : ScientificTheory) : Prop := exists (h : History), st h /\ extends_before h h0.
An event is possible if there is a scientifically possible history in which it happens.
\(\mathbf{Definition}\)
An event \(e \in E\) is said
possible according to a scientific theory if there exists a
history satisfying this theory in which \(e\) happens.
Definition is_possible (event : Event) (st : ScientificTheory) : Prop := exists (h : History), satisfies h st /\ event h = true.
The more patterns of behavior of the environment you take into account, the more precise (that is, restrictive) is your scientific theory.
\(\mathbf{Definition}\)
\(st_1 \in ST\) is said more
precise than \(st_2 \in ST\) if
\(\forall h \in H, st_2(h) = ⊥
\Rightarrow st_1(h) = ⊥\).
Definition more_precise (st1 st2 : ScientificTheory) : Prop := forall (h : History), st2 h -> st1 h.
Considering the scientific theories consistent with the current history, Occam’s razor recommends to adopt the simplest one (for example to predict the future). If you don’t, your quest to determine the scientific theory describing the laws of the environment as precisely as possible will not take the simplest way either. As an example, if you are given the sequence 0101010101 and must find the following digits, you will probably notice that the sequence alternates between 0 and 1 and predict accordingly, but you may also conjecture that the sequence stops alternating at the 100-th digit. This may be quite an artificial claim though.
\(\mathbf{Definition}\)
A history \(h_{t_0} \in H_{t_0}\)
being given, the scientific theory prefered by Occam’s razor is
the simplest one satisjfying \(h_{t_0}\) (whatever the total
relation order used to define the simplicity of scientific
theories).
Context {SimplerThan : TotalOrder ScientificTheory}. Definition occam_preferred {t0 : Time} (h0 : HistoryUntil t0) (st : ScientificTheory) : Prop := satisfies_until h0 st /\ forall (st2 : ScientificTheory), satisfies_until h0 st2 -> non_strict SimplerThan st st2.
