I hope somebody is going to explain this to me. It seems too rich for me not to understand it.
N On Sun, Nov 23, 2025 at 10:01 AM Marcus Daniels <[email protected]> wrote: > Migraine and dog examples, tested in a MCP server controlled by Claude. > > *Key aspects:* > > 1. *Universe-level encoding* - Discourse.{u} : Type (u+1) := Type u > allows self-reference through the type hierarchy without triggering > non-positivity errors > 2. *The three layers* captured in AsIfPosture: > > > - treatsAsReal - treating "migraine aura" as an objective category > - acknowledgesEmbodiment - Nick's particular, embodied instance > - acknowledgesDiscursive - the vocabulary comes from shared > discourse > > > 3. *Self-awareness* - the selfAware field and metaPosture show that > the posture can reflect on itself > 4. *All theorems verify* - proving we can coherently adopt this stance > > This achieves the coinductive spirit (self-referential structures that can > contain references to themselves) in a way that Lean 4's type checker > accepts. > > -- Migraine aura example with self-reference via universe levels > > -- (Lean 4's way of encoding coinductive-style structures) > > > > -- A discourse at universe level u references discourses at level u > > def Discourse.{u} : Type (u+1) := Type u > > > > -- Properties of a discourse state > > structure DiscourseState (D : Type) where > > category : String > > body : String > > treatedAsObjective : Bool > > acknowledgesEmbodiment : Bool > > acknowledgesDiscursive : Bool > > property : D → Prop > > > > -- Nick's migraine aura as a discourse state > > def MigraineAuraType : Discourse := Unit > > > > def migraineState : DiscourseState MigraineAuraType := { > > category := "migraine aura", > > body := "Nick", > > treatedAsObjective := true, > > acknowledgesEmbodiment := true, > > acknowledgesDiscursive := true, > > property := λ _ => True > > } > > > > -- The "as if" posture structure > > structure AsIfPosture where > > objectiveCategory : String > > embodiedInstance : String > > subjectiveVocabulary : String > > treatsAsReal : Bool > > acknowledgesEmbodiment : Bool > > acknowledgesDiscursive : Bool > > selfAware : Bool > > > > -- The posture adopted when saying "Nick is experiencing his own migraine > aura" > > def migrainePosture : AsIfPosture := { > > objectiveCategory := "migraine aura", > > embodiedInstance := "Nick", > > subjectiveVocabulary := "aural sensation", > > treatsAsReal := true, > > acknowledgesEmbodiment := true, > > acknowledgesDiscursive := true, > > selfAware := true > > } > > > > -- What it means to adopt this posture > > def adoptsPosture (p : AsIfPosture) : Prop := > > p.treatsAsReal = true ∧ > > p.acknowledgesEmbodiment = true ∧ > > p.acknowledgesDiscursive = true ∧ > > p.selfAware = true > > > > -- Verify we can adopt the migraine posture > > theorem can_adopt_migraine_posture : adoptsPosture migrainePosture := by > > unfold adoptsPosture migrainePosture > > exact ⟨rfl, rfl, rfl, rfl⟩ > > > > -- The self-referential twist: we can have a posture about postures > > def metaPosture : AsIfPosture := { > > objectiveCategory := "epistemic posture", > > embodiedInstance := "speaker", > > subjectiveVocabulary := "stance-taking", > > treatsAsReal := true, > > acknowledgesEmbodiment := true, > > acknowledgesDiscursive := true, > > selfAware := true > > } > > > > -- We can reflect on the posture itself > > theorem can_reflect_on_posture : adoptsPosture metaPosture := by > > unfold adoptsPosture metaPosture > > exact ⟨rfl, rfl, rfl, rfl⟩ > > > > -- Key property: the posture acknowledges all three layers simultaneously > > theorem posture_three_layers : > > migrainePosture.treatsAsReal = true ∧ > > migrainePosture.acknowledgesEmbodiment = true ∧ > > migrainePosture.acknowledgesDiscursive = true := by > > unfold migrainePosture > > exact ⟨rfl, rfl, rfl⟩ > > > > #check can_adopt_migraine_posture > > #check can_reflect_on_posture > > #check posture_three_layers > > > Now the dog example… > > *Cross-species coordination* (humanDogFairnessCoordination) - Dogs can > have a sense of fairness similar enough to humans for empathy and > coordination to work > > *Embodiment matters* (cone_adds_shared_features) - The cone-snout study: > changing embodiment features (adding "snout" to the human) improved > gaze-following coordination from failure to success > > *Coordination isn't guaranteed* (coordination_not_guaranteed_by_similarity) > - Even identical embodiment features don't guarantee successful > coordination, as shown by human-to-human failures > > This formalizes the gradient you described: as similarity increases, > coordination quality improves, but there's no deterministic guarantee. The > cone-snout example is particularly nice because it shows how specific > embodiment features affect what can be intersubjectively stabilized. > > The formalization also captures the point about lacking "high-quality > understanding" - we can model that coordination succeeds or fails, but the > structure doesn't claim to explain *why* the similarities are sufficient > in some cases and not others. It just tracks that they matter. > > -- Formalizing "as if" postures in discourse > > -- Extended: similarity, embodiment, and coordination failure > > > > structure ObjectiveCategory where > > name : String > > supposedlyReal : Prop > > > > structure EmbodiedInstance (C : ObjectiveCategory) where > > body : String > > embodimentFeatures : List String > > noDisembodiedAccess : Prop > > intersubjectivelyVerifiable : Prop > > > > -- Coordination can succeed or fail > > inductive CoordinationResult where > > | success : CoordinationResult > > | failure : CoordinationResult > > > > structure CoordinationAttempt (C : ObjectiveCategory) where > > instance1 : EmbodiedInstance C > > instance2 : EmbodiedInstance C > > result : CoordinationResult > > > > -- EXAMPLE 1: Cross-species fairness coordination > > def fairnessCategory : ObjectiveCategory := { > > name := "sense of fairness", > > supposedlyReal := True > > } > > > > def humanInstance : EmbodiedInstance fairnessCategory := { > > body := "human", > > embodimentFeatures := ["face", "hands", "upright"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > def dogInstance : EmbodiedInstance fairnessCategory := { > > body := "dog", > > embodimentFeatures := ["snout", "quadruped", "tail"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > -- We can coordinate on fairness with dogs (enough similarity for empathy) > > def humanDogFairnessCoordination : CoordinationAttempt fairnessCategory := > { > > instance1 := humanInstance, > > instance2 := dogInstance, > > result := CoordinationResult.success > > } > > > > -- EXAMPLE 2: The gaze-following / cone-snout study > > def gazeCategory : ObjectiveCategory := { > > name := "gaze direction", > > supposedlyReal := True > > } > > > > def humanGaze : EmbodiedInstance gazeCategory := { > > body := "human", > > embodimentFeatures := ["eyes", "face"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > def dogGaze : EmbodiedInstance gazeCategory := { > > body := "dog", > > embodimentFeatures := ["eyes", "snout"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > -- Without cone-snout: marginal to poor coordination > > def humanDogGazeBaseline : CoordinationAttempt gazeCategory := { > > instance1 := humanGaze, > > instance2 := dogGaze, > > result := CoordinationResult.failure > > } > > > > -- With cone-snout: improved coordination due to shared snout feature > > def humanWithConeSnout : EmbodiedInstance gazeCategory := { > > body := "human", > > embodimentFeatures := ["eyes", "face", "snout"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > def humanDogGazeWithCone : CoordinationAttempt gazeCategory := { > > instance1 := humanWithConeSnout, > > instance2 := dogGaze, > > result := CoordinationResult.success > > } > > > > -- Shared features predicate > > def hasSharedFeature (C : ObjectiveCategory) (i1 i2 : EmbodiedInstance C) > : Prop := > > ∃ f, f ∈ i1.embodimentFeatures ∧ f ∈ i2.embodimentFeatures > > > > -- Theorem: The cone-snout intervention adds shared features > > theorem cone_adds_shared_features : > > hasSharedFeature gazeCategory humanWithConeSnout dogGaze ∧ > > (∃ f, f = "snout" ∧ f ∈ humanWithConeSnout.embodimentFeatures ∧ f ∈ > dogGaze.embodimentFeatures) := by > > constructor > > · unfold hasSharedFeature humanWithConeSnout dogGaze > > exists "eyes" > > · exists "snout" > > > > -- EXAMPLE 3: Coordination can fail even between identical instances > > def humanInstance2 : EmbodiedInstance fairnessCategory := { > > body := "human", > > embodimentFeatures := ["face", "hands", "upright"], > > noDisembodiedAccess := True, > > intersubjectivelyVerifiable := True > > } > > > > def humanHumanFailure : CoordinationAttempt fairnessCategory := { > > instance1 := humanInstance, > > instance2 := humanInstance2, > > result := CoordinationResult.failure > > } > > > > -- Theorem: Even identical embodiment doesn't guarantee coordination > > theorem coordination_not_guaranteed_by_similarity : > > humanInstance.embodimentFeatures = humanInstance2.embodimentFeatures ∧ > > humanHumanFailure.result = CoordinationResult.failure := by > > constructor > > · rfl > > · rfl > .- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / > ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. > FRIAM Applied Complexity Group listserv > Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom > https://bit.ly/virtualfriam > to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com > FRIAM-COMIC http://friam-comic.blogspot.com/ > archives: 5/2017 thru present > https://redfish.com/pipermail/friam_redfish.com/ > 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/ > -- Nicholas S. Thompson Emeritus Professor of Psychology and Ethology Clark University [email protected] https://wordpress.clarku.edu/nthompson
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
