Phasal verbs

This file defines the meaning of the phasal verbs stop, start and continue. Such a verb takes a state description P and relates two indices: it asserts that P holds, or fails, at the index of evaluation, and presupposes that P held, or failed, at an earlier one. The indices may be times, eventualities or world-time pairs, so the relation R of an index to the earlier ones is a parameter, as it is for the repetitive presupposition of again, and the presupposition is possibility along it, ◇[R] of Logic/Modal.

The three classes differ only in the polarity they require of the prior state and of the result state (Phasal.Prior, Phasal.Result). An inception that is true is Dowty's BECOME, a state that holds having failed before (denote_inception_eq_one_iff). A cessation is the inception of the complementary state (denote_cessation_eq_inception) and the negation of a continuation (denote_cessation_eq_neg), and a continuation is again applied to the state (denote_continuation). Where R relates an index to every earlier one a state may have both held and failed before, so that a cessation and an inception of it are both defined; the two exclude one another exactly where the prior index is unique (forall_denote_cessation_eq_zero_or_inception_eq_zero_iff).

Main definitions

• Aspect.Phasal: the three classes of phasal verb, cessation, inception and continuation.
• Aspect.Phasal.Transition: the truth condition of a class on a prior and a result state.
• Aspect.Phasal.denote: the trivalent proposition of a class, a relation to the earlier indices and a state description.
• Aspect.Become: a state holds at an index and fails at an earlier one.

Main results

• Aspect.Phasal.denote_eq_one_iff: a phasal verb is true where some earlier index and the index of evaluation stand in its transition.
• Aspect.Phasal.result_iff_not_prior: the classes other than continuation are changes, the result state having the opposite polarity to the prior state.
• Aspect.Phasal.forall_denote_cessation_eq_zero_or_inception_eq_zero_iff: no state can both stop and start at an index exactly when the index has at most one earlier index.

References

• [Dow79]
• [vS96]

inductive Aspect.Phasal : Type

The classes of phasal verb by the prior state presupposed and the result state asserted, which are cessation (stop, quit, cease), inception (start, begin) and continuation (continue, keep).

• cessation : Phasal
• inception : Phasal
• continuation : Phasal

@[instance_reducible]

instance Aspect.instDecidableEqPhasal : DecidableEq Phasal

Equations

• Aspect.instDecidableEqPhasal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aspect.instReprPhasal : Repr Phasal

Equations

• Aspect.instReprPhasal = { reprPrec := Aspect.instReprPhasal.repr }

def Aspect.instReprPhasal.repr : Phasal → ℕ → Std.Format

Equations

• Aspect.instReprPhasal.repr Aspect.Phasal.cessation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.Phasal.cessation")).group prec✝
• Aspect.instReprPhasal.repr Aspect.Phasal.inception prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.Phasal.inception")).group prec✝
• Aspect.instReprPhasal.repr Aspect.Phasal.continuation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aspect.Phasal.continuation")).group prec✝

@[instance_reducible]

instance Aspect.instInhabitedPhasal : Inhabited Phasal

Equations

• Aspect.instInhabitedPhasal = { default := Aspect.instInhabitedPhasal.default }

def Aspect.Become {ι : Type u_1} (R : SetRel ι ι) (P : ι → Prop) (i : ι) : Prop

Become R P holds at an index where P holds and which R relates to an index where P fails, an earlier one.

Equations

