[FRIAM] mental imagery
glen
gepropella at gmail.com
Mon Nov 24 13:56:09 EST 2025
Yes. But it's more a matter of available energy than impedance matching. Mismatches are tolerable when there's plenty of energy available, intolerable otherwise. It's also scalable, composite. Matching in a crowd is different from matching with an individual. Energy is primary, matching secondary.
I can easily imagine that for *some*, it takes more energy to entertain others' "as if postures" than it does to well-place them in an arching structure. For example, it may be *easier* for a historian to politely correct someone at a dinner party than to simply stay quiet and allow a mistake to persist. Or for a good faith steelmanner to ask critical path questions. That may be less expensive to them than role-playing. (For those of us who can't do anything but role-play, with no identifiable "authentic self", attempts at authenticity are more expensive.)
The schema only evolve *if* I have enough energy to break them in little ways. Otherwise, they're static shunts for avoiding benefit-less costs, like querying a newly certified reiki masseuse about the mechanism of action. It's much much cheaper to simply play their game. As I age, my energy wanes. 8^D
On 11/24/25 7:36 AM, Marcus Daniels wrote:
> 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 <friam-bounces at redfish.com> On Behalf Of glen
> Sent: Monday, November 24, 2025 6:41 AM
> To: friam at redfish.com
> 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 μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.
More information about the Friam
mailing list