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.

• valency : Valency
• voiceType : Option VoiceType
• passivizable : Bool
• perfectAuxiliaries : Finset PerfectAuxiliary
• vendlerClass : Option Aspect.VendlerClass
• scaleDimension : Option Degree.ScalarDimension
• scalePolarity : Polarity
• direction : Option Spatial.Path.Direction
• incrementality : Option Aspect.Incrementality
• phasal : Option Aspect.Phasal
• factivity : Option Presupposition.Factivity
• implicative : NaturalLogic.ImplicationSignature
• opaqueContext : Bool
• attitude : Option _root_.Attitude
• readings : List Reading
• complementSig : Option NaturalLogic.Signature
• levinClasses : Finset ArgumentStructure.LevinClass
• levinExcluded : Finset ArgumentStructure.LevinClass
• root : Semantics.Root
• morphs : List Morphology.Morph
• speechActVerb : Bool
• senseTag : SenseTag
• base : Option Verb

  The transitive alternate, when one exists.

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 : Plurality.GroupStructure D) (GE : 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.