Sentence Polarity Asymmetries

@cite{he-kaiser-iskarous-2025}

Empirical data and domain types for modeling sentence polarity asymmetries with fuzzy interpretations in a possibly wonky world.

Key Phenomena

Two asymmetries between positive and negative polarity:

1. Cost asymmetry: Negation elicits higher production cost than positive polarity
2. Presupposition asymmetry: Negation presupposes prominence of its positive counterpart in common ground, but not vice versa

Domain

Part-whole relations (e.g., house-bathroom, classroom-stove):

• States: s_pos (A has B), s_neg (A doesn't have B)
• Utterances: u_pos, u_neg, u_null
• Costs: Cost(u_null)=0, Cost(u_pos)=1, Cost(u_neg)=2

Models

Model	Description
Standard RSA	Baseline with Boolean semantics
fuzzyRSA	Soft semantics with polarity-specific interpretation
wonkyRSA	Complex prior for common ground update
funkyRSA	Combination of fuzzy + wonky

inductive Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState : Type

Two states for part-whole relations.

• pos: The positive state (A has B)
• neg: The negative state (A doesn't have B)

• pos : HKIState
• neg : HKIState

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqHKIState : DecidableEq HKIState

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqHKIState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIState.beq : HKIState → HKIState → Bool

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIState : BEq HKIState

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIState = { beq := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIState.beq }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIState.repr : HKIState → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIState : Repr HKIState

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIState = { reprPrec := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIState.repr }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIState.default : HKIState

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIState.default = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState.pos

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIState : Inhabited HKIState

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIState = { default := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIState.default }

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instFintypeHKIState : Fintype HKIState

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instFinEnumHKIState : FinEnum HKIState

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allStates : List HKIState

All states

Equations

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

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allStates_length : allStates.length = 2

inductive Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance : Type

Three utterances for part-whole communication.

• uPos: "A has B" (positive polarity, cost 1)
• uNeg: "A doesn't have B" (negative polarity, cost 2)
• uNull: Say nothing (cost 0)

• uPos : HKIUtterance
• uNeg : HKIUtterance
• uNull : HKIUtterance

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqHKIUtterance : DecidableEq HKIUtterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqHKIUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIUtterance.beq : HKIUtterance → HKIUtterance → Bool

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIUtterance : BEq HKIUtterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIUtterance = { beq := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqHKIUtterance.beq }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIUtterance.repr : HKIUtterance → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIUtterance : Repr HKIUtterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIUtterance = { reprPrec := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprHKIUtterance.repr }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIUtterance.default : HKIUtterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIUtterance.default = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uPos

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIUtterance : Inhabited HKIUtterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIUtterance = { default := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedHKIUtterance.default }

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instFintypeHKIUtterance : Fintype HKIUtterance

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instFinEnumHKIUtterance : FinEnum HKIUtterance

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allUtterances : List HKIUtterance

All utterances

Equations

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

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allUtterances_length : allUtterances.length = 3

inductive Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity : Type

Sentence polarity

• positive : Polarity
• negative : Polarity
• null : Polarity

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPolarity.beq : Polarity → Polarity → Bool

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPolarity : BEq Polarity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPolarity = { beq := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPolarity.beq }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPolarity : Repr Polarity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPolarity = { reprPrec := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPolarity.repr }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.polarity : HKIUtterance → Polarity

Get polarity of an utterance

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uPos.polarity = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.positive
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNeg.polarity = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.negative
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNull.polarity = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.null

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.utteranceCost : HKIUtterance → ℚ

Utterance costs from the paper.

Cost(u_null) = 0 Cost(u_pos) = 1 Cost(u_neg) = 2

Negation has higher cost due to marked form / longer linguistic realization.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.utteranceCost Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNull = 0
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.utteranceCost Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uPos = 1
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.utteranceCost Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNeg = 2

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.neg_costs_more : utteranceCost HKIUtterance.uNeg > utteranceCost HKIUtterance.uPos

Negative utterances cost more than positive (Asymmetry Hypothesis 1)

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.literalTruth : HKIState → HKIUtterance → Bool

Boolean literal semantics: which utterance is true in which state.

• u_pos is true only in s_pos
• u_neg is true only in s_neg
• u_null is true in both (vacuously)

Equations

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

inductive Phenomena.Presupposition.Studies.HeKaiserIskarous2025.WorldType : Type

World types for wonkyRSA.

• normal: Prior reflects actual world knowledge
• wonky: Uniform prior (speaker's utterance choice is "odd")

• normal : WorldType
• wonky : WorldType

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqWorldType : DecidableEq WorldType

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqWorldType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqWorldType.beq : WorldType → WorldType → Bool

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqWorldType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqWorldType : BEq WorldType

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqWorldType = { beq := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqWorldType.beq }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprWorldType.repr : WorldType → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprWorldType : Repr WorldType

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprWorldType = { reprPrec := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprWorldType.repr }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedWorldType.default : WorldType

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedWorldType.default = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.WorldType.normal

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedWorldType : Inhabited WorldType

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedWorldType = { default := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instInhabitedWorldType.default }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allWorldTypes : List WorldType

All world types

Equations

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

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.allWorldTypes_length : allWorldTypes.length = 2

structure Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIPrior : Type

Prior probability over states.

In the He et al. study, priors were normed empirically for 81 part-whole pairs (e.g., house-bathroom has high prior, classroom-stove has low prior).

• p_pos : ℚ

  P(s_pos) - probability of positive state

• h_pos_nonneg : 0 ≤ self.p_pos

  Non-negative

• h_pos_le_one : self.p_pos ≤ 1

  At most 1

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIPrior.p_neg (prior : HKIPrior) : ℚ

P(s_neg) = 1 - P(s_pos)

Equations

• prior.p_neg = 1 - prior.p_pos

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIPrior.prob (prior : HKIPrior) : HKIState → ℚ

Get prior probability of a state

Equations

• prior.prob Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState.pos = prior.p_pos
• prior.prob Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState.neg = prior.p_neg

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.uniformPrior : HKIPrior

Uniform prior: P(s_pos) = P(s_neg) = 0.5

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.highPrior : HKIPrior

High prior: P(s_pos) = 0.9 (typical part, e.g., house-bathroom)

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.lowPrior : HKIPrior

Low prior: P(s_pos) = 0.1 (atypical part, e.g., classroom-stove)

Equations

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

structure Phenomena.Presupposition.Studies.HeKaiserIskarous2025.FuzzyParams : Type

Parameters for fuzzy interpretation functions.

For negative utterances: constant probability n For positive utterances: sigmoid function with parameters (L, k, x0, c)

• n : ℚ

  Negative interpretation: [u_neg] = n

• L : ℚ

  Sigmoid maximum value

• k : ℚ

  Sigmoid steepness

• x0 : ℚ

  Sigmoid midpoint

• c : ℚ

  Sigmoid vertical shift

• h_n_valid : 0 ≤ self.n ∧ self.n ≤ 1

  n in [0,1]

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.bestFitFuzzyParams : FuzzyParams

Best-fit parameters from the paper (Section 4.2).

n = 0.8, α = 1, θ = {L=0.7, k=6, x0=0.35, c=0.3}

Equations

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

structure Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIConfig : Type

Configuration for RSA model instances

• prior : HKIPrior

  Prior over states

• alpha : ℕ

  Rationality parameter

• p_wonky : ℚ

  Wonkiness prior P(wonky) for wonkyRSA

• fuzzyParams : FuzzyParams

  Fuzzy parameters for fuzzyRSA

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.defaultConfig : HKIConfig

Default configuration with uniform prior

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.defaultConfig = { prior := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.uniformPrior }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.highPriorConfig : HKIConfig

High-prior configuration (typical parts like house-bathroom)

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.highPriorConfig = { prior := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.highPrior }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.lowPriorConfig : HKIConfig

Low-prior configuration (atypical parts like classroom-stove)

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.lowPriorConfig = { prior := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.lowPrior }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.asymmetryHypothesis1 : String

Asymmetry Hypothesis 1: Negation has higher production cost.

Marked forms like negation use more complex structures and longer linguistic forms, eliciting higher production cost.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.asymmetryHypothesis1 = "Marked forms like negation elicit higher production cost than " ++ "their unmarked positive-polarity counterparts."

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.asymmetryHypothesis2 : String

Asymmetry Hypothesis 2: Negation presupposes positive prominence.

Negation presupposes that its positive-polarity counterpart is relevant or prominent in common ground, but not vice versa.

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.sigmoidApprox (x L k x0 c : ℚ) : ℚ

Simple sigmoid approximation using rational arithmetic.

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyNegInterpretation (n : ℚ) : HKIState → ℚ

Fuzzy interpretation for negative utterances. [u_neg] = n (constant) [u_neg] = 1 - n

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyNegInterpretation n Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState.neg = n
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyNegInterpretation n Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIState.pos = 1 - n

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyPosInterpretation (p_pos : ℚ) (params : FuzzyParams) : HKIState → ℚ

Fuzzy interpretation for positive utterances.

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyNullInterpretation : HKIState → ℚ

Fuzzy interpretation for null utterance (no information).

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyNullInterpretation x✝ = 1

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzyMeaning (cfg : HKIConfig) (u : HKIUtterance) (s : HKIState) : ℚ

Combined fuzzy meaning function for fuzzyRSA.

Equations

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

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.worldConditionedPrior (cfg : HKIConfig) : WorldType → HKIState → ℚ

World-conditioned prior for wonkyRSA.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.worldConditionedPrior cfg Phenomena.Presupposition.Studies.HeKaiserIskarous2025.WorldType.wonky x✝ = 1 / 2
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.worldConditionedPrior cfg Phenomena.Presupposition.Studies.HeKaiserIskarous2025.WorldType.normal x✝ = cfg.prior.prob x✝

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.wonkyGoalProject : WorldType → HKIState → HKIState → Bool

Goal projection for wonkyRSA.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.wonkyGoalProject x✝² x✝¹ x✝ = (x✝¹ == x✝)

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.standard_dimensions : allUtterances.length = 3 ∧ allStates.length = 2

Standard scenario has correct dimensions.

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.wonky_dimensions : allWorldTypes.length = 2

wonkyRSA has 2 goals (normal, wonky).

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.neg_higher_cost : utteranceCost HKIUtterance.uNeg > utteranceCost HKIUtterance.uPos

Negative utterances have higher cost in our model.

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.fuzzy_low_prior_effect : fuzzyMeaning lowPriorConfig HKIUtterance.uPos HKIState.pos < fuzzyMeaning highPriorConfig HKIUtterance.uPos HKIState.pos

fuzzyRSA with low prior: positive utterance becomes less reliable.

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.neg_interpretation_constant : fuzzyMeaning lowPriorConfig HKIUtterance.uNeg HKIState.neg = fuzzyMeaning highPriorConfig HKIUtterance.uNeg HKIState.neg

Negative interpretation is constant regardless of prior.

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.toContextPolarity : Polarity → Core.NaturalLogic.ContextPolarity

Map He et al.'s sentence polarity to compositional context polarity.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.toContextPolarity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.positive = Core.NaturalLogic.ContextPolarity.upward
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.toContextPolarity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.negative = Core.NaturalLogic.ContextPolarity.downward
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.toContextPolarity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.Polarity.null = Core.NaturalLogic.ContextPolarity.upward

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.cost_reflects_polarity : utteranceCost HKIUtterance.uPos < utteranceCost HKIUtterance.uNeg

Cost aligns with UE/DE distinction: DE costs more.

inductive Phenomena.Presupposition.Studies.HeKaiserIskarous2025.PWEntity : Type

A simple model for part-whole relations.

• house : PWEntity
• classroom : PWEntity
• bathroom : PWEntity
• stove : PWEntity

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqPWEntity : DecidableEq PWEntity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instDecidableEqPWEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPWEntity.beq : PWEntity → PWEntity → Bool

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPWEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPWEntity : BEq PWEntity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPWEntity = { beq := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instBEqPWEntity.beq }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPWEntity.repr : PWEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPWEntity : Repr PWEntity

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPWEntity = { reprPrec := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.instReprPWEntity.repr }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.pwModel : Semantics.Montague.Model

Part-whole model.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.pwModel = { Entity := Phenomena.Presupposition.Studies.HeKaiserIskarous2025.PWEntity, decEq := inferInstance }

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.has_sem : pwModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

The "has" relation: which containers have which parts.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.has_sem part container = false

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.posMeaning (container part : PWEntity) : pwModel.interpTy Semantics.Montague.Ty.t

Positive sentence meaning: "A has B".

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.posMeaning container part = Phenomena.Presupposition.Studies.HeKaiserIskarous2025.has_sem part container

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negMeaning (container part : PWEntity) : pwModel.interpTy Semantics.Montague.Ty.t

Negative sentence meaning: "A doesn't have B" = neg(has(A, B)).

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negMeaning container part = Semantics.Montague.neg (Phenomena.Presupposition.Studies.HeKaiserIskarous2025.posMeaning container part)

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.neg_is_compositional (container part : PWEntity) : negMeaning container part = Semantics.Montague.neg (posMeaning container part)

Key theorem: negative meaning is compositionally derived via neg.

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.house_has_bathroom : posMeaning PWEntity.house PWEntity.bathroom = true

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.house_doesnt_have_bathroom : negMeaning PWEntity.house PWEntity.bathroom = false

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.classroom_doesnt_have_stove : negMeaning PWEntity.classroom PWEntity.stove = true

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.liftToWorlds (s : HKIState) : BProp HKIState

Lift He et al. sentences to world-indexed propositions.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.liftToWorlds s w = (w == s)

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negMeaningW : BProp HKIState

Negative sentence meaning as world-indexed proposition. ⟦"A doesn't have B"⟧ = pnot(⟦"A has B"⟧)

Equations

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

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.pnot_reverses_entailment_HKI (p q : BProp HKIState) (h : ∀ (w : HKIState), p w = true → q w = true) (w : HKIState) : Core.Proposition.Decidable.pnot HKIState q w = true → Core.Proposition.Decidable.pnot HKIState p w = true

Negation reverses entailment (DE property).

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negSentencePolarity : Semantics.Entailment.Polarity.GroundedPolarity

The grounded polarity from Entailment.Polarity (uses pnot).

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negSentencePolarity = Semantics.Entailment.Polarity.negationPolarity

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.neg_sentence_is_de : negSentencePolarity.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward

Negative sentences have DE polarity (from Montague's proof).

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.pos_sentence_is_ue : Semantics.Entailment.Polarity.identityPolarity.toContextPolarity = Core.NaturalLogic.ContextPolarity.upward

Positive sentences have UE polarity (identity = no negation).

def Phenomena.Presupposition.Studies.HeKaiserIskarous2025.structuralComplexity : HKIUtterance → ℕ

Structural complexity: count of functional heads in the derivation.

Equations

• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.structuralComplexity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNull = 0
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.structuralComplexity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uPos = 1
• Phenomena.Presupposition.Studies.HeKaiserIskarous2025.structuralComplexity Phenomena.Presupposition.Studies.HeKaiserIskarous2025.HKIUtterance.uNeg = 2

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.cost_from_structure (u : HKIUtterance) : utteranceCost u = ↑(structuralComplexity u)

Utterance cost equals structural complexity.

theorem Phenomena.Presupposition.Studies.HeKaiserIskarous2025.negation_adds_one_head : structuralComplexity HKIUtterance.uNeg = structuralComplexity HKIUtterance.uPos + 1

Negation adds exactly one unit of complexity (the Neg functional head).