Interesting endeavor... this is nice to have an attempt at a formal definition with no axiom introduced.
