structure Alternatives.HornScale (α : Type) : Type

Horn scale: list of expressions ordered by semantic strength.

• members : List α

  Members ordered from weakest to strongest.

def Alternatives.instReprHornScale.repr {α✝ : Type} [Repr α✝] : HornScale α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.instReprHornScale {α✝ : Type} [Repr α✝] : Repr (HornScale α✝)

Equations

• Alternatives.instReprHornScale = { reprPrec := Alternatives.instReprHornScale.repr }

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

Equations

• Alternatives.scalePosition s x = List.findIdx? (fun (x_1 : α) => x_1 == x) s.members

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

Equations

• Alternatives.isWeaker s x y = match Alternatives.scalePosition s x, Alternatives.scalePosition s y with | some px, some py => decide (px < py) | x, x_1 => false

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

Equations

• Alternatives.isStronger s x y = Alternatives.isWeaker s y x

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

Equations

• Alternatives.strongerAlternatives s x = match Alternatives.scalePosition s x with | some px => List.drop (px + 1) s.members | none => []

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

Equations

• Alternatives.weakerAlternatives s x = match Alternatives.scalePosition s x with | some px => List.take px s.members | none => []

inductive Alternatives.Quantifiers.QuantExpr : Type

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

@[implicit_reducible]

instance Alternatives.Quantifiers.instDecidableEqQuantExpr : DecidableEq QuantExpr

Equations

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

def Alternatives.Quantifiers.instReprQuantExpr.repr : QuantExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.Quantifiers.instReprQuantExpr : Repr QuantExpr

Equations

• Alternatives.Quantifiers.instReprQuantExpr = { reprPrec := Alternatives.Quantifiers.instReprQuantExpr.repr }

@[implicit_reducible]

instance Alternatives.Quantifiers.instInhabitedQuantExpr : Inhabited QuantExpr

Equations

• Alternatives.Quantifiers.instInhabitedQuantExpr = { default := Alternatives.Quantifiers.instInhabitedQuantExpr.default }

def Alternatives.Quantifiers.instInhabitedQuantExpr.default : QuantExpr

Equations

• Alternatives.Quantifiers.instInhabitedQuantExpr.default = Alternatives.Quantifiers.QuantExpr.none_

def Alternatives.Quantifiers.QuantExpr.ofString? : String → Option QuantExpr

Equations

• Alternatives.Quantifiers.QuantExpr.ofString? "none" = some Alternatives.Quantifiers.QuantExpr.none_
• Alternatives.Quantifiers.QuantExpr.ofString? "some" = some Alternatives.Quantifiers.QuantExpr.some_
• Alternatives.Quantifiers.QuantExpr.ofString? "most" = some Alternatives.Quantifiers.QuantExpr.most
• Alternatives.Quantifiers.QuantExpr.ofString? "all" = some Alternatives.Quantifiers.QuantExpr.all
• Alternatives.Quantifiers.QuantExpr.ofString? "every" = some Alternatives.Quantifiers.QuantExpr.all
• Alternatives.Quantifiers.QuantExpr.ofString? x✝ = none

def Alternatives.Quantifiers.QuantExpr.toString : QuantExpr → String

Equations

• Alternatives.Quantifiers.QuantExpr.none_.toString = "none"
• Alternatives.Quantifiers.QuantExpr.some_.toString = "some"
• Alternatives.Quantifiers.QuantExpr.most.toString = "most"
• Alternatives.Quantifiers.QuantExpr.all.toString = "all"

@[implicit_reducible]

instance Alternatives.Quantifiers.instToStringQuantExpr : ToString QuantExpr

Equations

• Alternatives.Quantifiers.instToStringQuantExpr = { toString := Alternatives.Quantifiers.QuantExpr.toString }

def Alternatives.Quantifiers.quantScale : HornScale QuantExpr

Equations

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

def Alternatives.Quantifiers.entails : QuantExpr → QuantExpr → Bool

Equations

• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.some_ = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.most = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.all Alternatives.Quantifiers.QuantExpr.all = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.most Alternatives.Quantifiers.QuantExpr.some_ = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.most Alternatives.Quantifiers.QuantExpr.most = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.some_ Alternatives.Quantifiers.QuantExpr.some_ = true
• Alternatives.Quantifiers.entails Alternatives.Quantifiers.QuantExpr.none_ Alternatives.Quantifiers.QuantExpr.none_ = true
• Alternatives.Quantifiers.entails x✝¹ x✝ = false

theorem Alternatives.Quantifiers.scale_matches_entailment : isStronger quantScale QuantExpr.all QuantExpr.most = true ∧ isStronger quantScale QuantExpr.most QuantExpr.some_ = true ∧ isStronger quantScale QuantExpr.all QuantExpr.some_ = true

theorem Alternatives.Quantifiers.some_has_stronger_alternatives : strongerAlternatives quantScale QuantExpr.some_ = [QuantExpr.most, QuantExpr.all]

structure Alternatives.Quantifiers.QuantWorld (maxN : ℕ) : Type

Quantifier world: domain of size maxN with count of entities satisfying property.

• count : Fin (maxN + 1)

  How many entities satisfy the predicate (0 to maxN).

@[implicit_reducible]

instance Alternatives.Quantifiers.instDecidableEqQuantWorld {maxN✝ : ℕ} : DecidableEq (QuantWorld maxN✝)

Equations

• Alternatives.Quantifiers.instDecidableEqQuantWorld = Alternatives.Quantifiers.instDecidableEqQuantWorld.decEq

def Alternatives.Quantifiers.instDecidableEqQuantWorld.decEq {maxN✝ : ℕ} (x✝ x✝¹ : QuantWorld maxN✝) : Decidable (x✝ = x✝¹)

Equations

