Bondarenko (2020): factivity from pre-existence

Bondarenko accounts for the factivity alternation of Barguzin Buryat hanaxa, 'think' with a finite CP and 'remember' with a nominalized clause. The nominalized clause presupposes that the event it describes started before the thinking: a began continuation must place its start before the matrix time, a future child or a fictional cat cannot be the object, and the inference survives questions and negation. A CP modifies the thinking event, whose content its complementizer fixes, and adds no presupposition. A nominalized clause saturates the internal argument of the head θTh, which presupposes that this argument started before the matrix time; closed by Fox's strong Kleene existential, the report presupposes exactly that, and the factive inference follows.

Main definitions

• thetaTh: the head θTh with hanaxa.
• report: the past-tense report with a nominalized clause.
• reportThat: the past-tense report with a CP.

Main results

• reportThat_ne_zero: a report with a CP presupposes nothing.
• existsStrong_thetaTh_ne_zero_iff: the closed θTh-report presupposes pre-existence.
• exists_preExists_of_report_ne_zero: the past-tense report presupposes pre-existence at some past thinking time.
• exists_of_report_ne_zero: the factive inference.

Implementation notes

• Pre-existence is Event.PreExists of Semantics/Events/PreExistence.lean, shared with Studies/Williams2025. Time spans are a function τ into NonemptyInterval, the run time of an event or the life span of an entity, and the paper's LB(τ(x)) < t is (τ x).fst < t.fst.
• Truth values are trivalent, as in the paper: a sentence is a trivalent proposition W → SignType, defined when it is true or false. The existential closure (58) and the past tense (60) are both the strong Kleene existential Trivalent.existsStrong, the tense over the subtype of past times t' < t (t'.Precedes t) within the contextual interval g(1) (t' ≤ g₁).
• The simplification from (57) and (58) to (59) assumes a nonempty domain of events, as the paper's fn. 36 says, and (62) follows from (61) only for a nonempty contextual past: over an empty one the falsity condition of (61) holds vacuously and the sentence is defined whatever the complement. Both are hypotheses here.
• The verb and the Voice head are one predicate of events P at a world and time, so the external argument joins θTh's assertion and leaves its presupposition, as in (57). This is the weak Kleene conjunction SignType.meetWeak with a presuppositionless conjunct, not the strong Kleene one the paper adopts elsewhere; the two differ only when the subject is the experiencer of no event. θTh's about is a function from contentful events to their topics, as in (46).
• A report with both a nominalized clause and a CP (21) is θTh with a P that includes the CP's content condition, and has the nominalized clause's presupposition.
• Not formalized: the tuxai 'about' phrases (7), (48), which carry no presupposition and get no formula in the paper; the allosemy of θTh (49); and the plan readings of the future participle -xA (70)–(73), which the paper leaves open.

References

• [Bon20]
• [Fox13]
• [Kle52]
• [Wil25]

θTh and its presupposition, (55), (56)

noncomputable def Bondarenko2020.thetaTh {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] (τ : X → NonemptyInterval T) (about : E → X) (P : W → NonemptyInterval T → E → Prop) (Q : W → NonemptyInterval T → X → Prop) (t : NonemptyInterval T) (e : E) : W → SignType

With hanaxa, θTh holds of an event e at the matrix time t when e is a P-event about an individual of Q that started before t, and presupposes that Q describes such an individual, (55), (56).

Equations

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

noncomputable def Bondarenko2020.report {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] (τ : X → NonemptyInterval T) (about : E → X) (P : W → NonemptyInterval T → E → Prop) (Q : W → NonemptyInterval T → X → Prop) (g₁ t : NonemptyInterval T) : W → SignType

The report (61) is the past tense (60), within the contextual interval g₁, over the existentially closed (58) θTh-report (57).

Equations

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

noncomputable def Bondarenko2020.reportThat {W : Type u_1} {T : Type u_2} {E : Type u_4} {I : Type u_5} [LinearOrder T] [Anchor E I] (P : W → NonemptyInterval T → E → Prop) (p : I → Prop) (g₁ t : NonemptyInterval T) : W → SignType

A report with a CP, (29), is the past tense (28) over a thinking event whose content the complementizer (25) fixes as p.

Equations

• Bondarenko2020.reportThat P p g₁ t w = Trivalent.existsStrong fun (t' : { t' : NonemptyInterval T // t'.Precedes t ∧ t' ≤ g₁ }) => SignType.ofProp (∃ (e : E), P w (↑t') e ∧ Anchor.comp p e)

theorem Bondarenko2020.thetaTh_eq_one_iff {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {t : NonemptyInterval T} {w : W} {e : E} : thetaTh τ about P Q t e w = 1 ↔ ∃ (x : X), Q w t x ∧ (τ x).toProd.1 < t.toProd.1 ∧ P w t e ∧ about e = x

θTh's assertion repeats its presupposition, so θTh is true exactly when its assertion holds, (55), (56).

A CP adds no presupposition, §3.1

theorem Bondarenko2020.reportThat_ne_zero {W : Type u_1} {T : Type u_2} {E : Type u_4} {I : Type u_5} [LinearOrder T] {P : W → NonemptyInterval T → E → Prop} {g₁ t : NonemptyInterval T} {w : W} [Anchor E I] (p : I → Prop) : reportThat P p g₁ t w ≠ 0

A report with a CP is defined at every world, so it presupposes nothing about the actual world, §3.1.2.

A nominalized clause presupposes pre-existence, §3.2.3

theorem Bondarenko2020.existsStrong_thetaTh_ne_zero_iff {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {t : NonemptyInterval T} {w : W} [Nonempty E] : (Trivalent.existsStrong fun (e : E) => thetaTh τ about P Q t e w) ≠ 0 ↔ Event.PreExists τ (Q w t) t.toProd.1

The existentially closed θTh-report presupposes pre-existence, (59).

theorem Bondarenko2020.exists_preExists_of_report_ne_zero {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {g₁ t : NonemptyInterval T} {w : W} [Nonempty E] (hpast : ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ t' ≤ g₁) (h : report τ about P Q g₁ t w ≠ 0) : ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ t' ≤ g₁ ∧ Event.PreExists τ (Q w t') t'.toProd.1

Over a nonempty contextual past, the report presupposes that the complement describes something that started before a past thinking time, (62).

theorem Bondarenko2020.report_ne_zero_of_not_exists {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {g₁ t : NonemptyInterval T} {w : W} (hpast : ¬∃ (t' : NonemptyInterval T), t'.Precedes t ∧ t' ≤ g₁) : report τ about P Q g₁ t w ≠ 0

Over an empty contextual past the report is defined whatever the complement describes, so (62) needs the past to be nonempty.

theorem Bondarenko2020.exists_of_report_ne_zero {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {g₁ t : NonemptyInterval T} {w : W} [Nonempty E] (hpast : ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ t' ≤ g₁) (h : report τ about P Q g₁ t w ≠ 0) : ∃ (t' : NonemptyInterval T) (x : X), t'.Precedes t ∧ Q w t' x

The report presupposes that the complement describes something in the world of evaluation, the factive inference (2b), (3).

theorem Bondarenko2020.support_neg_report {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {Q : W → NonemptyInterval T → X → Prop} {g₁ t : NonemptyInterval T} : Function.support (-report τ about P Q g₁ t) = Function.support (report τ about P Q g₁ t)

Negation keeps the presupposition, (15).

theorem Bondarenko2020.existsStrong_thetaTh_comp_ne_zero_iff {W : Type u_1} {T : Type u_2} {X : Type u_3} {E : Type u_4} {I : Type u_5} [LinearOrder T] {τ : X → NonemptyInterval T} {about : E → X} {P : W → NonemptyInterval T → E → Prop} {t : NonemptyInterval T} {w : W} [Nonempty E] [Anchor X I] (p : I → Prop) : (Trivalent.existsStrong fun (e : E) => thetaTh τ about P (fun (x : W) (x_1 : NonemptyInterval T) => Anchor.comp p) t e w) ≠ 0 ↔ Event.PreExists τ (Anchor.comp p) t.toProd.1

With a nominalized CP, a predicate of contentful individuals, the presupposition is that an individual with the content started before the matrix time; it does not depend on the world of evaluation, so it cannot require the content to be true there, (64), (65).

The judgments

Days are integers, Monday 1, Tuesday 2, Wednesday 3 (fn. 3), and the thinking is on Tuesday.