Beavers et al. (2021): States and Changes of State

This file formalizes the argument of Beavers and colleagues that some roots entail change. A property-concept root, such as that of bright, describes a state that need not have come about. A result root, such as that of shatter, describes a state that always arises from a change (EventStructure.Interpretation.EntailsChange). This contradicts the Bifurcation Thesis, on which change is introduced by the verbal template and never by a root.

A root entails change exactly when its stative cannot be conjoined with a denial of change (entailsChange_iff_forall_not_deniesChange), and with such a root restitutive again presupposes an earlier change. The morphology follows from a default realization rule: a verb is unmarked iff its root entails change, and a stative is unmarked iff its complement does not, and in a model that respects a root's signature the rule agrees with the semantics (entailsChange_of_verbRealization_eq_unmarked). A language that spells out the unmarked form only when it spells out the marked one belongs to one of the three attested types (Exponence.trichotomy).

Implementation notes

• The semantics is stated on EventStructure.Interpretation, which interprets the primitives of Beavers and Koontz-Garboden's book, and again is Presupposition.again.
• The realization rule reads whether a root entails change off its kind signature.
• The tables of the typological survey are not represented. Its coding of markedness is (Code.IsMarked).

References

• [BEJ+21]
• [BKG20]
• [Emb09]
• [Ara05]
• [Has93]

State predicates that entail change

def BeaversEtAl2021.resultStative {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) (P : Entity → State → Prop) (x : Entity) (s : State) : Prop

The deverbal stative of P holds of the states of which P holds and that a change gave rise to.

Equations

• BeaversEtAl2021.resultStative M P x s = (P x s ∧ ∃ (e : Event), M.become s e)

def BeaversEtAl2021.DeniesChange {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) (P : Entity → State → Prop) (x : Entity) (s : State) : Prop

The stative description P holds of x in the state s, and no change gave rise to s.

Equations

• BeaversEtAl2021.DeniesChange M P x s = (P x s ∧ ¬∃ (e : Event), M.become s e)

theorem BeaversEtAl2021.not_deniesChange_resultStative {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) {P : Entity → State → Prop} {x : Entity} {s : State} : ¬DeniesChange M (resultStative M P) x s

A deverbal stative never survives the denial of change, whatever its root.

theorem BeaversEtAl2021.entailsChange_iff_forall_not_deniesChange {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) {P : Entity → State → Prop} : M.EntailsChange P ↔ ∀ (x : Entity) (s : State), ¬DeniesChange M P x s

A state predicate entails change iff it never survives the denial of change.

theorem BeaversEtAl2021.resultStative_iff {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) {P : Entity → State → Prop} {x : Entity} {s : State} (h : M.EntailsChange P) : resultStative M P x s ↔ P x s

For a state predicate that entails change the basic and the deverbal stative coincide.

theorem BeaversEtAl2021.exists_become_of_againAt_achievement_ne_zero {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) {R : SetRel Event Event} {P : Entity → State → Prop} {y x : Entity} {e : Event} (hp : BeaversKoontzGarboden2020.againAt M ArgumentStructure.EventStructure.Template.achievement R P y x e ≠ 0) : ∃ (e' : Event), (e, e') ∈ R ∧ ∃ (s : State), M.become s e'

Again attached to vbecome presupposes an earlier change with every root.

A knife forged sharp

def BeaversEtAl2021.forged : ArgumentStructure.EventStructure.Interpretation Unit Bool Unit

A knife forged sharp is sharp in its first state false, and in its later state true, which a sharpening gave rise to.

Equations

• BeaversEtAl2021.forged = { become := fun (s : Bool) (x : Unit) => s = true, cause := fun (x x_1 : Unit) => False, effector := fun (x x_1 : Unit) => False }

def BeaversEtAl2021.sharp : Unit → Bool → Prop

The knife is sharp in both of its states.

Equations

• BeaversEtAl2021.sharp x✝¹ x✝ = True

