Koev (2017): Evidentiality, Learning Events and Spatiotemporal Distance

Koev analyzes the Bulgarian evidential -l as spatiotemporal distance rather than a semantic primitive. An evidential sentence introduces a learning event, through which the speaker acquired the evidence for the claim, and requires it to be spatiotemporally distant from the described event: either not overlapping it in time, as with standard indirect evidence, or located elsewhere, as when smoke from a chimney shows a fire in progress. Direct witness, at the same time and place, is the one configuration the evidential excludes, and the constraint is independent of the ordering that past tense contributes. The evidential implication projects as the presupposition of a trivalent proposition whose assertion is the core proposition, with no modal weakening, against Izvorski.

Main definitions

• spatiotemporallyDistant: the distance condition.
• LearningScenario.toEvidentialProp: the evidential sentence as a trivalent proposition.

Main results

• direct_not_distant: direct witness is not distant.
• smoke_no_tense_ordering: the distance condition holds with simultaneous events.
• projection_past_negation: negation preserves the evidential presupposition.

Implementation notes

• Events carry no location, so the distance predicate takes a location function as a parameter.
• The learning predicate itself, the knowledge change it reports, and the evidence-source typology of §5 are not modelled; the scenarios record only the two events.

References

• [Koe17]
• [Izv97]

def Koev2017.temporallyDisjoint {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] (e₁ e₂ : E) : Prop

Two events are temporally disjoint when their temporal traces do not overlap, the first disjunct of Definition 24.

Equations

• Koev2017.temporallyDisjoint e₁ e₂ = ¬(Event.τ e₁).Overlaps (Event.τ e₂)

