inductive Semantics.Montague.Sentence.DomainWidening.AlternativeSource : Type

Where the alternatives for just come. Roothian alternatives are the standard focus-semantic alternatives; the other sources are what distinguish just from only.

• roothian : AlternativeSource
• granularity : AlternativeSource
• causal : AlternativeSource
• elaboration : AlternativeSource
• normative : AlternativeSource

instance Semantics.Montague.Sentence.DomainWidening.instReprAlternativeSource : Repr AlternativeSource

Equations

• Semantics.Montague.Sentence.DomainWidening.instReprAlternativeSource = { reprPrec := Semantics.Montague.Sentence.DomainWidening.instReprAlternativeSource.repr }

def Semantics.Montague.Sentence.DomainWidening.instReprAlternativeSource.repr : AlternativeSource → ℕ → Std.Format

Equations

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

instance Semantics.Montague.Sentence.DomainWidening.instDecidableEqAlternativeSource : DecidableEq AlternativeSource

Equations

• Semantics.Montague.Sentence.DomainWidening.instDecidableEqAlternativeSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Montague.Sentence.DomainWidening.instBEqAlternativeSource.beq : AlternativeSource → AlternativeSource → Bool

Equations

• Semantics.Montague.Sentence.DomainWidening.instBEqAlternativeSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Montague.Sentence.DomainWidening.instBEqAlternativeSource : BEq AlternativeSource

Equations

• Semantics.Montague.Sentence.DomainWidening.instBEqAlternativeSource = { beq := Semantics.Montague.Sentence.DomainWidening.instBEqAlternativeSource.beq }

def Semantics.Montague.Sentence.DomainWidening.associatedSource : Phenomena.Focus.Exclusives.JustFlavor → AlternativeSource

Map each flavor of just to its alternative source.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.complementExclusion = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.roothian
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.rankOrder = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.roothian
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.emphatic = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.granularity
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.precisifyingEquality = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.granularity
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.minimalSufficiency = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.causal
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.unexplanatory = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.causal
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.unelaboratory = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.elaboration
• Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.counterexpectational = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.normative

structure Semantics.Montague.Sentence.DomainWidening.DiscourseContext (W : Type u_1) : Type u_1

A discourse context provides construals of an underspecified question (UQ) together with Quality and Relevance filters.

W is the world/meaning type that questions partition over.

• construals : List (QUD W)

  The available construals of UQ_c

• quality : QUD W → Bool

  Does the speaker have sufficient evidence to answer this QUD?

• relevance : QUD W → Bool

  Is this QUD relevant to the current discourse?

• nonempty : self.construals ≠ []

  There must be at least one construal

def Semantics.Montague.Sentence.DomainWidening.answerable {W : Type u_1} (ctx : DiscourseContext W) (q : QUD W) : Bool

A QUD is answerable iff it passes both Quality and Relevance.

Equations

• Semantics.Montague.Sentence.DomainWidening.answerable ctx q = (ctx.quality q && ctx.relevance q)

def Semantics.Montague.Sentence.DomainWidening.strictlyWider {W : Type u_1} (q1 q2 : Questions.GSQuestion W) : Prop

q1 is strictly wider than q2 when q2 refines q1 but not vice versa. A wider question has a coarser partition — fewer distinctions.

Equations

• Semantics.Montague.Sentence.DomainWidening.strictlyWider q1 q2 = (QUD.refines q2 q1 ∧ ¬QUD.refines q1 q2)

def Semantics.Montague.Sentence.DomainWidening.isWidestAnswerable {W : Type u_1} (ctx : DiscourseContext W) (q : QUD W) : Prop

q is the widest answerable construal: it is answerable, it is in the construal set, and no strictly wider answerable construal exists.

Equations

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

def Semantics.Montague.Sentence.DomainWidening.classifyContext {W : Type u_1} (ctx : DiscourseContext W) (q : QUD W) : q ∈ ctx.construals → Phenomena.Focus.Exclusives.ContextType

Classify a discourse context by WHY the widest answerable construal is optimal. Connects to Phenomena.Focus.Exclusives.ContextType.

