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 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

@[implicit_reducible]

instance HeKaiserIskarous2025.instDecidableEqHKIState : DecidableEq HKIState

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instReprHKIState : Repr HKIState

Equations

• HeKaiserIskarous2025.instReprHKIState = { reprPrec := HeKaiserIskarous2025.instReprHKIState.repr }

def HeKaiserIskarous2025.instReprHKIState.repr : HKIState → ℕ → Std.Format

Equations

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

def HeKaiserIskarous2025.instInhabitedHKIState.default : HKIState

Equations

• HeKaiserIskarous2025.instInhabitedHKIState.default = HeKaiserIskarous2025.HKIState.pos

@[implicit_reducible]

instance HeKaiserIskarous2025.instInhabitedHKIState : Inhabited HKIState

Equations

• HeKaiserIskarous2025.instInhabitedHKIState = { default := HeKaiserIskarous2025.instInhabitedHKIState.default }

@[implicit_reducible]

instance HeKaiserIskarous2025.instFintypeHKIState : Fintype HKIState

Equations

• HeKaiserIskarous2025.instFintypeHKIState = { elems := {HeKaiserIskarous2025.HKIState.pos, HeKaiserIskarous2025.HKIState.neg}, complete := HeKaiserIskarous2025.instFintypeHKIState._proof_1 }

@[implicit_reducible]

instance HeKaiserIskarous2025.instFinEnumHKIState : FinEnum HKIState

Equations

• HeKaiserIskarous2025.instFinEnumHKIState = FinEnum.ofList [HeKaiserIskarous2025.HKIState.pos, HeKaiserIskarous2025.HKIState.neg] HeKaiserIskarous2025.instFinEnumHKIState._proof_1

def HeKaiserIskarous2025.allStates : List HKIState

All states

Equations

• HeKaiserIskarous2025.allStates = [HeKaiserIskarous2025.HKIState.pos, HeKaiserIskarous2025.HKIState.neg]

theorem HeKaiserIskarous2025.allStates_length : allStates.length = 2

inductive 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

@[implicit_reducible]

instance HeKaiserIskarous2025.instDecidableEqHKIUtterance : DecidableEq HKIUtterance

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instReprHKIUtterance : Repr HKIUtterance

Equations

• HeKaiserIskarous2025.instReprHKIUtterance = { reprPrec := HeKaiserIskarous2025.instReprHKIUtterance.repr }

def HeKaiserIskarous2025.instReprHKIUtterance.repr : HKIUtterance → ℕ → Std.Format

Equations

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

def HeKaiserIskarous2025.instInhabitedHKIUtterance.default : HKIUtterance

Equations

• HeKaiserIskarous2025.instInhabitedHKIUtterance.default = HeKaiserIskarous2025.HKIUtterance.uPos

@[implicit_reducible]

instance HeKaiserIskarous2025.instInhabitedHKIUtterance : Inhabited HKIUtterance

Equations

• HeKaiserIskarous2025.instInhabitedHKIUtterance = { default := HeKaiserIskarous2025.instInhabitedHKIUtterance.default }

@[implicit_reducible]

instance HeKaiserIskarous2025.instFintypeHKIUtterance : Fintype HKIUtterance

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instFinEnumHKIUtterance : FinEnum HKIUtterance

Equations

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

def HeKaiserIskarous2025.allUtterances : List HKIUtterance

All utterances

Equations

• HeKaiserIskarous2025.allUtterances = [HeKaiserIskarous2025.HKIUtterance.uPos, HeKaiserIskarous2025.HKIUtterance.uNeg, HeKaiserIskarous2025.HKIUtterance.uNull]

theorem HeKaiserIskarous2025.allUtterances_length : allUtterances.length = 3

inductive HeKaiserIskarous2025.Polarity : Type

Sentence polarity

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instDecidableEqPolarity : DecidableEq Polarity

Equations

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

def HeKaiserIskarous2025.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instReprPolarity : Repr Polarity

Equations

• HeKaiserIskarous2025.instReprPolarity = { reprPrec := HeKaiserIskarous2025.instReprPolarity.repr }

def HeKaiserIskarous2025.HKIUtterance.polarity : HKIUtterance → Polarity

Get polarity of an utterance

Equations

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

def 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

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

theorem HeKaiserIskarous2025.neg_costs_more : utteranceCost HKIUtterance.uNeg > utteranceCost HKIUtterance.uPos

Negative utterances cost more than positive (Asymmetry Hypothesis 1)

def 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

• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.pos HeKaiserIskarous2025.HKIUtterance.uPos = true
• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.pos HeKaiserIskarous2025.HKIUtterance.uNeg = false
• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.pos HeKaiserIskarous2025.HKIUtterance.uNull = true
• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.neg HeKaiserIskarous2025.HKIUtterance.uPos = false
• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.neg HeKaiserIskarous2025.HKIUtterance.uNeg = true
• HeKaiserIskarous2025.literalTruth HeKaiserIskarous2025.HKIState.neg HeKaiserIskarous2025.HKIUtterance.uNull = true

inductive 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

@[implicit_reducible]