• Alternatives.Quantifiers.instDecidableEqQuantWorld.decEq { count := a } { count := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Alternatives.Quantifiers.instReprQuantWorld {maxN✝ : ℕ} : Repr (QuantWorld maxN✝)

Equations

• Alternatives.Quantifiers.instReprQuantWorld = { reprPrec := Alternatives.Quantifiers.instReprQuantWorld.repr }

def Alternatives.Quantifiers.instReprQuantWorld.repr {maxN✝ : ℕ} : QuantWorld maxN✝ → ℕ → Std.Format

Equations

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

def Alternatives.Quantifiers.worldMeaning (maxN : ℕ) : QuantExpr → QuantWorld maxN → Bool

Intensional meaning: quantifier as function from worlds to truth values.

Equations

• Alternatives.Quantifiers.worldMeaning maxN Alternatives.Quantifiers.QuantExpr.none_ x✝ = (↑x✝.count == 0)
• Alternatives.Quantifiers.worldMeaning maxN Alternatives.Quantifiers.QuantExpr.some_ x✝ = decide (↑x✝.count ≥ 1)
• Alternatives.Quantifiers.worldMeaning maxN Alternatives.Quantifiers.QuantExpr.most x✝ = decide (↑x✝.count > maxN / 2)
• Alternatives.Quantifiers.worldMeaning maxN Alternatives.Quantifiers.QuantExpr.all x✝ = (↑x✝.count == maxN)

def Alternatives.Quantifiers.allWorlds (maxN : ℕ) : List (QuantWorld maxN)

Equations

• Alternatives.Quantifiers.allWorlds maxN = List.filterMap (fun (n : ℕ) => if h : n < maxN + 1 then some { count := ⟨n, h⟩ } else none) (List.range (maxN + 1))

def Alternatives.Quantifiers.w0 : QuantWorld 3

Equations

• Alternatives.Quantifiers.w0 = { count := ⟨0, Alternatives.Quantifiers.w0._proof_2⟩ }

def Alternatives.Quantifiers.w1 : QuantWorld 3

Equations

• Alternatives.Quantifiers.w1 = { count := ⟨1, Alternatives.Quantifiers.w1._proof_2⟩ }

def Alternatives.Quantifiers.w2 : QuantWorld 3

Equations

• Alternatives.Quantifiers.w2 = { count := ⟨2, Alternatives.Quantifiers.w2._proof_2⟩ }

def Alternatives.Quantifiers.w3 : QuantWorld 3

Equations

• Alternatives.Quantifiers.w3 = { count := ⟨3, Alternatives.Quantifiers.w3._proof_2⟩ }

theorem Alternatives.Quantifiers.entailment_preserved_all_some : (worldMeaning 3 QuantExpr.all w0 = true → worldMeaning 3 QuantExpr.some_ w0 = true) ∧ (worldMeaning 3 QuantExpr.all w1 = true → worldMeaning 3 QuantExpr.some_ w1 = true) ∧ (worldMeaning 3 QuantExpr.all w2 = true → worldMeaning 3 QuantExpr.some_ w2 = true) ∧ (worldMeaning 3 QuantExpr.all w3 = true → worldMeaning 3 QuantExpr.some_ w3 = true)

theorem Alternatives.Quantifiers.some_lower_bounded : worldMeaning 3 QuantExpr.some_ w0 = false ∧ worldMeaning 3 QuantExpr.some_ w1 = true ∧ worldMeaning 3 QuantExpr.some_ w2 = true ∧ worldMeaning 3 QuantExpr.some_ w3 = true

theorem Alternatives.Quantifiers.some_compatible_with_all : worldMeaning 3 QuantExpr.some_ w3 = true

inductive Alternatives.Connectives.ConnExpr : Type

• or_ : ConnExpr
• and_ : ConnExpr

@[implicit_reducible]

instance Alternatives.Connectives.instDecidableEqConnExpr : DecidableEq ConnExpr

Equations

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

@[implicit_reducible]

instance Alternatives.Connectives.instReprConnExpr : Repr ConnExpr

Equations

• Alternatives.Connectives.instReprConnExpr = { reprPrec := Alternatives.Connectives.instReprConnExpr.repr }

def Alternatives.Connectives.instReprConnExpr.repr : ConnExpr → ℕ → Std.Format

Equations

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

def Alternatives.Connectives.instInhabitedConnExpr.default : ConnExpr

Equations

• Alternatives.Connectives.instInhabitedConnExpr.default = Alternatives.Connectives.ConnExpr.or_

@[implicit_reducible]

instance Alternatives.Connectives.instInhabitedConnExpr : Inhabited ConnExpr

Equations

• Alternatives.Connectives.instInhabitedConnExpr = { default := Alternatives.Connectives.instInhabitedConnExpr.default }

def Alternatives.Connectives.ConnExpr.ofString? : String → Option ConnExpr

Equations

• Alternatives.Connectives.ConnExpr.ofString? "or" = some Alternatives.Connectives.ConnExpr.or_
• Alternatives.Connectives.ConnExpr.ofString? "and" = some Alternatives.Connectives.ConnExpr.and_
• Alternatives.Connectives.ConnExpr.ofString? x✝ = none

def Alternatives.Connectives.ConnExpr.toString : ConnExpr → String

Equations

• Alternatives.Connectives.ConnExpr.or_.toString = "or"
• Alternatives.Connectives.ConnExpr.and_.toString = "and"

@[implicit_reducible]

instance Alternatives.Connectives.instToStringConnExpr : ToString ConnExpr

Equations

• Alternatives.Connectives.instToStringConnExpr = { toString := Alternatives.Connectives.ConnExpr.toString }

def Alternatives.Connectives.connScale : HornScale ConnExpr

Equations

• Alternatives.Connectives.connScale = { members := [Alternatives.Connectives.ConnExpr.or_, Alternatives.Connectives.ConnExpr.and_] }

def Alternatives.Connectives.entails : ConnExpr → ConnExpr → Bool

Equations

• Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.and_ Alternatives.Connectives.ConnExpr.or_ = true
• Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.and_ Alternatives.Connectives.ConnExpr.and_ = true
• Alternatives.Connectives.entails Alternatives.Connectives.ConnExpr.or_ Alternatives.Connectives.ConnExpr.or_ = true
• Alternatives.Connectives.entails x✝¹ x✝ = false

theorem Alternatives.Connectives.and_stronger_than_or : isStronger connScale ConnExpr.and_ ConnExpr.or_ = true ∧ isStronger connScale ConnExpr.or_ ConnExpr.and_ = false

theorem Alternatives.Connectives.or_alternative : strongerAlternatives connScale ConnExpr.or_ = [ConnExpr.and_]

inductive Alternatives.Modals.ModalExpr : Type

• possible : ModalExpr
• necessary : ModalExpr

@[implicit_reducible]

instance Alternatives.Modals.instDecidableEqModalExpr : DecidableEq ModalExpr

Equations

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

@[implicit_reducible]

instance Alternatives.Modals.instReprModalExpr : Repr ModalExpr

Equations

• Alternatives.Modals.instReprModalExpr = { reprPrec := Alternatives.Modals.instReprModalExpr.repr }

def Alternatives.Modals.instReprModalExpr.repr : ModalExpr → ℕ → Std.Format

Equations

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

def Alternatives.Modals.instInhabitedModalExpr.default : ModalExpr

Equations

• Alternatives.Modals.instInhabitedModalExpr.default = Alternatives.Modals.ModalExpr.possible

@[implicit_reducible]

instance Alternatives.Modals.instInhabitedModalExpr : Inhabited ModalExpr

Equations

• Alternatives.Modals.instInhabitedModalExpr = { default := Alternatives.Modals.instInhabitedModalExpr.default }

def Alternatives.Modals.ModalExpr.ofString? : String → Option ModalExpr

Equations

• Alternatives.Modals.ModalExpr.ofString? "possible" = some Alternatives.Modals.ModalExpr.possible
• Alternatives.Modals.ModalExpr.ofString? "might" = some Alternatives.Modals.ModalExpr.possible
• Alternatives.Modals.ModalExpr.ofString? "may" = some Alternatives.Modals.ModalExpr.possible
• Alternatives.Modals.ModalExpr.ofString? "necessary" = some Alternatives.Modals.ModalExpr.necessary
• Alternatives.Modals.ModalExpr.ofString? "must" = some Alternatives.Modals.ModalExpr.necessary
• Alternatives.Modals.ModalExpr.ofString? x✝ = none

def Alternatives.Modals.ModalExpr.toString : ModalExpr → String

Equations

• Alternatives.Modals.ModalExpr.possible.toString = "possible"
• Alternatives.Modals.ModalExpr.necessary.toString = "necessary"

@[implicit_reducible]

instance Alternatives.Modals.instToStringModalExpr : ToString ModalExpr

Equations

• Alternatives.Modals.instToStringModalExpr = { toString := Alternatives.Modals.ModalExpr.toString }

def Alternatives.Modals.modalScale : HornScale ModalExpr

Equations

• Alternatives.Modals.modalScale = { members := [Alternatives.Modals.ModalExpr.possible, Alternatives.Modals.ModalExpr.necessary] }

def Alternatives.Modals.entails : ModalExpr → ModalExpr → Bool

Equations

• Alternatives.Modals.entails Alternatives.Modals.ModalExpr.necessary Alternatives.Modals.ModalExpr.possible = true
• Alternatives.Modals.entails Alternatives.Modals.ModalExpr.necessary Alternatives.Modals.ModalExpr.necessary = true
• Alternatives.Modals.entails Alternatives.Modals.ModalExpr.possible Alternatives.Modals.ModalExpr.possible = true
• Alternatives.Modals.entails x✝¹ x✝ = false

theorem Alternatives.Modals.necessary_stronger_than_possible : isStronger modalScale ModalExpr.necessary ModalExpr.possible = true

Numerals and Horn Scales

@cite{horn-1972} @cite{kennedy-2015}

Numerals are NOT represented as a HornScale here because:

1. 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).

