The generic operator

This file defines the generic operator GEN of characterizing sentences as the conditional quantifying over the normal cases of its restrictor. [KPC+95] survey the ways of spelling GEN out. On the prototype analysis a characterizing sentence quantifies universally over the typical instances of its restrictor, (80) and (81); on relevant quantification it quantifies over the restrictor cases that meet a contextual restriction, (78); on the modal analysis it is a conditional evaluated at the most normal worlds of a modal base, (86). Each picks out, for a restrictor, a set of normal cases inside it, and the generic holds when the matrix holds throughout that set. A normality is such a selection (Normality), and GEN is the conditional over its domain (Normality.gen), the domain conditional Conditional.ofDomain of the conditionals file.

Unlike the universal, GEN tolerates exceptions, (74) (Normality.exists_mem_gen_not_subset), though a universal generalization is a generic one (Normality.gen_eq_univ_of_subset), and when every case is normal it is the universal (Normality.mem_gen_top). A normality given by a fixed set of normal cases, as on relevant quantification, makes GEN the strict conditional (Normality.ofAccess, Normality.gen_ofAccess). It overgenerates, since the restriction can be the matrix itself, [KPC+95]'s (79) (Normality.gen_ofAccess_self). A normality given by a preorder on the cases makes GEN the conditional of the best accessible cases (Normality.ofOrdering, Normality.gen_ofOrdering). Whatever the normality, two generics with one restrictor and disjoint matrices leave the restrictor no normal case, and then every generic with that restrictor is true. This is the problem of (82) for the prototype analysis: male ducks have colorful feathers and female ducks lay whitish eggs, so no duck is typical for both, and every sentence a duck Fs comes out true (Normality.normal_eq_empty_of_disjoint, Normality.mem_gen_of_disjoint). Generics with disjoint matrices and different restrictors select disjoint normal cases (Normality.disjoint_normal_of_disjoint).

Main definitions

• Genericity.Normality: a selection of the normal cases of each restrictor.
• Genericity.Normality.gen: GEN, the conditional over the normal cases.
• Genericity.Normality.ofAccess, Genericity.Normality.ofOrdering: normality by a fixed set of normal cases and by a preorder.

Implementation notes

• GEN is evaluated at an index (a world, a world and a time, a context) and quantifies over cases of another type (individuals, events, situations, worlds), so a normality has both as parameters. Restrictors and matrices are sets of cases, as for the conditionals.
• The one law every analysis shares is that the normal cases of a restrictor are among its cases. Normality is not monotone in the restrictor: the normal penguins need not be normal birds.

TODO

• The probabilistic generic of [Coh99] and [TG19], a threshold on the conditional probability of the matrix given the restrictor, on mathlib measures.
• The homogeneity presupposition of GEN of Studies/Magri2009, beside Conditional.homogeneityCounterfactual.

References

• [KPC+95]
• [Coh99]
• [TG19]

structure Genericity.Normality (I : Type u_1) (X : Type u_2) : Type (max u_1 u_2)

A normality on cases X at indices I: for each index and restrictor, the normal cases of the restrictor, which are cases of it.

• normal : I → Set X → Set X

  The normal cases of a restrictor at an index.

• normal_subset (i : I) (R : Set X) : self.normal i R ⊆ R

  The normal cases of a restrictor are cases of it.

def Genericity.Normality.gen {I : Type u_1} {X : Type u_2} (N : Normality I X) (R S : Set X) : Set I

GEN with restrictor R and matrix S, true at the indices where every normal case of R is a case of S.

Equations

• N.gen R S = Conditional.ofDomain N.normal R S

@[simp]

theorem Genericity.Normality.mem_gen {I : Type u_1} {X : Type u_2} (N : Normality I X) {R S : Set X} {i : I} : i ∈ N.gen R S ↔ N.normal i R ⊆ S

theorem Genericity.Normality.gen_eq_univ_of_subset {I : Type u_1} {X : Type u_2} (N : Normality I X) {R S : Set X} (h : R ⊆ S) : N.gen R S = Set.univ

