Documentation

Studies.MartinezVera2026

Martínez Vera (2026) #

Martínez Vera analyzes the Saraguro Kichwa enclitic =mi as a focus marker. A sentence with =mi and scope p presupposes an alternative to p that is highlighted in the context and that, exhaustified relative to the alternatives, entails ¬p; a proposition is highlighted when a move on record addresses the question under discussion with it. A declarative with the direct evidential -rka is an assertion and addresses that question by p, while one with the reportative -shka presents p and addresses it by p or ¬p, so only the latter can be confirmed with =mi. In a correction the highlighted proposition is the corrected one, and exhaustifying it relative to the alternatives of the constituent =mi marks yields ¬p.

Main definitions #

withEvidential: an evidential applied to a sentence.
Move.assert, Move.present, Move.declare: the illocutionary operators, and the one a declarative with a given evidential performs.
Highlighted, MiDefined: highlighting, and the presupposition of =mi.

Main statements #

miDefined_univ_iff: for =mi on a clause exhaustification is vacuous, and =mi needs a highlighted proposition entailing ¬p.
miDefined_update_present, miDefined_update_assert_iff: presenting p licenses =mi on p, and asserting it does not.
miDefined_of_isInnocentlyExcludable: corrections.
judgment_eq_acceptable_iff_miDefined, judgment_eq_acceptable_iff_nonempty: an example is acceptable exactly when the analysis licenses its =mi, or its speaker stays consistent.

Implementation notes #

The paper's composition rule I is the bind of TwoDim, whose ⊤ plays the empty not-at-issue layer. An illocutionary operator is the move it puts on record: its speaker's commitments, without their addressee, and the propositions by which it addresses the question under discussion, addressing being partial answerhood. Exhaustification is innocent exclusion; the paper glosses the alternatives it may deny as those entailing the prejacent, under which a correction would not entail ¬p. Highlighting is the paper's notion, not the compositional highlighting of Semantics/Questions/Highlighting.lean. The operator name present is Faller's. The examples are evaluated in a model whose worlds are sets of events. The paper's survey of =mi across Quechuan, after Faller, Sánchez, Tellings, Grzech and Bendezú, finds the analyses hard to compare at present and is not formalized.

TODO #

The paper describes =mi in (27d) as marking the verb; with alternatives varying the verb phrase, which include buying a pig, (37) would license it.
Footnote 7's use of -rka by an authority without direct perception, and the past tense of -rka and -shka, are not modelled.

References #

Evidentials #

def MartinezVera2026.evidence {A : Type u_1} {W : Type u_2} (ev : A → Evidential.Parameter → Set W → Set W) (s : A) (e : Evidential) (p : Set W) :

Set W

evidence ev s e p is the not-at-issue proposition of the evidential e ((40b), (42b)), that s has evidence for p from a source e covers, where ev s π p is the set of worlds in which s has evidence of kind π for p. For -rka this is direct perceptual evidence and for -shka reportative evidence.

Equations

MartinezVera2026.evidence ev s e p = {w : W | ∃ π ∈ e.covers, w ∈ ev s π p}

Instances For

def MartinezVera2026.withEvidential {A : Type u_1} {W : Type u_2} (ev : A → Evidential.Parameter → Set W → Set W) (s : A) (e : Evidential) (S : ConventionalImplicature.TwoDim W (Set W)) :

ConventionalImplicature.TwoDim W (Set W)

withEvidential ev s e S applies the evidential e to the sentence S by rule I ((40a), (42a)), keeping the scope at issue and adding the speaker's evidence for it not at issue.

Equations

MartinezVera2026.withEvidential ev s e S = do let p ← S { atIssue := p, notAtIssue := fun (x : W) => x ∈ MartinezVera2026.evidence ev s e p }

Instances For

@[simp]

theorem MartinezVera2026.withEvidential_atIssue {A : Type u_1} {W : Type u_2} (ev : A → Evidential.Parameter → Set W → Set W) (s : A) (e : Evidential) (S : ConventionalImplicature.TwoDim W (Set W)) :

(withEvidential ev s e S).atIssue = S.atIssue

@[simp]

theorem MartinezVera2026.ofPred_notAtIssue_withEvidential_pure {A : Type u_1} {W : Type u_2} (ev : A → Evidential.Parameter → Set W → Set W) (s : A) (e : Evidential) (p : Set W) :

Set.ofPred (withEvidential ev s e (pure p)).notAtIssue = evidence ev s e p