2. 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 in Theories/Semantics/Numerals/Basic.lean:

• The five Prop meaning functions (bareMeaning, atLeastMeaning, ...) expose theory disagreement directly via the choice of bare-numeral semantics
• kennedyAlternatives (a single list of NumeralExpr) is Kennedy's anti-Horn-scale alternative set; Class A vs Class B emerges from asymmetric entailment, not from a pre-split sublist
• bare_not_upward_monotone / bare_not_downward_monotone / atLeast_strictly_weaker_than_bare 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).

inductive Alternatives.Number.NumberExpr : Type

• singular : NumberExpr
• plural : NumberExpr

@[implicit_reducible]

instance Alternatives.Number.instDecidableEqNumberExpr : DecidableEq NumberExpr

Equations

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

@[implicit_reducible]

instance Alternatives.Number.instReprNumberExpr : Repr NumberExpr

Equations

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

def Alternatives.Number.instReprNumberExpr.repr : NumberExpr → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.Number.instInhabitedNumberExpr : Inhabited NumberExpr

Equations

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

def Alternatives.Number.instInhabitedNumberExpr.default : NumberExpr

Equations

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

def Alternatives.Number.NumberExpr.toString : NumberExpr → String

Equations

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

@[implicit_reducible]

instance Alternatives.Number.instToStringNumberExpr : ToString NumberExpr

