Houlihan et al. (2023): Emotion prediction as computation over a generative theory of mind

This file formalizes the inverse planning and computed appraisal modules of [HKWH+23] for the Split or Steal game. A Player values an outcome by three Fehr–Schmidt base features, money against a reference point and the two inequities, weighted by preferences and passed through a value function; the expected base utility of an action under the player's belief about the opponent is (3.1) (Setting.expectedBaseUtility), the softmax policy is (3.3) (Setting.policy), and the observer's inverse inference (3.4) is the posterior kernel of the plan over a finite prior (Setting.posterior). The public game adds the reputation utilities of (3.2), the base weights an observer of the anonymous game would infer from the action (Setting.expectedPublicUtility).

The direction of the inferences in Figure 2 follows from the covariance form of Bayes' rule: observing cooperation raises the posterior expectation of any statistic that monovaries with the expected-utility gap in favour of cooperating, and in Split or Steal that gap increases in the advantageous-inequity weight and decreases in the money and disadvantageous-inequity weights. The appraisals of Section 4, achieved utility, prediction error and the two counterfactuals, then carry structural signs: a cooperator whose opponent stole has a negative disadvantageous-inequity prediction error and a positive opponent counterfactual, the two loadings of the learned envy concept, and a player who stole from a cooperator has a negative advantageous-inequity utility that cooperating would have spared.

Implementation notes

• The prior over preferences and beliefs is carried by a finite type of simulated players, as in the paper's sampled implementation; the value function ν is any strictly monotone function vanishing at zero, in place of the sign-adjusted logarithm.
• Figure 2's per-weight directions are stated for priors that vary in that weight alone, which is what makes the weight monovary with the utility gap; a correlated prior can reverse them, and the paper reports only its empirical prior.
• The lesion models of Section 5 are the constant posterior and the restriction to the money domain; the learned readout of Section 8 and the fitted concordances are not formalized.

References

• [HKWH+23]
• [FS99]

The game

inductive HoulihanEtAl2023.Action : Type

Split (cooperate) or steal (defect).

• cooperate : Action
• defect : Action

@[instance_reducible]

instance HoulihanEtAl2023.instDecidableEqAction : DecidableEq Action

Equations

• HoulihanEtAl2023.instDecidableEqAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HoulihanEtAl2023.instFintypeAction : Fintype Action

Equations

• One or more equations did not get rendered due to their size.

instance HoulihanEtAl2023.instNonemptyAction : Nonempty Action

@[instance_reducible]

instance HoulihanEtAl2023.instMeasurableSpaceAction : MeasurableSpace Action

Equations

• HoulihanEtAl2023.instMeasurableSpaceAction = ⊤

def HoulihanEtAl2023.Action.other : Action → Action

The action not chosen.

Equations

• HoulihanEtAl2023.Action.cooperate.other = HoulihanEtAl2023.Action.defect
• HoulihanEtAl2023.Action.defect.other = HoulihanEtAl2023.Action.cooperate

@[simp]

theorem HoulihanEtAl2023.Action.other_cooperate : cooperate.other = defect

@[simp]

theorem HoulihanEtAl2023.Action.other_defect : defect.other = cooperate

@[simp]

theorem HoulihanEtAl2023.Action.other_other (a : Action) : a.other.other = a

theorem HoulihanEtAl2023.sum_action {β : Type u_1} [AddCommMonoid β] (f : Action → β) : ∑ a : Action, f a = f Action.cooperate + f Action.defect

noncomputable def HoulihanEtAl2023.payoff (pot : ℝ) : Action → Action → ℝ

Player 1's share of the pot: half when both split, all of it when stealing from a splitter, and nothing otherwise.

Equations

• HoulihanEtAl2023.payoff pot HoulihanEtAl2023.Action.cooperate HoulihanEtAl2023.Action.cooperate = pot / 2
• HoulihanEtAl2023.payoff pot HoulihanEtAl2023.Action.cooperate HoulihanEtAl2023.Action.defect = 0
• HoulihanEtAl2023.payoff pot HoulihanEtAl2023.Action.defect HoulihanEtAl2023.Action.cooperate = pot
• HoulihanEtAl2023.payoff pot HoulihanEtAl2023.Action.defect HoulihanEtAl2023.Action.defect = 0

