White (2014): Factive-Implicatives and Modalized Complements

This file formalizes [Whi14]'s account of the factive-implicatives remember and forget, factive with a finite complement and implicative with a control infinitive (1). The verb is one item and always factive: the infinitival complement is headed by a modal complementizer that contributes the presuppositional modality (Modalized), so remembered to take the trash out presupposes that Bo had to, as remembered that he had to does (7). The attitude is a Hintikkan quantifier over the worlds a memory event gives access to (19), and the modal complementizer, unlike that, returns a property of events (26). The Rule of Semantic Restructuring puts the two together, applying the attitude to the property at the embedded event and summing that event with the attitude's into one compound event (27) (restructure), which matrix aspect binds in the actual world (30). Implicative entailments are then actuality entailments: a part of an actual compound event is actual, so the remembered VP-event occurred (actuality), and with negation above aspect no actual event is a remembering-to-VP (negated_actuality). A finite complement closes its own event below the complementizer (23), (24), so the finite variant leaves the event's actuality open (exists_finite_not_actual).

Implementation notes

The attitude's memory relation and the modal's best worlds are accessibility relations with event arguments ([Kra96], [Hac09]); the compound event is the join of its parts, and actual events are closed under parts and joins. The step from an actual event described as a VP-event in the accessible worlds to its being a VP-event in the actual world is the hypothesis EventDescriptionPreserved, with events persisting into accessible worlds. The again modification facts of the restructuring test and the coordination data are recorded as examples only.

References

• [Whi14]
• [Bha99]
• [Hac09]
• [Kar71a]
• [Kra96]
• [Wur14]

The modal complementizer

def White2014.Modalized (fr : ArgumentFrame) : Prop

Which complements are headed by the modal complementizer: the nonfinite ones.

Equations

• White2014.Modalized fr = ¬fr.HasFinite

@[instance_reducible]

instance White2014.instDecidablePredArgumentFrameModalized : DecidablePred Modalized

Equations

• White2014.instDecidablePredArgumentFrameModalized x✝ = { decide := !decide x✝.HasFinite, reflects_decide := ⋯ }

theorem White2014.modalized_infinitival_not_finite : Modalized ArgumentFrame.infinitival ∧ ¬Modalized ArgumentFrame.finiteClause

The control infinitive of (1b) is modalized, the finite clause of (1a) not.

Attitude, modal complementizer, and restructuring

def White2014.attitude {W : Type u_1} {E : Type u_2} (mem : E → W → Set W) (p : W → Prop) (e : E) (w : W) : Prop

The attitude (19): the proposition holds in every world the memory event gives access to.

Equations

• White2014.attitude mem p e w = ∀ w' ∈ mem e w, p w'

def White2014.cMod {W : Type u_1} {E : Type u_2} (best : W → Set W) (f : E → W → Prop) (e : E) (w : W) : Prop

The modal complementizer (26): a property of events holding of the event in every best world.

Equations

• White2014.cMod best f e w = ∀ w' ∈ best w, f e w'