A universal generalization is a generic one.

theorem Genericity.Normality.disjoint_normal_of_disjoint {I : Type u_1} {X : Type u_2} (N : Normality I X) {R S S' : Set X} {i : I} {R' : Set X} (hS : i ∈ N.gen R S) (hS' : i ∈ N.gen R' S') (h : Disjoint S S') : Disjoint (N.normal i R) (N.normal i R')

Two generics with disjoint matrices select disjoint normal cases of their restrictors: if birds fly and penguins don't, no bird is both a normal bird and a normal penguin.

theorem Genericity.Normality.normal_eq_empty_of_disjoint {I : Type u_1} {X : Type u_2} (N : Normality I X) {R S S' : Set X} {i : I} (hS : i ∈ N.gen R S) (hS' : i ∈ N.gen R S') (h : Disjoint S S') : N.normal i R = ∅

(82): two generics with one restrictor and disjoint matrices leave the restrictor no normal case.

theorem Genericity.Normality.mem_gen_of_disjoint {I : Type u_1} {X : Type u_2} (N : Normality I X) {R S S' : Set X} {i : I} (hS : i ∈ N.gen R S) (hS' : i ∈ N.gen R S') (h : Disjoint S S') (T : Set X) : i ∈ N.gen R T

(82): two generics with one restrictor and disjoint matrices make every generic with that restrictor true.

@[instance_reducible]

instance Genericity.Normality.instTop {I : Type u_1} {X : Type u_2} : Top (Normality I X)

The normality on which every case of a restrictor is normal.

Equations

• Genericity.Normality.instTop = { top := { normal := fun (x : I) (R : Set X) => R, normal_subset := ⋯ } }

@[simp]

theorem Genericity.Normality.mem_gen_top {I : Type u_1} {X : Type u_2} {R S : Set X} {i : I} : i ∈ ⊤.gen R S ↔ R ⊆ S

When every case is normal GEN is the universal.

def Genericity.Normality.ofAccess {I : Type u_1} {X : Type u_2} (B : I → Set X) : Normality I X

The normality of relevant quantification, (78): the normal cases of a restrictor at an index are its cases in a fixed set.

Equations

• Genericity.Normality.ofAccess B = { normal := fun (i : I) (R : Set X) => B i ∩ R, normal_subset := ⋯ }

theorem Genericity.Normality.gen_ofAccess {I : Type u_1} {X : Type u_2} (B : I → Set X) : (ofAccess B).gen = Conditional.strictImp B

Under a fixed set of normal cases GEN is the strict conditional.

theorem Genericity.Normality.gen_ofAccess_self {I : Type u_1} {X : Type u_2} {R S : Set X} : (ofAccess fun (x : I) => S).gen R S = Set.univ

(79): restricted to the cases of its own matrix, every generic is true, so relevant quantification needs a theory of the admissible restrictions.

theorem Genericity.Normality.exists_mem_gen_not_subset : ∃ (N : Normality Unit Bool) (R : Set Bool) (S : Set Bool), () ∈ N.gen R S ∧ ¬R ⊆ S

(74): unlike the universal, a generic tolerates exceptions; a cat that lost its tail does not falsify a cat has a tail.

def Genericity.Normality.ofOrdering {I : Type u_1} {X : Type u_2} (access : I → Set X) (ord : I → Preorder X) : Normality I X

The normality of a preorder on the cases: the normal cases of a restrictor at an index are its best accessible cases.

Equations

• Genericity.Normality.ofOrdering access ord = { normal := fun (i : I) (R : Set X) => (ord i).minimals (access i ∩ R), normal_subset := ⋯ }

theorem Genericity.Normality.gen_ofOrdering {I : Type u_1} {X : Type u_2} (access : I → Set X) (ord : I → Preorder X) : (ofOrdering access ord).gen = Conditional.orderingImp access ord

Under a preorder GEN is the conditional of the best accessible cases.