theorem BeaversEtAl2021.forged_deniesChange : DeniesChange forged sharp () false

The forged state of the knife survives the denial of change.

theorem BeaversEtAl2021.not_entailsChange_sharp : ¬forged.EntailsChange sharp

Being sharp does not entail change.

theorem BeaversEtAl2021.forged_restitutive : BeaversKoontzGarboden2020.againAt forged ArgumentStructure.EventStructure.Template.state {p : ArgumentStructure.EventStructure.Eventuality.Carrier Bool Unit ArgumentStructure.EventStructure.Eventuality.state × ArgumentStructure.EventStructure.Eventuality.Carrier Bool Unit ArgumentStructure.EventStructure.Eventuality.state | p.2 < p.1} sharp () () true ≠ 0 ∧ ¬∃ s' < true, ∃ (e : Unit), forged.become s' e

The restitutive presupposition holds at the later state of the knife although no change gave rise to an earlier one.

Default realization

inductive BeaversEtAl2021.Markedness : Type

The realization of a head in a category is the form for the unmarked semantic association or the form for the marked one.

• unmarked : Markedness
• marked : Markedness

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqMarkedness : DecidableEq Markedness

Equations

• BeaversEtAl2021.instDecidableEqMarkedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaversEtAl2021.instReprMarkedness.repr : Markedness → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprMarkedness : Repr Markedness

Equations

• BeaversEtAl2021.instReprMarkedness = { reprPrec := BeaversEtAl2021.instReprMarkedness.repr }

inductive BeaversEtAl2021.AdjectivalStructure : Type

The two structures of a stative.

• basic : AdjectivalStructure

  The stative head over the bare root.

• result : AdjectivalStructure

  The stative head over a vbecome phrase.

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqAdjectivalStructure : DecidableEq AdjectivalStructure

Equations

• BeaversEtAl2021.instDecidableEqAdjectivalStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversEtAl2021.instReprAdjectivalStructure : Repr AdjectivalStructure

Equations

• BeaversEtAl2021.instReprAdjectivalStructure = { reprPrec := BeaversEtAl2021.instReprAdjectivalStructure.repr }

def BeaversEtAl2021.instReprAdjectivalStructure.repr : AdjectivalStructure → ℕ → Std.Format

Equations

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

def BeaversEtAl2021.verbRealization (r : Semantics.Root) : Markedness

The default realization of vbecome over a root is unmarked iff the root entails change.

Equations

• BeaversEtAl2021.verbRealization r = if Semantics.Root.Kind.result ∈ r.closedKinds then BeaversEtAl2021.Markedness.unmarked else BeaversEtAl2021.Markedness.marked

def BeaversEtAl2021.stativeRealization (r : Semantics.Root) : AdjectivalStructure → Markedness

The default realization of the stative head is marked iff its complement entails change, as a vbecome phrase always does.

Equations

• One or more equations did not get rendered due to their size.
• BeaversEtAl2021.stativeRealization r BeaversEtAl2021.AdjectivalStructure.result = BeaversEtAl2021.Markedness.marked

theorem BeaversEtAl2021.verbRealization_ne_stativeRealization_basic {r : Semantics.Root} : verbRealization r ≠ stativeRealization r AdjectivalStructure.basic

The verb and the simple stative of a root are realized as mirror images.

theorem BeaversEtAl2021.stativeRealization_eq_unmarked_iff {r : Semantics.Root} {a : AdjectivalStructure} : stativeRealization r a = Markedness.unmarked ↔ a = AdjectivalStructure.basic ∧ Semantics.Root.Kind.result ∉ r.closedKinds

An unmarked stative is the simple stative of a root that does not entail change, so result roots lack one.

theorem BeaversEtAl2021.entailsChange_of_verbRealization_eq_unmarked {r : Semantics.Root} {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} (h : M.Respects P Q r.kinds) (hr : verbRealization r = Markedness.unmarked) : M.EntailsChange P