Equations

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

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

theorem Alternatives.Number.singular_stronger_than_plural : isStronger numberScale NumberExpr.singular NumberExpr.plural = true

theorem Alternatives.Number.plural_alternative : strongerAlternatives numberScale NumberExpr.plural = [NumberExpr.singular]

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

Equations

• Alternatives.scalarImplicatures s x = Alternatives.strongerAlternatives s x

inductive Alternatives.Monotonicity : Type

• upward : Monotonicity
• downward : Monotonicity

@[implicit_reducible]

instance Alternatives.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

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

def Alternatives.instReprMonotonicity.repr : Monotonicity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.instReprMonotonicity : Repr Monotonicity

Equations

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

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

Equations

• Alternatives.scalarAlternativesInContext s x Alternatives.Monotonicity.upward = Alternatives.strongerAlternatives s x
• Alternatives.scalarAlternativesInContext s x Alternatives.Monotonicity.downward = Alternatives.weakerAlternatives s x

theorem Alternatives.de_reversal_some : scalarAlternativesInContext Quantifiers.quantScale Quantifiers.QuantExpr.some_ Monotonicity.upward = [Quantifiers.QuantExpr.most, Quantifiers.QuantExpr.all] ∧ scalarAlternativesInContext Quantifiers.quantScale Quantifiers.QuantExpr.some_ Monotonicity.downward = [Quantifiers.QuantExpr.none_]

theorem Alternatives.de_blocks_some_not_all : scalarAlternativesInContext Quantifiers.quantScale Quantifiers.QuantExpr.all Monotonicity.downward = [Quantifiers.QuantExpr.none_, Quantifiers.QuantExpr.some_, Quantifiers.QuantExpr.most]

def Alternatives.Polarity.toMonotonicity : Features.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

• Alternatives.Polarity.toMonotonicity Features.Polarity.positive = Alternatives.Monotonicity.upward
• Alternatives.Polarity.toMonotonicity Features.Polarity.negative = Alternatives.Monotonicity.downward

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)

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}

@[reducible, inline]

abbrev Alternatives.SemQuantWorld : Type

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

Equations

• Alternatives.SemQuantWorld = Fin 4

def Alternatives.someQ : SemQuantWorld → Prop

"Some Ps are Q" = at least one.

Equations

• Alternatives.someQ w = (↑w ≥ 1)

def Alternatives.allQ : SemQuantWorld → Prop

"All Ps are Q" = all three.

Equations

• Alternatives.allQ w = (↑w = 3)

