Kirkpatrick (2023): The Dynamics of Generics

This file formalizes [Kir23]'s dynamic semantics for generics and its account of generic Sobel sequences: a generic followed by a statement of its exceptions, (1), is felicitous and judged true, while the reverse order, (2), is infelicitous and sounds contradictory. Static theories assign each generic a truth value on its own, so the truth of a sequence is a conjunction invariant under reordering and the contrast is invisible to them, §3 (static_perm). The theory builds on the normality-based semantics (22), on which a generic is true when every normal instance of its restrictor satisfies its matrix: the normality functor of (21) is a Genericity.Normality and (22) is its generic. The dynamic theory of (24) evaluates a generic against a modal horizon, the set of salient individuals, which the generic first expands with the normal instances of its restrictor when none is yet salient (update), and the generic is true when every salient instance of its restrictor satisfies its matrix (holds). This is again a generic, under the normality whose normal instances of a restrictor are those on the updated horizon (horizon), and discourse-initially it is the static generic (22) (holds_empty). In a Sobel sequence the exceptions are abnormal for the general and so absent from its horizon, while the reverse order puts them on the horizon first, where the general finds them and no longer expands: the two orders come apart exactly as the paper predicts (SobelPair.order_sensitive). The ravens of (25) and (28) are ranked by how they are coloured, the albino abnormal (ravenNormality), and a mixed sequence like (29) survives because each generic's restrictor excludes the individuals the other made salient (lions_both_orders). Appendix A's comparison with [Vel96] is checked on his eight worlds: the frame presented by accepted rules is insensitive to their order, so his theory predicts the reverse sequence consistent (veltman_reverse_consistent).

Implementation notes

• (24) is taken at a single world: the dispositional orbit is a point, so the normality functor of (21) is a normality at a single index and the modal horizon a set of individuals. The arguments of §5 are pointwise in the accessible world and survive the restriction.
• The contextual variable C of (20) is folded into the restrictor, as (26) and (31) do.

References

• [Kir23]
• [Vel96]
• [Coh99]

structure Kirkpatrick2023.GenericSentence (E : Type u_2) : Type u_2

A generic Gen[φ][ψ], (20): its restrictor, with the contextual variable folded in, and its matrix.

• restrictor : Set E

  The restrictor.

• scope : Set E

  The matrix.

def Kirkpatrick2023.update {E : Type u_1} (N : Genericity.Normality Unit E) (R σ : Set E) : Set E

The context change potential (24a): a generic presupposes a salient instance of its restrictor and, failing that, expands the horizon by the normal instances (21).

Equations

• Kirkpatrick2023.update N R σ = σ ∪ {x : E | x ∈ N.normal () R ∧ ∀ y ∈ σ, y ∉ R}

def Kirkpatrick2023.horizon {E : Type u_1} (N : Genericity.Normality Unit E) : Genericity.Normality (Set E) E

The normality of the dynamic generic: at a horizon, the normal instances of a restrictor are its instances on the horizon the generic updates.

Equations

• Kirkpatrick2023.horizon N = { normal := fun (σ R : Set E) => Kirkpatrick2023.update N R σ ∩ R, normal_subset := ⋯ }

def Kirkpatrick2023.holds {E : Type u_1} (N : Genericity.Normality Unit E) (g : GenericSentence E) (σ : Set E) : Prop

The truth conditions (24b): every salient instance of the restrictor on the updated horizon satisfies the matrix.

Equations

• Kirkpatrick2023.holds N g σ = (σ ∈ (Kirkpatrick2023.horizon N).gen g.restrictor g.scope)

theorem Kirkpatrick2023.update_of_exists {E : Type u_1} {N : Genericity.Normality Unit E} {R σ : Set E} (h : ∃ y ∈ σ, y ∈ R) : update N R σ = σ

theorem Kirkpatrick2023.update_of_forall {E : Type u_1} {N : Genericity.Normality Unit E} {R σ : Set E} (h : ∀ y ∈ σ, y ∉ R) : update N R σ = σ ∪ N.normal () R

theorem Kirkpatrick2023.update_empty {E : Type u_1} {N : Genericity.Normality Unit E} {R : Set E} : update N R ∅ = N.normal () R