instance HeKaiserIskarous2025.instDecidableEqWorldType : DecidableEq WorldType

Equations

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

def HeKaiserIskarous2025.instReprWorldType.repr : WorldType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instReprWorldType : Repr WorldType

Equations

• HeKaiserIskarous2025.instReprWorldType = { reprPrec := HeKaiserIskarous2025.instReprWorldType.repr }

@[implicit_reducible]

instance HeKaiserIskarous2025.instInhabitedWorldType : Inhabited WorldType

Equations

• HeKaiserIskarous2025.instInhabitedWorldType = { default := HeKaiserIskarous2025.instInhabitedWorldType.default }

def HeKaiserIskarous2025.instInhabitedWorldType.default : WorldType

Equations

• HeKaiserIskarous2025.instInhabitedWorldType.default = HeKaiserIskarous2025.WorldType.normal

def HeKaiserIskarous2025.allWorldTypes : List WorldType

All world types

Equations

• HeKaiserIskarous2025.allWorldTypes = [HeKaiserIskarous2025.WorldType.normal, HeKaiserIskarous2025.WorldType.wonky]

theorem HeKaiserIskarous2025.allWorldTypes_length : allWorldTypes.length = 2

structure 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 HeKaiserIskarous2025.HKIPrior.p_neg (prior : HKIPrior) : ℚ

P(s_neg) = 1 - P(s_pos)

Equations

• prior.p_neg = 1 - prior.p_pos

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

Get prior probability of a state

Equations

• prior.prob HeKaiserIskarous2025.HKIState.pos = prior.p_pos
• prior.prob HeKaiserIskarous2025.HKIState.neg = prior.p_neg

def HeKaiserIskarous2025.uniformPrior : HKIPrior

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

Equations

• HeKaiserIskarous2025.uniformPrior = { p_pos := 1 / 2, h_pos_nonneg := HeKaiserIskarous2025.uniformPrior._proof_1, h_pos_le_one := HeKaiserIskarous2025.uniformPrior._proof_2 }

def HeKaiserIskarous2025.highPrior : HKIPrior

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

Equations

• HeKaiserIskarous2025.highPrior = { p_pos := 9 / 10, h_pos_nonneg := HeKaiserIskarous2025.highPrior._proof_1, h_pos_le_one := HeKaiserIskarous2025.highPrior._proof_2 }

def HeKaiserIskarous2025.lowPrior : HKIPrior

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

Equations

• HeKaiserIskarous2025.lowPrior = { p_pos := 1 / 10, h_pos_nonneg := HeKaiserIskarous2025.lowPrior._proof_1, h_pos_le_one := HeKaiserIskarous2025.lowPrior._proof_2 }

structure 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 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

• HeKaiserIskarous2025.bestFitFuzzyParams = { n := 4 / 5, L := 7 / 10, k := 6, x0 := 7 / 20, c := 3 / 10, h_n_valid := HeKaiserIskarous2025.bestFitFuzzyParams._proof_1 }

structure 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 HeKaiserIskarous2025.defaultConfig : HKIConfig

Default configuration with uniform prior

Equations

• HeKaiserIskarous2025.defaultConfig = { prior := HeKaiserIskarous2025.uniformPrior }

def HeKaiserIskarous2025.highPriorConfig : HKIConfig

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

Equations

• HeKaiserIskarous2025.highPriorConfig = { prior := HeKaiserIskarous2025.highPrior }

def HeKaiserIskarous2025.lowPriorConfig : HKIConfig

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

Equations

• HeKaiserIskarous2025.lowPriorConfig = { prior := HeKaiserIskarous2025.lowPrior }

def 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

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

def 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

• HeKaiserIskarous2025.asymmetryHypothesis2 = "Negation presupposes that its positive-polarity counterpart is " ++ "relevant or prominent in the common ground, not the other way around."

def 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 HeKaiserIskarous2025.fuzzyNegInterpretation (n : ℚ) : HKIState → ℚ

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

Equations

• HeKaiserIskarous2025.fuzzyNegInterpretation n HeKaiserIskarous2025.HKIState.neg = n
• HeKaiserIskarous2025.fuzzyNegInterpretation n HeKaiserIskarous2025.HKIState.pos = 1 - n

def 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 HeKaiserIskarous2025.fuzzyNullInterpretation : HKIState → ℚ

Fuzzy interpretation for null utterance (no information).

Equations

• HeKaiserIskarous2025.fuzzyNullInterpretation x✝ = 1

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

Combined fuzzy meaning function for fuzzyRSA.

Equations

• HeKaiserIskarous2025.fuzzyMeaning cfg HeKaiserIskarous2025.HKIUtterance.uNeg s = HeKaiserIskarous2025.fuzzyNegInterpretation cfg.fuzzyParams.n s
• HeKaiserIskarous2025.fuzzyMeaning cfg HeKaiserIskarous2025.HKIUtterance.uPos s = HeKaiserIskarous2025.fuzzyPosInterpretation cfg.prior.p_pos cfg.fuzzyParams s
• HeKaiserIskarous2025.fuzzyMeaning cfg HeKaiserIskarous2025.HKIUtterance.uNull s = HeKaiserIskarous2025.fuzzyNullInterpretation s

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

