inductive Exhaustification.Interface.ExhPosition : Type

Positions where EXH can occur in a doubly-quantified sentence.

• M : ExhPosition
• O : ExhPosition
• I : ExhPosition

instance Exhaustification.Interface.instDecidableEqExhPosition : DecidableEq ExhPosition

Equations

• Exhaustification.Interface.instDecidableEqExhPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Exhaustification.Interface.instReprExhPosition.repr : ExhPosition → ℕ → Std.Format

Equations

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

instance Exhaustification.Interface.instReprExhPosition : Repr ExhPosition

Equations

• Exhaustification.Interface.instReprExhPosition = { reprPrec := Exhaustification.Interface.instReprExhPosition.repr }

instance Exhaustification.Interface.instBEqExhPosition : BEq ExhPosition

Equations

• Exhaustification.Interface.instBEqExhPosition = { beq := Exhaustification.Interface.instBEqExhPosition.beq }

def Exhaustification.Interface.instBEqExhPosition.beq : ExhPosition → ExhPosition → Bool

Equations

• Exhaustification.Interface.instBEqExhPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Exhaustification.Interface.instHashableExhPosition : Hashable ExhPosition

Equations

• Exhaustification.Interface.instHashableExhPosition = { hash := Exhaustification.Interface.instHashableExhPosition.hash }

def Exhaustification.Interface.instHashableExhPosition.hash : ExhPosition → UInt64

Equations

• Exhaustification.Interface.instHashableExhPosition.hash Exhaustification.Interface.ExhPosition.M = 0
• Exhaustification.Interface.instHashableExhPosition.hash Exhaustification.Interface.ExhPosition.O = 1
• Exhaustification.Interface.instHashableExhPosition.hash Exhaustification.Interface.ExhPosition.I = 2

def Exhaustification.Interface.parseFromExhPositions (positions : List ExhPosition) : Core.Parse

Convert EXH positions to a parse

Equations

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

def Exhaustification.Interface.exhParses : List Core.Parse

All 8 EXH parses for doubly-quantified sentences

Equations

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

def Exhaustification.Interface.parseHasExhAt (p : Core.Parse) (pos : ExhPosition) : Bool

Check if a parse includes a specific EXH position

Equations

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

theorem Exhaustification.Interface.exh_parses_count : exhParses.length = 8

inductive Exhaustification.Interface.ExhOperator : Type

Different exhaustification strategies from the literature.

• IE: Innocent Exclusion Excludes alternatives that can be consistently excluded in ALL maximal ways.

• MW: Maximal Worlds / Minimal Models Keeps only minimal worlds relative to the alternative ordering.

Theorem 9: When ALT is closed under ∧, exhIE = exhMW.

• IE : ExhOperator
• MW : ExhOperator

instance Exhaustification.Interface.instDecidableEqExhOperator : DecidableEq ExhOperator

Equations

• Exhaustification.Interface.instDecidableEqExhOperator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Exhaustification.Interface.instReprExhOperator : Repr ExhOperator

Equations

• Exhaustification.Interface.instReprExhOperator = { reprPrec := Exhaustification.Interface.instReprExhOperator.repr }

def Exhaustification.Interface.instReprExhOperator.repr : ExhOperator → ℕ → Std.Format

Equations

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

instance Exhaustification.Interface.instBEqExhOperator : BEq ExhOperator

Equations

• Exhaustification.Interface.instBEqExhOperator = { beq := Exhaustification.Interface.instBEqExhOperator.beq }

def Exhaustification.Interface.instBEqExhOperator.beq : ExhOperator → ExhOperator → Bool

Equations

