Generics: Dynamic Semantics with Horizon Expansion

@cite{kirkpatrick-2024}

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

Core idea

Generics expand a "modal horizon" — the set of salient individuals — as a side effect of assertion. When processing a generic Gen[φ][ψ]:

1. Check whether the horizon already contains restrictor-satisfying individuals
2. If not, expand the horizon to include normal restrictor-satisfying ones
3. Evaluate truth: all restrictor-satisfying individuals on the expanded horizon must satisfy the scope

This cumulative expansion explains why generic Sobel sequences ("Ravens are black; but albino ravens aren't") are consistent while their reverses ("#Albino ravens aren't black; but ravens are") are not: the evaluation order determines which individuals are salient.

Static as special case

Discourse-initial evaluation (evalGeneric []) reduces to a static restricted universal (evalGeneric_empty_eq_static). The fromPredicate constructor builds a GenericSentence from the same primitives as the classical traditionalGEN style (binary normalcy predicate).

Formal components

• GenericSentence E: restrictor + scope + normal instances (E → Prop with bundled DecidablePred)
• evalGeneric: single-generic evaluation, returning a Prop truth value
• evalSequence: sequence evaluation
• fromPredicate: construct from binary normalcy
• fromOrder: construct from normality ordering

What's not here

This formalizes the single-world case of Kirkpatrick's theory. The full multi-world version (definition 24, with dispositional orbits DO(w) and per-world modal horizons σ : W → ℘(W × Eⁿ)) quantifies over accessible worlds. The single-world simplification suffices for all the paper's examples about Sobel sequences.

structure Semantics.Genericity.GenericsDynamic.GenericSentence (E : Type) : Type

A generic sentence: restrictor, scope, and normal instances.

The normalInstances field packages the output of applying a normality restriction to the restrictor class. In a full implementation these would be computed from a NormalityOrder via optimal; here they are provided directly to keep the model concrete and the propositional theorems decidable on finite witnesses.

Kirkpatrick's contextual variable C (the set of alternatives to the matrix-clause property) is incorporated into the restrictor: the full restrictor is kind(x) ∧ C(x). Different generics about the same kind can have different C values, yielding different restrictors. This is how mixed generic sequences ("Lions have manes and lions give birth") avoid mutual interference (§5.3).

• restrictor : E → Prop
• scope : E → Prop
• normalInstances : List E
• decRestrictor : DecidablePred self.restrictor
• decScope : DecidablePred self.scope

def Semantics.Genericity.GenericsDynamic.evalGeneric {E : Type} (horizon : List E) (g : GenericSentence E) : List E × Prop

Process a single generic against a horizon.

Expansion rule (definition 24a): if no restrictor-satisfying individual is currently salient, expand the horizon to include the normal restrictor-satisfying individuals.

Truth rule (definition 24b): all restrictor-satisfying individuals on the (possibly expanded) horizon must satisfy the scope.

Equations

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

@[implicit_reducible]

instance Semantics.Genericity.GenericsDynamic.evalGeneric_snd_decidable {E : Type} (horizon : List E) (g : GenericSentence E) : Decidable (evalGeneric horizon g).snd

Equations

• Semantics.Genericity.GenericsDynamic.evalGeneric_snd_decidable horizon g = id inferInstance

def Semantics.Genericity.GenericsDynamic.evalSequenceFrom {E : Type} : List E → List (GenericSentence E) → Prop

Process a sequence of generics left-to-right, threading the horizon. Returns the conjunction of all truth values.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Genericity.GenericsDynamic.evalSequenceFrom x✝ [] = True

@[implicit_reducible]

instance Semantics.Genericity.GenericsDynamic.evalSequenceFrom_decidable {E : Type} (horizon : List E) (gs : List (GenericSentence E)) : Decidable (evalSequenceFrom horizon gs)

Equations

