Symmetric verbs

A symmetric verb denotes mutual atomic events — intransitive kiss, meet, collide, quarrel: the participants are identically involved in a single event, and linguistic diagnostics (count adverbials, modification) see no parts. The denotational contract, after [Lan00b], [Dim08], and [Sil12]: the verb's events are atomic, its role assigns the group atom over an unordered pair of participants, and dissolution recovers two events of the transitive base with crossed role values — a meaning postulate relating the two entries, not a decomposition, which is why the underlying events stay invisible. Formation-locus classification of reciprocal verbs lives in Verb.Reciprocal; the symmetric entries are the lexicon-formed ones (Studies/Siloni2012.lean).

structure Verb.Symmetricextends Verb : Type

A symmetric verb entry: an intransitive verb whose lexical meaning codes symmetry; base is the transitive alternate when the vocabulary has one.

• frames : List Frame
• subjectEntailments : Option ArgumentStructure.EntailmentProfile
• objectEntailments : Option ArgumentStructure.EntailmentProfile
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• vendlerClass : Option Features.VendlerClass
• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Semantics.Aspect.Incremental.VerbIncClass
• cosType : Option Features.ChangeOfState.CoSType
• presupType : Option PresupTriggerType
• projectionBehavior : Option ProjectionBehavior
• implicative : Option Implicative
• causative : Option Causative
• causalSource : Option Causation.Psych.CausalSource
• opaqueContext : Bool
• attitude : Option Features.Attitude
• readings : List Reading
• complementSig : Option NaturalLogic.Signature
• levinClass : Option ArgumentStructure.LevinClass
• root : Root
• form : String
• speechActVerb : Bool
• senseTag : SenseTag
• base : Option Verb

  The transitive alternate, when one exists.

def Verb.instReprSymmetric.repr : Symmetric → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Verb.instReprSymmetric : Repr Symmetric

Equations

• Verb.instReprSymmetric = { reprPrec := Verb.instReprSymmetric.repr }

def Verb.instBEqSymmetric.beq : Symmetric → Symmetric → Bool

Equations

• Verb.instBEqSymmetric.beq { toVerb := a, base := a_1 } { toVerb := b, base := b_1 } = (a == b && a_1 == b_1)
• Verb.instBEqSymmetric.beq x✝¹ x✝ = false

@[instance_reducible]

instance Verb.instBEqSymmetric : BEq Symmetric

Equations

• Verb.instBEqSymmetric = { beq := Verb.instBEqSymmetric.beq }

class Verb.SymmetricDenotation {D : Type u_1} {E : Type u_2} [SemilatticeSup D] [SemilatticeSup E] (GD : Semantics.Plurality.GroupStructure D) (GE : Semantics.Plurality.GroupStructure E) (base : Set E) (ag th : E → D) (sym : Set E) (agTh : E → D) : Prop

The symmetric-verb denotational contract: sym is a set of atomic events whose role agTh assigns the group atom over an unordered pair, and each event dissolves into two events of base with crossed Agent and Theme values.

• atomic (e : E) : e ∈ sym → Mereology.Atom e

  Symmetric verbs denote singular events: no proper parts.

• pairRole (e : E) : e ∈ sym → ∃ (d₁ : D) (d₂ : D), d₁ ≠ d₂ ∧ agTh e = GD.up (d₁ ⊔ d₂)

  The role assigns the group atom over an unordered pair.

• postulate (e : E) : e ∈ sym → ∀ (d₁ d₂ : D), d₁ ≠ d₂ → agTh e = GD.up (d₁ ⊔ d₂) → ∃ (e₁ : E) (e₂ : E), GE.down e = e₁ ⊔ e₂ ∧ e₁ ∈ base ∧ e₂ ∈ base ∧ ag e₁ = d₁ ∧ th e₁ = d₂ ∧ ag e₂ = d₂ ∧ th e₂ = d₁

  The meaning postulate: dissolution yields two base events with crossed role values.