theorem Kirkpatrick2023.subset_update {E : Type u_1} {N : Genericity.Normality Unit E} {R σ : Set E} : σ ⊆ update N R σ

Expansion is one-way, fn. 24: the horizon never shrinks.

theorem Kirkpatrick2023.update_update {E : Type u_1} {N : Genericity.Normality Unit E} {R σ : Set E} : update N R (update N R σ) = update N R σ

A second assertion of the same generic expands nothing.

theorem Kirkpatrick2023.holds_empty {E : Type u_1} (N : Genericity.Normality Unit E) (g : GenericSentence E) : holds N g ∅ ↔ () ∈ N.gen g.restrictor g.scope

Discourse-initial truth, (23) and (26): against an empty horizon the dynamic generic is the static generic (22) of the normality functor.

def Kirkpatrick2023.ConsistentFrom {E : Type u_1} (N : Genericity.Normality Unit E) : Set E → List (GenericSentence E) → Prop

A sequence of generics is consistent from a horizon when each is true against the horizon its predecessors have expanded, §5.

Equations

• Kirkpatrick2023.ConsistentFrom N x✝ [] = True
• Kirkpatrick2023.ConsistentFrom N x✝ (g :: gs) = (Kirkpatrick2023.holds N g x✝ ∧ Kirkpatrick2023.ConsistentFrom N (Kirkpatrick2023.update N g.restrictor x✝) gs)

@[reducible, inline]

abbrev Kirkpatrick2023.Consistent {E : Type u_1} (N : Genericity.Normality Unit E) (gs : List (GenericSentence E)) : Prop

Consistency from the empty discourse-initial horizon, §5.1.

Equations

• Kirkpatrick2023.Consistent N gs = Kirkpatrick2023.ConsistentFrom N ∅ gs

Static theories, §3

@[reducible, inline]

abbrev Kirkpatrick2023.Static {E : Type u_1} (truth : GenericSentence E → Prop) (gs : List (GenericSentence E)) : Prop

A static semantics assigns each generic a truth value on its own, so a sequence is true when each member is, whatever the order: the probabilistic truth conditions (18) of [Coh99], the normality-based ones of (19) and the indexical approach of §3.3 all take this form.

Equations

• Kirkpatrick2023.Static truth gs = ∀ g ∈ gs, truth g

theorem Kirkpatrick2023.static_perm {E : Type u_1} (truth : GenericSentence E → Prop) {gs gs' : List (GenericSentence E)} (h : gs.Perm gs') : Static truth gs ↔ Static truth gs'

§3.4: no static semantics is sensitive to the order of a sequence.

Generic Sobel sequences, §5

theorem Kirkpatrick2023.consistent_pair {E : Type u_1} {N : Genericity.Normality Unit E} {g₁ g₂ : GenericSentence E} (h₁ : holds N g₁ ∅) (h₂ : holds N g₂ ∅) (hdis : ∀ e ∈ N.normal () g₁.restrictor, e ∉ g₂.restrictor) : Consistent N [g₁, g₂]

Two generics true on their own, the second of which finds no instance of its restrictor among the first's normal instances, are consistent in that order: the second expands the horizon and is evaluated on its own normal instances.

theorem Kirkpatrick2023.consistent_both_orders {E : Type u_1} {N : Genericity.Normality Unit E} {g₁ g₂ : GenericSentence E} (h₁ : holds N g₁ ∅) (h₂ : holds N g₂ ∅) (h₁₂ : ∀ e ∈ N.normal () g₁.restrictor, e ∉ g₂.restrictor) (h₂₁ : ∀ e ∈ N.normal () g₂.restrictor, e ∉ g₁.restrictor) : Consistent N [g₁, g₂] ∧ Consistent N [g₂, g₁]

§5.3: two generics true on their own whose restrictors exclude each other's normal instances are consistent in both orders, each expanding the horizon in turn.

structure Kirkpatrick2023.SobelPair {E : Type u_1} (N : Genericity.Normality Unit E) : Type u_1

A pair of generics forming a Sobel sequence in the order general, exception, (1): the exception's restrictor picks out a subkind of the general's, §5.2, its matrix contradicts the general's, and the general's normal instances are not exceptions.