Equations

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

structure Semantics.Montague.Sentence.DomainWidening.JustSemantics (W : Type u_2) : Type u_2

The unified lexical entry for just (@cite{deo-thomas-2025}: §3).

Not-at-issue: The CQ is the widest answerable construal of UQ_c. At-issue: The prejacent, interpreted relative to CQ's granularity.

The 7 flavors are NOT separate entries — they are the same entry interacting with different discourse contexts and alternative sources.

• context : DiscourseContext W

  The underspecified question and its construals

• cq : QUD W

  The widest answerable construal (= the CQ for just)

• cq_widest : isWidestAnswerable self.context self.cq

  The CQ is indeed widest answerable

• prejacent : W → Bool

  The prejacent proposition

structure Semantics.Montague.Sentence.DomainWidening.OnlySemantics (W : Type u_2) : Type u_2

The lexical entry for only (standard Roothian analysis).

Unlike just, only requires the CQ to be commonly shared and alternatives to be Roothian (focus-semantic).

• cq : QUD W

  The shared CQ (must be commonly known)

• prejacent : W → Bool

  The prejacent

• alternatives : List (W → Bool)

  Roothian focus alternatives

• cqShared : Bool

  The CQ must be shared between interlocutors

def Semantics.Montague.Sentence.DomainWidening.OnlySemantics.assertion {W : Type u_1} (sem : OnlySemantics W) (w : W) : Bool

only presupposes the prejacent and asserts no stronger alternative is true.

Equations

• sem.assertion w = (sem.prejacent w && sem.alternatives.all fun (alt : W → Bool) => !alt w || alt w == sem.prejacent w)

theorem Semantics.Montague.Sentence.DomainWidening.only_substitutes_iff_roothian (d : Phenomena.Focus.Exclusives.JustDatum) : d ∈ Phenomena.Focus.Exclusives.allJustData → (d.onlyOk = true ↔ associatedSource d.flavor = AlternativeSource.roothian)

Only can replace just exactly when the alternatives are Roothian (complement-exclusion and rank-order). Verified against all empirical data.

theorem Semantics.Montague.Sentence.DomainWidening.quality_fail_implies_causal (d : Phenomena.Focus.Exclusives.JustDatum) : d ∈ Phenomena.Focus.Exclusives.allJustData → d.contextType = Phenomena.Focus.Exclusives.ContextType.qualityFail → associatedSource d.flavor = AlternativeSource.causal

Quality-failure contexts yield only causal-alternative flavors (unexplanatory, minimal sufficiency).

theorem Semantics.Montague.Sentence.DomainWidening.relevance_fail_implies_elaboration (d : Phenomena.Focus.Exclusives.JustDatum) : d ∈ Phenomena.Focus.Exclusives.allJustData → d.contextType = Phenomena.Focus.Exclusives.ContextType.relevanceFail → associatedSource d.flavor = AlternativeSource.elaboration

Relevance-failure contexts yield only elaboration-alternative flavors (unelaboratory).

theorem Semantics.Montague.Sentence.DomainWidening.only_requires_shared_cq (d : Phenomena.Focus.Exclusives.JustDatum) : d ∈ Phenomena.Focus.Exclusives.allJustData → d.onlyOk = true → associatedSource d.flavor = AlternativeSource.roothian

only is felicitous only with Roothian alternatives (shared CQ). just is felicitous regardless of alternative source. This is WHY they diverge: only exhaustifies over shared alternatives, just widens the question.

theorem Semantics.Montague.Sentence.DomainWidening.all_flavors_one_entry (d : Phenomena.Focus.Exclusives.JustDatum) : d ∈ Phenomena.Focus.Exclusives.allJustData → ∃ (src : AlternativeSource) (ct : Phenomena.Focus.Exclusives.ContextType), associatedSource d.flavor = src ∧ d.contextType = ct

The 7 flavors are not separate lexical entries. Every flavor in the data is compatible with the unified analysis: the associated source is always well-defined, and context type is always well-defined. No flavor requires a distinct lexical entry.