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 errors2. *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 μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. 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/
