[WCLD23]

Waldon, B., Condoravdi, C., Levin, B., & Degen, J. (2023). On the context dependence of artifact noun interpretation. In Proceedings of Sinn und Bedeutung 27, pp. 674–692.

Key Claims

1. Goal Sensitivity: policy goals systematically modulate artifact noun category boundaries. A flashlight is more likely to count as an "electronic device" when the goal is limiting distracting light than when it's limiting noise.

2. Multi-dimensional degree semantics for artifact nouns (eq. 8): ⟦vehicle⟧ = λx. Σ_{f ∈ F(vehicle)} f(x) · W(vehicle, f) where F returns context-relevant measure functions and W weights them. Artifact nouns compose additively ([SF17]), in contrast to natural kinds which compose multiplicatively.

   This is the weightedScore substrate primitive in Semantics/Degree/Aggregation.lean. Tham 2025 adds a third aggregation mode (spatialNormalizedScore, with a host-extent denominator) for physical disturbance predicates — see Studies/Tham2025.lean §15 for the substrate-level contrast (Waldon's domain has no host-extent denominator naturally; Tham's does).

3. Interpretive model (§4.2, the paper's implemented version per its own simplifying assumptions): a literal Bayesian update over each object's prohibition status. The threshold s is uniform on [0, 1] and marginalised analytically; F/W are fixed per condition; the prohibition prior is 1/2. The marginal posterior that o is prohibited then equals the goal-weighted measure m(o) (prohibitionPosterior_eq_measure), so every behavioural prediction reduces to a measure comparison.

4. Goal Sensitive vs. Goal Insensitive (§4.3): the single free parameter γ weights the context-independent cat dimension against the goal-relevant dimensions. γ = 1 is the Goal Insensitive null — provably condition-independent (goal_insensitive_at_one) — while every qualitative prediction below holds for all γ < 1; the BDA maximum-likelihood estimate is γ = 0.758 (95% CrI [0.756, 0.758]).

Model

m_g(o)  = γ·cat(o) + (1−γ)·f_g(o)                      (eq. 13)
m_B(o)  = γ·cat(o) + (1−γ)·Σ_g p(g)·f_g(o)             (eq. 14)
P(o prohibited | rule) = m(o)                           (eq. 12, fn. 20-21)

where cat is the category-membership measure, f_g the goal-relevant feature measures, and p the goal-plausibility function. Both measure forms are weightedScore instances ([SF17] additive aggregation).

inductive WaldonEtAl2023.Object : Type

Objects in the "No electronic devices" scenario (Fig. 1).

• candle : Object
• flashlight : Object
• boombox : Object
• tablet : Object

def WaldonEtAl2023.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WaldonEtAl2023.instReprObject : Repr Object

Equations

• WaldonEtAl2023.instReprObject = { reprPrec := WaldonEtAl2023.instReprObject.repr }

@[implicit_reducible]

instance WaldonEtAl2023.instDecidableEqObject : DecidableEq Object

Equations

• WaldonEtAl2023.instDecidableEqObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WaldonEtAl2023.instFintypeObject : Fintype Object

Equations

• WaldonEtAl2023.instFintypeObject = { elems := { val := ↑WaldonEtAl2023.Object.enumList, nodup := WaldonEtAl2023.Object.enumList_nodup }, complete := WaldonEtAl2023.instFintypeObject._proof_1 }

inductive WaldonEtAl2023.Goal : Type

The signaler's policy goals (Appendix A).

• limitLight : Goal
• limitNoise : Goal
• preventRecordings : Goal

def WaldonEtAl2023.instReprGoal.repr : Goal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WaldonEtAl2023.instReprGoal : Repr Goal

Equations

• WaldonEtAl2023.instReprGoal = { reprPrec := WaldonEtAl2023.instReprGoal.repr }

@[implicit_reducible]

instance WaldonEtAl2023.instDecidableEqGoal : DecidableEq Goal

Equations

• WaldonEtAl2023.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WaldonEtAl2023.instFintypeGoal : Fintype Goal

Equations

• WaldonEtAl2023.instFintypeGoal = { elems := { val := ↑WaldonEtAl2023.Goal.enumList, nodup := WaldonEtAl2023.Goal.enumList_nodup }, complete := WaldonEtAl2023.instFintypeGoal._proof_1 }

inductive WaldonEtAl2023.GoalCondition : Type

Experimental conditions (determines latentPrior over Goals).

• neutral : GoalCondition
• limitLight : GoalCondition
• limitNoise : GoalCondition
• preventRecordings : GoalCondition

def WaldonEtAl2023.instReprGoalCondition.repr : GoalCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance WaldonEtAl2023.instReprGoalCondition : Repr GoalCondition

Equations

• WaldonEtAl2023.instReprGoalCondition = { reprPrec := WaldonEtAl2023.instReprGoalCondition.repr }

@[implicit_reducible]

instance WaldonEtAl2023.instDecidableEqGoalCondition : DecidableEq GoalCondition

Equations

• WaldonEtAl2023.instDecidableEqGoalCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WaldonEtAl2023.instFintypeGoalCondition : Fintype GoalCondition

Equations

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

These values are schematic approximations, not from the paper's actual norming data. The paper parameterizes the feature measures f_g(o), the category measure cat(o), and the goal plausibilities p(g) via separate norming studies (feature attribution, category membership, and goal plausibility, §3.1). The actual values are available at the OSF links cited in the paper. The values below capture the qualitative pattern described in the paper (flashlights emit light but not noise; boomboxes emit noise but not light; etc.); the prediction theorems in §5 are additionally γ-generic, so no fitted parameter value is assumed.

def WaldonEtAl2023.emitLight : Object → ℚ

Goal-relevant feature measures — the components of the paper's eq. (8), parameterised in the paper by the feature-attribution norming study.

Equations

• WaldonEtAl2023.emitLight WaldonEtAl2023.Object.candle = 7 / 10
• WaldonEtAl2023.emitLight WaldonEtAl2023.Object.flashlight = 9 / 10
• WaldonEtAl2023.emitLight WaldonEtAl2023.Object.boombox = 1 / 10
• WaldonEtAl2023.emitLight WaldonEtAl2023.Object.tablet = 6 / 10

def WaldonEtAl2023.emitNoise : Object → ℚ

Equations

• WaldonEtAl2023.emitNoise WaldonEtAl2023.Object.candle = 1 / 20
• WaldonEtAl2023.emitNoise WaldonEtAl2023.Object.flashlight = 1 / 20
• WaldonEtAl2023.emitNoise WaldonEtAl2023.Object.boombox = 9 / 10
• WaldonEtAl2023.emitNoise WaldonEtAl2023.Object.tablet = 3 / 10

def WaldonEtAl2023.canRecord : Object → ℚ

Equations

• WaldonEtAl2023.canRecord WaldonEtAl2023.Object.candle = 1 / 20
• WaldonEtAl2023.canRecord WaldonEtAl2023.Object.flashlight = 1 / 20
• WaldonEtAl2023.canRecord WaldonEtAl2023.Object.boombox = 1 / 20
• WaldonEtAl2023.canRecord WaldonEtAl2023.Object.tablet = 9 / 10

def WaldonEtAl2023.goalFeature : Goal → Object → ℚ

The feature measure a policy goal makes relevant (eq. 13).

Equations

• WaldonEtAl2023.goalFeature WaldonEtAl2023.Goal.limitLight = WaldonEtAl2023.emitLight
• WaldonEtAl2023.goalFeature WaldonEtAl2023.Goal.limitNoise = WaldonEtAl2023.emitNoise
• WaldonEtAl2023.goalFeature WaldonEtAl2023.Goal.preventRecordings = WaldonEtAl2023.canRecord

def WaldonEtAl2023.cat : Object → ℚ

cat: the context-independent category-membership measure (the paper's cat^{elec.device}, from the category-membership norming study).

Equations

• WaldonEtAl2023.cat WaldonEtAl2023.Object.candle = 1 / 20
• WaldonEtAl2023.cat WaldonEtAl2023.Object.flashlight = 1 / 2
• WaldonEtAl2023.cat WaldonEtAl2023.Object.boombox = 19 / 20
• WaldonEtAl2023.cat WaldonEtAl2023.Object.tablet = 19 / 20

theorem WaldonEtAl2023.cat_pos (o : Object) : 0 < cat o

def WaldonEtAl2023.plausibility : Goal → ℚ

Goal-plausibility function p for the goal-neutral condition (eq. 14, fn. 22: values from the goal-plausibility norming, summing to 1 over the three goals; uniform here, schematically).

Equations

• WaldonEtAl2023.plausibility x✝ = 1 / 3

def WaldonEtAl2023.deviceMeasure (γ : ℚ) : GoalCondition → Object → ℚ

The context-sensitive measure ⟦electronic device⟧^{F,W} under each experimental condition (eqs. 13–14): a weightedScore over the cat dimension (weight γ) and the goal-relevant dimensions (weight 1−γ, plausibility-split in the goal-neutral condition).

Equations

• One or more equations did not get rendered due to their size.
• WaldonEtAl2023.deviceMeasure γ WaldonEtAl2023.GoalCondition.limitLight = Semantics.Gradability.Aggregation.weightedScore [γ, 1 - γ] [WaldonEtAl2023.cat, WaldonEtAl2023.emitLight]
• WaldonEtAl2023.deviceMeasure γ WaldonEtAl2023.GoalCondition.limitNoise = Semantics.Gradability.Aggregation.weightedScore [γ, 1 - γ] [WaldonEtAl2023.cat, WaldonEtAl2023.emitNoise]
• WaldonEtAl2023.deviceMeasure γ WaldonEtAl2023.GoalCondition.preventRecordings = Semantics.Gradability.Aggregation.weightedScore [γ, 1 - γ] [WaldonEtAl2023.cat, WaldonEtAl2023.canRecord]

theorem WaldonEtAl2023.deviceMeasure_limitLight (γ : ℚ) (o : Object) : deviceMeasure γ GoalCondition.limitLight o = γ * cat o + (1 - γ) * emitLight o

Closed form for the explicit-goal conditions (eq. 13).

theorem WaldonEtAl2023.deviceMeasure_limitNoise (γ : ℚ) (o : Object) : deviceMeasure γ GoalCondition.limitNoise o = γ * cat o + (1 - γ) * emitNoise o

theorem WaldonEtAl2023.deviceMeasure_preventRecordings (γ : ℚ) (o : Object) : deviceMeasure γ GoalCondition.preventRecordings o = γ * cat o + (1 - γ) * canRecord o

theorem WaldonEtAl2023.deviceMeasure_neutral (γ : ℚ) (o : Object) : deviceMeasure γ GoalCondition.neutral o = γ * cat o + (1 - γ) * (plausibility Goal.limitLight * emitLight o + plausibility Goal.limitNoise * emitNoise o + plausibility Goal.preventRecordings * canRecord o)

Closed form for the goal-neutral condition (eq. 14): the goal weight is split by plausibility.

theorem WaldonEtAl2023.deviceMeasure_mem_Icc {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ ≤ 1) (c : GoalCondition) (o : Object) : deviceMeasure γ c o ∈ Set.Icc 0 1

The measure stays in [0, 1] for γ ∈ [0, 1] — the domain on which the threshold semantics reads it as a probability.

noncomputable def WaldonEtAl2023.posProb (m : ℚ) : ENNReal

Probability that an object meets the standard: the threshold s is uniform on [0, 1] (fn. 20), so P(pos^s(o) = 1) = P(s ≤ m(o)) is the Lebesgue mass of [0, m].

Equations

• WaldonEtAl2023.posProb m = MeasureTheory.volume (Set.Icc 0 ↑m)

theorem WaldonEtAl2023.posProb_eq (m : ℚ) : posProb m = ENNReal.ofReal ↑m

noncomputable def WaldonEtAl2023.ruleUpdateWeight (m : ℚ) : Bool → ENNReal

Eq. (12) under the paper's implementation assumptions (fn. 21): the joint posterior weight of a prohibition status is the threshold-marginalised standard-meeting indicator times the uniform prohibition prior.

Equations

• WaldonEtAl2023.ruleUpdateWeight m true = 2⁻¹ * WaldonEtAl2023.posProb m
• WaldonEtAl2023.ruleUpdateWeight m false = 2⁻¹ * (1 - WaldonEtAl2023.posProb m)

noncomputable def WaldonEtAl2023.prohibitionPMF (m : ℚ) : PMF Bool

The listener's posterior over an object's prohibition status after observing the rule (eq. 12, marginalised over the uniform threshold).

Equations

• WaldonEtAl2023.prohibitionPMF m = PMF.normalize (WaldonEtAl2023.ruleUpdateWeight m) ⋯ ⋯

noncomputable def WaldonEtAl2023.prohibitionPosterior (γ : ℚ) (c : GoalCondition) (o : Object) : ENNReal

Marginal posterior probability that o is prohibited in condition c (the L^γ(o prohibited | rule) of eq. 15c).

Equations

• WaldonEtAl2023.prohibitionPosterior γ c o = (WaldonEtAl2023.prohibitionPMF (WaldonEtAl2023.deviceMeasure γ c o)) true

theorem WaldonEtAl2023.prohibitionPMF_eq_measure {m : ℚ} (h0 : 0 ≤ m) (h1 : m ≤ 1) : (prohibitionPMF m) true = ENNReal.ofReal ↑m

The posterior is the measure (fns. 20–21): with the threshold uniform on [0, 1] and a 1/2 prohibition prior, the marginal posterior probability of prohibition collapses to the goal-weighted measure itself. Every behavioural prediction below is therefore a measure comparison.

theorem WaldonEtAl2023.prohibitionPosterior_eq_measure {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ ≤ 1) (c : GoalCondition) (o : Object) : prohibitionPosterior γ c o = ENNReal.ofReal ↑(deviceMeasure γ c o)

Every prediction holds for all γ ∈ [0, 1) — the entire Goal Sensitive regime — via prohibitionPosterior_eq_measure plus rational arithmetic on the measures. The proofs need no fitted parameter value.

theorem WaldonEtAl2023.limitLight_flashlight_gt_candle {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitLight Object.flashlight > prohibitionPosterior γ GoalCondition.limitLight Object.candle

Under limitLight, the flashlight (edge case) is more likely prohibited than the candle (clear non-member): both cat and emit-light favour it.

theorem WaldonEtAl2023.limitNoise_boombox_gt_flashlight {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitNoise Object.boombox > prohibitionPosterior γ GoalCondition.limitNoise Object.flashlight

Under limitNoise, the boombox is the primary target.

theorem WaldonEtAl2023.limitLight_tablet_gt_boombox {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitLight Object.tablet > prohibitionPosterior γ GoalCondition.limitLight Object.boombox

Under limitLight, the tablet (clear member + emits light) outranks the boombox (clear member, no light): the cat dimension ties, so the goal dimension decides — strict only in the Goal Sensitive regime γ < 1.

theorem WaldonEtAl2023.goal_sensitivity_flashlight {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitLight Object.flashlight > prohibitionPosterior γ GoalCondition.limitNoise Object.flashlight

Goal sensitivity for flashlights (the paper's key result, Fig. 1): the flashlight is more likely prohibited under limitLight than limitNoise — the measure difference is (1−γ)·(emitLight − emitNoise)(flashlight), positive exactly when γ < 1.

theorem WaldonEtAl2023.goal_sensitivity_boombox {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitNoise Object.boombox > prohibitionPosterior γ GoalCondition.limitLight Object.boombox

Goal sensitivity for boomboxes (reverse pattern, Fig. 1).

theorem WaldonEtAl2023.goal_sensitivity_tablet {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.preventRecordings Object.tablet > prohibitionPosterior γ GoalCondition.limitNoise Object.tablet

Goal sensitivity for tablets under preventRecordings vs limitNoise.

theorem WaldonEtAl2023.light_goal_bidirectional {γ : ℚ} (h0 : 0 ≤ γ) (h1 : γ < 1) : prohibitionPosterior γ GoalCondition.limitLight Object.flashlight > prohibitionPosterior γ GoalCondition.neutral Object.flashlight ∧ prohibitionPosterior γ GoalCondition.limitLight Object.boombox < prohibitionPosterior γ GoalCondition.neutral Object.boombox

No single threshold shift explains the goal effect (the paper's argument against a purely context-shifted standard, pp. 681–682): relative to the goal-neutral baseline, the limitLight goal raises the flashlight and simultaneously lowers the boombox. A shifted threshold θ_B moves all objects the same direction; goal-sensitive dimension weights do not.

theorem WaldonEtAl2023.goal_insensitive_at_one (c c' : GoalCondition) (o : Object) : deviceMeasure 1 c o = deviceMeasure 1 c' o

The Goal Insensitive null (γ = 1): the measure ignores the goal dimensions entirely, so no condition manipulation can move any object's posterior. The experiment's Bayesian model comparison rejects this value (γ̂ = 0.758, 95% CrI [0.756, 0.758], §4.3).

def WaldonEtAl2023.fittedGamma : ℚ

The BDA maximum-likelihood estimate of γ (§4.3). Strictly inside the Goal Sensitive regime, so every prediction theorem above applies to it.

Equations

• WaldonEtAl2023.fittedGamma = 758 / 1000

theorem WaldonEtAl2023.fittedGamma_goal_sensitive : 0 ≤ fittedGamma ∧ fittedGamma < 1

theorem WaldonEtAl2023.flashlight_light_gt_noise : emitLight Object.flashlight > emitNoise Object.flashlight

The flashlight's goal-relevant feature is much stronger under limitLight than limitNoise — the driver of goal_sensitivity_flashlight.

theorem WaldonEtAl2023.boombox_noise_gt_light : emitNoise Object.boombox > emitLight Object.boombox

The boombox's pattern reverses — the driver of goal_sensitivity_boombox.

[SF17] contrast artifact nouns (additive: Σ) with natural kinds (multiplicative: Π). Under multiplicative composition, a zero on ANY dimension kills membership. Under additive, other dimensions compensate.

def WaldonEtAl2023.allFeatures : List (Object → ℚ)

All feature measures as a list (for aggregation functions).

Equations

• WaldonEtAl2023.allFeatures = [WaldonEtAl2023.emitLight, WaldonEtAl2023.emitNoise, WaldonEtAl2023.canRecord]

theorem WaldonEtAl2023.flashlight_multiplicative_negligible : Semantics.Gradability.Aggregation.multiplicativeScore allFeatures Object.flashlight < 1 / 100

Under multiplicative composition, the flashlight gets ZERO because emitNoise(flashlight) = canRecord(flashlight) = 1/20 ≈ 0. The product is negligibly small.

theorem WaldonEtAl2023.flashlight_additive_positive : Semantics.Gradability.Aggregation.weightedScore [1, 1, 1] allFeatures Object.flashlight > 1 / 2

Under additive composition, the flashlight gets a positive score despite near-zero on noise/recording — emitLight compensates.

theorem WaldonEtAl2023.artifact_aggregation_is_utilitarian : Semantics.Gradability.Aggregation.AggregationType.utilitarian ≠ Semantics.Gradability.Aggregation.AggregationType.counting

Artifact noun aggregation is utilitarian, not counting — the same point made by [DAH24] for multidimensional adjectives. [Sas13]'s binding types (conjunctive, disjunctive, mixed) are all counting aggregation and cannot capture the weighted, continuous-measure structure of artifact noun interpretation.