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

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

def NeoGricean.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.
• NeoGricean.AlternativeGeneration.alternativeFrames f lex Core.NaturalLogic.ContextPolarity.downward = []
• NeoGricean.AlternativeGeneration.alternativeFrames f lex Core.NaturalLogic.ContextPolarity.nonMonotonic = []

def NeoGricean.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

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

@[reducible, inline]

abbrev NeoGricean.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

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

def NeoGricean.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

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

def NeoGricean.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 NeoGricean.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

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

def NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.AlternativeGeneration.Student : Type

Three students

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

instance NeoGricean.AlternativeGeneration.instDecidableEqStudent : DecidableEq Student

Equations

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

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

Equations

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

instance NeoGricean.AlternativeGeneration.instReprStudent : Repr Student

Equations

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

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

Equations

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

instance NeoGricean.AlternativeGeneration.instBEqStudent : BEq Student

Equations

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

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

Student model

Equations

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

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

Equations

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

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

All entities are students

Equations

• NeoGricean.AlternativeGeneration.isStudent x✝ = true

@[reducible, inline]

abbrev NeoGricean.AlternativeGeneration.PassWorld : Type

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

Equations

• NeoGricean.AlternativeGeneration.PassWorld = Fin 4

def NeoGricean.AlternativeGeneration.passedAt : WorldIndexedVP studentModel PassWorld

"passed" indexed by world

Equations

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

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

Equations

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

def NeoGricean.AlternativeGeneration.someStudentsFrame : SentenceFrame studentModel

Frame for "some students passed"

Equations

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

def NeoGricean.AlternativeGeneration.allStudentsFrame : SentenceFrame studentModel

Frame for "all students passed"

Equations

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

def NeoGricean.AlternativeGeneration.somePassed : Prop' PassWorld

Equations

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

def NeoGricean.AlternativeGeneration.allPassed : Prop' PassWorld

Equations

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

def NeoGricean.AlternativeGeneration.w1 : PassWorld

Equations

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

def NeoGricean.AlternativeGeneration.w3 : PassWorld

Equations

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

theorem NeoGricean.AlternativeGeneration.somePassed_at_w1 : somePassed w1

somePassed holds at w1

theorem NeoGricean.AlternativeGeneration.allPassed_not_w1 : ¬allPassed w1

allPassed does NOT hold at w1

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

Both hold at w3

theorem NeoGricean.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 NeoGricean.AlternativeGeneration.altSet_contains_base : somePassed ∈ altSet someStudentsFrame passedAt studentLexicon

The automatically generated ALT set contains somePassed.

def NeoGricean.AlternativeGeneration.exhSomePassed : Prop' PassWorld

The exhaustified "some students passed"

Equations

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

theorem NeoGricean.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.