structure Implicature.AlternativeGeneration.SentenceFrame (m : Semantics.Montague.Model) : Type

A sentence frame for Det-N-VP sentences.

Captures the structure needed to:

1. Evaluate the sentence at any world (given world-indexed VP)
2. Generate alternatives by substituting the quantifier

• quant : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det

  The quantifier denotation (e.g., some_sem, every_sem)

• noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

  The noun denotation (e.g., isStudent)

• form : String

  Surface form of the quantifier (for display/lookup)

• scaleMembership : Option Semantics.Montague.ScaleMembership

  Which scale the quantifier belongs to

def Implicature.AlternativeGeneration.SentenceFrame.eval {m : Semantics.Montague.Model} (f : SentenceFrame m) (vp : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) : Bool

Evaluate a sentence frame with a specific VP.

For Det-N-VP: ⟦Det⟧(⟦N⟧)(⟦VP⟧)

Equations

• f.eval vp = f.quant f.noun vp

def Implicature.AlternativeGeneration.frameFromEntry {m : Semantics.Montague.Model} (entry : Semantics.Montague.SemLexEntry m) (noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (h : entry.ty = Semantics.Lexical.Determiner.Quantifier.Ty.det := by rfl) : SentenceFrame m

Create a frame from a lexical entry and noun denotation.

Equations

• Implicature.AlternativeGeneration.frameFromEntry entry noun h = { quant := h ▸ entry.denot, noun := noun, form := entry.form, scaleMembership := entry.scaleMembership }

def Implicature.AlternativeGeneration.alternativeFrames {m : Semantics.Montague.Model} (f : SentenceFrame m) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity) : List (SentenceFrame m)

Generate alternative frames by substituting stronger quantifiers.

For "some students VP":

• Looks up "some" → gets stronger alternatives ["most", "all"]
• For each alternative, creates a new frame with that quantifier

The context polarity determines whether we use stronger (UE) or weaker (DE) alternatives.

Equations

• One or more equations did not get rendered due to their size.
• Implicature.AlternativeGeneration.alternativeFrames f lex Core.NaturalLogic.ContextPolarity.downward = []
• Implicature.AlternativeGeneration.alternativeFrames f lex Core.NaturalLogic.ContextPolarity.nonMonotonic = []

def Implicature.AlternativeGeneration.allFrames {m : Semantics.Montague.Model} (f : SentenceFrame m) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity) : List (SentenceFrame m)

Get all frames (original + alternatives).

Equations

• Implicature.AlternativeGeneration.allFrames f lex ctx = f :: Implicature.AlternativeGeneration.alternativeFrames f lex ctx

@[reducible, inline]

abbrev Implicature.AlternativeGeneration.WorldIndexedVP (m : Semantics.Montague.Model) (World : Type) : Type

A world-indexed VP: for each world, gives the VP denotation.

Example: passedAt w returns which students passed at world w.

Equations

• Implicature.AlternativeGeneration.WorldIndexedVP m World = (World → m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t))

def Implicature.AlternativeGeneration.frameToProp {m : Semantics.Montague.Model} {World : Type} (f : SentenceFrame m) (vpAt : WorldIndexedVP m World) : Prop' World

Convert a sentence frame to Prop' World given a world-indexed VP.

For each world w: frameToProp f vpAt w = (f.quant f.noun (vpAt w)) = true

Equations

• Implicature.AlternativeGeneration.frameToProp f vpAt w = (f.eval (vpAt w) = true)