theorem HoulihanEtAl2023.payoff_cooperate_le_defect {pot : ℝ} (hpot : 0 ≤ pot) (a₂ : Action) : payoff pot Action.cooperate a₂ ≤ payoff pot Action.defect a₂

Stealing weakly dominates in money.

inductive HoulihanEtAl2023.Domain : Type

The three base features of an outcome: money and the two inequities of Fehr and Schmidt's utility.

• money : Domain
• aia : Domain
• dia : Domain

@[instance_reducible]

instance HoulihanEtAl2023.instDecidableEqDomain : DecidableEq Domain

Equations

• HoulihanEtAl2023.instDecidableEqDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HoulihanEtAl2023.instFintypeDomain : Fintype Domain

Equations

• One or more equations did not get rendered due to their size.

theorem HoulihanEtAl2023.sum_domain {β : Type u_1} [AddCommMonoid β] (f : Domain → β) : ∑ d : Domain, f d = f Domain.money + f Domain.aia + f Domain.dia

noncomputable def HoulihanEtAl2023.Domain.feature (pot ref : ℝ) (a₁ a₂ : Action) : Domain → ℝ

The base feature of an outcome in a domain, money measured against the reference point ref.

Equations

• HoulihanEtAl2023.Domain.feature pot ref a₁ a₂ HoulihanEtAl2023.Domain.money = HoulihanEtAl2023.payoff pot a₁ a₂ - ref
• HoulihanEtAl2023.Domain.feature pot ref a₁ a₂ HoulihanEtAl2023.Domain.aia = (HoulihanEtAl2023.payoff pot a₁ a₂ - HoulihanEtAl2023.payoff pot a₂ a₁)⁺
• HoulihanEtAl2023.Domain.feature pot ref a₁ a₂ HoulihanEtAl2023.Domain.dia = (HoulihanEtAl2023.payoff pot a₂ a₁ - HoulihanEtAl2023.payoff pot a₁ a₂)⁺

def HoulihanEtAl2023.Domain.sign : Domain → ℝ

Money is sought and the inequities are avoided: the signs of (3.1).

Equations

• HoulihanEtAl2023.Domain.money.sign = 1
• HoulihanEtAl2023.Domain.aia.sign = -1
• HoulihanEtAl2023.Domain.dia.sign = -1

def HoulihanEtAl2023.Domain.repuSign (d : Domain) : ℝ

The reputation utilities of (3.2) carry the opposite signs: players want to be seen as motivated by equality rather than by money.

Equations

• d.repuSign = -d.sign

theorem HoulihanEtAl2023.feature_aia_cooperate {pot ref : ℝ} (hpot : 0 ≤ pot) (a₂ : Action) : Domain.feature pot ref Action.cooperate a₂ Domain.aia = 0

theorem HoulihanEtAl2023.feature_aia_defect_cooperate {pot ref : ℝ} (hpot : 0 ≤ pot) : Domain.feature pot ref Action.defect Action.cooperate Domain.aia = pot

theorem HoulihanEtAl2023.feature_dia_defect {pot ref : ℝ} (hpot : 0 ≤ pot) (a₂ : Action) : Domain.feature pot ref Action.defect a₂ Domain.dia = 0

theorem HoulihanEtAl2023.feature_dia_cooperate_defect {pot ref : ℝ} (hpot : 0 ≤ pot) : Domain.feature pot ref Action.cooperate Action.defect Domain.dia = pot

theorem HoulihanEtAl2023.feature_aia_defect_defect {pot ref : ℝ} : Domain.feature pot ref Action.defect Action.defect Domain.aia = 0

theorem HoulihanEtAl2023.feature_dia_cooperate_cooperate {pot ref : ℝ} : Domain.feature pot ref Action.cooperate Action.cooperate Domain.dia = 0

theorem HoulihanEtAl2023.feature_money {pot ref : ℝ} (a₁ a₂ : Action) : Domain.feature pot ref a₁ a₂ Domain.money = payoff pot a₁ a₂ - ref