The realization rule and the semantics agree. In a model that respects the signature of a root for its state predicate, a root whose verb is realized unmarked entails change.

structure BeaversEtAl2021.Exponence : Type

A language's spell-out of the two realizations, in which the unmarked one is overt only if the marked one is.

• Overt : Markedness → Prop

  The realization is spelled out overtly.

• overt_marked : self.Overt Markedness.unmarked → self.Overt Markedness.marked

  The unmarked realization is overt only if the marked one is.

theorem BeaversEtAl2021.Exponence.trichotomy (L : Exponence) : ¬L.Overt Markedness.unmarked ∧ L.Overt Markedness.marked ∨ L.Overt Markedness.unmarked ∧ L.Overt Markedness.marked ∨ ¬L.Overt Markedness.unmarked ∧ ¬L.Overt Markedness.marked

A language is asymmetric, with only the marked realization overt, equipollent, with both overt, or labile, with neither.

theorem BeaversEtAl2021.Exponence.not_reverse_asymmetric {r p : Semantics.Root} (L : Exponence) (hr : Semantics.Root.Kind.result ∈ r.closedKinds) (hp : Semantics.Root.Kind.result ∉ p.closedKinds) : ¬(L.Overt (verbRealization r) ∧ ¬L.Overt (verbRealization p))

No language is the reverse of English, with overt verbs for the roots that entail change and bare verbs for those that do not.

The coding of the survey

inductive BeaversEtAl2021.ParadigmPosition : Type

The five positions of a root's paradigm.

• underlyingRoot : ParadigmPosition
• simpleStative : ParadigmPosition
• inchoative : ParadigmPosition
• causative : ParadigmPosition
• resultStative : ParadigmPosition

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqParadigmPosition : DecidableEq ParadigmPosition

Equations

• BeaversEtAl2021.instDecidableEqParadigmPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversEtAl2021.instFintypeParadigmPosition : Fintype ParadigmPosition

Equations

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

def BeaversEtAl2021.instReprParadigmPosition.repr : ParadigmPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprParadigmPosition : Repr ParadigmPosition

Equations

• BeaversEtAl2021.instReprParadigmPosition = { reprPrec := BeaversEtAl2021.instReprParadigmPosition.repr }

inductive BeaversEtAl2021.MorphRelation : Type

The relation of a form X to a member Y of its paradigm.

• input : MorphRelation

  The code i says that X is the input to a rule forming Y.

• derived : MorphRelation

  The code d says that X is the output of a rule on Y.

• transitive : MorphRelation

  The code t says that X is related to Y through a series of input and output pairs.

• labile : MorphRelation

  The code l says that X and Y are labile.

• equipollent : MorphRelation

  The code e says that X and Y are equipollent.

• unrelated : MorphRelation

  The code u says that no other relation applies.

• unattested : MorphRelation

  The code n says that Y is unattested.

• same : MorphRelation

  The code s says that X is Y.

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqMorphRelation : DecidableEq MorphRelation

Equations

• BeaversEtAl2021.instDecidableEqMorphRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaversEtAl2021.instReprMorphRelation.repr : MorphRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprMorphRelation : Repr MorphRelation

Equations

• BeaversEtAl2021.instReprMorphRelation = { reprPrec := BeaversEtAl2021.instReprMorphRelation.repr }

@[reducible, inline]

abbrev BeaversEtAl2021.Code : Type

The code of a form gives its relation to each position of its paradigm.

Equations

• BeaversEtAl2021.Code = (BeaversEtAl2021.ParadigmPosition → BeaversEtAl2021.MorphRelation)

def BeaversEtAl2021.Code.of (a b c d e : MorphRelation) : Code

The code with the given relations to the five positions, in their order.

Equations