• general : GenericSentence E

  The general.

• exception : GenericSentence E

  The exception.

• sub : self.exception.restrictor ⊆ self.general.restrictor
• contra : Disjoint self.exception.scope self.general.scope
• abnormal (e : E) : e ∈ N.normal () self.general.restrictor → e ∉ self.exception.restrictor

theorem Kirkpatrick2023.SobelPair.consistent {E : Type u_1} {N : Genericity.Normality Unit E} (p : SobelPair N) (hg : holds N p.general ∅) (he : holds N p.exception ∅) : Consistent N [p.general, p.exception]

§5.1: a Sobel sequence whose generics are each true on their own is consistent, the exceptions being absent from the general's horizon.

theorem Kirkpatrick2023.SobelPair.reverse_inconsistent {E : Type u_1} {N : Genericity.Normality Unit E} (p : SobelPair N) (he : holds N p.exception ∅) (hne : (N.normal () p.exception.restrictor).Nonempty) : ¬Consistent N [p.exception, p.general]

§5.2: the reverse order is inconsistent once there is an exception: it is salient when the general is evaluated, satisfies the general's restrictor, and contradicts its matrix.

theorem Kirkpatrick2023.SobelPair.order_sensitive {E : Type u_1} {N : Genericity.Normality Unit E} (p : SobelPair N) (hg : holds N p.general ∅) (he : holds N p.exception ∅) (hne : (N.normal () p.exception.restrictor).Nonempty) : Consistent N [p.general, p.exception] ∧ ¬Consistent N [p.exception, p.general]

The order sensitivity of §5: the same two generics, each true on its own, are consistent in the Sobel order and inconsistent in the reverse.

Ravens, (1a) and (2a)

inductive Kirkpatrick2023.Raven : Type

Two normally coloured ravens and an albino one.

• normal₁ : Raven
• normal₂ : Raven
• albino : Raven

@[instance_reducible]

instance Kirkpatrick2023.instDecidableEqRaven : DecidableEq Raven

Equations

• Kirkpatrick2023.instDecidableEqRaven x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kirkpatrick2023.Raven.rank : Raven → ℕ

How abnormally a raven is coloured: the albino is, the others are not.

Equations

• Kirkpatrick2023.Raven.albino.rank = 1
• x✝.rank = 0

def Kirkpatrick2023.ravenNormality : Genericity.Normality Unit Raven

The normality functor (21) on ravens: the normal instances of a property are its best-coloured instances.

Equations

• Kirkpatrick2023.ravenNormality = Genericity.Normality.ofOrdering (fun (x : Unit) => Set.univ) fun (x : Unit) => Preorder.lift Kirkpatrick2023.Raven.rank

def Kirkpatrick2023.Raven.black : Set Raven

Black ravens: all but the albino.

Equations

• Kirkpatrick2023.Raven.black = {x : Kirkpatrick2023.Raven | x ≠ Kirkpatrick2023.Raven.albino}

def Kirkpatrick2023.ravensAreBlack : GenericSentence Raven

Ravens are black, (20a): every raven is coloured in some way.

Equations

• Kirkpatrick2023.ravensAreBlack = { restrictor := Set.univ, scope := Kirkpatrick2023.Raven.black }

def Kirkpatrick2023.albinoRavensArentBlack : GenericSentence Raven

Albino ravens aren't black.

Equations

• Kirkpatrick2023.albinoRavensArentBlack = { restrictor := {Kirkpatrick2023.Raven.albino}, scope := Kirkpatrick2023.Raven.blackᶜ }

theorem Kirkpatrick2023.ne_albino_of_mem_normal {x : Raven} (hx : x ∈ ravenNormality.normal () Set.univ) : x ≠ Raven.albino

The normal ravens are not albino.

theorem Kirkpatrick2023.mem_normal_albino {x : Raven} : x ∈ ravenNormality.normal () {Raven.albino} ↔ x = Raven.albino

The normal albino ravens are the albino.

def Kirkpatrick2023.ravenPair : SobelPair ravenNormality