Players and the forward model

structure HoulihanEtAl2023.Player : Type

A simulated player: base preference weights, reputation weights, the belief π_{a₂} that the opponent cooperates, and the reference point π_Money.

• base : Domain → ℝ
• repu : Domain → ℝ
• belief : ℝ
• reference : ℝ

def HoulihanEtAl2023.Player.beliefOn (q : Player) : Action → ℝ

The belief as a distribution over the opponent's action.

Equations

• q.beliefOn HoulihanEtAl2023.Action.cooperate = q.belief
• q.beliefOn HoulihanEtAl2023.Action.defect = 1 - q.belief

def HoulihanEtAl2023.Player.knowing (q : Player) (a₂ : Action) : Player

The player after learning the opponent's action (footnote 3).

Equations

• q.knowing a₂ = { base := q.base, repu := q.repu, belief := if a₂ = HoulihanEtAl2023.Action.cooperate then 1 else 0, reference := q.reference }

structure HoulihanEtAl2023.Setting : Type

The fixed parameters of a game: the value function ν, the rationality lam of the softmax (the paper's λ) and the pot.

• ν : ℝ → ℝ
• ν_zero : self.ν 0 = 0
• ν_strictMono : StrictMono self.ν
• lam : ℝ
• lam_pos : 0 < self.lam
• pot : ℝ
• pot_pos : 0 < self.pot

theorem HoulihanEtAl2023.Setting.ν_pot_nonneg (S : Setting) : 0 ≤ S.ν S.pot

noncomputable def HoulihanEtAl2023.Setting.domainUtility (S : Setting) (q : Player) (a₁ a₂ : Action) (d : Domain) : ℝ

The subjective utility of an outcome in one domain: the signed, weighted value of its feature, the summands of (3.1).

Equations

• S.domainUtility q a₁ a₂ d = d.sign * q.base d * S.ν (HoulihanEtAl2023.Domain.feature S.pot q.reference a₁ a₂ d)

noncomputable def HoulihanEtAl2023.Setting.baseUtility (S : Setting) (q : Player) (a₁ a₂ : Action) : ℝ

The base utility of an outcome, summed over the domains.

Equations

• S.baseUtility q a₁ a₂ = ∑ d : HoulihanEtAl2023.Domain, S.domainUtility q a₁ a₂ d

noncomputable def HoulihanEtAl2023.Setting.expectedBaseUtility (S : Setting) (q : Player) (a₁ : Action) : ℝ

(3.1): the expected base utility of an action under the belief about the opponent.

Equations

• S.expectedBaseUtility q a₁ = ∑ a₂ : HoulihanEtAl2023.Action, q.beliefOn a₂ * S.baseUtility q a₁ a₂

theorem HoulihanEtAl2023.Setting.expectedBaseUtility_cooperate_sub_defect (S : Setting) (q : Player) : S.expectedBaseUtility q Action.cooperate - S.expectedBaseUtility q Action.defect = q.belief * (q.base Domain.money * (S.ν (S.pot / 2 - q.reference) - S.ν (S.pot - q.reference)) + q.base Domain.aia * S.ν S.pot) - (1 - q.belief) * q.base Domain.dia * S.ν S.pot

The expected-utility gap in favour of cooperating: cooperation forgoes money and risks disadvantageous inequity, and avoids advantageous inequity.

noncomputable def HoulihanEtAl2023.Setting.policy (S : Setting) (U : Player → Action → ℝ) (q : Player) (a : Action) : ℝ

(3.3): the softmax policy at rationality lam for a utility U.

Equations

• S.policy U q a = Real.exp (S.lam * U q a) / ∑ a' : HoulihanEtAl2023.Action, Real.exp (S.lam * U q a')

theorem HoulihanEtAl2023.Setting.policy_eq_sigmoid (S : Setting) (U : Player → Action → ℝ) (q : Player) (a : Action) : S.policy U q a = (S.lam * (U q a - U q a.other)).sigmoid

With two actions the softmax is the logistic function of the scaled utility gap.