• Exhaustification.Interface.instBEqExhOperator.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Exhaustification.Interface.applyExh {World : Type u_1} (op : ExhOperator) (ALT : Set (Prop' World)) (φ : Prop' World) : Prop' World

Apply an exhaustification operator to a proposition given alternatives.

This is the single entry point for applying EXH to a proposition. All theories should use this rather than calling exhIE/exhMW directly.

Equations

• Exhaustification.Interface.applyExh Exhaustification.Interface.ExhOperator.IE ALT φ = Exhaustification.exhIE ALT φ
• Exhaustification.Interface.applyExh Exhaustification.Interface.ExhOperator.MW ALT φ = Exhaustification.exhMW ALT φ

theorem Exhaustification.Interface.ie_eq_mw_when_closed {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (hclosed : closedUnderConj ALT) : applyExh ExhOperator.IE ALT φ = applyExh ExhOperator.MW ALT φ

When ALT is closed under conjunction, both operators agree. This is Theorem 9 from @cite{spector-2016}.

@[reducible, inline]

abbrev Exhaustification.Interface.AlternativesAtPosition (World : Type u_1) : Type u_1

Alternatives can vary by EXH position.

For "Q₁ Xs V'd Q₂ Ys":

• Position M (matrix): alternatives to the whole sentence
• Position O (outer): alternatives to Q₁
• Position I (inner): alternatives to Q₂

Each position may have different scalar alternatives.

Equations

• Exhaustification.Interface.AlternativesAtPosition World = (Exhaustification.Interface.ExhPosition → Set (Prop' World))

def Exhaustification.Interface.applyExhAtParse {World : Type u_1} (op : ExhOperator) (p : Core.Parse) (base : Prop' World) (altsAt : AlternativesAtPosition World) : Prop' World

Apply EXH at positions indicated by a Parse.

This is the single entry point for parse-guided exhaustification.

Given:

• op: Which EXH operator to use (IE or MW)
• p: A parse indicating EXH positions (e.g., "MOI" means EXH at M, O, and I)
• base: The literal meaning (no EXH)
• altsAt: Alternatives at each position

Returns: The meaning after applying EXH at all indicated positions.

Application order: I → O → M (innermost first, standard scope convention).

Equations

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

theorem Exhaustification.Interface.literal_parse_is_identity {World : Type u_1} (op : ExhOperator) (base : Prop' World) (altsAt : AlternativesAtPosition World) : applyExhAtParse op Core.Parse.literal base altsAt = base

The literal parse (no EXH) returns the base meaning unchanged.

theorem Exhaustification.Interface.single_position_exh {World : Type u_1} (op : ExhOperator) (pos : ExhPosition) (base : Prop' World) (altsAt : AlternativesAtPosition World) : have p := parseFromExhPositions [pos]; applyExhAtParse op p base altsAt = applyExh op (altsAt pos) base

EXH at a single position applies that operator once.

class Exhaustification.Interface.Exhaustifiable (Sentence World : Type) : Type

Typeclass for sentence types where EXH can insert at parse positions.

Design decisions:

1. exhOperator: Which operator to use (default: IE)
2. literalMeaning: Base meaning before any EXH
3. alternativesAt: Position-dependent alternatives

The meaning under a parse is computed by meaningAtParse, which calls applyExhAtParse with the unified EXH machinery.

When to use this:

• RSA models with grammatical ambiguity about EXH placement
• Any theory that needs to reason about EXH insertion sites

When not to use this:

• Scope ambiguity (use Core.scopeParses directly)
• Direct application of EXH (use applyExh directly)

• exhOperator : ExhOperator

  Which EXH operator to use (default: Innocent Exclusion)

• parses : List Core.Parse

  Available EXH parses (typically Core.exhParses)

• literalMeaning : Sentence → World → Bool

  Literal meaning (no EXH applied)

• alternativesAt : Sentence → AlternativesAtPosition World

  Alternatives at each EXH position, given a sentence

def Exhaustification.Interface.Exhaustifiable.meaningAtParse {S W : Type} [inst : Exhaustifiable S W] (p : Core.Parse) (s : S) : Prop' W

Compute the meaning of a sentence under a specific parse.

This uses the unified applyExhAtParse machinery, ensuring all theories that use Exhaustifiable apply EXH consistently.

Equations

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

def Exhaustification.Interface.Exhaustifiable.meaningAtParseBool {S W : Type} [Exhaustifiable S W] (p : Core.Parse) (s : S) (w : W) : Bool

Boolean version for RSA integration.

Equations

• Exhaustification.Interface.Exhaustifiable.meaningAtParseBool p s w = Exhaustification.Interface.Exhaustifiable.literalMeaning s w

theorem Exhaustification.Interface.Exhaustifiable.literal_is_literal {S W : Type} [inst : Exhaustifiable S W] (s : S) : meaningAtParse Core.Parse.literal s = fun (w : W) => literalMeaning s w = true

The literal parse gives the literal meaning.

def Exhaustification.Interface.griceanJustification : String

@cite{spector-2007}'s insight: Exhaustification is derivable from Gricean maxims.

This doesn't add computational content, but documents the theoretical connection between:

• WHY we exhaustify (Gricean reasoning, @cite{spector-2007})
• HOW we exhaustify (exhIE/exhMW operators, @cite{spector-2016})
• WHERE we exhaustify (Parse positions, this interface)

Equations

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

def Exhaustification.Interface.getParses (S W : Type) [Exhaustifiable S W] : List Core.Parse

Get parses for RSAScenario.ambiguous

Equations

• Exhaustification.Interface.getParses S W = Exhaustification.Interface.Exhaustifiable.parses S W

def Exhaustification.Interface.toRSAMeaning {S W : Type} [Exhaustifiable S W] (p : Core.Parse) (w : W) (s : S) : Bool

Convert to RSA meaning function (φ : Interp → World → Utt → Bool)

Equations

• Exhaustification.Interface.toRSAMeaning p w s = Exhaustification.Interface.Exhaustifiable.meaningAtParseBool p s w