Documentation

Linglib.Phenomena.Generics.Studies.Kirkpatrick2024

@cite{kirkpatrick-2024}: The Dynamics of Generics #

James Ravi Kirkpatrick, "The Dynamics of Generics." Journal of Semantics 40(4), 2024. 523–548.

Core Contribution #

Explains the asymmetry between generic Sobel sequences and their reverses using a dynamic semantic theory where generics expand a "modal horizon."

Sobel sequence: "Ravens are black; but albino ravens aren't." (felicitous)
Reverse Sobel: "#Albino ravens aren't black; but ravens are." (infelicitous)

Existing static theories (Cohen's probabilistic account, @cite{cohen-1999a}; Greenberg's normality-based account; Sterken's indexical approach) assign equivalent truth conditions to both orders and cannot explain the asymmetry.

The key mechanism is that generics expand the set of salient individuals (the modal horizon) as a side effect of assertion. The first generic in a discourse excludes exceptional individuals from the horizon; subsequent generics are evaluated against the expanded horizon. Reversing the order makes exceptional individuals salient before the general claim is assessed.

Key predictions (verified below) #

Generic Sobel sequences are consistent (sobel_consistent)
Reverse generic Sobel sequences are inconsistent (reverse_sobel_inconsistent)
Mixed generic sequences with non-overlapping contextual variables are consistent (mixed_consistent)

Connection to other Generics studies #

@cite{cohen-1999a} (Studies/Cohen1999.lean): static probabilistic GEN with threshold 0.5 — cannot explain order effects
@cite{tessler-goodman-2019} (Studies/TesslerGoodman2019.lean): RSA model explaining prevalence-based judgments — complementary, not competing

inductive Phenomena.Generics.Studies.Kirkpatrick2024.Raven :

Three entities: two normal ravens and one albino raven.

normal1 : Raven
normal2 : Raven
albino : Raven

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqRaven :

DecidableEq Raven

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqRaven x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.Studies.Kirkpatrick2024.instBEqRaven.beq :

Raven → Raven → Bool

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqRaven.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instBEqRaven :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqRaven = { beq := Phenomena.Generics.Studies.Kirkpatrick2024.instBEqRaven.beq }

def Phenomena.Generics.Studies.Kirkpatrick2024.instReprRaven.repr :

Raven → Nat → Std.Format

Equations

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

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instReprRaven :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instReprRaven = { reprPrec := Phenomena.Generics.Studies.Kirkpatrick2024.instReprRaven.repr }

def Phenomena.Generics.Studies.Kirkpatrick2024.isRaven :

All entities are ravens.

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.isRaven x✝ = true

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.isAlbinoRaven :

Only the albino raven is an albino raven.

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.isBlack :

Normal ravens are black; the albino is not.

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.normalRavens :

Normal ravens for the "raven" restrictor class: the non-albino ones. These are the output of NormalityOrder.optimal applied to ravens.

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.normalRavens = [Phenomena.Generics.Studies.Kirkpatrick2024.Raven.normal1 , Phenomena.Generics.Studies.Kirkpatrick2024.Raven.normal2 ]

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.normalAlbinoRavens :

Normal albino ravens: all albino ravens are "normal" for their subkind. (Albino is not abnormal qua albino raven — it's abnormal qua raven.)

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.normalAlbinoRavens = [Phenomena.Generics.Studies.Kirkpatrick2024.Raven.albino ]

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.ravensAreBlack :

Semantics.Dynamic.Generics.GenericSentence Raven

"Ravens are black"

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.albinoRavensArentBlack :

Semantics.Dynamic.Generics.GenericSentence Raven

"Albino ravens aren't black"

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.sobelSequence :

List (Semantics.Dynamic.Generics.GenericSentence Raven)

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.sobelSequence = [Phenomena.Generics.Studies.Kirkpatrick2024.ravensAreBlack , Phenomena.Generics.Studies.Kirkpatrick2024.albinoRavensArentBlack ]

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.sobel_consistent :

Semantics.Dynamic.Generics.isConsistent sobelSequence = true

def Phenomena.Generics.Studies.Kirkpatrick2024.reverseSobelSequence :

List (Semantics.Dynamic.Generics.GenericSentence Raven)

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.reverseSobelSequence = [Phenomena.Generics.Studies.Kirkpatrick2024.albinoRavensArentBlack , Phenomena.Generics.Studies.Kirkpatrick2024.ravensAreBlack ]

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.reverse_sobel_inconsistent :

Semantics.Dynamic.Generics.isConsistent reverseSobelSequence = false

inductive Phenomena.Generics.Studies.Kirkpatrick2024.Animal :

Two entities: a male lion and a female lion.

maleLion : Animal
femaleLion : Animal

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqAnimal :

DecidableEq Animal

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqAnimal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.Studies.Kirkpatrick2024.instBEqAnimal :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqAnimal = { beq := Phenomena.Generics.Studies.Kirkpatrick2024.instBEqAnimal.beq }

def Phenomena.Generics.Studies.Kirkpatrick2024.instBEqAnimal.beq :

Animal → Animal → Bool

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqAnimal.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.instReprAnimal.repr :

Animal → Nat → Std.Format

Equations

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

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instReprAnimal :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instReprAnimal = { reprPrec := Phenomena.Generics.Studies.Kirkpatrick2024.instReprAnimal.repr }

def Phenomena.Generics.Studies.Kirkpatrick2024.hasMane :

Animal → Bool

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.givesLiveBirth :

Animal → Bool

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.lionsHaveManes :

Semantics.Dynamic.Generics.GenericSentence Animal

"Lions have manes" — restrictor incorporates Kirkpatrick's contextual variable C = alternatives to having a mane (sexually-selected traits). Only male lions are in the domain of "mane alternatives."

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.lionsGiveBirth :

Semantics.Dynamic.Generics.GenericSentence Animal

"Lions give birth to live young" — restrictor incorporates C = alternatives to giving birth (modes of reproduction). Only female lions are in the domain of "reproduction alternatives."

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.mixedSequence :

List (Semantics.Dynamic.Generics.GenericSentence Animal)

Mixed sequence: both generics use different contextual variables C, so the first generic's salient individuals don't satisfy the second generic's restrictor. No mutual interference.

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.mixedSequence = [Phenomena.Generics.Studies.Kirkpatrick2024.lionsHaveManes , Phenomena.Generics.Studies.Kirkpatrick2024.lionsGiveBirth ]

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.mixed_consistent :

Semantics.Dynamic.Generics.isConsistent mixedSequence = true

Mixed generic sequences are consistent: the two generics don't interfere because they have non-overlapping restrictors (different contextual variables C).

theorem Phenomena.Generics.Studies.Kirkpatrick2024.mixed_reverse_consistent :

Semantics.Dynamic.Generics.isConsistent [lionsGiveBirth , lionsHaveManes ] = true

The reverse mixed sequence is also consistent — mixed sequences are symmetric because the restrictors don't overlap.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.sobel_consistent_general :

Semantics.Dynamic.Generics.isConsistent sobelSequence = true

The raven Sobel pair satisfies the general consistency theorem. This derives sobel_consistent from the paper's general argument (§5.1) rather than finite model checking.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.reverse_sobel_inconsistent_general :

Semantics.Dynamic.Generics.isConsistent reverseSobelSequence = false

The raven reverse Sobel pair satisfies the general inconsistency theorem. This derives reverse_sobel_inconsistent from the general argument (§5.2).

inductive Phenomena.Generics.Studies.Kirkpatrick2024.Person :

Example (4): "Teachers care for their students; but bad teachers don't." Another Sobel pair demonstrating the generality of the phenomenon.

goodTeacher1 : Person
goodTeacher2 : Person
badTeacher : Person

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqPerson :

DecidableEq Person

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.Studies.Kirkpatrick2024.instBEqPerson.beq :

Person → Person → Bool

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Generics.Studies.Kirkpatrick2024.instBEqPerson :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instBEqPerson = { beq := Phenomena.Generics.Studies.Kirkpatrick2024.instBEqPerson.beq }

instance Phenomena.Generics.Studies.Kirkpatrick2024.instReprPerson :

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.instReprPerson = { reprPrec := Phenomena.Generics.Studies.Kirkpatrick2024.instReprPerson.repr }

def Phenomena.Generics.Studies.Kirkpatrick2024.instReprPerson.repr :

Person → Nat → Std.Format

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.isTeacher :

Person → Bool

Equations

Phenomena.Generics.Studies.Kirkpatrick2024.isTeacher x✝ = true

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.isBadTeacher :

Person → Bool

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.caresForStudents :

Person → Bool

Equations

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.teachersCare :

Semantics.Dynamic.Generics.GenericSentence Person

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.badTeachersDontCare :

Semantics.Dynamic.Generics.GenericSentence Person

Equations

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

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.teachers_sobel_consistent :

Semantics.Dynamic.Generics.isConsistent [teachersCare , badTeachersDontCare ] = true

theorem Phenomena.Generics.Studies.Kirkpatrick2024.teachers_reverse_inconsistent :

Semantics.Dynamic.Generics.isConsistent [badTeachersDontCare , teachersCare ] = false

theorem Phenomena.Generics.Studies.Kirkpatrick2024.static_both_true_independently :

(Semantics.Dynamic.Generics.evalGeneric [] ravensAreBlack).snd = true ∧ (Semantics.Dynamic.Generics.evalGeneric [] albinoRavensArentBlack).snd = true

In discourse-initial position, Kirkpatrick's dynamic semantics reduces to static truth conditions. Both "Ravens are black" and "Albino ravens aren't black" are true when evaluated against an empty horizon — matching the predictions of static GEN.

The dynamic theory diverges from statics only in multi-sentence discourse, where prior generics have expanded the horizon.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.ravens_static_dynamic_bridge :

(Semantics.Dynamic.Generics.evalGeneric [] ravensAreBlack).snd = (List.filter isRaven normalRavens).all isBlack

The static-dynamic bridge instantiated for the raven model: discourse-initial evaluation of "Ravens are black" equals the static truth condition (all normal ravens satisfy the scope).

theorem Phenomena.Generics.Studies.Kirkpatrick2024.order_matters :

Semantics.Dynamic.Generics.isConsistent sobelSequence ≠ Semantics.Dynamic.Generics.isConsistent reverseSobelSequence

Yet the order matters for the dynamic evaluation.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.raven_forward_horizons :

Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack (Semantics.Dynamic.Generics.horizonStep ravensAreBlack []) = normalRavens ++ normalAlbinoRavens

Forward Sobel: the raven model instantiates the structural horizon theorem. Both expansions fire — normal ravens first, then the albino raven.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.raven_reverse_horizons :

Semantics.Dynamic.Generics.horizonStep ravensAreBlack (Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack []) = normalAlbinoRavens

Reverse Sobel: the general's expansion is blocked because the albino raven (made salient by the first generic) satisfies the "is a raven" restrictor. The final horizon contains only [albino].

theorem Phenomena.Generics.Studies.Kirkpatrick2024.raven_horizon_noncommutative :

Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack (Semantics.Dynamic.Generics.horizonStep ravensAreBlack []) ≠ Semantics.Dynamic.Generics.horizonStep ravensAreBlack (Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack [])

The raven model witnesses horizon non-commutativity: the forward horizon [normal1, normal2, albino] differs from the reverse horizon [albino].

theorem Phenomena.Generics.Studies.Kirkpatrick2024.raven_idempotent (horizon : List Raven) :

Semantics.Dynamic.Generics.horizonStep ravensAreBlack (Semantics.Dynamic.Generics.horizonStep ravensAreBlack horizon) = Semantics.Dynamic.Generics.horizonStep ravensAreBlack horizon

The raven generic is idempotent: processing "Ravens are black" twice against any horizon gives the same result as processing it once. This instantiates the general horizonStep_idempotent.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.albino_idempotent (horizon : List Raven) :

Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack (Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack horizon) = Semantics.Dynamic.Generics.horizonStep albinoRavensArentBlack horizon

The albino raven generic is also idempotent.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.mixed_consistent_structural :

Semantics.Dynamic.Generics.isConsistent [lionsHaveManes , lionsGiveBirth ] = true ∧ Semantics.Dynamic.Generics.isConsistent [lionsGiveBirth , lionsHaveManes ] = true

The mixed lion sequence derives from the structural non-interference theorem rather than finite model checking.

The structural horizon theorems above explain WHY the asymmetry arises: the subset relation between restrictors (albino raven ⊆ raven) creates asymmetric blocking in horizon evolution. The abstract impossibility theorem (commutative_implies_equal_verdicts in Generics.lean) then rules out ANY commutative framework — including @cite{veltman-1996}'s normallyUpdate — from modeling this asymmetry.

@cite{veltman-1996}'s normallyUpdate is commutative (normallyUpdate_comm in UpdateSemantics/Default.lean), meaning that processing "normally (ravens are black)" then "normally (albino ravens aren't black)" produces the same expectation state as the reverse order. Since the state is identical, any consistency test must give the same verdict for both orders — predicting the reverse Sobel is also felicitous, contrary to empirical judgment.

def Phenomena.Generics.Studies.Kirkpatrick2024.allRavens :

The full raven domain.

Equations

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

Instances For

def Phenomena.Generics.Studies.Kirkpatrick2024.ravenNormality :

Raven → Raven → Bool

Normality ordering on ravens: normal ravens are equally normal; the albino raven is less normal than both. This encodes the normality intuition that @cite{kirkpatrick-2024}'s theory relies on: normal-colored ravens are the "default" for raven-kind.

ravenNormality e₁ e₂ = true means e₁ is at least as normal as e₂.

Equations

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.ravensAreBlack_grounded :

(Semantics.Dynamic.Generics.GenericSentence.fromOrder isRaven isBlack allRavens ravenNormality).normalInstances = normalRavens

The stipulated normalRavens are exactly the optimal ravens under ravenNormality. This grounds the raven model: the normal instances are derived from a normality ordering, not ad hoc.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.albinoRavensArentBlack_grounded :

(Semantics.Dynamic.Generics.GenericSentence.fromOrder isAlbinoRaven (fun (e : Raven) => !isBlack e) allRavens ravenNormality).normalInstances = normalAlbinoRavens

The stipulated normalAlbinoRavens are the optimal albino ravens. Within the albino-restricted domain, the albino raven is trivially optimal (it's the only member).

def Phenomena.Generics.Studies.Kirkpatrick2024.isNormalRaven :

Binary normalcy predicate: normal ravens are not albino.

Equations

Instances For

theorem Phenomena.Generics.Studies.Kirkpatrick2024.ravensAreBlack_fromPredicate :

(Semantics.Dynamic.Generics.GenericSentence.fromPredicate isRaven isBlack allRavens isNormalRaven).normalInstances = normalRavens

fromPredicate constructs the same generic sentence as the hand-stipulated ravensAreBlack, grounding normalInstances via a binary normalcy predicate rather than a normality ordering.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.fromPredicate_agrees_fromOrder :

(Semantics.Dynamic.Generics.GenericSentence.fromPredicate isRaven isBlack allRavens isNormalRaven).normalInstances = (Semantics.Dynamic.Generics.GenericSentence.fromOrder isRaven isBlack allRavens ravenNormality).normalInstances

fromPredicate and fromOrder agree on the raven model: both constructors derive the same normal instances from their respective primitives.

This demonstrates that binary normalcy (traditional GEN) and normality orderings (Kirkpatrick/Greenberg) coincide when the ordering has exactly two equivalence classes.

@cite{kirkpatrick-2024} §3 argues that static theories — @cite{cohen-1999a}'s probabilistic account, @cite{greenberg-2003}'s normality-based account, @cite{sterken-2015}'s indexical approach — all fail to predict the Sobel asymmetry. The formal reason: static theories evaluate each generic independently (no state threading), so the conjunction of truth values is commutative. If both generics are independently true, both orders yield true ∧ true = true.

This is a special case of commutative_implies_equal_verdicts from Generics.lean: any evaluation where each generic's truth value is determined independently of discourse position is trivially commutative.

theorem Phenomena.Generics.Studies.Kirkpatrick2024.static_order_irrelevant {α : Type} (truth : α → Bool) (g₁ g₂ : α) :

(truth g₁ && truth g₂) = (truth g₂ && truth g₁)

Any state-independent evaluation assigns the same conjunction truth value regardless of presentation order.

Both raven generics are true when evaluated discourse-initially (= statically), yet the dynamic theory distinguishes the orders.

Static theories predict true ∧ true for both orders and therefore cannot model the asymmetry that @cite{kirkpatrick-2024}'s dynamic theory captures via horizon expansion and blocking.