theorem HoulihanEtAl2023.Setting.policy_pos (S : Setting) (U : Player → Action → ℝ) (q : Player) (a : Action) : 0 < S.policy U q a

theorem HoulihanEtAl2023.Setting.policy_cooperate_add_defect (S : Setting) (U : Player → Action → ℝ) (q : Player) : S.policy U q Action.cooperate + S.policy U q Action.defect = 1

@[simp]

theorem HoulihanEtAl2023.Setting.toReal_ofReal_policy (S : Setting) (U : Player → Action → ℝ) (q : Player) (a : Action) : (ENNReal.ofReal (S.policy U q a)).toReal = S.policy U q a

theorem HoulihanEtAl2023.Setting.policy_cooperate_le_half_of_belief_eq_zero (S : Setting) (q : Player) (hb : q.belief = 0) (hd : 0 ≤ q.base Domain.dia) : S.policy S.expectedBaseUtility q Action.cooperate ≤ 1 / 2

A player certain that the opponent will steal cooperates at most half the time: the gap of (3.1) is then the disadvantageous-inequity cost of cooperating.

theorem HoulihanEtAl2023.Setting.half_le_policy_cooperate_iff (S : Setting) (q : Player) (hb : q.belief = 1) : 1 / 2 ≤ S.policy S.expectedBaseUtility q Action.cooperate ↔ q.base Domain.money * (S.ν (S.pot - q.reference) - S.ν (S.pot / 2 - q.reference)) ≤ q.base Domain.aia * S.ν S.pot

A player certain that the opponent will split prefers to cooperate exactly when the advantageous-inequity cost of stealing outweighs the money it gains: the Fehr–Schmidt account of cooperation.

Inverse planning

noncomputable def HoulihanEtAl2023.Setting.plan (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) : ProbabilityTheory.Kernel Ω Action

The forward model as a kernel from the prior's support to actions.

Equations

• S.plan U p = ProbabilityTheory.Kernel.ofWeights fun (ω : Ω) (a : HoulihanEtAl2023.Action) => ENNReal.ofReal (S.policy U (p ω) a)

theorem HoulihanEtAl2023.Setting.plan_real (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) (ω : Ω) (a : Action) : ((S.plan U p) ω).real {a} = S.policy U (p ω) a

theorem HoulihanEtAl2023.Setting.plan_apply_singleton_ne_zero (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) (ω : Ω) (a : Action) : ((S.plan U p) ω) {a} ≠ 0

instance HoulihanEtAl2023.Setting.instIsMarkovKernelActionPlan (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) : ProbabilityTheory.IsMarkovKernel (S.plan U p)

theorem HoulihanEtAl2023.Setting.comp_plan_ne_zero (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (a : Action) : (μ.bind ⇑(S.plan U p)) {a} ≠ 0

noncomputable def HoulihanEtAl2023.Setting.posterior (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty Ω] : ProbabilityTheory.Kernel Action Ω

(3.4): the observer's inverse inference, the posterior kernel of the plan.

Equations

• S.posterior U p μ = ProbabilityTheory.posterior (S.plan U p) μ

noncomputable def HoulihanEtAl2023.Setting.expectation (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty Ω] (f : Player → ℝ) (a : Action) : ℝ

The posterior expectation of a statistic of the player after observing an action.

Equations

• S.expectation U p μ f a = ∫ (ω : Ω), f (p ω) ∂(S.posterior U p μ) a

noncomputable def HoulihanEtAl2023.priorExpectation {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : Ω → Player) (f : Player → ℝ) : ℝ

The prior expectation of a statistic of the player.

Equations

• HoulihanEtAl2023.priorExpectation μ p f = ∫ (ω : Ω), f (p ω) ∂μ

theorem HoulihanEtAl2023.Setting.priorExpectation_le_expectation_cooperate (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Player → ℝ} (hf : Monovary (f ∘ p) fun (ω : Ω) => U (p ω) Action.cooperate - U (p ω) Action.defect) : priorExpectation μ p f ≤ S.expectation U p μ f Action.cooperate

Observing cooperation raises the expectation of any statistic that monovaries with the utility gap in favour of cooperating: Bayes' rule reweights the prior by the policy, which is increasing in the gap.

theorem HoulihanEtAl2023.Setting.expectation_defect_le_priorExpectation (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Player → ℝ} (hf : Monovary (f ∘ p) fun (ω : Ω) => U (p ω) Action.cooperate - U (p ω) Action.defect) : S.expectation U p μ f Action.defect ≤ priorExpectation μ p f

Observing defection lowers it.

theorem HoulihanEtAl2023.Setting.expectation_defect_le_expectation_cooperate (S : Setting) (U : Player → Action → ℝ) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Player → ℝ} (hf : Monovary (f ∘ p) fun (ω : Ω) => U (p ω) Action.cooperate - U (p ω) Action.defect) : S.expectation U p μ f Action.defect ≤ S.expectation U p μ f Action.cooperate

