Linglib.Theories.Semantics.Alternatives.Lexical

Under lower-bound semantics, numerals do form a scale (⟨1, 2, 3,...⟩), but it is infinite — a finite HornScale list can't represent it correctly ("five" would have no stronger alternatives).
Under bilateral semantics, numerals are non-monotonic and do NOT form a Horn scale at all. The relevant alternatives are {bare n, Class A n, Class B n}, not other numerals.

Both cases are handled properly in Theories/Semantics.Montague/Determiner/Numeral/Semantics.lean:

NumeralTheory.isStrongerThan computes strength for any theory
NumeralAlternative represents Kennedy's alternative sets
lowerBound_monotonic / bilateral_not_monotonic prove the key contrast

Singular/Plural as a Horn Scale #

@cite{sauerland-2003} @cite{spector-2007} @cite{tieu-etal-2020}

The singular and plural morphemes form a Horn scale ⟨singular, plural⟩ where singular ("a giraffe") is the stronger alternative to plural ("giraffes").

Under the implicature approach to multiplicity inferences, the plural literally means "one or more" and the "more than one" inference arises as a scalar implicature: the listener reasons that the speaker chose the weaker "giraffes" over the stronger "a giraffe," implying that the singular alternative is false — hence more than one.

This scale is structurally unusual: the alternatives differ in morphology (number marking), not in lexical choice (unlike some/all, or/and).

source

inductive Alternatives.Number.NumberExpr :

Type

singular : NumberExpr
plural : NumberExpr

Instances For

source

instance Alternatives.Number.instDecidableEqNumberExpr :

DecidableEq NumberExpr

Equations

Alternatives.Number.instDecidableEqNumberExpr x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Alternatives.Number.instBEqNumberExpr :

BEq NumberExpr

Equations

Alternatives.Number.instBEqNumberExpr = { beq := Alternatives.Number.instBEqNumberExpr.beq }

source

def Alternatives.Number.instBEqNumberExpr.beq :

NumberExpr → NumberExpr → Bool

Equations

Alternatives.Number.instBEqNumberExpr.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Alternatives.Number.instReprNumberExpr :

Repr NumberExpr

Equations

Alternatives.Number.instReprNumberExpr = { reprPrec := Alternatives.Number.instReprNumberExpr.repr }

source

def Alternatives.Number.instReprNumberExpr.repr :

NumberExpr → ℕ → Std.Format

Equations

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

Instances For

source

def Alternatives.Number.instInhabitedNumberExpr.default :

NumberExpr

Equations

Alternatives.Number.instInhabitedNumberExpr.default = Alternatives.Number.NumberExpr.singular

Instances For

source

instance Alternatives.Number.instInhabitedNumberExpr :

Inhabited NumberExpr

Equations

Alternatives.Number.instInhabitedNumberExpr = { default := Alternatives.Number.instInhabitedNumberExpr.default }

source

def Alternatives.Number.NumberExpr.toString :

NumberExpr → String

Equations

Alternatives.Number.NumberExpr.singular.toString = "singular"
Alternatives.Number.NumberExpr.plural.toString = "plural"

Instances For

source

instance Alternatives.Number.instToStringNumberExpr :

ToString NumberExpr

Equations

Alternatives.Number.instToStringNumberExpr = { toString := Alternatives.Number.NumberExpr.toString }

source

def Alternatives.Number.numberScale :

HornScale NumberExpr

Singular is stronger: "a giraffe" entails "giraffes" (one or more).

Equations

Alternatives.Number.numberScale = { members := [Alternatives.Number.NumberExpr.plural , Alternatives.Number.NumberExpr.singular ] }

Instances For

source

theorem Alternatives.Number.singular_stronger_than_plural :

isStronger numberScale NumberExpr.singular NumberExpr.plural = true

source

theorem Alternatives.Number.plural_alternative :

strongerAlternatives numberScale NumberExpr.plural = [NumberExpr.singular ]

source

def Alternatives.scalarImplicatures {α : Type} [BEq α] (s : HornScale α) (x : α) :

List α

Equations

Alternatives.scalarImplicatures s x = Alternatives.strongerAlternatives s x

Instances For

source

inductive Alternatives.Monotonicity :

Type

upward : Monotonicity
downward : Monotonicity

Instances For