• Semantics.Genericity.GenericsDynamic.evalSequenceFrom_decidable x✝ [] = isTrue trivial
• Semantics.Genericity.GenericsDynamic.evalSequenceFrom_decidable x✝ (g :: gs) = ⋯.mpr inferInstance

def Semantics.Genericity.GenericsDynamic.isConsistent {E : Type} (gs : List (GenericSentence E)) : Prop

A generic sequence is consistent iff every generic evaluates to true.

Equations

• Semantics.Genericity.GenericsDynamic.isConsistent gs = Semantics.Genericity.GenericsDynamic.evalSequenceFrom [] gs

@[implicit_reducible]

instance Semantics.Genericity.GenericsDynamic.isConsistent_decidable {E : Type} (gs : List (GenericSentence E)) : Decidable (isConsistent gs)

Equations

• Semantics.Genericity.GenericsDynamic.isConsistent_decidable gs = id inferInstance

theorem Semantics.Genericity.GenericsDynamic.evalGeneric_horizon_superset {E : Type} (horizon : List E) (g : GenericSentence E) (e : E) (he : e ∈ horizon) : e ∈ (evalGeneric horizon g).fst

Horizon expansion is monotone: every individual on the input horizon remains on the output horizon.

theorem Semantics.Genericity.GenericsDynamic.sobel_pair_consistent {E : Type} (general exception : GenericSentence E) (hgs : ∀ (e : E), e ∈ general.normalInstances → general.scope e) (hdis : ∀ (e : E), e ∈ general.normalInstances → ¬exception.restrictor e) (her : ∀ (e : E), e ∈ exception.normalInstances → exception.restrictor e) (hes : ∀ (e : E), e ∈ exception.normalInstances → exception.scope e) : isConsistent [general, exception]

General Sobel sequence consistency (§5.1).

If two generics form a Sobel pair — the general's normal instances satisfy the general scope, the exception's normal instances satisfy their restrictor and scope, and the general's normal instances are disjoint from the exception's restrictor — then the Sobel sequence [general, exception] is consistent.

theorem Semantics.Genericity.GenericsDynamic.reverse_sobel_pair_inconsistent {E : Type} (general exception : GenericSentence E) (her : ∀ (e : E), e ∈ exception.normalInstances → exception.restrictor e) (hsub : ∀ (e : E), exception.restrictor e → general.restrictor e) (hcounter : ∀ (e : E), e ∈ exception.normalInstances → ¬general.scope e) (hne : exception.normalInstances ≠ []) : ¬isConsistent [exception, general]

General reverse Sobel inconsistency (§5.2).

If exception normal instances satisfy the exception restrictor and scope, the exception restrictor implies the general restrictor (subset), all exception normal instances violate the general scope (genuine counterexamples), and the exception class is nonempty, then the reverse sequence [exception, general] is inconsistent.

This is the paper's key novel prediction: the dynamic theory explains why reverse Sobel sequences are infelicitous, which static theories cannot account for.

theorem Semantics.Genericity.GenericsDynamic.evalGeneric_empty_eq_static {E : Type} (g : GenericSentence E) : (evalGeneric [] g).snd ↔ ∀ (e : E), e ∈ g.normalInstances → g.restrictor e → g.scope e

Discourse-initial evaluation reduces to a restricted universal over normalInstances — the propositional analogue of static traditionalGEN with situations = normalInstances, normal ≡ True.

Structural characterization of horizon evolution

The horizon-step function is the state-transition component of evalGeneric: it describes how the set of salient individuals evolves as generics are processed. The step has exactly two behaviors, controlled by a conditional test:

• Expansion (horizonStep_expand): when no element of the current horizon satisfies the restrictor, the normal instances are appended
• Blocking (horizonStep_blocked): when some element already satisfies the restrictor, the horizon is unchanged