def HoulihanEtAl2023.Setting.VariesOnly {Ω : Type u_1} (p : Ω → Player) (d : Domain) : Prop

A prior that varies only in the weight of one domain.

Equations

• One or more equations did not get rendered due to their size.

theorem HoulihanEtAl2023.Setting.expectation_aia_defect_le_cooperate (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : VariesOnly p Domain.aia) (hb : ∀ (ω : Ω), 0 ≤ (p ω).belief) : S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.aia) Action.defect ≤ S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.aia) Action.cooperate

Figure 2: a cooperator is inferred to be more averse to advantageous inequity.

theorem HoulihanEtAl2023.Setting.expectation_money_cooperate_le_defect (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : VariesOnly p Domain.money) (hb : ∀ (ω : Ω), 0 ≤ (p ω).belief) : S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.money) Action.cooperate ≤ S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.money) Action.defect

Figure 2: a cooperator is inferred to be less motivated by money.

theorem HoulihanEtAl2023.Setting.expectation_dia_cooperate_le_defect (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : VariesOnly p Domain.dia) (hb : ∀ (ω : Ω), (p ω).belief ≤ 1) : S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.dia) Action.cooperate ≤ S.expectation S.expectedBaseUtility p μ (fun (x : Player) => x.base Domain.dia) Action.defect

Figure 2: a cooperator is inferred to be less averse to disadvantageous inequity.

The public game