• BeaversEtAl2021.Code.of a b c d e BeaversEtAl2021.ParadigmPosition.underlyingRoot = a
• BeaversEtAl2021.Code.of a b c d e BeaversEtAl2021.ParadigmPosition.simpleStative = b
• BeaversEtAl2021.Code.of a b c d e BeaversEtAl2021.ParadigmPosition.inchoative = c
• BeaversEtAl2021.Code.of a b c d e BeaversEtAl2021.ParadigmPosition.causative = d
• BeaversEtAl2021.Code.of a b c d e BeaversEtAl2021.ParadigmPosition.resultStative = e

def BeaversEtAl2021.Code.IsMarked (c : Code) : Prop

A form is marked when it is derived from or equipollent to another member of its paradigm; a form with only the other relations is unmarked.

Equations

• c.IsMarked = ∃ (k : BeaversEtAl2021.ParadigmPosition), c k = BeaversEtAl2021.MorphRelation.derived ∨ c k = BeaversEtAl2021.MorphRelation.equipollent

@[instance_reducible]

instance BeaversEtAl2021.instDecidablePredCodeIsMarked : DecidablePred Code.IsMarked

Equations

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

def BeaversEtAl2021.VerbalParadigmMarked (inchoative causative : Code) : Prop

A root's verbal paradigm is marked when its inchoative and its causative both are.

Equations

• BeaversEtAl2021.VerbalParadigmMarked inchoative causative = (inchoative.IsMarked ∧ causative.IsMarked)

@[instance_reducible]

instance BeaversEtAl2021.instDecidableVerbalParadigmMarked (i c : Code) : Decidable (VerbalParadigmMarked i c)

Equations

• BeaversEtAl2021.instDecidableVerbalParadigmMarked i c = { decide := decide i.IsMarked && decide c.IsMarked, reflects_decide := ⋯ }

theorem BeaversEtAl2021.tzeltal_small : ¬(Code.of MorphRelation.unattested MorphRelation.same MorphRelation.input MorphRelation.transitive MorphRelation.transitive).IsMarked ∧ VerbalParadigmMarked (Code.of MorphRelation.unattested MorphRelation.derived MorphRelation.same MorphRelation.input MorphRelation.input) (Code.of MorphRelation.unattested MorphRelation.transitive MorphRelation.derived MorphRelation.same MorphRelation.equipollent) ∧ (Code.of MorphRelation.unattested MorphRelation.transitive MorphRelation.derived MorphRelation.equipollent MorphRelation.same).IsMarked

In the Tzeltal paradigm of 'small' the simple stative tut is unmarked, and the verbs tut-ub and tut-ub-tes and the deverbal stative tut-ub-en are marked.

theorem BeaversEtAl2021.oromo_long : (Code.of MorphRelation.derived MorphRelation.same MorphRelation.equipollent MorphRelation.equipollent MorphRelation.unattested).IsMarked ∧ VerbalParadigmMarked (Code.of MorphRelation.derived MorphRelation.equipollent MorphRelation.same MorphRelation.equipollent MorphRelation.unattested) (Code.of MorphRelation.derived MorphRelation.equipollent MorphRelation.equipollent MorphRelation.same MorphRelation.unattested)

In the Oromo paradigm of 'long' every form is built on the underlying root dheer-, so the simple stative dheer-aa is marked along with the verbs.

The judgments

theorem BeaversEtAl2021.changeDenial_acceptable_iff (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" = some "change denial" → e.feature? "judgedBy" ≠ some "some speakers" → (e.judgment = Judgment.acceptable ↔ e.feature? "root class" = some "property concept")

A stative survives the denial of change in the examples exactly when its root is a property-concept root, setting aside (13), acceptable only to the speakers for whom broken has drifted to a 'not functioning' sense.

theorem BeaversEtAl2021.restitutive_unacceptable_of_result (e : Datum) : e ∈ Examples.all → e.feature? "diagnostic" = some "restitutive again" → e.language ≠ "cash1251" → e.feature? "root class" = some "result" → e.judgment = Judgment.unacceptable

Outside Kakataibo no result root is accepted with restitutive again.