theorem Alternatives.all_entails_some (w : SemQuantWorld) : allQ w → someQ w

All entails some.

theorem Alternatives.some_not_entails_all : ¬∀ (w : SemQuantWorld), someQ w → allQ w

Some does not entail all.

def Alternatives.someAllScale : SemanticScale SemQuantWorld

The some/all semantic scale.

Equations

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

inductive Alternatives.ConnWorld : Type

Worlds for connective scale.

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

@[implicit_reducible]

instance Alternatives.instDecidableEqConnWorld : DecidableEq ConnWorld

Equations

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

@[implicit_reducible]

instance Alternatives.instReprConnWorld : Repr ConnWorld

Equations

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

def Alternatives.instReprConnWorld.repr : ConnWorld → ℕ → Std.Format

Equations

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

def Alternatives.orConn : ConnWorld → Prop

"A or B" (inclusive).

Equations

• Alternatives.orConn Alternatives.ConnWorld.neither = False
• Alternatives.orConn Alternatives.ConnWorld.onlyA = True
• Alternatives.orConn Alternatives.ConnWorld.onlyB = True
• Alternatives.orConn Alternatives.ConnWorld.both = True

def Alternatives.andConn : ConnWorld → Prop

"A and B".

Equations

• Alternatives.andConn Alternatives.ConnWorld.neither = False
• Alternatives.andConn Alternatives.ConnWorld.onlyA = False
• Alternatives.andConn Alternatives.ConnWorld.onlyB = False
• Alternatives.andConn Alternatives.ConnWorld.both = True

theorem Alternatives.and_entails_or (w : ConnWorld) : andConn w → orConn w

And entails or.

theorem Alternatives.or_not_entails_and : ¬∀ (w : ConnWorld), orConn w → andConn w

Or does not entail and.

def Alternatives.orAndScale : SemanticScale ConnWorld

The or/and semantic scale.

Equations

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

inductive Alternatives.ModalWorld : Type

Worlds for modal scale: accessibility relation outcomes.

• none : ModalWorld
• some : ModalWorld
• all : ModalWorld

@[implicit_reducible]

instance Alternatives.instDecidableEqModalWorld : DecidableEq ModalWorld

Equations

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

def Alternatives.instReprModalWorld.repr : ModalWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.instReprModalWorld : Repr ModalWorld

Equations

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

def Alternatives.possibleP : ModalWorld → Prop

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

Equations

• Alternatives.possibleP Alternatives.ModalWorld.none = False
• Alternatives.possibleP Alternatives.ModalWorld.some = True
• Alternatives.possibleP Alternatives.ModalWorld.all = True

def Alternatives.necessaryP : ModalWorld → Prop

"Necessarily P" = all accessible worlds have P.

Equations

• Alternatives.necessaryP Alternatives.ModalWorld.none = False
• Alternatives.necessaryP Alternatives.ModalWorld.some = False
• Alternatives.necessaryP Alternatives.ModalWorld.all = True

theorem Alternatives.necessary_entails_possible (w : ModalWorld) : necessaryP w → possibleP w

Necessary entails possible.

theorem Alternatives.possible_not_entails_necessary : ¬∀ (w : ModalWorld), possibleP w → necessaryP w

Possible does not entail necessary.

def Alternatives.possibleNecessaryScale : SemanticScale ModalWorld

The possible/necessary semantic scale.

Equations

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

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.

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

Build an AlternativeSource from any HornScale.

Equations

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

@[implicit_reducible]

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 }

@[implicit_reducible]

instance Alternatives.instAlternativeSourceConnExpr : AlternativeSource Connectives.ConnExpr

Connective alternatives: {or, and}.

Equations

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

@[implicit_reducible]

instance Alternatives.instAlternativeSourceModalExpr : AlternativeSource Modals.ModalExpr

Modal alternatives: {possible, necessary}.

Equations

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

@[implicit_reducible]

instance Alternatives.instAlternativeSourceNumberExpr : AlternativeSource Number.NumberExpr