Albino ravens are ravens, are not black, and are abnormal as ravens.

Equations

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

theorem Kirkpatrick2023.holds_ravensAreBlack : holds ravenNormality ravensAreBlack ∅

theorem Kirkpatrick2023.holds_albinoRavensArentBlack : holds ravenNormality albinoRavensArentBlack ∅

theorem Kirkpatrick2023.ravens_order_sensitive : Consistent ravenNormality [ravensAreBlack, albinoRavensArentBlack] ∧ ¬Consistent ravenNormality [albinoRavensArentBlack, ravensAreBlack]

(25) and (28): Ravens are black; but albino ravens aren't is consistent and its reverse is not, though each generic is true on its own.

theorem Kirkpatrick2023.ravens_static : Static (fun (x : GenericSentence Raven) => holds ravenNormality x ∅) [albinoRavensArentBlack, ravensAreBlack]

A static semantics accepts the reverse order, §3.1.

Mixed generics, (12)

inductive Kirkpatrick2023.Lion : Type

A male and a female lion.

• male : Lion
• female : Lion

@[instance_reducible]

instance Kirkpatrick2023.instDecidableEqLion : DecidableEq Lion

Equations

• Kirkpatrick2023.instDecidableEqLion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kirkpatrick2023.lionsHaveManes : GenericSentence Lion

Lions have manes, (31): the restrictor is lions with some male sexually selected trait.

Equations

• Kirkpatrick2023.lionsHaveManes = { restrictor := {Kirkpatrick2023.Lion.male}, scope := {Kirkpatrick2023.Lion.male} }

def Kirkpatrick2023.lionsGiveBirth : GenericSentence Lion

Lions give birth to live young, (32): the restrictor is lions that produce offspring in some way.

Equations

• Kirkpatrick2023.lionsGiveBirth = { restrictor := {Kirkpatrick2023.Lion.female}, scope := {Kirkpatrick2023.Lion.female} }

theorem Kirkpatrick2023.lions_both_orders : Consistent ⊤ [lionsHaveManes, lionsGiveBirth] ∧ Consistent ⊤ [lionsGiveBirth, lionsHaveManes]

(29): the mixed sequence is consistent in both orders, every instance of each restrictor being normal, since each generic's restrictor excludes the lions the other makes salient.

Appendix A: Veltman (1996)

def Kirkpatrick2023.sobelState : Veltman1996.State Veltman1996.World

σ₁ of Appendix A: the minimal state after p ⇝ r then (p ∧ q) ⇝ ¬r, with p raven, q albino and r black on the eight worlds of Table 1.

Equations

• Kirkpatrick2023.sobelState = Veltman1996.rule (Veltman1996.p ∩ Veltman1996.q) Veltman1996.rᶜ (Veltman1996.rule Veltman1996.p Veltman1996.r Veltman1996.State.init)

def Kirkpatrick2023.reverseState : Veltman1996.State Veltman1996.World

σ₂ of Appendix A: the rules accepted in the reverse order.

Equations

• Kirkpatrick2023.reverseState = Veltman1996.rule Veltman1996.p Veltman1996.r (Veltman1996.rule (Veltman1996.p ∩ Veltman1996.q) Veltman1996.rᶜ Veltman1996.State.init)

theorem Kirkpatrick2023.sobelState_eq : sobelState = { rules := [{ domain := Veltman1996.p ∩ Veltman1996.q, default := Veltman1996.rᶜ }, { domain := Veltman1996.p, default := Veltman1996.r }], info := Finset.univ }

theorem Kirkpatrick2023.reverseState_eq : reverseState = { rules := [{ domain := Veltman1996.p, default := Veltman1996.r }, { domain := Veltman1996.p ∩ Veltman1996.q, default := Veltman1996.rᶜ }], info := Finset.univ }

theorem Kirkpatrick2023.veltman_reverse_consistent : sobelState ≠ Veltman1996.State.absurd ∧ reverseState ≠ Veltman1996.State.absurd ∧ sobelState.frame = reverseState.frame

Appendix A: neither order crashes and both reach the same frame, since a presented frame does not depend on the order of its rules, so Veltman's theory predicts the reverse Sobel sequence consistent.