I think in your own description of role-playing at parties, you've described "as if" as data collection, not a grand unified theory. The counterparty is described by an evolving schema that is just good enough to "pass"?
-----Original Message----- From: Friam <[email protected]> On Behalf Of glen Sent: Monday, November 24, 2025 6:41 AM To: [email protected] Subject: Re: [FRIAM] mental imagery I don't understand how we can instantiate our ability to hold a counterfactual posture. The very existence of AsIfPosture argues it can obtain or not. We can turn it on and off, use it or not, without changing the discourse. That's what "as if" means. But I don't see it in the formalism. It's something like a complement to AsIfPosture, while retaining metaPosture. Or maybe the dependency is backwards, AsIfPosture should instead derive from metaPosture, because the only context in which you can even have AsIfPosture is when you can have a metaPosture. (Yes, I know. I'm lazy and *should* do the homework myself.) On 11/23/25 8:59 AM, Marcus Daniels 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 -- ¡sıɹƎ ןıɐH ⊥ ɐןןǝdoɹ ǝ uǝןƃ ὅτε oi μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.
smime.p7s
Description: S/MIME cryptographic signature
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. 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/