Number alternatives: {plural, singular}.

Equations

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

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.

• quantifier (pos : Quantifiers.QuantExpr) : ScaleMembership
• connective (pos : Connectives.ConnExpr) : ScaleMembership
• modal (pos : Modals.ModalExpr) : ScaleMembership

def Alternatives.instDecidableEqScaleMembership.decEq (x✝ x✝¹ : ScaleMembership) : Decidable (x✝ = x✝¹)

Equations

• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.quantifier a) (Alternatives.ScaleMembership.quantifier b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.quantifier pos) (Alternatives.ScaleMembership.connective pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.quantifier pos) (Alternatives.ScaleMembership.modal pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.connective pos) (Alternatives.ScaleMembership.quantifier pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.connective a) (Alternatives.ScaleMembership.connective b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.connective pos) (Alternatives.ScaleMembership.modal pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.modal pos) (Alternatives.ScaleMembership.quantifier pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.modal pos) (Alternatives.ScaleMembership.connective pos_1) = isFalse ⋯
• Alternatives.instDecidableEqScaleMembership.decEq (Alternatives.ScaleMembership.modal a) (Alternatives.ScaleMembership.modal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Alternatives.instDecidableEqScaleMembership : DecidableEq ScaleMembership

Equations

• Alternatives.instDecidableEqScaleMembership = Alternatives.instDecidableEqScaleMembership.decEq

def Alternatives.instReprScaleMembership.repr : ScaleMembership → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alternatives.instReprScaleMembership : Repr ScaleMembership

Equations

• Alternatives.instReprScaleMembership = { reprPrec := Alternatives.instReprScaleMembership.repr }

def Alternatives.scaleOf : String → Option ScaleMembership

Look up the scale position of a word form.

Equations

• Alternatives.scaleOf "some" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.some_)
• Alternatives.scaleOf "every" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.all)
• Alternatives.scaleOf "all" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.all)
• Alternatives.scaleOf "most" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.most)
• Alternatives.scaleOf "no" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.none_)
• Alternatives.scaleOf "none" = some (Alternatives.ScaleMembership.quantifier Alternatives.Quantifiers.QuantExpr.none_)
• Alternatives.scaleOf "or" = some (Alternatives.ScaleMembership.connective Alternatives.Connectives.ConnExpr.or_)
• Alternatives.scaleOf "and" = some (Alternatives.ScaleMembership.connective Alternatives.Connectives.ConnExpr.and_)
• Alternatives.scaleOf "might" = some (Alternatives.ScaleMembership.modal Alternatives.Modals.ModalExpr.possible)
• Alternatives.scaleOf "may" = some (Alternatives.ScaleMembership.modal Alternatives.Modals.ModalExpr.possible)
• Alternatives.scaleOf "possible" = some (Alternatives.ScaleMembership.modal Alternatives.Modals.ModalExpr.possible)
• Alternatives.scaleOf "must" = some (Alternatives.ScaleMembership.modal Alternatives.Modals.ModalExpr.necessary)
• Alternatives.scaleOf "necessary" = some (Alternatives.ScaleMembership.modal Alternatives.Modals.ModalExpr.necessary)
• Alternatives.scaleOf x✝ = none

def Alternatives.strongerAlternativeForms (sm : ScaleMembership) : List String

The stronger alternatives of a scale position, as surface forms.

Equations

• Alternatives.strongerAlternativeForms (Alternatives.ScaleMembership.quantifier a) = List.map toString (Alternatives.strongerAlternatives Alternatives.Quantifiers.quantScale a)
• Alternatives.strongerAlternativeForms (Alternatives.ScaleMembership.connective a) = List.map toString (Alternatives.strongerAlternatives Alternatives.Connectives.connScale a)
• Alternatives.strongerAlternativeForms (Alternatives.ScaleMembership.modal a) = List.map toString (Alternatives.strongerAlternatives Alternatives.Modals.modalScale a)