structure Phenomena.Generics.PrevalenceAsymmetry : Type

Same prevalence, different truth judgments.

• sentence1 : String
• sentence2 : String
• prevalence : ℚ
• judgment1 : ℚ
• judgment2 : ℚ
• source : String

def Phenomena.Generics.laysEggsVsIsFemale : PrevalenceAsymmetry

Classic asymmetry: "lays eggs" vs "is female"

Equations

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

def Phenomena.Generics.hasLiverVsHasBrownEyes : PrevalenceAsymmetry

"Has a liver" vs "has brown eyes"

Equations

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

structure Phenomena.Generics.RarePropertyGeneric : Type

True generic despite very low prevalence.

• sentence : String
• prevalence : ℚ
• judgment : ℚ
• explanation : String
• source : String

def Phenomena.Generics.mosquitosMalaria : RarePropertyGeneric

"Mosquitos carry malaria" - classic rare property generic

Equations

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

def Phenomena.Generics.sharksAttack : RarePropertyGeneric

"Sharks attack swimmers"

Equations

• Phenomena.Generics.sharksAttack = { sentence := "Sharks attack swimmers", prevalence := 1 / 1000, judgment := 8 / 10, explanation := "Dangerous property", source := "Leslie 2008" }

def Phenomena.Generics.ticksLyme : RarePropertyGeneric

"Ticks carry Lyme disease"

Equations

• Phenomena.Generics.ticksLyme = { sentence := "Ticks carry Lyme disease", prevalence := 1 / 50, judgment := 85 / 100, explanation := "Dangerous property", source := "Tessler & Goodman 2019" }

def Phenomena.Generics.peacocksTails : RarePropertyGeneric

"Peacocks have colorful tails" - only males

Equations

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

structure Phenomena.Generics.StrikingPropertyEffect : Type

Dangerous/distinctive properties require less prevalence for generic acceptance.

• neutralSentence : String
• neutralPrevalenceNeeded : ℚ
• strikingSentence : String
• strikingPrevalenceNeeded : ℚ
• source : String

def Phenomena.Generics.malariaVsWings : StrikingPropertyEffect

Comparison: "carry malaria" needs less prevalence than "have wings"

Equations

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

inductive Phenomena.Generics.PrincipledSubtype : Type

Subtypes of principled connections (@cite{prasada-dillingham-2006}).

Principled connections link a kind to a property via an explanatory relation — one can say why members have the property. The three subtypes differ in their tolerance for exceptions:

• formal: definitional/analytic ("Triangles have three sides"). Zero exceptions tolerated.
• constitutive: proper physical makeup ("Dogs have four legs"). Few exceptions tolerated (birth defects, injury).
• causal: causal mechanism ("Mosquitos carry malaria"). Many exceptions tolerated — the mechanism exists even if rarely manifested.

• formal : PrincipledSubtype
• constitutive : PrincipledSubtype
• causal : PrincipledSubtype

def Phenomena.Generics.instReprPrincipledSubtype.repr : PrincipledSubtype → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.instReprPrincipledSubtype : Repr PrincipledSubtype

Equations

• Phenomena.Generics.instReprPrincipledSubtype = { reprPrec := Phenomena.Generics.instReprPrincipledSubtype.repr }

instance Phenomena.Generics.instDecidableEqPrincipledSubtype : DecidableEq PrincipledSubtype

Equations

• Phenomena.Generics.instDecidableEqPrincipledSubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.instBEqPrincipledSubtype : BEq PrincipledSubtype

Equations

• Phenomena.Generics.instBEqPrincipledSubtype = { beq := Phenomena.Generics.instBEqPrincipledSubtype.beq }

def Phenomena.Generics.instBEqPrincipledSubtype.beq : PrincipledSubtype → PrincipledSubtype → Bool

Equations

• Phenomena.Generics.instBEqPrincipledSubtype.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Generics.ConnectionType : Type

Kind–property connection type (@cite{prasada-dillingham-2006}).

Principled connections support "bare" generics at any prevalence because the explanatory relation licenses the generalization. Statistical connections require high prevalence — there is no explanatory "why", just observed frequency.

• principled (sub : PrincipledSubtype) : ConnectionType
• statistical : ConnectionType

def Phenomena.Generics.instReprConnectionType.repr : ConnectionType → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.instReprConnectionType : Repr ConnectionType

Equations

• Phenomena.Generics.instReprConnectionType = { reprPrec := Phenomena.Generics.instReprConnectionType.repr }

instance Phenomena.Generics.instDecidableEqConnectionType : DecidableEq ConnectionType

Equations

• Phenomena.Generics.instDecidableEqConnectionType = Phenomena.Generics.instDecidableEqConnectionType.decEq