source

instance Alternatives.instDecidableEqMonotonicity :

DecidableEq Monotonicity

Equations

Alternatives.instDecidableEqMonotonicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Alternatives.instBEqMonotonicity :

BEq Monotonicity

Equations

Alternatives.instBEqMonotonicity = { beq := Alternatives.instBEqMonotonicity.beq }

source

def Alternatives.instBEqMonotonicity.beq :

Monotonicity → Monotonicity → Bool

Equations

Alternatives.instBEqMonotonicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Alternatives.instReprMonotonicity :

Repr Monotonicity

Equations

Alternatives.instReprMonotonicity = { reprPrec := Alternatives.instReprMonotonicity.repr }

source

def Alternatives.instReprMonotonicity.repr :

Monotonicity → ℕ → Std.Format

Equations

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

Instances For

source

def Alternatives.scalarAlternativesInContext {α : Type} [BEq α] (s : HornScale α) (x : α) (m : Monotonicity) :

List α

Equations

Instances For

source

theorem Alternatives.de_blocks_some_not_all :

scalarAlternativesInContext Quantifiers.quantScale Quantifiers.QuantExpr.all Monotonicity.downward = [Quantifiers.QuantExpr.none_, Quantifiers.QuantExpr.some_, Quantifiers.QuantExpr.most ]

source

def Alternatives.Polarity.toMonotonicity :

Core.Polarity → Monotonicity

Sentence polarity determines monotonicity context: positive sentences are upward-entailing, negative are downward-entailing. This is the Ladusaw (1979) / Fauconnier (1975) connection.

Equations

Instances For

source

structure Alternatives.SemanticScale (World : Type u_1) :

Type u_1

A Horn scale with semantic content: a pair of propositions where stronger entails weaker but not vice versa.

This is the proposition-level counterpart of HornScale α (form-level). The entailment asymmetry drives scalar implicatures via exhaustification.

name : String
Name of the scale
weakerTerm : String
The weaker scalar term (e.g., "some")
strongerTerm : String
The stronger scalar term (e.g., "all")
weaker : World → Prop
Semantic denotation of weaker term
stronger : World → Prop
Semantic denotation of stronger term
entailment (w : World) : self.stronger w → self.weaker w
Stronger entails weaker
nonTrivial : ¬∀ (w : World), self.weaker w → self.stronger w
Weaker does not entail stronger (non-trivial scale)

Instances For

source

def Alternatives.SemanticScale.alts {World : Type u_1} (s : SemanticScale World) :

Set (World → Prop)

Alternative set for a semantic scale: {weaker, stronger}.

Equations

s.alts = {s.weaker, s.stronger}

Instances For

source

@[reducible, inline]

abbrev Alternatives.SemQuantWorld :

Type

Worlds for quantifier scale: number satisfying predicate (0 to 3).

Equations

Alternatives.SemQuantWorld = Fin 4

Instances For

source

def Alternatives.someQ :

SemQuantWorld → Prop

"Some Ps are Q" = at least one.

Equations

Alternatives.someQ w = (↑w ≥ 1)

Instances For

source

def Alternatives.allQ :

SemQuantWorld → Prop

"All Ps are Q" = all three.

Equations

Alternatives.allQ w = (↑w = 3)

Instances For

source

theorem Alternatives.all_entails_some (w : SemQuantWorld) :

allQ w → someQ w

All entails some.

source

theorem Alternatives.some_not_entails_all :

¬∀ (w : SemQuantWorld), someQ w → allQ w

Some does not entail all.

source

def Alternatives.someAllScale :

SemanticScale SemQuantWorld

The some/all semantic scale.

Equations

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

Instances For

source

inductive Alternatives.ConnWorld :

Type

Worlds for connective scale.

neither : ConnWorld
onlyA : ConnWorld
onlyB : ConnWorld
both : ConnWorld

Instances For

source

instance Alternatives.instDecidableEqConnWorld :

DecidableEq ConnWorld

Equations

Alternatives.instDecidableEqConnWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Alternatives.instReprConnWorld :

Repr ConnWorld

Equations

Alternatives.instReprConnWorld = { reprPrec := Alternatives.instReprConnWorld.repr }

source

def Alternatives.instReprConnWorld.repr :

ConnWorld → ℕ → Std.Format

