English Scales

[Hor72] [Ken07] [Chi13] [Fox07] [Spe16]Horn scales for quantifiers, modals, and degrees.

Main definitions

• Scale: ordered list from weak to strong
• someAll, mightMust: standard scales

structure English.Scales.Scale (α : Type) : Type

Horn scale: ordered list from weak to strong.

• items : List α
• name : String

def English.Scales.Scale.alternatives {α : Type} [BEq α] (s : Scale α) (x : α) : List α

Equations

• s.alternatives x = match List.dropWhile (fun (x_1 : α) => x_1 != x) s.items with | [] => [] | head :: rest => rest

def English.Scales.Scale.strongest {α : Type} (s : Scale α) : Option α

Equations

• s.strongest = s.items.getLast?

def English.Scales.Scale.weakest {α : Type} (s : Scale α) : Option α

Equations

• s.weakest = s.items.head?

def English.Scales.Scale.weaker {α : Type} [BEq α] (s : Scale α) (x y : α) : Bool

Equations

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

inductive English.Scales.QuantExpr : Type

• some_ : QuantExpr
• most : QuantExpr
• all : QuantExpr

def English.Scales.instReprQuantExpr.repr : QuantExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprQuantExpr : Repr QuantExpr

Equations

• English.Scales.instReprQuantExpr = { reprPrec := English.Scales.instReprQuantExpr.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqQuantExpr : DecidableEq QuantExpr

Equations

• English.Scales.instDecidableEqQuantExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedQuantExpr : Inhabited QuantExpr

Equations

• English.Scales.instInhabitedQuantExpr = { default := English.Scales.instInhabitedQuantExpr.default }

def English.Scales.someAll : Scale QuantExpr

Equations

• English.Scales.someAll = { items := [English.Scales.QuantExpr.some_, English.Scales.QuantExpr.all], name := "⟨some, all⟩" }

def English.Scales.someMostAll : Scale QuantExpr

Equations

• English.Scales.someMostAll = { items := [English.Scales.QuantExpr.some_, English.Scales.QuantExpr.most, English.Scales.QuantExpr.all], name := "⟨some, most, all⟩" }

inductive English.Scales.ConnExpr : Type

• or_ : ConnExpr
• and_ : ConnExpr

@[implicit_reducible]

instance English.Scales.instReprConnExpr : Repr ConnExpr

Equations

• English.Scales.instReprConnExpr = { reprPrec := English.Scales.instReprConnExpr.repr }

def English.Scales.instReprConnExpr.repr : ConnExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instDecidableEqConnExpr : DecidableEq ConnExpr

Equations

• English.Scales.instDecidableEqConnExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedConnExpr : Inhabited ConnExpr

Equations

• English.Scales.instInhabitedConnExpr = { default := English.Scales.instInhabitedConnExpr.default }

def English.Scales.orAnd : Scale ConnExpr

Equations

• English.Scales.orAnd = { items := [English.Scales.ConnExpr.or_, English.Scales.ConnExpr.and_], name := "⟨or, and⟩" }

inductive English.Scales.ModalExpr : Type

• might : ModalExpr
• must : ModalExpr
• possible : ModalExpr
• necessary : ModalExpr
• allowed : ModalExpr
• required : ModalExpr

def English.Scales.instReprModalExpr.repr : ModalExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprModalExpr : Repr ModalExpr

Equations

• English.Scales.instReprModalExpr = { reprPrec := English.Scales.instReprModalExpr.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqModalExpr : DecidableEq ModalExpr

Equations

• English.Scales.instDecidableEqModalExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedModalExpr : Inhabited ModalExpr

Equations

• English.Scales.instInhabitedModalExpr = { default := English.Scales.instInhabitedModalExpr.default }

def English.Scales.mightMust : Scale ModalExpr

Equations

• English.Scales.mightMust = { items := [English.Scales.ModalExpr.might, English.Scales.ModalExpr.must], name := "⟨might, must⟩" }

def English.Scales.possibleNecessary : Scale ModalExpr

Equations

• English.Scales.possibleNecessary = { items := [English.Scales.ModalExpr.possible, English.Scales.ModalExpr.necessary], name := "⟨possible, necessary⟩" }

def English.Scales.allowedRequired : Scale ModalExpr

Equations

• English.Scales.allowedRequired = { items := [English.Scales.ModalExpr.allowed, English.Scales.ModalExpr.required], name := "⟨allowed, required⟩" }

inductive English.Scales.DegreeExpr : Type

Degree/gradable adjective expressions

• warm : DegreeExpr
• hot : DegreeExpr
• good : DegreeExpr
• excellent : DegreeExpr
• like : DegreeExpr
• love : DegreeExpr

def English.Scales.instReprDegreeExpr.repr : DegreeExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprDegreeExpr : Repr DegreeExpr

Equations

• English.Scales.instReprDegreeExpr = { reprPrec := English.Scales.instReprDegreeExpr.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqDegreeExpr : DecidableEq DegreeExpr

Equations

• English.Scales.instDecidableEqDegreeExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedDegreeExpr : Inhabited DegreeExpr

Equations

• English.Scales.instInhabitedDegreeExpr = { default := English.Scales.instInhabitedDegreeExpr.default }

def English.Scales.warmHot : Scale DegreeExpr

The ⟨warm, hot⟩ scale

Equations

• English.Scales.warmHot = { items := [English.Scales.DegreeExpr.warm, English.Scales.DegreeExpr.hot], name := "⟨warm, hot⟩" }

def English.Scales.goodExcellent : Scale DegreeExpr

The ⟨good, excellent⟩ scale

Equations

• English.Scales.goodExcellent = { items := [English.Scales.DegreeExpr.good, English.Scales.DegreeExpr.excellent], name := "⟨good, excellent⟩" }

def English.Scales.likeLove : Scale DegreeExpr

The ⟨like, love⟩ scale

Equations

• English.Scales.likeLove = { items := [English.Scales.DegreeExpr.like, English.Scales.DegreeExpr.love], name := "⟨like, love⟩" }

inductive English.Scales.EvalExpr : Type

Evaluative adjective expressions for quality judgments.

This scale is used in:

• [YTGF20] politeness model
• Review/feedback contexts

The scale goes from strongly negative to strongly positive: ⟨terrible, bad, good, amazing⟩

• terrible : EvalExpr
• bad : EvalExpr
• good : EvalExpr
• amazing : EvalExpr

def English.Scales.instReprEvalExpr.repr : EvalExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprEvalExpr : Repr EvalExpr

Equations

• English.Scales.instReprEvalExpr = { reprPrec := English.Scales.instReprEvalExpr.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqEvalExpr : DecidableEq EvalExpr

Equations

• English.Scales.instDecidableEqEvalExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedEvalExpr : Inhabited EvalExpr

Equations

• English.Scales.instInhabitedEvalExpr = { default := English.Scales.instInhabitedEvalExpr.default }

def English.Scales.terribleAmazing : Scale EvalExpr

The ⟨terrible, bad, good, amazing⟩ evaluative scale

Equations

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

inductive English.Scales.NegatedEvalExpr : Type

Negated evaluative: "not terrible", "not amazing", etc.

• notTerrible : NegatedEvalExpr
• notBad : NegatedEvalExpr
• notGood : NegatedEvalExpr
• notAmazing : NegatedEvalExpr

def English.Scales.instReprNegatedEvalExpr.repr : NegatedEvalExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprNegatedEvalExpr : Repr NegatedEvalExpr

Equations

• English.Scales.instReprNegatedEvalExpr = { reprPrec := English.Scales.instReprNegatedEvalExpr.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqNegatedEvalExpr : DecidableEq NegatedEvalExpr

Equations

• English.Scales.instDecidableEqNegatedEvalExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedNegatedEvalExpr : Inhabited NegatedEvalExpr

Equations

• English.Scales.instInhabitedNegatedEvalExpr = { default := English.Scales.instInhabitedNegatedEvalExpr.default }

def English.Scales.EvalExpr.negate : EvalExpr → NegatedEvalExpr

Convert evaluative to negated form

Equations

• English.Scales.EvalExpr.terrible.negate = English.Scales.NegatedEvalExpr.notTerrible
• English.Scales.EvalExpr.bad.negate = English.Scales.NegatedEvalExpr.notBad
• English.Scales.EvalExpr.good.negate = English.Scales.NegatedEvalExpr.notGood
• English.Scales.EvalExpr.amazing.negate = English.Scales.NegatedEvalExpr.notAmazing

def English.Scales.NegatedEvalExpr.base : NegatedEvalExpr → EvalExpr

Get the base (unnegated) form

Equations

• English.Scales.NegatedEvalExpr.notTerrible.base = English.Scales.EvalExpr.terrible
• English.Scales.NegatedEvalExpr.notBad.base = English.Scales.EvalExpr.bad
• English.Scales.NegatedEvalExpr.notGood.base = English.Scales.EvalExpr.good
• English.Scales.NegatedEvalExpr.notAmazing.base = English.Scales.EvalExpr.amazing

inductive English.Scales.EvalUtterance : Type

Combined evaluative utterance type (positive + negated).

This is the full utterance set for politeness scenarios: 8 utterances = 4 positive + 4 negated.

• pos : EvalExpr → EvalUtterance
• neg : NegatedEvalExpr → EvalUtterance

def English.Scales.instReprEvalUtterance.repr : EvalUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprEvalUtterance : Repr EvalUtterance

Equations

• English.Scales.instReprEvalUtterance = { reprPrec := English.Scales.instReprEvalUtterance.repr }

@[implicit_reducible]

instance English.Scales.instDecidableEqEvalUtterance : DecidableEq EvalUtterance

Equations

• English.Scales.instDecidableEqEvalUtterance = English.Scales.instDecidableEqEvalUtterance.decEq

def English.Scales.instDecidableEqEvalUtterance.decEq (x✝ x✝¹ : EvalUtterance) : Decidable (x✝ = x✝¹)

Equations

• English.Scales.instDecidableEqEvalUtterance.decEq (English.Scales.EvalUtterance.pos a) (English.Scales.EvalUtterance.pos b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• English.Scales.instDecidableEqEvalUtterance.decEq (English.Scales.EvalUtterance.pos a) (English.Scales.EvalUtterance.neg a_1) = isFalse ⋯
• English.Scales.instDecidableEqEvalUtterance.decEq (English.Scales.EvalUtterance.neg a) (English.Scales.EvalUtterance.pos a_1) = isFalse ⋯
• English.Scales.instDecidableEqEvalUtterance.decEq (English.Scales.EvalUtterance.neg a) (English.Scales.EvalUtterance.neg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instInhabitedEvalUtterance : Inhabited EvalUtterance

Equations

• English.Scales.instInhabitedEvalUtterance = { default := English.Scales.instInhabitedEvalUtterance.default }

def English.Scales.allEvalUtterances : List EvalUtterance

All evaluative utterances (positive and negated)

Equations

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

def English.Scales.EvalUtterance.isNegated : EvalUtterance → Bool

Is this a negated utterance?

Equations

• (English.Scales.EvalUtterance.pos a).isNegated = false
• (English.Scales.EvalUtterance.neg a).isNegated = true

def English.Scales.numerals (n : ℕ) : Scale ℕ

Build a numeral scale from 1 to n

Equations

• English.Scales.numerals n = { items := List.map (fun (x : ℕ) => x + 1) (List.range n), name := toString "⟨1, ..., " ++ toString n ++ toString "⟩" }

def English.Scales.scalarImplicatures {α : Type} [BEq α] [Repr α] (s : Scale α) (x : α) : List (String × α)

Compute scalar implicature: x implicates ¬y for each stronger y

Equations

• English.Scales.scalarImplicatures s x = List.map (fun (y : α) => (toString "¬" ++ toString (repr y), y)) (s.alternatives x)

Closure Under Conjunction

A crucial property for exhaustification: whether the alternative set is CLOSED UNDER CONJUNCTION.

[Spe16] Theorem 9

When alternatives are closed under ∧, the two exhaustivity operators exh_mw and exh_ie are EQUIVALENT.

[Chi13] EFCI Analysis

The puzzle of Free Choice Items depends on alternatives NOT being closed:

• Standard scalar alternatives ⟨some, all⟩: closed under ∧
• Domain alternatives {P(d) | d ∈ D}: NOT closed under ∧

When domain alternatives are NOT closed, exhaustification can lead to contradiction (the EFCI puzzle), which is then resolved by rescue mechanisms.

Insight

Alternative Type	Closed?	Exhaustification Result
Scalar ⟨some, all⟩	✓	Clean SI: "some but not all"
Domain {P(d)}	✗	Contradiction (needs rescue)

def English.Scales.PropConj (α : Type) : Type

Conjunction operation on propositions (semantic level).

Equations

• English.Scales.PropConj α = (α → α → α)

structure English.Scales.ClosedUnderConj (α : Type) : Type

A set of alternatives is closed under conjunction if conjoining any two members yields another member (or a stronger proposition in the set).

For semantic alternatives as propositions, this means: ∀ p q ∈ ALT, p ∧ q ∈ ALT (or is entailed by something in ALT)

• alts : List α

  The set of alternatives

• conj : α → α → α

  The conjunction operation

• isClosed : Bool

  Is it closed?

• nonClosureWitness : Option (α × α × String)

  Witness to non-closure (if not closed)

def English.Scales.quantifierScaleClosed : ClosedUnderConj QuantExpr

Standard scalar alternatives are closed under conjunction.

For ⟨some, all⟩:

• some ∧ some = some ✓
• some ∧ all = all ✓ (entailed by all)
• all ∧ all = all ✓

Equations

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

def English.Scales.connScaleClosed : ClosedUnderConj ConnExpr

Connective alternatives are closed.

For ⟨or, and⟩:

• or ∧ or = or ✓
• or ∧ and = and ✓
• and ∧ and = and ✓

Equations

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

structure English.Scales.DomainAlternatives (Entity : Type) : Type

Domain alternatives (singleton domains) are NOT closed under conjunction.

For domain D = {a, b, c} with predicate P:

• Alternatives: {P(a), P(b), P(c)}
• P(a) ∧ P(b) = "exactly a and b" is NOT in the set
• This non-closure causes the EFCI puzzle

Represented symbolically: conjoining "exactly a" with "exactly b" gives a proposition NOT in the original alternative set.

• domain : List Entity

  The domain

• isClosed : Bool

  Is it closed under conjunction?

• explanation : String

  Why not closed?

def English.Scales.threeDomain : DomainAlternatives ℕ

Example: three-element domain shows non-closure.

Equations

• English.Scales.threeDomain = { domain := [1, 2, 3], explanation := "P(1) ∧ P(2) = 'exactly 1 and 2' ∉ singleton alternatives" }

inductive English.Scales.ClosureEffect : Type

Closure status affects exhaustification behavior.

• cleanSI : ClosureEffect
• contradiction : ClosureEffect
• needsRescue : ClosureEffect

@[implicit_reducible]

instance English.Scales.instDecidableEqClosureEffect : DecidableEq ClosureEffect

Equations

• English.Scales.instDecidableEqClosureEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Scales.instReprClosureEffect : Repr ClosureEffect

Equations

• English.Scales.instReprClosureEffect = { reprPrec := English.Scales.instReprClosureEffect.repr }

def English.Scales.instReprClosureEffect.repr : ClosureEffect → ℕ → Std.Format

Equations

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

def English.Scales.predictExhEffect (isClosed : Bool) : ClosureEffect

Predict exhaustification effect from closure status.

Equations

• English.Scales.predictExhEffect isClosed = if isClosed = true then English.Scales.ClosureEffect.cleanSI else English.Scales.ClosureEffect.needsRescue

Spector's Theorem 9

Theorem 9: When ALT is closed under conjunction, exh_mw = exh_ie.

This is proven in Semantics/Exhaustification/Operators/Basic.lean.

The closure property ensures that the different ways of computing "what to exclude" all converge to the same result.

Practical Implication

For standard scalar alternatives (which ARE closed):

• We can use either exh_mw or exh_ie
• They give identical results
• Simple "negate the stronger alternatives" suffices

For EFCI alternatives (which are NOT closed):

• exh_mw ≠ exh_ie in general
• Innocent exclusion (exh_ie) is preferred
• But even exh_ie can lead to contradiction without rescue

structure English.Scales.ClosureSummary : Type

Summary of closure and its effects.

• altType : String

  Alternative type

• isClosed : Bool

  Is it closed?

• effect : String

  Effect on exhaustification

• reference : String

  Relevant theory reference

def English.Scales.instReprClosureSummary.repr : ClosureSummary → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Scales.instReprClosureSummary : Repr ClosureSummary

Equations

• English.Scales.instReprClosureSummary = { reprPrec := English.Scales.instReprClosureSummary.repr }

def English.Scales.scalarClosureSummary : ClosureSummary

Equations

• English.Scales.scalarClosureSummary = { altType := "Scalar ⟨some, all⟩", isClosed := true, effect := "exh_mw = exh_ie; clean SI", reference := "Spector (2016) Theorem 9" }

def English.Scales.domainClosureSummary : ClosureSummary

Equations

• English.Scales.domainClosureSummary = { altType := "Domain {P(d) | d ∈ D}", isClosed := false, effect := "exh can contradict; needs rescue", reference := "Chierchia (2013) EFCI" }

def English.Scales.closureSummaries : List ClosureSummary

Equations

• English.Scales.closureSummaries = [English.Scales.scalarClosureSummary, English.Scales.domainClosureSummary]