• Aspect.Become R P i = (ModalLogic.Diamond R (fun (i' : ι) => ¬P i') i ∧ P i)

def Aspect.Phasal.Prior : Phasal → Prop → Prop

t.Prior p is what the class t requires of the prior state p, that it held or, for an inception, that it did not.

Equations

• Aspect.Phasal.cessation.Prior x✝ = x✝
• Aspect.Phasal.inception.Prior x✝ = ¬x✝
• Aspect.Phasal.continuation.Prior x✝ = x✝

def Aspect.Phasal.Result : Phasal → Prop → Prop

t.Result p is what the class t requires of the result state p, that it holds or, for a cessation, that it does not.

Equations

• Aspect.Phasal.cessation.Result x✝ = ¬x✝
• Aspect.Phasal.inception.Result x✝ = x✝
• Aspect.Phasal.continuation.Result x✝ = x✝

def Aspect.Phasal.Transition (t : Phasal) (p q : Prop) : Prop

t.Transition p q is the truth condition of the class t on a prior state p and a result state q.

Equations

• t.Transition p q = (t.Prior p ∧ t.Result q)

@[instance_reducible]

instance Aspect.Phasal.instDecidablePrior (t : Phasal) (p : Prop) [Decidable p] : Decidable (t.Prior p)

Equations

• Aspect.Phasal.cessation.instDecidablePrior x✝¹ = x✝
• Aspect.Phasal.inception.instDecidablePrior x✝¹ = { decide := !decide x✝¹, reflects_decide := ⋯ }
• Aspect.Phasal.continuation.instDecidablePrior x✝¹ = x✝

@[instance_reducible]

instance Aspect.Phasal.instDecidableResult (t : Phasal) (p : Prop) [Decidable p] : Decidable (t.Result p)

Equations

• Aspect.Phasal.cessation.instDecidableResult x✝¹ = { decide := !decide x✝¹, reflects_decide := ⋯ }
• Aspect.Phasal.inception.instDecidableResult x✝¹ = x✝
• Aspect.Phasal.continuation.instDecidableResult x✝¹ = x✝

@[instance_reducible]

instance Aspect.Phasal.instDecidableTransition {p q : Prop} (t : Phasal) [Decidable p] [Decidable q] : Decidable (t.Transition p q)

Equations

• t.instDecidableTransition = { decide := decide (t.Prior p) && decide (t.Result q), reflects_decide := ⋯ }

@[simp]

theorem Aspect.Phasal.prior_cessation {p : Prop} : cessation.Prior p ↔ p

@[simp]

theorem Aspect.Phasal.prior_inception {p : Prop} : inception.Prior p ↔ ¬p

@[simp]

theorem Aspect.Phasal.prior_continuation {p : Prop} : continuation.Prior p ↔ p

@[simp]

theorem Aspect.Phasal.result_cessation {p : Prop} : cessation.Result p ↔ ¬p

@[simp]

theorem Aspect.Phasal.result_inception {p : Prop} : inception.Result p ↔ p

@[simp]

theorem Aspect.Phasal.result_continuation {p : Prop} : continuation.Result p ↔ p

theorem Aspect.Phasal.transition_iff {p q : Prop} (t : Phasal) : t.Transition p q ↔ t.Prior p ∧ t.Result q

theorem Aspect.Phasal.result_iff_not_prior {p : Prop} {t : Phasal} (ht : t ≠ continuation) : t.Result p ↔ ¬t.Prior p

A cessation and an inception are changes, the result state having the opposite polarity to the prior state.

theorem Aspect.Phasal.result_continuation_eq_prior : continuation.Result = continuation.Prior

A continuation is no change, the result state having the polarity of the prior state.

theorem Aspect.Phasal.not_transition_cessation_of_continuation {p q : Prop} (h : continuation.Transition p q) : ¬cessation.Transition p q

No state is left by one transition and continued by another.

noncomputable def Aspect.Phasal.denote {ι : Type u_1} (t : Phasal) (R : SetRel ι ι) (P : ι → Prop) : ι → SignType

t.denote R P asserts the result state of P at an index and presupposes its prior state at one of the indices that R relates it to, the earlier ones.

Equations

• t.denote R P = {i : ι | ModalLogic.Diamond R (fun (i : ι) => t.Prior (P i)) i}.indicator fun (i : ι) => SignType.ofProp (t.Result (P i))

@[simp]

theorem Aspect.Phasal.denote_eq_zero_iff {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} {i : ι} {t : Phasal} : t.denote R P i = 0 ↔ ¬ModalLogic.Diamond R (fun (i : ι) => t.Prior (P i)) i

theorem Aspect.Phasal.denote_eq_one_iff {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} {i : ι} {t : Phasal} : t.denote R P i = 1 ↔ ∃ (i' : ι), (i, i') ∈ R ∧ t.Transition (P i') (P i)

A phasal verb is true where an earlier index and the index of evaluation stand in its transition.

theorem Aspect.Phasal.denote_inception_eq_one_iff {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} {i : ι} : inception.denote R P i = 1 ↔ Become R P i

An inception that is true is a becoming.

theorem Aspect.Phasal.denote_continuation {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} : continuation.denote R P = Presupposition.again R P

A continuation is again applied to the state.

theorem Aspect.Phasal.denote_cessation_eq_neg {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} : cessation.denote R P = -continuation.denote R P

A cessation is the negation of a continuation, the two sharing the presupposition that the state held.

theorem Aspect.Phasal.denote_cessation_eq_inception {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} : cessation.denote R P = inception.denote R fun (i : ι) => ¬P i

A cessation is the inception of the complementary state.

theorem Aspect.Phasal.denote_cessation_eq_one_iff {ι : Type u_1} {R : SetRel ι ι} {P : ι → Prop} {i : ι} : cessation.denote R P i = 1 ↔ Become R (fun (i : ι) => ¬P i) i

A cessation that is true is the becoming of the complementary state.

theorem Aspect.Phasal.forall_denote_cessation_eq_zero_or_inception_eq_zero_iff {ι : Type u_1} {R : SetRel ι ι} {i : ι} : (∀ (P : ι → Prop), cessation.denote R P i = 0 ∨ inception.denote R P i = 0) ↔ ∀ ⦃j : ι⦄, (i, j) ∈ R → ∀ ⦃k : ι⦄, (i, k) ∈ R → j = k

A cessation and an inception presuppose contradictory prior states, though possibly of different earlier indices, so that for no state are both defined at an index exactly when the index has at most one earlier index.