Affectedness

This file defines Beavers's affectedness hierarchy. A predicate affects a theme to one of four degrees according to how specific it is about the theme's change along a scale. It may entail that the theme reaches a goal the predicate fixes (a quantized change), that the theme reaches some goal (a non-quantized change), that the theme is related to a scale without necessarily changing (potential for change), or nothing about change at all. Each degree is an existential generalization of the one above it, over the goal, over the result and over the scalar relation, so the degrees form a chain of weakening truth conditions. The three degrees above the bottom are the entailments, and each degree is the set of entailments at most as strong as it.

Main definitions

• AffectednessDegree: the four degrees, ordered by strength.
• AffectednessEntailment: the three degrees above the bottom, the affectedness entailments.
• AffectednessDegree.entailments: a degree as the set of entailments it comprises.
• QuantizedChange: the predicate entails that the theme reaches a goal it fixes.
• NonQuantizedChange: the predicate entails that the theme reaches some goal.
• PotentialChange: the predicate relates the theme to a scale.
• AffectednessDegree.Holds: the condition each degree names.

Main results

• AffectednessDegree.holds_antitone: each degree entails every weaker one.

Implementation notes

• A predicate φ x e comes with its scalar θ-relation θ x s e, relating its theme to a scale in an event, and a result relation R x s g e, the theme reaching the state g on the scale s. Beavers defines the result only together with the predicate's scalar relation, so the result conditions conjoin the two, and every step of the hierarchy is then existential generalization.
• Potential for change is lexical data, not a consequence of the predicate's truth conditions. Beavers's existential over θ-relations is trivial unless it ranges over the predicate's own roles, so the scalar relation θ is a parameter, and any predicate has potential for change under θ := fun _ _ _ ↦ True. For the same reason the unspecified degree holds of every predicate.
• A quantized change fixes one goal for every event of the predicate, and a non-quantized change one goal for each event, ∃ g, ∀ x e against ∀ x e, ∃ g.
• The paper binds the event existentially and states the degrees of a sentence; here they are stated of a relation between themes and events.

References

• J. Beavers, On Affectedness (2011)

The degrees

inductive ArgumentStructure.AffectednessDegree : Type

The degrees of affectedness, weakest first ([Bea11] (62)).

• unspecified : AffectednessDegree

  Nothing is entailed about change, as for the object of see or ponder.

• potential : AffectednessDegree

  The theme is related to a scale without necessarily changing, as for hit or wipe.

• nonquantized : AffectednessDegree

  The theme reaches some goal on a scale, as for widen or cool.

• quantized : AffectednessDegree

  The theme reaches a goal the predicate fixes, as for break or destroy.

@[instance_reducible]

instance ArgumentStructure.instDecidableEqAffectednessDegree : DecidableEq AffectednessDegree

Equations

• ArgumentStructure.instDecidableEqAffectednessDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArgumentStructure.instFintypeAffectednessDegree : Fintype AffectednessDegree

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprAffectednessDegree : Repr AffectednessDegree

Equations

• ArgumentStructure.instReprAffectednessDegree = { reprPrec := ArgumentStructure.instReprAffectednessDegree.repr }

def ArgumentStructure.instReprAffectednessDegree.repr : AffectednessDegree → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instInhabitedAffectednessDegree : Inhabited AffectednessDegree

Equations

• ArgumentStructure.instInhabitedAffectednessDegree = { default := ArgumentStructure.instInhabitedAffectednessDegree.default }

def ArgumentStructure.AffectednessDegree.strength : AffectednessDegree → ℕ

The strength of a degree is its position in the chain.

Equations

• ArgumentStructure.AffectednessDegree.unspecified.strength = 0
• ArgumentStructure.AffectednessDegree.potential.strength = 1
• ArgumentStructure.AffectednessDegree.nonquantized.strength = 2
• ArgumentStructure.AffectednessDegree.quantized.strength = 3

@[instance_reducible]

instance ArgumentStructure.AffectednessDegree.instLinearOrder : LinearOrder AffectednessDegree

Equations

• ArgumentStructure.AffectednessDegree.instLinearOrder = LinearOrder.lift' ArgumentStructure.AffectednessDegree.strength ⋯

theorem ArgumentStructure.AffectednessDegree.le_iff_strength_le {a b : AffectednessDegree} : a ≤ b ↔ a.strength ≤ b.strength

@[instance_reducible]

instance ArgumentStructure.AffectednessDegree.instOrderBot : OrderBot AffectednessDegree

Equations

• ArgumentStructure.AffectednessDegree.instOrderBot = { bot := ArgumentStructure.AffectednessDegree.unspecified, bot_le := ⋯ }