Moves and contexts #

structure MartinezVera2026.Move (A : Type u_3) (W : Type u_4) :

Type (max u_3 u_4)

A move on the conversational record has a speaker, the propositions the speaker commits to, and the propositions by means of which it addresses the question under discussion.

speaker : A
The speaker.
commitments : Set (Set W)
The propositions the speaker commits to.
addressers : Set (Set W)
The propositions by means of which the move addresses the question under discussion.

Instances For

def MartinezVera2026.Move.assert {A : Type u_1} {W : Type u_2} (s : A) (S : ConventionalImplicature.TwoDim W (Set W)) :

Move A W

The operator assert (39) commits the speaker to the scope, by means of which she addresses the question under discussion, and to the not-at-issue content.

Equations

MartinezVera2026.Move.assert s S = { speaker := s, commitments := {S.atIssue, Set.ofPred S.notAtIssue}, addressers := {S.atIssue} }

Instances For

def MartinezVera2026.Move.present {A : Type u_1} {W : Type u_2} (s : A) (S : ConventionalImplicature.TwoDim W (Set W)) :

Move A W

The operator present (41) brings the scope to the addressee's attention, addresses the question under discussion by means of it or its negation, and commits the speaker only to the not-at-issue content.

Equations

MartinezVera2026.Move.present s S = { speaker := s, commitments := {Set.ofPred S.notAtIssue}, addressers := {S.atIssue, S.atIssueᶜ} }

Instances For

def MartinezVera2026.Move.biasedQuestion {A : Type u_1} {W : Type u_2} (s : A) (q : Set W) :

Move A W

A question biased toward q steers the exchange toward adopting q, and so addresses the question under discussion by means of it (§4.2).

Equations

MartinezVera2026.Move.biasedQuestion s q = { speaker := s, commitments := ∅, addressers := {q} }

Instances For

def MartinezVera2026.Move.declare {A : Type u_1} {W : Type u_2} (s : A) (e : Evidential) (S : ConventionalImplicature.TwoDim W (Set W)) :

Option (Move A W)

A declarative with a direct evidential is asserted and one with a reportative is presented ((40c), (42c)), and declare s e S is the move of a declarative with evidential e, if the paper analyzes e.

Equations

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

Instances For

theorem MartinezVera2026.Move.declare_of_isDirect {A : Type u_1} {W : Type u_2} (s : A) {e : Evidential} (he : e.IsDirect) (S : ConventionalImplicature.TwoDim W (Set W)) :

declare s e S = some (assert s S)

theorem MartinezVera2026.Move.declare_of_isReportative {A : Type u_1} {W : Type u_2} (s : A) {e : Evidential} (he : e.IsReportative) (S : ConventionalImplicature.TwoDim W (Set W)) :

declare s e S = some (present s S)

@[simp]

theorem MartinezVera2026.Move.declare_rka {A : Type u_1} {W : Type u_2} (s : A) (S : ConventionalImplicature.TwoDim W (Set W)) :

declare s Quechua.SaraguroKichwa.Evidentiality.rka S = some (assert s S)

@[simp]

theorem MartinezVera2026.Move.declare_shka {A : Type u_1} {W : Type u_2} (s : A) (S : ConventionalImplicature.TwoDim W (Set W)) :

declare s Quechua.SaraguroKichwa.Evidentiality.shka S = some (present s S)

structure MartinezVera2026.Context (A : Type u_3) (W : Type u_4) :

Type (max u_3 u_4)

A context of utterance consists of the moves on record and the question under discussion.

moves : Set (Move A W)
The moves on record.
qud : Question W
The question under discussion.

Instances For

def MartinezVera2026.Context.update {A : Type u_1} {W : Type u_2} (c : Context A W) (m : Move A W) :

c.update m puts the move m on record.

Equations

c.update m = { moves := insert m c.moves, qud := c.qud }

Instances For

def MartinezVera2026.Context.declare {A : Type u_1} {W : Type u_2} (c : Context A W) (s : A) (e : Evidential) (S : ConventionalImplicature.TwoDim W (Set W)) :

c.declare s e S puts on record the move of a declarative with evidential e, if the paper analyzes e.

Equations

c.declare s e S = (Option.map c.update (MartinezVera2026.Move.declare s e S)).getD c

Instances For

def MartinezVera2026.Context.ask {A : Type u_1} {W : Type u_2} (c : Context A W) (Q : Question W) :