World-conditioned prior for wonkyRSA.

Equations

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

def HeKaiserIskarous2025.wonkyGoalProject : WorldType → HKIState → HKIState → Bool

Goal projection for wonkyRSA.

Equations

• HeKaiserIskarous2025.wonkyGoalProject x✝² x✝¹ x✝ = (x✝¹ == x✝)

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

Standard scenario has correct dimensions.

theorem HeKaiserIskarous2025.wonky_dimensions : allWorldTypes.length = 2

wonkyRSA has 2 goals (normal, wonky).

theorem HeKaiserIskarous2025.neg_higher_cost : utteranceCost HKIUtterance.uNeg > utteranceCost HKIUtterance.uPos

Negative utterances have higher cost in our model.

theorem 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 HeKaiserIskarous2025.neg_interpretation_constant : fuzzyMeaning lowPriorConfig HKIUtterance.uNeg HKIState.neg = fuzzyMeaning highPriorConfig HKIUtterance.uNeg HKIState.neg

Negative interpretation is constant regardless of prior.

def HeKaiserIskarous2025.toContextPolarity : Polarity → Core.NaturalLogic.ContextPolarity

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

Equations

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

theorem HeKaiserIskarous2025.cost_reflects_polarity : utteranceCost HKIUtterance.uPos < utteranceCost HKIUtterance.uNeg

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

inductive HeKaiserIskarous2025.PWEntity : Type

A simple model for part-whole relations.

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instDecidableEqPWEntity : DecidableEq PWEntity

Equations

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

def HeKaiserIskarous2025.instReprPWEntity.repr : PWEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HeKaiserIskarous2025.instReprPWEntity : Repr PWEntity

Equations

• HeKaiserIskarous2025.instReprPWEntity = { reprPrec := HeKaiserIskarous2025.instReprPWEntity.repr }

def HeKaiserIskarous2025.pwFrame : Core.Logic.Intensional.Frame

Part-whole frame.

Equations

• HeKaiserIskarous2025.pwFrame = { Entity := HeKaiserIskarous2025.PWEntity, Index := Unit }

def HeKaiserIskarous2025.has_sem : pwFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

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

Equations

• HeKaiserIskarous2025.has_sem HeKaiserIskarous2025.PWEntity.bathroom HeKaiserIskarous2025.PWEntity.house = True
• HeKaiserIskarous2025.has_sem HeKaiserIskarous2025.PWEntity.stove HeKaiserIskarous2025.PWEntity.classroom = False
• HeKaiserIskarous2025.has_sem part container = False

def HeKaiserIskarous2025.posMeaning (container part : PWEntity) : pwFrame.Denot Core.Logic.Intensional.Ty.t

Positive sentence meaning: "A has B".

Equations

• HeKaiserIskarous2025.posMeaning container part = HeKaiserIskarous2025.has_sem part container

def HeKaiserIskarous2025.negMeaning (container part : PWEntity) : pwFrame.Denot Core.Logic.Intensional.Ty.t

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

Equations

• HeKaiserIskarous2025.negMeaning container part = Core.Logic.Intensional.neg (HeKaiserIskarous2025.posMeaning container part)

theorem HeKaiserIskarous2025.neg_is_compositional (container part : PWEntity) : negMeaning container part = Core.Logic.Intensional.neg (posMeaning container part)

Key theorem: negative meaning is compositionally derived via neg.

theorem HeKaiserIskarous2025.house_has_bathroom : posMeaning PWEntity.house PWEntity.bathroom

theorem HeKaiserIskarous2025.house_doesnt_have_bathroom : ¬negMeaning PWEntity.house PWEntity.bathroom

theorem HeKaiserIskarous2025.classroom_doesnt_have_stove : negMeaning PWEntity.classroom PWEntity.stove

def HeKaiserIskarous2025.liftToWorlds (s : HKIState) : HKIState → Bool

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

Equations

• HeKaiserIskarous2025.liftToWorlds s w = (w == s)

def HeKaiserIskarous2025.negMeaningW : HKIState → Bool

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

Equations

• HeKaiserIskarous2025.negMeaningW w = !HeKaiserIskarous2025.liftToWorlds HeKaiserIskarous2025.HKIState.pos w

theorem HeKaiserIskarous2025.pnot_reverses_entailment_HKI (p q : HKIState → Bool) (h : ∀ (w : HKIState), p w = true → q w = true) (w : HKIState) : (!q w) = true → (!p w) = true

Negation reverses entailment (DE property).

def HeKaiserIskarous2025.negSentencePolarity : Semantics.Entailment.Polarity.GroundedPolarity

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

Equations

• HeKaiserIskarous2025.negSentencePolarity = Semantics.Entailment.Polarity.negationPolarity

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

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

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

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

def HeKaiserIskarous2025.structuralComplexity : HKIUtterance → ℕ

Structural complexity: count of functional heads in the derivation.

Equations

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

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

Utterance cost equals structural complexity.

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

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