structure Phenomena.Questions.Exhaustivity.MentionSomeDatum : Type

A mention-some datum: questions where partial answers suffice.

• question : String

  The question

• partialAnswer : String

  A sufficient partial answer

• explanation : String

  Why partial answer suffices

• implicitGoal : String

  The implicit goal/decision problem

• source : String

  Source

def Phenomena.Questions.Exhaustivity.instReprMentionSomeDatum.repr : MentionSomeDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Exhaustivity.instReprMentionSomeDatum : Repr MentionSomeDatum

Equations

• Phenomena.Questions.Exhaustivity.instReprMentionSomeDatum = { reprPrec := Phenomena.Questions.Exhaustivity.instReprMentionSomeDatum.repr }

def Phenomena.Questions.Exhaustivity.whereBuyCoffee : MentionSomeDatum

Classic mention-some: "Where can I buy X?" Source: @cite{groenendijk-stokhof-1984}

Equations

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

def Phenomena.Questions.Exhaustivity.whereBuyNewspaper : MentionSomeDatum

Equations

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

def Phenomena.Questions.Exhaustivity.whoHasPen : MentionSomeDatum

Equations

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

def Phenomena.Questions.Exhaustivity.mentionSomeExamples : List MentionSomeDatum

Equations

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

structure Phenomena.Questions.Exhaustivity.MentionAllDatum : Type

A mention-all datum: questions requiring exhaustive answers.

• question : String

  The question

• explanation : String

  Why exhaustive answer is required

• partialAnswer : String

  An incomplete answer

• whyInsufficient : String

  Why partial is insufficient

• source : String

  Source

def Phenomena.Questions.Exhaustivity.instReprMentionAllDatum.repr : MentionAllDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.Exhaustivity.instReprMentionAllDatum : Repr MentionAllDatum

Equations

• Phenomena.Questions.Exhaustivity.instReprMentionAllDatum = { reprPrec := Phenomena.Questions.Exhaustivity.instReprMentionAllDatum.repr }

def Phenomena.Questions.Exhaustivity.whoCame : MentionAllDatum

"Who came?" typically requires exhaustive answer

Equations

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

def Phenomena.Questions.Exhaustivity.whichStudentsPassed : MentionAllDatum

"Which students passed?" requires all passers

Equations

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

def Phenomena.Questions.Exhaustivity.mentionAllExamples : List MentionAllDatum

Equations

• Phenomena.Questions.Exhaustivity.mentionAllExamples = [Phenomena.Questions.Exhaustivity.whoCame, Phenomena.Questions.Exhaustivity.whichStudentsPassed]

structure Phenomena.Questions.Exhaustivity.TermTypeExhDatum : Type

@cite{groenendijk-stokhof-1984}, pp. 296-298: Term type determines exhaustive interpretation.

• question : String

  The question

• answer : String

  Answer with specific term type

• termType : TermType

  The term type used

• exhaustive : Bool

  Does this answer get exhaustive interpretation?

• exhaustiveReading : String

  The exhaustive reading (if applicable)

• source : String

  Source

@[implicit_reducible]

instance Phenomena.Questions.Exhaustivity.instReprTermTypeExhDatum : Repr TermTypeExhDatum

Equations

• Phenomena.Questions.Exhaustivity.instReprTermTypeExhDatum = { reprPrec := Phenomena.Questions.Exhaustivity.instReprTermTypeExhDatum.repr }

def Phenomena.Questions.Exhaustivity.instReprTermTypeExhDatum.repr : TermTypeExhDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Exhaustivity.singularDefinite : TermTypeExhDatum

Singular definite: exhaustive (uniqueness presupposition)

Equations

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

def Phenomena.Questions.Exhaustivity.pluralDefinite : TermTypeExhDatum

Plural definite: exhaustive

Equations

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

def Phenomena.Questions.Exhaustivity.indefiniteTerm : TermTypeExhDatum

Indefinite: NON-exhaustive

Equations

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

def Phenomena.Questions.Exhaustivity.universalTerm : TermTypeExhDatum

Universal: exhaustive (trivially - all satisfiers mentioned)

Equations

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

def Phenomena.Questions.Exhaustivity.termTypeExamples : List TermTypeExhDatum

Equations

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

theorem Phenomena.Questions.Exhaustivity.termType_exhaustivity_data_consistent : (termTypeExamples.all fun (d : TermTypeExhDatum) => d.termType.exhaustive == d.exhaustive) = true

Data consistency: for each concrete datum, if the term type predicts exhaustivity then the datum confirms it, and if the term type is non-exhaustive then so is the datum.

This is a per-datum verification over our @cite{groenendijk-stokhof-1984} examples, not a universal claim (arbitrary TermTypeExhDatum values can violate any pattern).

structure Phenomena.Questions.Exhaustivity.NonExhMarkerDatum : Type

Some languages have overt markers for non-exhaustive answers.

• language : String

  Language

• marker : String

  The marker/construction

• example_ : String

  Example sentence

• translation : String

  Translation/gloss

• effect : String

  Effect on exhaustivity

• source : String

  Source

@[implicit_reducible]

instance Phenomena.Questions.Exhaustivity.instReprNonExhMarkerDatum : Repr NonExhMarkerDatum

Equations

• Phenomena.Questions.Exhaustivity.instReprNonExhMarkerDatum = { reprPrec := Phenomena.Questions.Exhaustivity.instReprNonExhMarkerDatum.repr }

def Phenomena.Questions.Exhaustivity.instReprNonExhMarkerDatum.repr : NonExhMarkerDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Exhaustivity.englishForExample : NonExhMarkerDatum

English "for example" blocks exhaustivity

Equations

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

def Phenomena.Questions.Exhaustivity.germanZumBeispiel : NonExhMarkerDatum

German "zum Beispiel"

Equations

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

def Phenomena.Questions.Exhaustivity.englishAmongOthers : NonExhMarkerDatum

English "among others"

Equations

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

def Phenomena.Questions.Exhaustivity.nonExhMarkerExamples : List NonExhMarkerDatum

Equations

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

structure Phenomena.Questions.Exhaustivity.DecisionTheoreticDatum : Type

@cite{van-rooy-2003}: Exhaustivity depends on the decision problem.

Mention-some arises when:

• Multiple answers resolve the decision problem equally
• Knowing more doesn't help choose better

Mention-all required when:

• Complete information is needed to decide

• question : String

  The question

• decisionProblem : String

  The decision problem

• requiresExhaustive : Bool

  Does resolution require exhaustive answer?

• explanation : String

  Explanation

@[implicit_reducible]

instance Phenomena.Questions.Exhaustivity.instReprDecisionTheoreticDatum : Repr DecisionTheoreticDatum

Equations

• Phenomena.Questions.Exhaustivity.instReprDecisionTheoreticDatum = { reprPrec := Phenomena.Questions.Exhaustivity.instReprDecisionTheoreticDatum.repr }

def Phenomena.Questions.Exhaustivity.instReprDecisionTheoreticDatum.repr : DecisionTheoreticDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Exhaustivity.whereBuyCoffee_dt : DecisionTheoreticDatum

Equations

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

def Phenomena.Questions.Exhaustivity.whoCame_dt : DecisionTheoreticDatum

Equations

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

def Phenomena.Questions.Exhaustivity.decisionTheoreticExamples : List DecisionTheoreticDatum

Equations

• Phenomena.Questions.Exhaustivity.decisionTheoreticExamples = [Phenomena.Questions.Exhaustivity.whereBuyCoffee_dt, Phenomena.Questions.Exhaustivity.whoCame_dt]