Asking a question that addresses no prior one makes it the question under discussion.

Equations

c.ask Q = { moves := c.moves, qud := Q }

Instances For

def MartinezVera2026.Context.commitments {A : Type u_1} {W : Type u_2} (c : Context A W) :

Commitment.State A W

The commitment state of the record commits the speaker of each move to each of its commitments.

Equations

c.commitments = {k : Commitment A W | ∃ m ∈ c.moves, ∃ p ∈ m.commitments, k = Commitment.commit m.speaker p}

Instances For

def MartinezVera2026.Context.contextSetOf {A : Type u_1} {W : Type u_2} (c : Context A W) (s : A) :

Set W

c.contextSetOf s is the set of worlds compatible with the commitments of s.

Equations

c.contextSetOf s = Commitment.contextSet (Commitment.ofCommitter c.commitments s)

Instances For

theorem MartinezVera2026.Context.mem_contextSetOf {A : Type u_1} {W : Type u_2} {c : Context A W} {s : A} {w : W} :

w ∈ c.contextSetOf s ↔ ∀ m ∈ c.moves, m.speaker = s → ∀ p ∈ m.commitments, w ∈ p

def MartinezVera2026.Highlighted {A : Type u_1} {W : Type u_2} (c : Context A W) (q : Set W) :

A proposition is highlighted (38) when a move on record addresses the question under discussion by means of it and it partially answers that question.

Equations

MartinezVera2026.Highlighted c q = ((∃ m ∈ c.moves, q ∈ m.addressers) ∧ c.qud.PartiallyAnsweredBy q)

Instances For

def MartinezVera2026.MiDefined {A : Type u_1} {W : Type u_2} (c : Context A W) (ALT : Set (Set W)) (p : Set W) :

The presupposition of =mi (37) holds when some alternative to the scope p is highlighted and, exhaustified relative to the alternatives, entails ¬p. Where defined, =mi is the identity on its argument.

Equations

MartinezVera2026.MiDefined c ALT p = ∃ q ∈ ALT, MartinezVera2026.Highlighted c q ∧ Exhaustification.exhIE ALT q ⊆ pᶜ

Instances For

theorem MartinezVera2026.ne_of_exhIE_subset_compl {W : Type u_2} {ALT : Set (Set W)} {p q : Set W} (h : Exhaustification.exhIE ALT q ⊆ pᶜ) (hne : (Exhaustification.exhIE ALT q).Nonempty) :

q ≠ p

The witness of (37) differs from the scope, as the paper's prose requires, whenever its exhaustification is consistent.

theorem MartinezVera2026.not_miDefined_of_addressers {A : Type u_1} {W : Type u_2} {c : Context A W} {ALT : Set (Set W)} {p : Set W} (h : ∀ m ∈ c.moves, m.addressers = ∅) :

¬MiDefined c ALT p

When nothing on record addresses the question under discussion, =mi is undefined, as out of the blue ((7), (28)) and after an unbiased polar question (8) or a constituent question (29).

theorem MartinezVera2026.miDefined_univ_iff {A : Type u_1} {W : Type u_2} {c : Context A W} {p : Set W} :

MiDefined c Set.univ p ↔ ∃ (q : Set W), Highlighted c q ∧ q ⊆ pᶜ

For clausal =mi the alternatives are all propositions ((44d), (51d)), exhaustification is vacuous, and (37) asks for a highlighted proposition entailing ¬p.

theorem MartinezVera2026.miDefined_of_highlighted_compl {A : Type u_1} {W : Type u_2} {c : Context A W} {p : Set W} (h : Highlighted c pᶜ) :

MiDefined c Set.univ p

A highlighted ¬p licenses clausal =mi on p ((43), (44)).

theorem MartinezVera2026.highlighted_update_iff {A : Type u_1} {W : Type u_2} {c : Context A W} {q : Set W} {m : Move A W} :

Highlighted (c.update m) q ↔ (q ∈ m.addressers ∨ ∃ m' ∈ c.moves, q ∈ m'.addressers) ∧ c.qud.PartiallyAnsweredBy q

theorem MartinezVera2026.miDefined_update_present {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) (h : c.qud.PartiallyAnsweredBy S.atIssueᶜ) :

MiDefined (c.update (Move.present s S)) Set.univ S.atIssue

Presenting p licenses clausal =mi on p ((48), (50), (51)), wherever ¬p addresses the question under discussion.

