Closure of the eventuality argument

A clause denotes a world-indexed predicate of eventualities until some head closes the eventuality argument existentially. Accounts of complement choice differ on the head: [Gra24] makes it mood, the indicative closing the argument and one subjunctive passing it up, while [FS26] make it a head that a clause-sized infinitive contains and a smaller one lacks. They agree on why it matters. The content of an intention is causally self-referential ([Sea83], [Har76]): it is satisfied only by an eventuality that the intention itself brings about. Such content closes the argument over the eventualities the attitude state causes, which needs the open predicate and cannot be computed from the closed proposition.

Main declarations

• Event.closure: existential closure of the eventuality argument.
• Event.causedClosure: closure over the eventualities a given state causes, the causally self-referential prejacent.

Main statements

• Event.causedClosure_factorsThrough_iff: the causally self-referential prejacent is a function of the closed proposition exactly when causation by the state is trivial at every world, relating the state to every eventuality or to none.

Implementation notes

Causation is a relation cause s e w between two eventualities and a world, as both papers write it. For a fixed world causedClosure is the preimage of the complement's eventualities under the causal relation, mathlib's SetRel.preimage; the relation is kept as a function because it is only ever applied, and the lemmas follow the names of the SetRel.preimage API.

References

• [Gra24]
• [FS26]
• [Sea83]
• [Har76]

def Event.closure {Ev : Type u_1} {W : Type u_2} (P : W → Ev → Prop) (w : W) : Prop

Existential closure of a clause's eventuality argument, yielding a proposition.

Equations

• Event.closure P w = ∃ (e : Ev), P w e

def Event.causedClosure {Ev : Type u_1} {W : Type u_2} (cause : Ev → Ev → W → Prop) (s : Ev) (P : W → Ev → Prop) (w : W) : Prop

Closure of a clause's eventuality argument over the eventualities that the state s causes: the causally self-referential prejacent of an intention ([Sea83]).

Equations

• Event.causedClosure cause s P w = ∃ (e : Ev), cause s e w ∧ P w e

theorem Event.closure_mono {Ev : Type u_1} {W : Type u_2} {P Q : W → Ev → Prop} {w : W} (h : ∀ (e : Ev), P w e → Q w e) : closure P w → closure Q w

theorem Event.causedClosure_mono {Ev : Type u_1} {W : Type u_2} {cause : Ev → Ev → W → Prop} {s : Ev} {P Q : W → Ev → Prop} {w : W} (h : ∀ (e : Ev), cause s e w → P w e → Q w e) : causedClosure cause s P w → causedClosure cause s Q w

theorem Event.causedClosure_mono_left {Ev : Type u_1} {W : Type u_2} {cause cause' : Ev → Ev → W → Prop} {s : Ev} {P : W → Ev → Prop} {w : W} (h : ∀ (e : Ev), cause s e w → cause' s e w) : causedClosure cause s P w → causedClosure cause' s P w

theorem Event.causedClosure.closure {Ev : Type u_1} {W : Type u_2} {cause : Ev → Ev → W → Prop} {s : Ev} {P : W → Ev → Prop} {w : W} (h : causedClosure cause s P w) : Event.closure P w

The causally self-referential prejacent entails the closed proposition.

theorem Event.causedClosure_iff_of_forall {Ev : Type u_1} {W : Type u_2} {cause : Ev → Ev → W → Prop} {s : Ev} {P : W → Ev → Prop} {w : W} (h : ∀ (e : Ev), cause s e w) : causedClosure cause s P w ↔ closure P w

A state that causes every eventuality adds nothing to plain closure.

theorem Event.not_causedClosure_of_forall_not {Ev : Type u_1} {W : Type u_2} {cause : Ev → Ev → W → Prop} {s : Ev} {P : W → Ev → Prop} {w : W} (h : ∀ (e : Ev), ¬cause s e w) : ¬causedClosure cause s P w

A state that causes nothing has an unsatisfiable prejacent.

theorem Event.causedClosure_factorsThrough_iff {Ev : Type u_1} {W : Type u_2} {cause : Ev → Ev → W → Prop} {s : Ev} : Function.FactorsThrough (causedClosure cause s) closure ↔ ∀ (w : W), (∀ (e : Ev), cause s e w) ∨ ∀ (e : Ev), ¬cause s e w

Causal self-reference needs the open eventuality argument. The prejacent is a function of the closed proposition exactly when causation by the state is trivial at every world, relating the state to every eventuality or to none.