def White2014.restructure {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (att : (W → Prop) → E → W → Prop) (f : E → W → Prop) (e₀ : E) (w : W) : Prop

The Rule of Semantic Restructuring (27): the attitude applied to the property at the embedded event, the two events summed into one compound event.

Equations

• White2014.restructure att f e₀ w = ∃ (e₁ : E) (e₂ : E), e₀ = e₁ ⊔ e₂ ∧ att (f e₂) e₁ w

theorem White2014.restructure_attitude_cMod {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (mem : E → W → Set W) (best : W → Set W) (vp : E → W → Prop) (e₀ : E) (w : W) : restructure (attitude mem) (cMod best vp) e₀ w ↔ ∃ (e₁ : E) (e₂ : E), e₀ = e₁ ⊔ e₂ ∧ ∀ w' ∈ mem e₁ w, ∀ w'' ∈ best w', vp e₂ w''

(28): remember restructured with the modalized complement.

def White2014.rememberedTo {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (occurs : E → W → Prop) (mem : E → W → Set W) (best : W → Set W) (vp : E → W → Prop) (w : W) : Prop

(30): Bo remembered to VP, with matrix aspect binding the compound event in the evaluation world.

Equations

• White2014.rememberedTo occurs mem best vp w = ∃ (e₀ : E), occurs e₀ w ∧ White2014.restructure (White2014.attitude mem) (White2014.cMod best vp) e₀ w

def White2014.rememberedThat {W : Type u_1} {E : Type u_2} (mem : E → W → Set W) (vp : E → W → Prop) (e : E) (w : W) : Prop

(24): Bo remembered that he VPed, whose complement closes its own event.

Equations

• White2014.rememberedThat mem vp e w = White2014.attitude mem (fun (w' : W) => ∃ (e' : E), vp e' w') e w

def White2014.EventDescriptionPreserved {W : Type u_1} {E : Type u_2} (occurs vp : E → W → Prop) : Prop

Preservation of event description: an event occurring in two worlds is described by the same predicate in both.

Equations

• White2014.EventDescriptionPreserved occurs vp = ∀ (e : E) (w w' : W), occurs e w → occurs e w' → vp e w → vp e w'

def White2014.Persists {W : Type u_1} {E : Type u_2} (occurs : E → W → Prop) (acc : W → Set W) : Prop

Events persist into the accessible worlds.

Equations

• White2014.Persists occurs acc = ∀ (e : E) (w w' : W), occurs e w → w' ∈ acc w → occurs e w'

def White2014.PartsOccur {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (occurs : E → W → Prop) : Prop

The actual events are closed under parts.

Equations

• White2014.PartsOccur occurs = ∀ (e e' : E) (w : W), e ≤ e' → occurs e' w → occurs e w

def White2014.JoinsOccur {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (occurs : E → W → Prop) : Prop

The actual events are closed under joins.

Equations

• White2014.JoinsOccur occurs = ∀ (e e' : E) (w : W), occurs e w → occurs e' w → occurs (e ⊔ e') w

theorem White2014.actuality {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {occurs : E → W → Prop} {mem : E → W → Set W} {best : W → Set W} {vp : E → W → Prop} (hpart : PartsOccur occurs) (hped : EventDescriptionPreserved occurs vp) (hmem : Persists occurs fun (w : W) => ⋃ (e : E), mem e w) (hbest : Persists occurs best) (hne : ∀ (e : E) (w : W), ∃ w' ∈ mem e w, (best w').Nonempty) {w : W} (h : rememberedTo occurs mem best vp w) : ∃ (e : E), occurs e w ∧ vp e w

The positive implicative entailment as an actuality entailment: the VP-event is part of an actual compound event, so it is actual, and it is a VP-event there.

theorem White2014.negated_actuality {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {occurs : E → W → Prop} {mem : E → W → Set W} {best : W → Set W} {vp : E → W → Prop} (hjoin : JoinsOccur occurs) (hped : EventDescriptionPreserved occurs vp) (hmem : Persists occurs fun (w : W) => ⋃ (e : E), mem e w) (hbest : Persists occurs best) {w : W} {e₁ : E} (he₁ : occurs e₁ w) (h : ¬rememberedTo occurs mem best vp w) : ¬∃ (e : E), occurs e w ∧ vp e w

The negative implicative entailment (31): with negation above aspect no actual event is a remembering-to-VP, so an actual VP-event is excluded, given an actual memory event whose accessible worlds it would persist into.

theorem White2014.exists_finite_not_actual : ∃ (mem : Unit → Bool → Set Bool) (vp : Unit → Bool → Prop) (occurs : Unit → Bool → Prop), rememberedThat mem vp () true ∧ ¬∃ (e : Unit), occurs e true ∧ vp e true

No actuality entailment with a finite complement (32): the remembered content can hold while no VP-event is actual.