def Koev2017.spatiotemporallyDistant {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {L : Type u_3} (loc : E → L) (e₁ e₂ : E) : Prop

Two events are spatiotemporally distant, Definition 24, when they do not overlap in time or occur at different locations.

Equations

• Koev2017.spatiotemporallyDistant loc e₁ e₂ = (Koev2017.temporallyDisjoint e₁ e₂ ∨ loc e₁ ≠ loc e₂)

@[instance_reducible]

instance Koev2017.instDecidableTemporallyDisjointOfDecidableEq {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] [DecidableEq T] (e₁ e₂ : E) : Decidable (temporallyDisjoint e₁ e₂)

Equations

• Koev2017.instDecidableTemporallyDisjointOfDecidableEq e₁ e₂ = { decide := !decide ((Event.τ e₁).Overlaps (Event.τ e₂)), reflects_decide := ⋯ }

@[instance_reducible]

instance Koev2017.instDecidableSpatiotemporallyDistantOfDecidableEq {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {L : Type u_3} [DecidableEq T] [DecidableEq L] (loc : E → L) (e₁ e₂ : E) : Decidable (spatiotemporallyDistant loc e₁ e₂)

Equations

• Koev2017.instDecidableSpatiotemporallyDistantOfDecidableEq loc e₁ e₂ = { decide := decide (Koev2017.temporallyDisjoint e₁ e₂) || decide (loc e₁ ≠ loc e₂), reflects_decide := ⋯ }

theorem Koev2017.temporallyDisjoint_of_precedes {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {e₁ e₂ : E} (h : (Event.τ e₁).Precedes (Event.τ e₂)) : temporallyDisjoint e₁ e₂

An event that precedes another is temporally disjoint from it, as in standard indirect evidence, where the described event is over before the learning event begins.

structure Koev2017.LearningScenario (E : Type u_4) : Type u_4

A learning scenario pairs the described event with the learning event through which the speaker acquired the evidence for the claim, (74b).

• described : E

  The described event.

• learning : E

  The learning event.

noncomputable def Koev2017.LearningScenario.toEvidentialProp {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {L : Type u_3} (loc : E → L) (s : LearningScenario E) {W : Type u_4} (p : W → Prop) : W → SignType

The evidential sentence is a trivalent proposition whose presupposition is the distance condition of the learning event, which restricts the context set, (74b), and whose assertion is the core proposition, to which the declarative operator (72) commits the speaker.

Equations

• Koev2017.LearningScenario.toEvidentialProp loc s p = {_w : W | Koev2017.spatiotemporallyDistant loc s.described s.learning}.indicator fun (w : W) => SignType.ofProp (p w)

theorem Koev2017.projection_past_negation {T : Type u_1} {E : Type u_2} [LinearOrder T] [Event.TemporalTrace E T] {L : Type u_3} (loc : E → L) (s : LearningScenario E) {W : Type u_4} (p : W → Prop) : Function.support (-LearningScenario.toEvidentialProp loc s p) = Function.support (LearningScenario.toEvidentialProp loc s p)

Negation preserves the evidential presupposition while negating the core proposition, (78).

The scenarios of §4

inductive Koev2017.Place : Type

A Place locates the events of the scenarios.

• here : Place
• there : Place

@[instance_reducible]

instance Koev2017.instDecidableEqPlace : DecidableEq Place

Equations

• Koev2017.instDecidableEqPlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Koev2017.instReprPlace.repr : Place → ℕ → Std.Format

Equations

• Koev2017.instReprPlace.repr Koev2017.Place.here prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Place.here")).group prec✝
• Koev2017.instReprPlace.repr Koev2017.Place.there prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Place.there")).group prec✝

@[instance_reducible]

instance Koev2017.instReprPlace : Repr Place

Equations

• Koev2017.instReprPlace = { reprPrec := Koev2017.instReprPlace.repr }

inductive Koev2017.Ev : Type

The events of the scenarios are the described event and the learning events of standard indirect evidence, of direct witness, and of seeing smoke from the chimney.

• described : Ev
• learnIndirect : Ev
• learnDirect : Ev
• learnSmoke : Ev

@[instance_reducible]

instance Koev2017.instDecidableEqEv : DecidableEq Ev

Equations

• Koev2017.instDecidableEqEv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Koev2017.instReprEv : Repr Ev

Equations

• Koev2017.instReprEv = { reprPrec := Koev2017.instReprEv.repr }

def Koev2017.instReprEv.repr : Ev → ℕ → Std.Format

Equations

• Koev2017.instReprEv.repr Koev2017.Ev.described prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Ev.described")).group prec✝
• Koev2017.instReprEv.repr Koev2017.Ev.learnIndirect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Ev.learnIndirect")).group prec✝
• Koev2017.instReprEv.repr Koev2017.Ev.learnDirect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Ev.learnDirect")).group prec✝
• Koev2017.instReprEv.repr Koev2017.Ev.learnSmoke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Koev2017.Ev.learnSmoke")).group prec✝

@[instance_reducible]

instance Koev2017.instTemporalTraceEvInt : Event.TemporalTrace Ev ℤ

The described event runs over [0, 5]; the speaker learns of it afterwards, witnesses it during [2, 4], or sees the smoke over the same interval [0, 5].

Equations

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

def Koev2017.indirect : LearningScenario Ev

In standard indirect evidence, (25a), the speaker learns of the event afterwards.

Equations

• Koev2017.indirect = { described := Koev2017.Ev.described, learning := Koev2017.Ev.learnIndirect }

def Koev2017.direct : LearningScenario Ev

In direct witness the speaker perceives the event as it happens, in the same place.

Equations

• Koev2017.direct = { described := Koev2017.Ev.described, learning := Koev2017.Ev.learnDirect }

def Koev2017.smoke : LearningScenario Ev

With smoke from the chimney, (25b), the speaker perceives the evidence at the same time from elsewhere.

Equations

• Koev2017.smoke = { described := Koev2017.Ev.described, learning := Koev2017.Ev.learnSmoke }

def Koev2017.loc : Ev → Place

The location of every event is here except the seeing of the smoke.

Equations

• Koev2017.loc Koev2017.Ev.learnSmoke = Koev2017.Place.there
• Koev2017.loc x✝ = Koev2017.Place.here

theorem Koev2017.felicity : spatiotemporallyDistant loc indirect.described indirect.learning ∧ spatiotemporallyDistant loc smoke.described smoke.learning ∧ ¬spatiotemporallyDistant loc direct.described direct.learning

The evidential is felicitous with indirect evidence, by temporal disjointness, and with smoke from the chimney, by spatial distance alone, and infelicitous under direct witness.

theorem Koev2017.direct_not_distant {L : Type u_3} (loc : Ev → L) (h : loc direct.described = loc direct.learning) : ¬spatiotemporallyDistant loc direct.described direct.learning

Direct witness fails both disjuncts of Definition 24.

theorem Koev2017.smoke_no_tense_ordering : (Event.τ indirect.described).Precedes (Event.τ indirect.learning) ∧ ¬(Event.τ smoke.described).Precedes (Event.τ smoke.learning) ∧ temporallyDisjoint indirect.described indirect.learning ∧ ¬temporallyDisjoint smoke.described smoke.learning

The two constraints of (74b) are independent. Past tense orders the described event before the learning event in the indirect scenario, while the smoke scenario satisfies the distance condition with the two events simultaneous.