theorem MartinezVera2026.miDefined_update_assert_iff {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) (hp : S.atIssue.Nonempty) :

MiDefined (c.update (Move.assert s S)) Set.univ S.atIssue ↔ MiDefined c Set.univ S.atIssue

Asserting a consistent p adds nothing that licenses clausal =mi on p ((47), (49)).

theorem MartinezVera2026.miDefined_of_isInnocentlyExcludable {A : Type u_1} {W : Type u_2} {c : Context A W} {ALT : Set (Set W)} {p q : Set W} (hq : q ∈ ALT) (hh : Highlighted c q) (h : Exhaustification.IsInnocentlyExcludable ALT q p) :

MiDefined c ALT p

A highlighted alternative that innocently excludes the scope licenses =mi ((45), (46)), as exhaustifying "Juan bought a cow" relative to what Juan might have bought denies that he bought a pig.

theorem MartinezVera2026.not_miDefined_of_disjoint {A : Type u_1} {W : Type u_2} {c : Context A W} {ALT : Set (Set W)} {p : Set W} (h : ∀ (q : Set W), Highlighted c q → q ∉ ALT) :

¬MiDefined c ALT p

When no highlighted proposition is among the alternatives, =mi is undefined, as in a correction of the object with =mi on the subject or the verb ((27c), (27d)).

Commitments #