Equations

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

Instances For

source

def Alternatives.orConn :

ConnWorld → Prop

"A or B" (inclusive).

Equations

Instances For

source

def Alternatives.andConn :

ConnWorld → Prop

"A and B".

Equations

Instances For

source

theorem Alternatives.and_entails_or (w : ConnWorld) :

andConn w → orConn w

And entails or.

source

theorem Alternatives.or_not_entails_and :

¬∀ (w : ConnWorld), orConn w → andConn w

Or does not entail and.

source

def Alternatives.orAndScale :

SemanticScale ConnWorld

The or/and semantic scale.

Equations

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

Instances For

source

inductive Alternatives.ModalWorld :

Type

Worlds for modal scale: accessibility relation outcomes.

none : ModalWorld
some : ModalWorld
all : ModalWorld

Instances For

source

instance Alternatives.instDecidableEqModalWorld :

DecidableEq ModalWorld

Equations

Alternatives.instDecidableEqModalWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Alternatives.instReprModalWorld.repr :

ModalWorld → ℕ → Std.Format

Equations

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

Instances For

source

instance Alternatives.instReprModalWorld :

Repr ModalWorld

Equations

Alternatives.instReprModalWorld = { reprPrec := Alternatives.instReprModalWorld.repr }

source

def Alternatives.possibleP :

ModalWorld → Prop

"Possibly P" = at least one accessible world has P.

Equations

Instances For

source

def Alternatives.necessaryP :

ModalWorld → Prop

"Necessarily P" = all accessible worlds have P.

Equations

Instances For

source

theorem Alternatives.necessary_entails_possible (w : ModalWorld) :

necessaryP w → possibleP w

Necessary entails possible.

source

theorem Alternatives.possible_not_entails_necessary :

¬∀ (w : ModalWorld), possibleP w → necessaryP w

Possible does not entail necessary.

source

def Alternatives.possibleNecessaryScale :

SemanticScale ModalWorld

The possible/necessary semantic scale.

Equations

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

Instances For

source

class Alternatives.AlternativeSource (Form : Type) :

Type

An alternative source generates candidate alternatives for an expression.

Alternatives include the expression itself (standard convention). The exhaustification operator (exhB) determines which alternatives to exclude — the source just provides the candidates.

alternatives : Form → List Form
Candidate alternatives to x, including x itself.

Instances

source

def Alternatives.alternativeSourceOfScale {α : Type} (s : HornScale α) :

AlternativeSource α

Build an AlternativeSource from any HornScale.

Equations

Alternatives.alternativeSourceOfScale s = { alternatives := fun (x : α) => s.members }

Instances For

source

instance Alternatives.instAlternativeSourceQuantExpr :

AlternativeSource Quantifiers.QuantExpr

Quantifier alternatives: {none, some, most, all}.

Equations

Alternatives.instAlternativeSourceQuantExpr = { alternatives := fun (x : Alternatives.Quantifiers.QuantExpr) => Alternatives.Quantifiers.quantScale.members }

source

instance Alternatives.instAlternativeSourceConnExpr :

AlternativeSource Connectives.ConnExpr

Connective alternatives: {or, and}.

Equations

Alternatives.instAlternativeSourceConnExpr = { alternatives := fun (x : Alternatives.Connectives.ConnExpr) => Alternatives.Connectives.connScale.members }

source

instance Alternatives.instAlternativeSourceModalExpr :

AlternativeSource Modals.ModalExpr

Modal alternatives: {possible, necessary}.

Equations

Alternatives.instAlternativeSourceModalExpr = { alternatives := fun (x : Alternatives.Modals.ModalExpr) => Alternatives.Modals.modalScale.members }

source

instance Alternatives.instAlternativeSourceNumberExpr :

AlternativeSource Number.NumberExpr

Number alternatives: {plural, singular}.

Equations

Alternatives.instAlternativeSourceNumberExpr = { alternatives := fun (x : Alternatives.Number.NumberExpr) => Alternatives.Number.numberScale.members }

source

inductive Alternatives.ScaleMembership :

Type

Which Horn scale a closed-class expression belongs to, and where.

Numerals are excluded: under lower-bound semantics they form an infinite scale (not representable as a finite HornScale), and under bilateral semantics they don't form a scale at all.