def Implicature.AlternativeGeneration.framesToProps {m : Semantics.Montague.Model} {World : Type} (frames : List (SentenceFrame m)) (vpAt : WorldIndexedVP m World) : List (Prop' World)

Convert all frames to propositions.

Equations

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

def Implicature.AlternativeGeneration.altSet {m : Semantics.Montague.Model} {World : Type} (f : SentenceFrame m) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Set (Prop' World)

Generate the ALT set from a sentence frame.

This is the main interface to exhaustivity operators.

Equations

• Implicature.AlternativeGeneration.altSet f vpAt lex ctx = {p : Prop' World | p ∈ Implicature.AlternativeGeneration.framesToProps (Implicature.AlternativeGeneration.allFrames f lex ctx) vpAt}

def Implicature.AlternativeGeneration.strictAltSet {m : Semantics.Montague.Model} {World : Type} (f : SentenceFrame m) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Set (Prop' World)

Generate ALT set without the base proposition (just alternatives).

Equations

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

def Implicature.AlternativeGeneration.exhMW_frame {m : Semantics.Montague.Model} {World : Type} (f : SentenceFrame m) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Prop' World

Apply exhMW to a sentence frame.

Equations

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

def Implicature.AlternativeGeneration.exhIE_frame {m : Semantics.Montague.Model} {World : Type} (f : SentenceFrame m) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Prop' World

Apply exhIE to a sentence frame.

Equations

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

def Implicature.AlternativeGeneration.frameFromDerivation {m : Semantics.Montague.Model} (d : Semantics.Montague.Derivation.SemDeriv m) (noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) : Option (SentenceFrame m)

Extract a sentence frame from a derivation's scalar item.

Requires:

• The derivation has exactly one scalar item (at position 0, the determiner)
• The scalar item is a quantifier
• The noun denotation is provided separately

Returns none if the derivation doesn't match the expected pattern.

Equations

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

def Implicature.AlternativeGeneration.altSetFromDerivation {m : Semantics.Montague.Model} {World : Type} (d : Semantics.Montague.Derivation.SemDeriv m) (noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Option (Set (Prop' World))

Generate ALT set directly from a derivation.

Combines frameFromDerivation and altSet.

Equations

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

def Implicature.AlternativeGeneration.exhMW_derivation {m : Semantics.Montague.Model} {World : Type} (d : Semantics.Montague.Derivation.SemDeriv m) (noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Option (Prop' World)

Apply exhMW directly to a derivation.

Equations

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

def Implicature.AlternativeGeneration.exhIE_derivation {m : Semantics.Montague.Model} {World : Type} (d : Semantics.Montague.Derivation.SemDeriv m) (noun : m.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (vpAt : WorldIndexedVP m World) (lex : Semantics.Montague.SemLexicon m) (ctx : Core.NaturalLogic.ContextPolarity := Core.NaturalLogic.ContextPolarity.upward) : Option (Prop' World)

Apply exhIE directly to a derivation.

Equations

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

inductive Implicature.AlternativeGeneration.Student : Type

Three students

• alice : Student
• bob : Student
• carol : Student

instance Implicature.AlternativeGeneration.instDecidableEqStudent : DecidableEq Student

Equations

• Implicature.AlternativeGeneration.instDecidableEqStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Implicature.AlternativeGeneration.instReprStudent : Repr Student

Equations

• Implicature.AlternativeGeneration.instReprStudent = { reprPrec := Implicature.AlternativeGeneration.instReprStudent.repr }

def Implicature.AlternativeGeneration.instReprStudent.repr : Student → ℕ → Std.Format

Equations

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

def Implicature.AlternativeGeneration.instBEqStudent.beq : Student → Student → Bool

Equations

• Implicature.AlternativeGeneration.instBEqStudent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.AlternativeGeneration.instBEqStudent : BEq Student

Equations

• Implicature.AlternativeGeneration.instBEqStudent = { beq := Implicature.AlternativeGeneration.instBEqStudent.beq }

def Implicature.AlternativeGeneration.studentModel : Semantics.Montague.Model

Student model

Equations

• Implicature.AlternativeGeneration.studentModel = { Entity := Implicature.AlternativeGeneration.Student, decEq := inferInstance }

instance Implicature.AlternativeGeneration.instFiniteModelStudentModel : Semantics.Lexical.Determiner.Quantifier.FiniteModel studentModel

Equations

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

def Implicature.AlternativeGeneration.isStudent : studentModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

All entities are students

Equations

• Implicature.AlternativeGeneration.isStudent x✝ = true

@[reducible, inline]

abbrev Implicature.AlternativeGeneration.PassWorld : Type

World = number of students who passed (0-3)

Equations

• Implicature.AlternativeGeneration.PassWorld = Fin 4

def Implicature.AlternativeGeneration.passedAt : WorldIndexedVP studentModel PassWorld

"passed" indexed by world

Equations

• Implicature.AlternativeGeneration.passedAt w s✝ = false
• Implicature.AlternativeGeneration.passedAt w Implicature.AlternativeGeneration.Student.alice = true
• Implicature.AlternativeGeneration.passedAt w s✝ = false
• Implicature.AlternativeGeneration.passedAt w Implicature.AlternativeGeneration.Student.alice = true
• Implicature.AlternativeGeneration.passedAt w Implicature.AlternativeGeneration.Student.bob = true
• Implicature.AlternativeGeneration.passedAt w Implicature.AlternativeGeneration.Student.carol = false
• Implicature.AlternativeGeneration.passedAt w s✝ = true
• Implicature.AlternativeGeneration.passedAt w s✝ = false

def Implicature.AlternativeGeneration.studentLexicon : Semantics.Montague.SemLexicon studentModel

Equations

• One or more equations did not get rendered due to their size.
• Implicature.AlternativeGeneration.studentLexicon form = none

def Implicature.AlternativeGeneration.someStudentsFrame : SentenceFrame studentModel

Frame for "some students passed"

Equations

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

def Implicature.AlternativeGeneration.allStudentsFrame : SentenceFrame studentModel

Frame for "all students passed"

Equations

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

def Implicature.AlternativeGeneration.somePassed : Prop' PassWorld

Equations

• Implicature.AlternativeGeneration.somePassed = Implicature.AlternativeGeneration.frameToProp Implicature.AlternativeGeneration.someStudentsFrame Implicature.AlternativeGeneration.passedAt

def Implicature.AlternativeGeneration.allPassed : Prop' PassWorld

Equations

• Implicature.AlternativeGeneration.allPassed = Implicature.AlternativeGeneration.frameToProp Implicature.AlternativeGeneration.allStudentsFrame Implicature.AlternativeGeneration.passedAt

def Implicature.AlternativeGeneration.w1 : PassWorld

Equations

• Implicature.AlternativeGeneration.w1 = ⟨1, Implicature.AlternativeGeneration.w1._proof_2⟩

def Implicature.AlternativeGeneration.w3 : PassWorld

Equations

• Implicature.AlternativeGeneration.w3 = ⟨3, Implicature.AlternativeGeneration.w3._proof_2⟩

theorem Implicature.AlternativeGeneration.somePassed_at_w1 : somePassed w1

somePassed holds at w1

theorem Implicature.AlternativeGeneration.allPassed_not_w1 : ¬allPassed w1

allPassed does NOT hold at w1

theorem Implicature.AlternativeGeneration.both_at_w3 : somePassed w3 ∧ allPassed w3

Both hold at w3

theorem Implicature.AlternativeGeneration.some_has_all_alternative : ((alternativeFrames someStudentsFrame studentLexicon Core.NaturalLogic.ContextPolarity.upward).any fun (f : SentenceFrame studentModel) => f.form == "all") = true

Alternative frames include "all" (via lookupAlternatives)

theorem Implicature.AlternativeGeneration.altSet_contains_base : somePassed ∈ altSet someStudentsFrame passedAt studentLexicon

The automatically generated ALT set contains somePassed.

def Implicature.AlternativeGeneration.exhSomePassed : Prop' PassWorld

The exhaustified "some students passed"

Equations

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

theorem Implicature.AlternativeGeneration.exh_some_at_w1 : exhSomePassed w1

Exhaustified "some" holds at w1 (automatic ALT).

This theorem shows that with automatically generated alternatives, exhMW correctly derives "some but not all" at w1.

The proof requires showing w1 is minimal: no world makes strictly fewer alternatives true while still satisfying "some passed".

Proof sketch:

• w1 makes true: {somePassed}
• w2 makes true: {somePassed, mostPassed}
• w3 makes true: {somePassed, mostPassed, allPassed}
• w0 makes true: {} (but doesn't satisfy somePassed)

So w1 is minimal among some-worlds, hence exhMW(some)(w1) holds.