The Sobel asymmetry arises because the subset relation between restrictors (exception ⊆ general) makes this conditional test asymmetric: in the forward direction both expansions fire (general normals don't satisfy the exception restrictor); in the reverse direction the exception's expansion blocks the general's (exception normals DO satisfy the general restrictor).

def Semantics.Genericity.GenericsDynamic.horizonStep {E : Type} (g : GenericSentence E) (horizon : List E) : List E

The horizon-step function: how evalGeneric updates the horizon (ignoring the truth value). This is the state-transition component of the generic CCP.

Equations

• Semantics.Genericity.GenericsDynamic.horizonStep g horizon = (Semantics.Genericity.GenericsDynamic.evalGeneric horizon g).fst

@[simp]

theorem Semantics.Genericity.GenericsDynamic.horizonStep_empty {E : Type} (g : GenericSentence E) : horizonStep g [] = g.normalInstances

Empty horizon always expands: the output is exactly normalInstances.

theorem Semantics.Genericity.GenericsDynamic.horizonStep_expand {E : Type} (g : GenericSentence E) (horizon : List E) (h : ∀ (e : E), e ∈ horizon → ¬g.restrictor e) : horizonStep g horizon = horizon ++ g.normalInstances

Expansion: when no horizon element satisfies the restrictor, the normal instances are appended to the horizon.

theorem Semantics.Genericity.GenericsDynamic.horizonStep_blocked {E : Type} (g : GenericSentence E) (horizon : List E) {e : E} (he : e ∈ horizon) (hr : g.restrictor e) : horizonStep g horizon = horizon

Blocking: when some horizon element satisfies the restrictor, the horizon is unchanged — no expansion occurs.

This is the mechanism that creates the Sobel asymmetry: exception individuals made salient by a prior generic block the expansion of a subsequent general generic, because (by the subset condition) they satisfy the general's restrictor.

Closure operator analysis

horizonStep satisfies two of the three axioms of a closure operator (Mathlib: Order.ClosureOperator):

1. Extensive (horizonStep_subset): horizon ⊆ horizonStep g horizon
2. Idempotent (horizonStep_idempotent): horizonStep g (horizonStep g h) = horizonStep g h (under the natural hypothesis that normal instances satisfy the restrictor)

But it fails the third axiom:

3. NOT monotone (horizonStep_not_monotone): ∃ g h₁ h₂, h₁ ⊆ h₂ but horizonStep g h₁ ⊄ horizonStep g h₂

This is structurally interesting: eliminative updates (assertion, test) ARE monotone (updateFromSat_monotone in Core/CCP.lean), so they form closure operators on the dual lattice. Expansive generic updates fail monotonicity precisely because a LARGER input can BLOCK expansion that a smaller input would trigger — a phenomenon impossible in eliminative semantics.

theorem Semantics.Genericity.GenericsDynamic.horizonStep_subset {E : Type} (g : GenericSentence E) (horizon : List E) : horizon ⊆ horizonStep g horizon

horizonStep is extensive: the input horizon is always a subset of the output. Together with idempotency, this gives two of the three closure operator axioms.

theorem Semantics.Genericity.GenericsDynamic.horizonStep_idempotent {E : Type} (g : GenericSentence E) (hnr : ∀ (e : E), e ∈ g.normalInstances → g.restrictor e) (hne : g.normalInstances ≠ []) (horizon : List E) : horizonStep g (horizonStep g horizon) = horizonStep g horizon

horizonStep is idempotent when normal instances satisfy their own restrictor: applying it twice gives the same result as applying it once.

The hypothesis hnr ensures that after the first application, the horizon contains restrictor-satisfying elements. The second application therefore sees these elements and triggers the blocking branch — no further expansion occurs.

Together with horizonStep_subset, this establishes that horizonStep satisfies 2/3 closure operator axioms.

theorem Semantics.Genericity.GenericsDynamic.horizonStep_not_monotone : ∃ (g : GenericSentence Bool), ∃ (h₁ : List Bool), ∃ (h₂ : List Bool), h₁ ⊆ h₂ ∧ ¬horizonStep g h₁ ⊆ horizonStep g h₂

horizonStep is NOT monotone: there exist g, h₁ ⊆ h₂ such that horizonStep g h₁ ⊄ horizonStep g h₂.

Witness: over Bool, take restrictor = (· = true) (the identity Prop on Bool) and normalInstances = [false]. Then h₁ = [] triggers expansion (producing [false]), but h₂ = [true] triggers blocking (because true satisfies the restrictor). So false ∈ horizonStep g [] but false ∉ horizonStep g [true].

This contrasts with eliminative updates, which ARE monotone (updateFromSat_monotone in Core/CCP.lean): for eliminative semantics, s ⊆ t → u(s) ⊆ u(t). The failure of monotonicity for expansive updates is what prevents horizonStep from being a closure operator (Order.ClosureOperator in Mathlib), despite satisfying extensiveness and idempotency.

theorem Semantics.Genericity.GenericsDynamic.sobel_forward_horizons {E : Type} (general exception : GenericSentence E) (hdis : ∀ (e : E), e ∈ general.normalInstances → ¬exception.restrictor e) : horizonStep exception (horizonStep general []) = general.normalInstances ++ exception.normalInstances

Forward Sobel: both expansions fire.

In the forward sequence [general, exception], the general's normal instances don't satisfy the exception restrictor (disjointness), so the exception's expansion is not blocked. The final horizon contains both sets of normal instances.

theorem Semantics.Genericity.GenericsDynamic.sobel_reverse_horizons {E : Type} (general exception : GenericSentence E) (her : ∀ (e : E), e ∈ exception.normalInstances → exception.restrictor e) (hsub : ∀ (e : E), exception.restrictor e → general.restrictor e) (hne : exception.normalInstances ≠ []) : horizonStep general (horizonStep exception []) = exception.normalInstances

Reverse Sobel: the general's expansion is blocked.

In the reverse sequence [exception, general], the exception's normal instances satisfy the general restrictor (by the subset condition), so the general's conditional expansion test finds restrictor-satisfying individuals already on the horizon. The general does NOT expand — its normal instances never become salient. The final horizon contains only the exception's normal instances.

This is the structural reason for the reverse Sobel's inconsistency: the general is evaluated against a horizon containing only counterexamples (exception normals that violate the general scope).

theorem Semantics.Genericity.GenericsDynamic.sobel_horizon_noncommutative {E : Type} (general exception : GenericSentence E) (hdis : ∀ (e : E), e ∈ general.normalInstances → ¬exception.restrictor e) (her : ∀ (e : E), e ∈ exception.normalInstances → exception.restrictor e) (hsub : ∀ (e : E), exception.restrictor e → general.restrictor e) (hne : exception.normalInstances ≠ []) (hne_gen : general.normalInstances ≠ []) : horizonStep exception (horizonStep general []) ≠ horizonStep general (horizonStep exception [])

Horizon non-commutativity under Sobel conditions.

The forward and reverse horizons are structurally different: the forward horizon is general.normalInstances ++ exception.normalInstances while the reverse is just exception.normalInstances. Since the general has nonempty normal instances, these lists have different lengths.

This is the structural content of the Sobel asymmetry: horizon evolution is non-commutative precisely because the restrictor subset relation is asymmetric — exception normals satisfy the general restrictor but general normals do not satisfy the exception restrictor.

theorem Semantics.Genericity.GenericsDynamic.disjoint_pair_consistent {E : Type} (g₁ g₂ : GenericSentence E) (h₁r : ∀ (e : E), e ∈ g₁.normalInstances → g₁.restrictor e) (h₁s : ∀ (e : E), e ∈ g₁.normalInstances → g₁.scope e) (h₂r : ∀ (e : E), e ∈ g₂.normalInstances → g₂.restrictor e) (h₂s : ∀ (e : E), e ∈ g₂.normalInstances → g₂.scope e) (hdis₁₂ : ∀ (e : E), e ∈ g₁.normalInstances → ¬g₂.restrictor e) (hdis₂₁ : ∀ (e : E), e ∈ g₂.normalInstances → ¬g₁.restrictor e) : isConsistent [g₁, g₂] ∧ isConsistent [g₂, g₁]

Non-interference for disjoint restrictors (§5.3).

When two generics have disjoint restrictors — neither's normal instances satisfy the other's restrictor — both orders are consistent, provided each generic's normal instances satisfy their own restrictor and scope.

This is the structural explanation for why mixed generic sequences like "Lions have manes and lions give birth to live young" are felicitous in both orders: the two generics use different contextual variables C, making their restrictors disjoint.

Note that this follows directly from sobel_pair_consistent applied symmetrically — the disjointness conditions play the same role as the Sobel pair's hdis hypothesis, but in both directions.

Appendix A: Why @cite{veltman-1996} cannot model the asymmetry

@cite{kirkpatrick-2024} Appendix A (pp. 544–548) shows that @cite{veltman-1996}'s update semantics predicts both generic Sobel sequences and their reverses are consistent, because Veltman's normallyUpdate is commutative (normallyUpdate_comm in UpdateSemantics/Default.lean): the final expectation state σ₁ = σ₂ regardless of processing order, since the expectation frame π₁ = π₂.

The theorem commutative_implies_equal_verdicts generalizes this: ANY commutative state-transformer forces any state-dependent predicate to agree on both orders. Combined with sobel_horizon_noncommutative, this establishes that Kirkpatrick's theory escapes the impossibility precisely because horizon evolution is non-commutative.

theorem Semantics.Genericity.GenericsDynamic.commutative_implies_equal_verdicts {G S : Type} (process : G → S → S) (P : S → Prop) (hcomm : ∀ (a b : G) (s : S), process a (process b s) = process b (process a s)) (init : S) (g₁ g₂ : G) : P (process g₂ (process g₁ init)) ↔ P (process g₁ (process g₂ init))

Commutativity forces equal verdicts (Appendix A, abstract form).

If the state-transformation function commutes, then any predicate on the final state gives the same truth value in both orders.

This is the formal content of Kirkpatrick's argument against Veltman: since normallyUpdate commutes, the consistency predicate cannot distinguish σ[φ₁][φ₂] from σ[φ₂][φ₁]. In particular, if a Sobel sequence is consistent under Veltman's semantics, its reverse must be too — contrary to empirical judgment.

The proof is trivial (congruence under commutativity), but the theorem is substantive: it rules out an entire class of theories from modeling order-sensitive phenomena.

theorem Semantics.Genericity.GenericsDynamic.sobel_asymmetry_rules_out_commutativity {G S : Type} (process : G → S → S) (P : S → Prop) (init : S) (g₁ g₂ : G) (hfwd : P (process g₂ (process g₁ init))) (hrev : ¬P (process g₁ (process g₂ init))) : ∃ (a : G), ∃ (b : G), ∃ (s : S), process a (process b s) ≠ process b (process a s)

Contrapositive: if a pair exhibits the Sobel asymmetry for any predicate P, then the processing function is not commutative.

Horizon expansion as presupposition-triggered accommodation

@cite{kirkpatrick-2024} §4.2 (fn. 23) credits @cite{von-fintel-2001} and @cite{gillies-2007}: the expansion mechanism adapts their dynamic semantics for counterfactuals. Both use presupposition failure to trigger context adjustment, but in opposite directions:

• Eliminative accommodation (Presupposition/Accommodation.lean): presupposition failure → shrink context (remove non-presupposition worlds)
• Expansive accommodation (horizon expansion): presupposition failure → grow context (add normal restrictor-satisfying individuals)

Both share the same abstract structure:

1. A presupposition test: does the context already satisfy a condition?
2. On success: no change (the context already works)
3. On failure: adjust the context minimally to satisfy the condition
4. Idempotent: once satisfied, further applications are no-ops

The key divergence: eliminative accommodation is monotone (larger contexts yield larger results); expansive accommodation is NOT (horizonStep_not_monotone), because a larger horizon can BLOCK expansion that a smaller one triggers.

def Semantics.Genericity.GenericsDynamic.horizonPresupposition {E : Type} (restrictor : E → Prop) (horizon : List E) : Prop

The horizon presupposition: restrictor-satisfying individuals are already salient. When this holds, no expansion occurs.

Equations

• Semantics.Genericity.GenericsDynamic.horizonPresupposition restrictor horizon = ∃ (e : E), e ∈ horizon ∧ restrictor e

theorem Semantics.Genericity.GenericsDynamic.presup_success_no_expansion {E : Type} (g : GenericSentence E) (horizon : List E) (h : horizonPresupposition g.restrictor horizon) : horizonStep g horizon = horizon

Presupposition success → no expansion. Delegates to horizonStep_blocked.

theorem Semantics.Genericity.GenericsDynamic.presup_failure_expansion {E : Type} (g : GenericSentence E) (horizon : List E) (h : ¬horizonPresupposition g.restrictor horizon) : horizonStep g horizon = horizon ++ g.normalInstances

Presupposition failure → expansion fires. Delegates to horizonStep_expand.

Constructors for GenericSentence

The normalInstances field of GenericSentence is a stipulation — the constructors below derive it from different theoretical primitives:

• fromPredicate — binary normalcy predicate (classical traditionalGEN style). Normal instances = domain elements satisfying both restrictor and normalcy.

• fromOrder — normality ordering (NormalityOrder style). Normal instances = optimal restrictor-satisfying entities under the ordering. Bridges to @cite{kirkpatrick-2024} Definition 21's N_n functors.

Why no fromThreshold? Threshold semantics (Cohen's prevalence > θ) measures the proportion of restrictor-satisfying cases where scope holds. This is a single Boolean judgment — it doesn't decompose into "select normal instances, then universally quantify." The GenericSentence shape (restrict → select normals → ∀) captures the normality-based family of theories; threshold semantics is a genuinely different algebraic shape. See CovertQuantifier.reduces_to_threshold for the threshold ↔ GEN eliminability result.

def Semantics.Genericity.GenericsDynamic.GenericSentence.fromPredicate {E : Type} (restrictor scope : E → Prop) [DecidablePred restrictor] [DecidablePred scope] (domain : List E) (normal : E → Prop) [DecidablePred normal] : GenericSentence E

Construct a GenericSentence from a binary normalcy predicate.

The normal instances are exactly those domain elements satisfying both restrictor and normalcy. Discourse-initial evaluation reduces to a restricted universal over those elements.

Equations

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

theorem Semantics.Genericity.GenericsDynamic.fromPredicate_static {E : Type} (restrictor scope : E → Prop) [DecidablePred restrictor] [DecidablePred scope] (domain : List E) (normal : E → Prop) [DecidablePred normal] : (evalGeneric [] (GenericSentence.fromPredicate restrictor scope domain normal)).snd ↔ ∀ (e : E), e ∈ domain → restrictor e → normal e → restrictor e → scope e

Discourse-initial evaluation of fromPredicate is a restricted universal over normal restrictor-satisfying elements of the domain.

def Semantics.Genericity.GenericsDynamic.GenericSentence.fromOrder {E : Type} (restrictor scope : E → Prop) [DecidablePred restrictor] [DecidablePred scope] (domain : List E) (le : E → E → Prop) [DecidableRel le] : GenericSentence E

Compute a GenericSentence from a decidable normality ordering.

le e₁ e₂ means e₁ is at least as normal as e₂, matching NormalityOrder.le. The normal instances are the optimal restrictor-satisfying entities: those not strictly dominated by any other restrictor-satisfying entity in the domain.

This is the computable realization of @cite{kirkpatrick-2024} Definition 21's N_n functors: N(P)(w) = { a ∈ P(w) | ∀ b ∈ P(w), b ≤ a → a ≤ b }.

Equations

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