noncomputable def HoulihanEtAl2023.Setting.reputation (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (d : Domain) (a₁ : Action) : ℝ

The expected reputation in a domain: the base weight an observer of the anonymous game would infer from the action.

Equations

• S.reputation p μ d a₁ = S.expectation S.expectedBaseUtility p μ (fun (x : HoulihanEtAl2023.Player) => x.base d) a₁

noncomputable def HoulihanEtAl2023.Setting.expectedPublicUtility (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (a₁ : Action) : ℝ

(3.2): the expected utility of an action in the public game, the base utility plus the reputation utilities, each the value of the inferred base weight scaled by the pot.

Equations

• S.expectedPublicUtility p μ q a₁ = S.expectedBaseUtility q a₁ + ∑ d : HoulihanEtAl2023.Domain, d.repuSign * q.repu d * S.ν (S.reputation p μ d a₁ * S.pot)

theorem HoulihanEtAl2023.Setting.policy_cooperate_le_policy_public (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (hm : q.repu Domain.money = 0) (hd : q.repu Domain.dia = 0) (ha : 0 ≤ q.repu Domain.aia) (hrep : S.reputation p μ Domain.aia Action.defect ≤ S.reputation p μ Domain.aia Action.cooperate) : S.policy S.expectedBaseUtility q Action.cooperate ≤ S.policy (S.expectedPublicUtility p μ) q Action.cooperate

A player whose reputation concern is to be seen as averse to advantageous inequity cooperates at least as often in public as in private, since cooperating is inferred to reflect more of that aversion.

theorem HoulihanEtAl2023.Setting.policy_public_le_policy_cooperate (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (hm : q.repu Domain.money = 0) (ha : q.repu Domain.aia = 0) (hd : 0 ≤ q.repu Domain.dia) (hrep : S.reputation p μ Domain.dia Action.cooperate ≤ S.reputation p μ Domain.dia Action.defect) : S.policy (S.expectedPublicUtility p μ) q Action.cooperate ≤ S.policy S.expectedBaseUtility q Action.cooperate

A player whose reputation concern is to be seen as averse to disadvantageous inequity cooperates at most as often in public, since stealing is inferred to reflect more of it.

noncomputable def HoulihanEtAl2023.Setting.publicPosterior (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.Kernel Action Ω

(3.4) for the public game: the inverse inference over the six weights and the belief.

Equations

• S.publicPosterior p μ = S.posterior (S.expectedPublicUtility p μ) p μ

Computed appraisals (Section 4)

noncomputable def HoulihanEtAl2023.Setting.expectedDomainUtility (S : Setting) (q : Player) (a₁ : Action) (d : Domain) : ℝ

The expected utility of an action in a domain during planning.

Equations

• S.expectedDomainUtility q a₁ d = ∑ a₂ : HoulihanEtAl2023.Action, q.beliefOn a₂ * S.domainUtility q a₁ a₂ d

theorem HoulihanEtAl2023.Setting.expectedBaseUtility_eq_sum (S : Setting) (q : Player) (a₁ : Action) : S.expectedBaseUtility q a₁ = ∑ d : Domain, S.expectedDomainUtility q a₁ d

noncomputable def HoulihanEtAl2023.Setting.predictionError (S : Setting) (q : Player) (a₁ a₂ : Action) (d : Domain) : ℝ

Prediction error: the achieved utility of the outcome less the utility expected during planning.

Equations

• S.predictionError q a₁ a₂ d = S.domainUtility q a₁ a₂ d - S.expectedDomainUtility q a₁ d

noncomputable def HoulihanEtAl2023.Setting.opponentCounterfactual (S : Setting) (q : Player) (a₁ a₂ : Action) (d : Domain) : ℝ

The opponent counterfactual CFa₂: the utility the opponent's other choice would have brought, weighted by the belief that the opponent would make it.

Equations

• S.opponentCounterfactual q a₁ a₂ d = q.beliefOn a₂.other * (S.domainUtility q a₁ a₂.other d - S.domainUtility q a₁ a₂ d)

noncomputable def HoulihanEtAl2023.Setting.agentCounterfactual (S : Setting) (q : Player) (U : Player → Action → ℝ) (a₁ a₂ : Action) (d : Domain) : ℝ

The agent counterfactual CFa₁: the utility the player's other choice would have brought, weighted by the probability of that choice under the policy of the player who knows the opponent's action (footnote 3).

Equations

• S.agentCounterfactual q U a₁ a₂ d = S.policy U (q.knowing a₂) a₁.other * (S.domainUtility q a₁.other a₂ d - S.domainUtility q a₁ a₂ d)

def HoulihanEtAl2023.Setting.beliefError (q : Player) (a₂ : Action) : ℝ

The absolute prediction error of the opponent's action, |PE_{π_{a₂}}|.

Equations

• HoulihanEtAl2023.Setting.beliefError q a₂ = |1 - q.beliefOn a₂|

theorem HoulihanEtAl2023.Setting.predictionError_dia_cooperate_defect_nonpos (S : Setting) (q : Player) (hd : 0 ≤ q.base Domain.dia) (hb : 0 ≤ q.belief) : S.predictionError q Action.cooperate Action.defect Domain.dia ≤ 0

Envy's first loading (Figure 5b): a cooperator whose opponent stole is in a more disadvantageous position than expected.

theorem HoulihanEtAl2023.Setting.opponentCounterfactual_dia_cooperate_defect_nonneg (S : Setting) (q : Player) (hd : 0 ≤ q.base Domain.dia) (hb : 0 ≤ q.belief) : 0 ≤ S.opponentCounterfactual q Action.cooperate Action.defect Domain.dia

Envy's second loading (Figure 5b): had the opponent split, the cooperator would have been in a less disadvantageous position.

theorem HoulihanEtAl2023.Setting.domainUtility_aia_defect_cooperate_nonpos (S : Setting) (q : Player) (ha : 0 ≤ q.base Domain.aia) : S.domainUtility q Action.defect Action.cooperate Domain.aia ≤ 0

Guilt's structural condition: stealing from a splitter costs advantageous-inequity utility.

theorem HoulihanEtAl2023.Setting.agentCounterfactual_aia_defect_cooperate_nonneg (S : Setting) (q : Player) (U : Player → Action → ℝ) (ha : 0 ≤ q.base Domain.aia) : 0 ≤ S.agentCounterfactual q U Action.defect Action.cooperate Domain.aia

Guilt's structural condition: splitting would have spared that cost.

theorem HoulihanEtAl2023.Setting.opponentCounterfactual_money_cooperate_cooperate_nonpos (S : Setting) (q : Player) (hm : 0 ≤ q.base Domain.money) (hb : q.belief ≤ 1) : S.opponentCounterfactual q Action.cooperate Action.cooperate Domain.money ≤ 0

Gratitude's structural condition: had the opponent stolen from a splitter, the money would have been worse.

theorem HoulihanEtAl2023.Setting.agentCounterfactual_dia_defect_defect_nonpos (S : Setting) (q : Player) (U : Player → Action → ℝ) (hd : 0 ≤ q.base Domain.dia) : S.agentCounterfactual q U Action.defect Action.defect Domain.dia ≤ 0

When both steal, a defector who had split would have been left with nothing against a full pot: the base agent counterfactual is relief rather than regret in the disadvantageous domain, so regret after mutual stealing must come from reputation.

noncomputable def HoulihanEtAl2023.Setting.reputationUtility (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (a₁ : Action) (d : Domain) : ℝ

The reputation utility of an action in a domain, the summands of (3.2).

Equations

• S.reputationUtility p μ q a₁ d = d.repuSign * q.repu d * S.ν (S.reputation p μ d a₁ * S.pot)

noncomputable def HoulihanEtAl2023.Setting.reputationAgentCounterfactual (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (U : Player → Action → ℝ) (a₁ a₂ : Action) (d : Domain) : ℝ

The agent counterfactual over reputation.

Equations

• S.reputationAgentCounterfactual p μ q U a₁ a₂ d = S.policy U (q.knowing a₂) a₁.other * (S.reputationUtility p μ q a₁.other d - S.reputationUtility p μ q a₁ d)

theorem HoulihanEtAl2023.Setting.reputationAgentCounterfactual_aia_defect_nonneg (S : Setting) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] (p : Ω → Player) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (q : Player) (U : Player → Action → ℝ) (ha : 0 ≤ q.repu Domain.aia) (hrep : S.reputation p μ Domain.aia Action.defect ≤ S.reputation p μ Domain.aia Action.cooperate) (a₂ : Action) : 0 ≤ S.reputationAgentCounterfactual p μ q U Action.defect a₂ Domain.aia

Regret and guilt over reputation: whatever the opponent did, a defector who cares to be seen as averse to advantageous inequity would have been seen as more so had they split.

Lesions (Section 5)

theorem HoulihanEtAl2023.Setting.domainUtility_money_cooperate_lt_defect (S : Setting) (q : Player) (hm : 0 < q.base Domain.money) : S.domainUtility q Action.cooperate Action.cooperate Domain.money < S.domainUtility q Action.defect Action.cooperate Domain.money

The social lesion keeps only the money appraisals; a reader of monetary achieved utility then ranks stealing from a splitter above splitting with one, whereas observers predict similar joy for both.

def HoulihanEtAl2023.lesionedPosterior {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.Kernel Action Ω

The inverse planning lesion: the posterior of (3.4) replaced by the prior, so that the inferred preferences and beliefs no longer depend on the action.

Equations

• HoulihanEtAl2023.lesionedPosterior μ = ProbabilityTheory.Kernel.const HoulihanEtAl2023.Action μ

theorem HoulihanEtAl2023.lesionedPosterior_expectation {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : Ω → Player) (f : Player → ℝ) (a : Action) : ∫ (ω : Ω), f (p ω) ∂(lesionedPosterior μ) a = priorExpectation μ p f