theorem MartinezVera2026.contextSetOf_eq_empty {A : Type u_1} {W : Type u_2} {c : Context A W} {p : Set W} {s : A} {m m' : Move A W} (hm : m ∈ c.moves) (hm' : m' ∈ c.moves) (hs : m.speaker = s) (hs' : m'.speaker = s) (hp : p ∈ m.commitments) (hp' : pᶜ ∈ m'.commitments) :

c.contextSetOf s = ∅

A speaker committed to a proposition and to its negation is inconsistent.

theorem MartinezVera2026.contextSetOf_update {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} {m : Move A W} {w : W} :

w ∈ (c.update m).contextSetOf s ↔ (m.speaker = s → ∀ p ∈ m.commitments, w ∈ p) ∧ w ∈ c.contextSetOf s

theorem MartinezVera2026.contextSetOf_assert_assert_compl {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) :

((c.update (Move.assert s S)).update (Move.assert s (pure S.atIssueᶜ))).contextSetOf s = ∅

Asserting p and then ¬p is inconsistent (18a), as is the -rka counterpart of footnote 9, where =mi on ¬p is licensed but the speaker contradicts herself.

theorem MartinezVera2026.mem_contextSetOf_present_assert_compl {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) {w : W} (hc : w ∈ c.contextSetOf s) (hN : S.notAtIssue w) (hA : w ∉ S.atIssue) :

w ∈ ((c.update (Move.present s S)).update (Move.assert s (pure S.atIssueᶜ))).contextSetOf s

Presenting p and then asserting ¬p is consistent wherever the speaker's evidence for p is compatible with ¬p (19a).

theorem MartinezVera2026.contextSetOf_update_assert_compl_notAtIssue {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) {m : Move A W} (hs : m.speaker = s) (hm : Set.ofPred S.notAtIssue ∈ m.commitments) :

((c.update m).update (Move.assert s (pure (Set.ofPred S.notAtIssue)ᶜ))).contextSetOf s = ∅

Denying the evidence a declarative commits to is inconsistent, after an assertion (18b) or a presentation (19b).

theorem MartinezVera2026.contextSetOf_present_assert_assert_compl {A : Type u_1} {W : Type u_2} (s : A) {c : Context A W} (S : ConventionalImplicature.TwoDim W (Set W)) :

(((c.update (Move.present s S)).update (Move.assert s (pure S.atIssue))).update (Move.assert s (pure S.atIssueᶜ))).contextSetOf s = ∅

Confirming a presented p with =mi asserts it, so denying it afterwards is inconsistent (footnote 10).

The examples #

The examples are evaluated in a model whose worlds are sets of events: an event fixes a value at each constituent site of the scope sentence, a world is the set of events that happened, and the question under discussion asks which event happened. The scope is that the scope event happened, and a correction asserts that its variant at the contrasted site did. The propositions in play are the scope, its negation and the variants, named by Answer; miDefined_iff reduces the presupposition of =mi in each example's context to a check on these names, and judgment_eq_acceptable_iff_miDefined compares it with the paper's judgments.

inductive MartinezVera2026.Site :

A Site is a constituent that =mi marks or a correction contrasts in the examples.

subject : Site
object : Site
goal : Site
verbPhrase : Site
verb : Site
modifier : Site

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqSite :

DecidableEq Site

Equations

MartinezVera2026.instDecidableEqSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev MartinezVera2026.Event :

An event fixes a value at each site.

Equations

MartinezVera2026.Event = (MartinezVera2026.Site → Bool)

Instances For

def MartinezVera2026.happened (e : Event) :

Set (Set Event)

happened e is the proposition that the event e happened.

Equations

MartinezVera2026.happened e = {w : Set MartinezVera2026.Event | e ∈ w}

Instances For

def MartinezVera2026.vary (k : Site) (b : Bool) :

vary k b is the scope event with the value at k set to b, the scope event itself when b is true.

Equations

MartinezVera2026.vary k b = Function.update (fun (x : MartinezVera2026.Site) => true) k b

Instances For

inductive MartinezVera2026.Answer :

An Answer names a proposition in play, the scope, its negation, or the variant at a site.

scope : Answer
negation : Answer
variant (k : Site) : Answer

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqAnswer :

DecidableEq Answer

Equations

MartinezVera2026.instDecidableEqAnswer = MartinezVera2026.instDecidableEqAnswer.decEq

def MartinezVera2026.instDecidableEqAnswer.decEq (x✝ x✝¹ : Answer) :

Decidable (x✝ = x✝¹)

Equations

MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.scope MartinezVera2026.Answer.scope = isTrue ⋯
MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.scope MartinezVera2026.Answer.negation = isFalse MartinezVera2026.instDecidableEqAnswer.decEq._proof_3
MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.scope (MartinezVera2026.Answer.variant k) = isFalse ⋯
MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.negation MartinezVera2026.Answer.scope = isFalse MartinezVera2026.instDecidableEqAnswer.decEq._proof_5
MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.negation MartinezVera2026.Answer.negation = isTrue ⋯
MartinezVera2026.instDecidableEqAnswer.decEq MartinezVera2026.Answer.negation (MartinezVera2026.Answer.variant k) = isFalse ⋯
MartinezVera2026.instDecidableEqAnswer.decEq (MartinezVera2026.Answer.variant k) MartinezVera2026.Answer.scope = isFalse ⋯
MartinezVera2026.instDecidableEqAnswer.decEq (MartinezVera2026.Answer.variant k) MartinezVera2026.Answer.negation = isFalse ⋯
MartinezVera2026.instDecidableEqAnswer.decEq (MartinezVera2026.Answer.variant a) (MartinezVera2026.Answer.variant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

def MartinezVera2026.Answer.prop :

Answer → Set (Set Event)

a.prop is the proposition the answer a names.

Equations

MartinezVera2026.Answer.scope.prop = MartinezVera2026.happened fun (x : MartinezVera2026.Site) => true
MartinezVera2026.Answer.negation.prop = (MartinezVera2026.happened fun (x : MartinezVera2026.Site) => true)ᶜ
(MartinezVera2026.Answer.variant k).prop = MartinezVera2026.happened (MartinezVera2026.vary k false)

Instances For

def MartinezVera2026.whichEvent :

Question (Set Event)

The question under discussion of the model asks which event happened.

Equations

MartinezVera2026.whichEvent = Question.which Set.univ MartinezVera2026.happened

Instances For

def MartinezVera2026.alternatives :

Option Site → Set (Set (Set Event))

The alternatives of =mi on a clause are all propositions ((44d), (51d)), and those of =mi on the constituent at a site are the variants at that site ((46d)).

Equations

MartinezVera2026.alternatives none = Set.univ
MartinezVera2026.alternatives (some k) = Set.range fun (b : Bool) => MartinezVera2026.happened (MartinezVera2026.vary k b)

Instances For

def MartinezVera2026.evModel :

Discourse.Role → Evidential.Parameter → Set (Set Event) → Set (Set Event)

The model's speaker has evidence of every kind for everything.

Equations

MartinezVera2026.evModel x✝² x✝¹ x✝ = Set.univ

Instances For

def MartinezVera2026.sentence (s : Discourse.Role) (e : Evidential) (p : Set (Set Event)) :

ConventionalImplicature.TwoDim (Set Event) (Set (Set Event))

sentence s e p is the declarative of s with evidential e and scope p.

Equations

MartinezVera2026.sentence s e p = MartinezVera2026.withEvidential MartinezVera2026.evModel s e (pure p)

Instances For

inductive MartinezVera2026.Prior :

A Prior is the discourse before a =mi sentence as the paper describes its examples. It is empty, an assertion of the negated scope (6), a debate between the scope and its negation ((9), (11)), a declarative of the scope with -rka (20) or -shka (21), or a correction asserting a variant ((22)–(30)).

none : Prior
assertedNegation : Prior
debate : Prior
direct : Prior
reportative : Prior
correction (k : Site) : Prior

Instances For

def MartinezVera2026.instDecidableEqPrior.decEq (x✝ x✝¹ : Prior) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqPrior :

DecidableEq Prior

Equations

MartinezVera2026.instDecidableEqPrior = MartinezVera2026.instDecidableEqPrior.decEq

inductive MartinezVera2026.Asked :

An Asked is the question asked right before the =mi sentence, an unbiased polar question ((8), (9)), a constituent question (29), or a question biased toward the negation (10) or toward the scope (11).

polar : Asked
constituent : Asked
negativeBiased : Asked
positiveBiased : Asked

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqAsked :

DecidableEq Asked

Equations

MartinezVera2026.instDecidableEqAsked x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinezVera2026.Prior.context :

Prior → Context Discourse.Role (Set Event)

p.context is the context the prior discourse p sets up.

Equations

One or more equations did not get rendered due to their size.
MartinezVera2026.Prior.none.context = { moves := ∅, qud := MartinezVera2026.whichEvent }

Instances For

def MartinezVera2026.Asked.context :

Asked → Context Discourse.Role (Set Event) → Context Discourse.Role (Set Event)

a.context c asks the question a in the context c.

Equations

One or more equations did not get rendered due to their size.
MartinezVera2026.Asked.polar.context x✝ = x✝.ask (Question.polar MartinezVera2026.Answer.scope.prop)
MartinezVera2026.Asked.constituent.context x✝ = x✝.ask MartinezVera2026.whichEvent

Instances For

structure MartinezVera2026.MiExample :

A =mi example records its prior discourse, the question asked, the constituent =mi marks, and the polarity of its scope.

prior : Prior
The discourse before the =mi sentence.
asked : Option Asked
The question asked right before it, if any.
focus : Option Site
The constituent =mi marks, or none for the clause.
polarity : Polarity
The polarity of the scope.

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqMiExample :

DecidableEq MiExample

Equations

MartinezVera2026.instDecidableEqMiExample = MartinezVera2026.instDecidableEqMiExample.decEq

def MartinezVera2026.instDecidableEqMiExample.decEq (x✝ x✝¹ : MiExample) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def MartinezVera2026.MiExample.context (r : MiExample) :

Context Discourse.Role (Set Event)

r.context is the context of the =mi sentence.

Equations

r.context = (Option.map MartinezVera2026.Asked.context r.asked).getD id r.prior.context

Instances For

def MartinezVera2026.MiExample.scope (r : MiExample) :

r.scope names the scope of the =mi sentence.

Equations

r.scope = match r.polarity with | Polarity.positive => MartinezVera2026.Answer.scope | Polarity.negative => MartinezVera2026.Answer.negation

Instances For

def MartinezVera2026.MiExample.addressers (r : MiExample) :

r.addressers lists the answers by means of which the moves on record address the question under discussion.

Equations

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

Instances For

def MartinezVera2026.MiExample.Addresses (r : MiExample) :

Answer → Prop

Every answer in play addresses the question under discussion, except that a variant does not address a polar question about the scope.

Equations

r.Addresses (MartinezVera2026.Answer.variant k) = (r.asked = none ∨ r.asked = some MartinezVera2026.Asked.constituent)
r.Addresses x✝ = True

Instances For

def MartinezVera2026.MiExample.Fits (r : MiExample) (a : Answer) :

An answer fits the =mi sentence when it is one of its alternatives and its exhaustification entails the negated scope, as fits_iff shows.

Equations

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

Instances For

def MartinezVera2026.MiExample.Licensed (r : MiExample) :

The analysis licenses the =mi sentence when some answer on record addresses the question under discussion and fits it.

Equations

r.Licensed = ∃ a ∈ r.addressers, r.Addresses a ∧ r.Fits a

Instances For

@[instance_reducible]

instance MartinezVera2026.MiExample.instDecidableAddresses (r : MiExample) (a : Answer) :

Decidable (r.Addresses a)

Equations

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

@[instance_reducible]

instance MartinezVera2026.MiExample.instDecidableFits (r : MiExample) (a : Answer) :

Decidable (r.Fits a)

Equations

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

@[instance_reducible]

instance MartinezVera2026.MiExample.instDecidableLicensed (r : MiExample) :

Decidable r.Licensed

Equations

r.instDecidableLicensed = id inferInstance

The model's propositions #

theorem MartinezVera2026.happened_subset_happened {e e' : Event} :

happened e ⊆ happened e' ↔ e = e'

theorem MartinezVera2026.vary_true (k : Site) :

vary k true = fun (x : Site) => true

theorem MartinezVera2026.vary_false_ne (k : Site) :

vary k false ≠ fun (x : Site) => true

theorem MartinezVera2026.vary_false_inj {j k : Site} :

vary j false = vary k false ↔ j = k

theorem MartinezVera2026.empty_mem_negation :

∅ ∈ Answer.negation.prop

theorem MartinezVera2026.empty_notMem_happened (e : Event) :

∅ ∉ happened e

theorem MartinezVera2026.mem_alternatives_iff {a : Answer} {k : Site} :

a.prop ∈ alternatives (some k) ↔ a = Answer.scope ∨ a = Answer.variant k

theorem MartinezVera2026.happened_mem_alt_whichEvent (e : Event) :

happened e ∈ whichEvent.alt

theorem MartinezVera2026.partiallyAnsweredBy_whichEvent (a : Answer) :

whichEvent.PartiallyAnsweredBy a.prop

theorem MartinezVera2026.partiallyAnsweredBy_polar_iff (a : Answer) :

(Question.polar Answer.scope.prop).PartiallyAnsweredBy a.prop ↔ ∀ (k : Site), a ≠ Answer.variant k

theorem MartinezVera2026.finite_alternatives (k : Site) :

(alternatives (some k)).Finite

theorem MartinezVera2026.forall_mem_alternatives {k : Site} {P : Set (Set Event) → Prop} :

(∀ a ∈ alternatives (some k), P a) ↔ P Answer.scope.prop ∧ P (Answer.variant k).prop

theorem MartinezVera2026.singleton_mem_happened (e : Event) :

{e} ∈ happened e

theorem MartinezVera2026.exhIE_variant_subset (k : Site) :

Exhaustification.exhIE (alternatives (some k)) (Answer.variant k).prop ⊆ Answer.scope.propᶜ

Exhaustifying the variant at k relative to the alternatives at k denies the scope.

theorem MartinezVera2026.singleton_mem_exhIE_variant (k : Site) :

{vary k false} ∈ Exhaustification.exhIE (alternatives (some k)) (Answer.variant k).prop

theorem MartinezVera2026.singleton_mem_exhIE_scope (k : Site) :

{fun (x : Site) => true} ∈ Exhaustification.exhIE (alternatives (some k)) Answer.scope.prop

theorem MartinezVera2026.prop_negation :

Answer.negation.prop = Answer.scope.propᶜ

theorem MartinezVera2026.compl_negation :

Answer.negation.propᶜ = Answer.scope.prop

theorem MartinezVera2026.scope_ne_empty :

Answer.scope.prop ≠ ∅

theorem MartinezVera2026.variant_not_subset_compl (k : Site) :

¬(Answer.variant k).prop ⊆ Answer.scope.propᶜ

theorem MartinezVera2026.negation_not_subset_scope :

¬Answer.negation.prop ⊆ Answer.scope.prop

theorem MartinezVera2026.variant_not_subset_scope (k : Site) :

¬(Answer.variant k).prop ⊆ Answer.scope.prop

theorem MartinezVera2026.MiExample.fits_iff (r : MiExample) (a : Answer) :

a.prop ∈ alternatives r.focus ∧ Exhaustification.exhIE (alternatives r.focus) a.prop ⊆ r.scope.propᶜ ↔ r.Fits a

An answer fits the =mi sentence exactly when it is an alternative whose exhaustification entails the negated scope.

theorem MartinezVera2026.MiExample.exists_mem_moves_iff (r : MiExample) (q : Set (Set Event)) :

(∃ m ∈ r.context.moves, q ∈ m.addressers) ↔ ∃ a ∈ r.addressers, a.prop = q

theorem MartinezVera2026.MiExample.qud_context (r : MiExample) :

r.context.qud = if r.asked = none ∨ r.asked = some Asked.constituent then whichEvent else Question.polar Answer.scope.prop

theorem MartinezVera2026.MiExample.highlighted_context_iff (r : MiExample) (q : Set (Set Event)) :

Highlighted r.context q ↔ ∃ a ∈ r.addressers, r.Addresses a ∧ a.prop = q

theorem MartinezVera2026.MiExample.miDefined_iff (r : MiExample) :

MiDefined r.context (alternatives r.focus) r.scope.prop ↔ r.Licensed

In each example's context, the presupposition of =mi holds exactly when the analysis licenses it.

def MartinezVera2026.siteLabels :

List (String × Site)

The examples name sites by their constructors.

Equations

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

Instances For

def MartinezVera2026.focusLabels :

List (String × Option Site)

The examples name the constituent =mi marks, the clause or a site.

Equations

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

Instances For

def MartinezVera2026.priorLabels :

List (String × Prior)

The examples name prior discourses other than a correction by their constructors.

Equations

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

Instances For

def MartinezVera2026.askedLabels :

List (String × Asked)

The examples name the questions asked by their constructors.

Equations

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

Instances For

def MartinezVera2026.polarityLabels :

List (String × Polarity)

The examples name the polarity of a negative scope.

Equations

MartinezVera2026.polarityLabels = [("negative", Polarity.negative)]

Instances For

def MartinezVera2026.MiExample.ofDatum? (x : Datum) :

Option MiExample

ofDatum? x is the =mi example the row x records, if it records one, a correction naming its contrasted site.

Equations

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

Instances For

theorem MartinezVera2026.judgment_eq_acceptable_iff_miDefined (x : Datum) :

x ∈ Examples.all → ∀ r ∈ MiExample.ofDatum? x, x.judgment = Judgment.acceptable ↔ MiDefined r.context (alternatives r.focus) r.scope.prop

Every =mi example is acceptable exactly when its presupposition holds in its context.

inductive MartinezVera2026.Continuation :

A Continuation is how the speaker continues her declarative in a commitment test. She denies its scope ((18a), (19a)), denies her evidence ((18b), (19b)), or confirms the scope with =mi and then denies it (footnote 10).

deniesScope : Continuation
deniesEvidence : Continuation
confirmsThenDeniesScope : Continuation

Instances For

@[instance_reducible]

instance MartinezVera2026.instDecidableEqContinuation :

DecidableEq Continuation

Equations

MartinezVera2026.instDecidableEqContinuation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure MartinezVera2026.CommitmentExample :

A commitment test is a declarative of the scope with an evidential, continued by its speaker.

evidential : Evidential
The evidential of the declarative.
continuation : Continuation
How the speaker continues.

Instances For

def MartinezVera2026.CommitmentExample.context (r : CommitmentExample) :

Context Discourse.Role (Set Event)

r.context is the record after the declarative and its continuation.

Equations

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

Instances For

theorem MartinezVera2026.CommitmentExample.nonempty_contextSetOf_iff (r : CommitmentExample) (he : r.evidential.IsDirect ∨ r.evidential.IsReportative) :

(r.context.contextSetOf Discourse.Role.speaker).Nonempty ↔ r.evidential.IsReportative ∧ r.continuation = Continuation.deniesScope

The speaker of a declarative with a direct or reportative evidential stays consistent exactly when the evidential is reportative and she denies only the scope.

def MartinezVera2026.CommitmentExample.evidentialLabels :

List (String × Evidential)

The examples name the evidentials of the commitment tests by their evidence type.

Equations

MartinezVera2026.CommitmentExample.evidentialLabels = [("direct", Quechua.SaraguroKichwa.Evidentiality.rka), ("reportative", Quechua.SaraguroKichwa.Evidentiality.shka)]

Instances For

def MartinezVera2026.CommitmentExample.continuationLabels :

List (String × Continuation)

The examples name the continuations by their constructors.

Equations

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

Instances For

def MartinezVera2026.CommitmentExample.ofDatum? (x : Datum) :

Option CommitmentExample

ofDatum? x is the commitment test the row x records, if it records one.

Equations

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

Instances For

theorem MartinezVera2026.judgment_eq_acceptable_iff_nonempty (x : Datum) :

x ∈ Examples.all → ∀ r ∈ CommitmentExample.ofDatum? x, x.judgment = Judgment.acceptable ↔ (r.context.contextSetOf Discourse.Role.speaker).Nonempty

Every commitment test is acceptable exactly when its speaker's commitments are consistent ((18), (19), footnote 10).