def Phenomena.Generics.instDecidableEqConnectionType.decEq (x✝ x✝¹ : ConnectionType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Generics.instDecidableEqConnectionType.decEq (Phenomena.Generics.ConnectionType.principled sub) Phenomena.Generics.ConnectionType.statistical = isFalse ⋯
• Phenomena.Generics.instDecidableEqConnectionType.decEq Phenomena.Generics.ConnectionType.statistical (Phenomena.Generics.ConnectionType.principled sub) = isFalse ⋯
• Phenomena.Generics.instDecidableEqConnectionType.decEq Phenomena.Generics.ConnectionType.statistical Phenomena.Generics.ConnectionType.statistical = isTrue ⋯

instance Phenomena.Generics.instBEqConnectionType : BEq ConnectionType

Equations

• Phenomena.Generics.instBEqConnectionType = { beq := Phenomena.Generics.instBEqConnectionType.beq }

def Phenomena.Generics.instBEqConnectionType.beq : ConnectionType → ConnectionType → Bool

Equations

• Phenomena.Generics.instBEqConnectionType.beq (Phenomena.Generics.ConnectionType.principled a) (Phenomena.Generics.ConnectionType.principled b) = (a == b)
• Phenomena.Generics.instBEqConnectionType.beq Phenomena.Generics.ConnectionType.statistical Phenomena.Generics.ConnectionType.statistical = true
• Phenomena.Generics.instBEqConnectionType.beq x✝¹ x✝ = false

structure Phenomena.Generics.ConnectionDatum : Type

Connection type datum.

• sentence : String
• connectionType : ConnectionType
• toleratesExceptions : Bool
• acceptanceThreshold : ℚ
• source : String

def Phenomena.Generics.trianglesSides : ConnectionDatum

"Triangles have three sides" — formal/definitional connection.

Equations

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

def Phenomena.Generics.hasHeart : ConnectionDatum

"Dogs have a heart" — constitutive connection.

Equations

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

def Phenomena.Generics.mosquitosMalariaCxn : ConnectionDatum

"Mosquitos carry malaria" — causal connection.

Equations

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

def Phenomena.Generics.hasBrownFur : ConnectionDatum

"Dogs have brown fur" — statistical connection.

Equations

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

theorem Phenomena.Generics.principled_lower_threshold : hasHeart.acceptanceThreshold < hasBrownFur.acceptanceThreshold ∧ mosquitosMalariaCxn.acceptanceThreshold < hasBrownFur.acceptanceThreshold ∧ trianglesSides.acceptanceThreshold < hasHeart.acceptanceThreshold

Principled connections have lower acceptance thresholds than statistical.

theorem Phenomena.Generics.formal_no_exceptions : trianglesSides.toleratesExceptions = false ∧ hasHeart.toleratesExceptions = true ∧ mosquitosMalariaCxn.toleratesExceptions = true ∧ hasBrownFur.toleratesExceptions = true

Formal connections tolerate no exceptions; others do.

def Phenomena.Generics.connectionData : List ConnectionDatum

All connection data entries.

Equations

• Phenomena.Generics.connectionData = [Phenomena.Generics.trianglesSides, Phenomena.Generics.hasHeart, Phenomena.Generics.mosquitosMalariaCxn, Phenomena.Generics.hasBrownFur]

theorem Phenomena.Generics.threshold_ordering : trianglesSides.acceptanceThreshold < hasHeart.acceptanceThreshold ∧ hasHeart.acceptanceThreshold > mosquitosMalariaCxn.acceptanceThreshold ∧ mosquitosMalariaCxn.acceptanceThreshold < hasBrownFur.acceptanceThreshold

Acceptance thresholds decrease as connection strength increases: formal < constitutive < causal < statistical.

structure Phenomena.Generics.HabitualDatum : Type

Habitual sentence datum.

• sentence : String
• frequency : String
• judgment : ℚ
• source : String

def Phenomena.Generics.johnSmokes : HabitualDatum

"John smokes" requires regular behavior

Equations

• Phenomena.Generics.johnSmokes = { sentence := "John smokes", frequency := "regularly (e.g., daily)", judgment := 9 / 10, source := "Carlson 1977" }

def Phenomena.Generics.johnSmokedOnce : HabitualDatum

"John smokes" false for one-time event

Equations

• Phenomena.Generics.johnSmokedOnce = { sentence := "John smokes", frequency := "once at a party", judgment := 1 / 10, source := "Carlson 1977" }

def Phenomena.Generics.johnDrinksAmbiguity : HabitualDatum

"John drinks" (alcohol) vs "John drinks" (any liquid)

Equations

• Phenomena.Generics.johnDrinksAmbiguity = { sentence := "John drinks", frequency := "habitual alcohol consumption", judgment := 85 / 100, source := "Carlson 1977" }

structure Phenomena.Generics.CausalGenericDatum : Type

Causal generic datum.

• sentence : String
• causalPower : ℚ
• judgment : ℚ
• source : String

def Phenomena.Generics.smokingCancer : CausalGenericDatum

"Smoking causes cancer"

Equations

• Phenomena.Generics.smokingCancer = { sentence := "Smoking causes cancer", causalPower := 15 / 100, judgment := 9 / 10, source := "Tessler & Goodman 2019" }

def Phenomena.Generics.pillsClots : CausalGenericDatum

"Birth control pills cause blood clots"

Equations

• Phenomena.Generics.pillsClots = { sentence := "Birth control pills cause blood clots", causalPower := 1 / 1000, judgment := 6 / 10, source := "Tessler & Goodman 2019" }

structure Phenomena.Generics.QuantifierContrast : Type

Generics vs explicit quantifiers.

• generic : String
• quantified : String
• genericJudgment : ℚ
• quantifiedJudgment : ℚ
• source : String

def Phenomena.Generics.tigersStriped : QuantifierContrast

"Tigers are striped" vs "All tigers are striped"

Equations

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

def Phenomena.Generics.ducksLay : QuantifierContrast

"Ducks lay eggs" vs "All ducks lay eggs"

Equations

• Phenomena.Generics.ducksLay = { generic := "Ducks lay eggs", quantified := "All ducks lay eggs", genericJudgment := 9 / 10, quantifiedJudgment := 3 / 10, source := "Leslie 2008" }

structure Phenomena.Generics.AcquisitionDatum : Type

Child generic acceptance with minimal evidence.

• sentence : String
• evidence : String
• childAcceptance : ℚ
• adultAcceptance : ℚ
• source : String

def Phenomena.Generics.lorpsPurple : AcquisitionDatum

Equations

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