inductive Phenomena.Focus.Exclusives.JustFlavor : Type

The interpretive flavors of just (@cite{deo-thomas-2025}: §2). Nine constructors covering the paper's 7 major categories, with precisifying split into equality/proximity (§2.3.1-2) and complement exclusion separated from rank order (§2.1).

• complementExclusion : JustFlavor
• rankOrder : JustFlavor
• emphatic : JustFlavor
• precisifyingEquality : JustFlavor
• precisifyingProximity : JustFlavor
• minimalSufficiency : JustFlavor
• unexplanatory : JustFlavor
• unelaboratory : JustFlavor
• counterexpectational : JustFlavor

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instReprJustFlavor : Repr JustFlavor

Equations

• Phenomena.Focus.Exclusives.instReprJustFlavor = { reprPrec := Phenomena.Focus.Exclusives.instReprJustFlavor.repr }

def Phenomena.Focus.Exclusives.instReprJustFlavor.repr : JustFlavor → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instDecidableEqJustFlavor : DecidableEq JustFlavor

Equations

• Phenomena.Focus.Exclusives.instDecidableEqJustFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Focus.Exclusives.ContextType : Type

Why the widest answerable construal is optimal at context. Corresponds to @cite{deo-thomas-2025}).

• answerable : ContextType
• qualityFail : ContextType
• relevanceFail : ContextType

def Phenomena.Focus.Exclusives.instReprContextType.repr : ContextType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instReprContextType : Repr ContextType

Equations

• Phenomena.Focus.Exclusives.instReprContextType = { reprPrec := Phenomena.Focus.Exclusives.instReprContextType.repr }

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instDecidableEqContextType : DecidableEq ContextType

Equations

• Phenomena.Focus.Exclusives.instDecidableEqContextType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Focus.Exclusives.JustDatum : Type

Datum for a just example with flavor classification.

• sentence : String
• flavor : JustFlavor
• onlyOk : Bool

  Can only be felicitously substituted?

• contextType : ContextType

  Which context type from (37)

• qud : String

  The relevant QUD / underspecified question

• inference : String

  The inference triggered

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instReprJustDatum : Repr JustDatum

Equations

• Phenomena.Focus.Exclusives.instReprJustDatum = { reprPrec := Phenomena.Focus.Exclusives.instReprJustDatum.repr }

def Phenomena.Focus.Exclusives.instReprJustDatum.repr : JustDatum → Nat → Std.Format

Equations

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

def Phenomena.Focus.Exclusives.complementExclusion_vacation : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.rankOrder_intern : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.emphatic_amazing : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.emphatic_enormous : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.precisifying_eq_full : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.precisifying_prox_older : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.precisifying_temporal : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.minSuff_cat : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.minSuff_gpa : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.unexplanatory_lamp : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.unexplanatory_mangoes : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.unelaboratory_dog : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.unelaboratory_proton : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.unelaboratory_mad : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.counterexp_texting : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.counterexp_wafer : JustDatum

Equations

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

def Phenomena.Focus.Exclusives.allJustData : List JustDatum

All just examples from the paper.

Equations

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

theorem Phenomena.Focus.Exclusives.only_substitutes_iff_exclusive : complementExclusion_vacation.onlyOk = true ∧ rankOrder_intern.onlyOk = true ∧ emphatic_amazing.onlyOk = false ∧ precisifying_eq_full.onlyOk = false ∧ minSuff_cat.onlyOk = false ∧ unexplanatory_lamp.onlyOk = false ∧ unelaboratory_dog.onlyOk = false ∧ counterexp_texting.onlyOk = false

Only can substitute for just only in complement-exclusion and rank-order uses.

theorem Phenomena.Focus.Exclusives.unexplanatory_is_quality_fail : unexplanatory_lamp.contextType = ContextType.qualityFail ∧ unexplanatory_mangoes.contextType = ContextType.qualityFail

Unexplanatory uses arise when wider construals fail Quality.

