<div dir="ltr"><div dir="ltr"><div class="gmail_default" style="font-family:verdana,sans-serif;font-size:small;color:#333333">Nick,</div><div class="gmail_default" style="font-family:verdana,sans-serif;font-size:small;color:#333333"><br></div><div class="gmail_default" style="font-family:verdana,sans-serif;font-size:small;color:#333333">The code is a formal reporting of each of Eric&#39;s claims, along with theorems demonstrating the internal validity of his reasoning. There is a lot of boilerplate, because you know, formal languages. The use of dependent typing and coinduction do some heavy lifting wrt self-reference in the following snippets:</div><div class="gmail_default" style="font-family:verdana,sans-serif;font-size:small;color:#333333"><br></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="monospace">def Discourse.{u} : Type (u+1) := Type u<br><br>structure DiscourseState (D : Type) where ... property : D \u2192 Prop</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="monospace"><br>structure EmbodiedInstance (C : ObjectiveCategory) where ...<br><br></font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">as Eric posited:</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif"><br></font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">&quot;&quot;&quot;</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><pre style="color:rgb(0,0,0)"><font face="verdana, sans-serif">It feels like there ought to be some formal-language way, using some representation for self-reference, to articulate what it means to (said objectively) \u201cbe in a posture of\u201d treating the state of discourse \u201cas if\u201d it entailed these affordances-from-the-objective, while acknowledging that the whole thing is self-referent within a system that could be free-floating.
</font></pre><font face="verdana, sans-serif">&quot;&quot;&quot;</font></div></div>
</div>