theorem ArgumentStructure.AffectednessDegree.supIrred_iff_ne_bot {d : AffectednessDegree} : SupIrred d ↔ d ≠ ⊥

@[instance_reducible]

instance ArgumentStructure.AffectednessDegree.instDecidablePredSupIrred : DecidablePred SupIrred

Equations

• x✝.instDecidablePredSupIrred = decidable_of_iff (x✝ ≠ ⊥) ⋯

@[reducible, inline]

abbrev ArgumentStructure.AffectednessEntailment : Type

An affectedness entailment is a degree that is not the join of weaker ones, one of the three degrees above unspecified, entailing a quantized change, a non-quantized change or potential for change.

Equations

• ArgumentStructure.AffectednessEntailment = { d : ArgumentStructure.AffectednessDegree // SupIrred d }

noncomputable def ArgumentStructure.AffectednessDegree.entailments : AffectednessDegree ≃o LowerSet AffectednessEntailment

A degree is the set of entailments at most as strong as it, and every set of entailments closed under entailment is a degree, by Birkhoff's representation of the chain of degrees.

Equations

• ArgumentStructure.AffectednessDegree.entailments = OrderIso.lowerSetSupIrred

theorem ArgumentStructure.AffectednessDegree.coe_entailments (d : AffectednessDegree) : ↑(entailments d) = {e : AffectednessEntailment | ↑e ≤ d}

The affectedness conditions

def ArgumentStructure.QuantizedChange {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} (θ : α → S → β → Prop) (R : α → S → G → β → Prop) (φ : α → β → Prop) (g : G) : Prop

A predicate effects a quantized change to the goal g when every event of it relates its theme to a scale on which the theme reaches g ([Bea11] (60a)).

Equations

• ArgumentStructure.QuantizedChange θ R φ g = ∀ (x : α) (e : β), φ x e → ∃ (s : S), θ x s e ∧ R x s g e

def ArgumentStructure.NonQuantizedChange {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} (θ : α → S → β → Prop) (R : α → S → G → β → Prop) (φ : α → β → Prop) : Prop

A predicate effects a non-quantized change when every event of it relates its theme to a scale on which the theme reaches some goal ([Bea11] (60b)).

Equations

• ArgumentStructure.NonQuantizedChange θ R φ = ∀ (x : α) (e : β), φ x e → ∃ (s : S), θ x s e ∧ ∃ (g : G), R x s g e

def ArgumentStructure.PotentialChange {α : Type u_1} {S : Type u_2} {β : Type u_4} (θ : α → S → β → Prop) (φ : α → β → Prop) : Prop

A predicate gives its theme potential for change when every event of it relates the theme to a scale ([Bea11] (60c)).

Equations

• ArgumentStructure.PotentialChange θ φ = ∀ (x : α) (e : β), φ x e → ∃ (s : S), θ x s e

theorem ArgumentStructure.QuantizedChange.nonQuantizedChange {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} {θ : α → S → β → Prop} {R : α → S → G → β → Prop} {φ : α → β → Prop} {g : G} (h : QuantizedChange θ R φ g) : NonQuantizedChange θ R φ

theorem ArgumentStructure.NonQuantizedChange.potentialChange {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} {θ : α → S → β → Prop} {R : α → S → G → β → Prop} {φ : α → β → Prop} (h : NonQuantizedChange θ R φ) : PotentialChange θ φ

def ArgumentStructure.AffectednessDegree.Holds {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} (θ : α → S → β → Prop) (R : α → S → G → β → Prop) (φ : α → β → Prop) : AffectednessDegree → Prop

The condition an affectedness degree names is a quantized change to some goal, a non-quantized change, potential for change, or nothing ([Bea11] (60)).

Equations

• ArgumentStructure.AffectednessDegree.Holds θ R φ ArgumentStructure.AffectednessDegree.unspecified = True
• ArgumentStructure.AffectednessDegree.Holds θ R φ ArgumentStructure.AffectednessDegree.potential = ArgumentStructure.PotentialChange θ φ
• ArgumentStructure.AffectednessDegree.Holds θ R φ ArgumentStructure.AffectednessDegree.nonquantized = ArgumentStructure.NonQuantizedChange θ R φ
• ArgumentStructure.AffectednessDegree.Holds θ R φ ArgumentStructure.AffectednessDegree.quantized = ∃ (g : G), ArgumentStructure.QuantizedChange θ R φ g

theorem ArgumentStructure.AffectednessDegree.holds_antitone {α : Type u_1} {S : Type u_2} {G : Type u_3} {β : Type u_4} (θ : α → S → β → Prop) (R : α → S → G → β → Prop) (φ : α → β → Prop) : Antitone (Holds θ R φ)

Each degree entails every weaker one, the Affectedness Hierarchy ([Bea11] (62)).