Leibniz' Project
Here is formalized the scientific process of an agent in an evironment.
One relies on this article.
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\) the set of actions.
Context {TimePerception : Type}. Context {SpacePerception : Type}. Context {Action : Type}. Context {Before : TotalOrder TimePerception}. Context {SimplerThan : TotalOrder ( @ScientificTheory TimePerception (SpacePerception * Action) )}.
If at some instant you have a scientific theory satisfying the history, we have to put it to the test. Otherwise an agent connected to internet would conclude that it never receives any signal and stick to this without trying to send different signals, which can lead to some www.existing_website.com and thus to an incoming signal. When the agent makes actions such that the scientific theory prefered by Occam’s razor changes, its insight has improved.
\(\mathbf{Definition}\)
Let \(t_1 < t_2\) be instants
of \(T\) and \(h_2\) a history until \(t_2\).
It is said that insight improved if the scientific theory prefered
by Occam’s razor at \(t_1\) is
strictly simpler than the one at \(t_2\).
Definition brought_insight {t1 t2 : TimePerception} (bef : non_strict Before t1 t2) (h2 : @HistoryUntil TimePerception (SpacePerception * Action) Before t2) : Prop := forall (st1 st2 : @ScientificTheory TimePerception (SpacePerception * Action)), @occam_preferred TimePerception (SpacePerception * Action) Before SimplerThan t1 ( @HistoryUntil_restriction TimePerception (SpacePerception * Action) Before t1 t2 bef h2 ) st1 -> @occam_preferred TimePerception ( SpacePerception * Action ) Before SimplerThan t2 h2 st2 -> strict SimplerThan st1 st2.