theorem Phenomena.Focus.Exclusives.unelaboratory_is_relevance_fail : unelaboratory_dog.contextType = ContextType.relevanceFail ∧ unelaboratory_proton.contextType = ContextType.relevanceFail

Unelaboratory uses arise when wider construals fail Relevance.

theorem Phenomena.Focus.Exclusives.standard_uses_are_answerable : complementExclusion_vacation.contextType = ContextType.answerable ∧ rankOrder_intern.contextType = ContextType.answerable ∧ emphatic_amazing.contextType = ContextType.answerable ∧ precisifying_eq_full.contextType = ContextType.answerable ∧ counterexp_texting.contextType = ContextType.answerable

The complement-exclusion, rank-order, emphatic, precisifying, and counterexpectational uses all arise when the widest construal IS answerable.

structure Phenomena.Focus.Exclusives.EmphatiConstraint : Type

Emphatic just requires extreme adjectives. With non-extreme adjectives, just gets complement-exclusion instead.

"The food was just amazing" → emphatic (amazing is extreme) "The soup was just tasty" → complement-exclusion (tasty is NOT extreme) i.e. "The soup was no more than tasty"

• sentence : String
• adjIsExtreme : Bool
• reading : JustFlavor

def Phenomena.Focus.Exclusives.instReprEmphatiConstraint.repr : EmphatiConstraint → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instReprEmphatiConstraint : Repr EmphatiConstraint

Equations

• Phenomena.Focus.Exclusives.instReprEmphatiConstraint = { reprPrec := Phenomena.Focus.Exclusives.instReprEmphatiConstraint.repr }

def Phenomena.Focus.Exclusives.emphatic_extreme : EmphatiConstraint

Equations

• Phenomena.Focus.Exclusives.emphatic_extreme = { sentence := "The food was just amazing", adjIsExtreme := true, reading := Phenomena.Focus.Exclusives.JustFlavor.emphatic }

def Phenomena.Focus.Exclusives.nonextreme_gets_exclusion : EmphatiConstraint

Equations

• Phenomena.Focus.Exclusives.nonextreme_gets_exclusion = { sentence := "The soup was just tasty", adjIsExtreme := false, reading := Phenomena.Focus.Exclusives.JustFlavor.complementExclusion }

structure Phenomena.Focus.Exclusives.ImprecisionTest : Type

Extreme adjectives never combine with imprecision markers. This is why emphatic just ≠ precisifying just.

• sentence : String
• felicitous : Bool

@[implicit_reducible]

instance Phenomena.Focus.Exclusives.instReprImprecisionTest : Repr ImprecisionTest

Equations

• Phenomena.Focus.Exclusives.instReprImprecisionTest = { reprPrec := Phenomena.Focus.Exclusives.instReprImprecisionTest.repr }

def Phenomena.Focus.Exclusives.instReprImprecisionTest.repr : ImprecisionTest → Nat → Std.Format

Equations

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

def Phenomena.Focus.Exclusives.extreme_no_roughly : ImprecisionTest

Equations

• Phenomena.Focus.Exclusives.extreme_no_roughly = { sentence := "#Roughly speaking, this soup is amazing", felicitous := false }

def Phenomena.Focus.Exclusives.maxstd_roughly_ok : ImprecisionTest

Equations

• Phenomena.Focus.Exclusives.maxstd_roughly_ok = { sentence := "Roughly speaking, this tank is full", felicitous := true }

def Phenomena.Focus.Exclusives.no_emphatic_objective_closed : ImprecisionTest

Emphatic reading blocked when endpoint is objective.

Equations

• Phenomena.Focus.Exclusives.no_emphatic_objective_closed = { sentence := "#The door is just [closed]F!", felicitous := false }

def Phenomena.Focus.Exclusives.no_emphatic_objective_full : ImprecisionTest

Equations

• Phenomena.Focus.Exclusives.no_emphatic_objective_full = { sentence := "#The tank is just [full]F!", felicitous := false }