Siloni (2012): Reciprocal Verbs and Symmetry

@cite{siloni-2012} @cite{siloni-2008}

Natural Language and Linguistic Theory 30(1): 261–320.

Beyond periphrastic reciprocals (each other), languages have reciprocal verbs — predicates that express reciprocity without an anaphoric object. These split into two types based on where reciprocalization applies:

• Lexical (Hebrew hitnašek, English intransitive kiss): formed in the lexicon via θ-role bundling. Produces symmetric verbs whose reciprocity involves a singular atomic event.
• Syntactic (French s'embrasser, Czech se políbit): formed in the syntax via a clitic (se). Reciprocity involves accumulation of sub-events; the operation is productive.

Nine empirical properties cluster along this divide, verified across ten languages (Hebrew, Russian, Hungarian, English, French, Italian, Spanish, Czech, Romanian, Serbo-Croatian). Both types disallow the "I" reading of embedded reciprocals — because both associate the subject with two θ-roles, blocking the sole-role requirement for distribution under embedding.

Connections

• RecipFormation from Typology.lean — extended with nine predicted properties and per-language verification
• EntailmentProfile — used to define θ-role bundling
• VerbDistributivity in Events/StratifiedReference.lean — the meet_agent_not_sdr axiom captures the same property: symmetric verbs denote singular events that do not distribute over atomic agents

inductive Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass : Type

The three classes of reciprocal constructions.

Class (i): periphrastic — reciprocal anaphor in object position (each other, l'un l'autre). Subject bears one θ-role.

Class (ii): lexical reciprocal verb — formed in the lexicon by θ-role bundling. Subject bears a complex [Agent-Theme] role. The verb is symmetric: reciprocity involves a singular atomic event.

Class (iii): syntactic reciprocal verb — formed in the syntax by a clitic (se). Subject bears two θ-roles via parasitic assignment. Reciprocity involves accumulation of sub-events.

• periphrastic : RecipClass
• lexicalVerb : RecipClass
• syntacticVerb : RecipClass

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqRecipClass : DecidableEq RecipClass

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqRecipClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqRecipClass.beq : RecipClass → RecipClass → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqRecipClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqRecipClass : BEq RecipClass

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqRecipClass = { beq := Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqRecipClass.beq }

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instReprRecipClass : Repr RecipClass

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instReprRecipClass = { reprPrec := Phenomena.ArgumentStructure.Studies.Siloni2012.instReprRecipClass.repr }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instReprRecipClass.repr : RecipClass → ℕ → Std.Format

Equations

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

def Phenomena.ArgumentStructure.Studies.Siloni2012.toRecipClass : Typology.RecipFormation → RecipClass

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Siloni2012.toRecipClass Phenomena.ArgumentStructure.Typology.RecipFormation.lexical = Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.lexicalVerb

def Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.subjectRoleCount : RecipClass → ℕ

Number of θ-roles associated with the subject. Periphrastic: subject = Agent only (Theme on anaphoric object). Reciprocal verbs: subject = Agent + Theme (bundled or parasitic).

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.periphrastic.subjectRoleCount = 1
• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.lexicalVerb.subjectRoleCount = 2
• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.syntacticVerb.subjectRoleCount = 2

def Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.allowsSubEventReading : RecipClass → Bool

Whether the sub-event reading is available (§2.2). Periphrastic and syntactic reciprocals build reciprocity from sub-events. Lexical reciprocal verbs (symmetric verbs) denote a singular atomic event — sub-events are inaccessible.

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.periphrastic.allowsSubEventReading = true
• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.lexicalVerb.allowsSubEventReading = false
• Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.syntacticVerb.allowsSubEventReading = true

structure Phenomena.ArgumentStructure.Studies.Siloni2012.PropertyCluster : Type

Nine empirical properties that systematically distinguish lexical from syntactic reciprocal verbs. Each Bool indicates whether the property holds for that formation type.

• singularEvent : Bool

  (i) Reciprocity involves a singular atomic event. Diagnostic: count adverbials (five times) yield N mutual events, not 2N directional sub-events (§2.2–2.3).

• productive : Bool

  (ii) The reciprocalization operation is productive — applies freely to transitive verbs (§3.5, §5).

• ecmReciprocals : Bool

  (iii) ECM reciprocal verbs are possible — reciprocalization spans a clause boundary (§5.2).

• frozenInput : Bool

  (iv) Can be formed from a frozen lexical entry (one without a transitive alternate in the vocabulary) (§5.3).

• semanticDrift : Bool

  (v) The reciprocal verb can undergo semantic drift — acquire a meaning not shared by the transitive alternate (§5.3).

• retainsAccOnDativeSuppression : Bool

  (vi) Can retain accusative case when the dative (not accusative) argument is suppressed by reciprocalization (§5.1).

• eventNominals : Bool

  (vii) Can derive reciprocal event nominals (§6). Exception: Czech allows reciprocal event nominals despite a syntactic setting, because Czech nominalization is itself a syntactic operation that can access syntactic reciprocal outputs (Hron 2005).

• phrasalIdioms : Bool

  (viii) Can head phrasal idioms unavailable for the transitive alternate (§5.3).

• discontinuous : Bool

  (ix) Allows the discontinuous reciprocal construction — subject + comitative "with"-phrase (§7).

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqPropertyCluster : DecidableEq PropertyCluster

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqPropertyCluster = Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqPropertyCluster.decEq

def Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqPropertyCluster.decEq (x✝ x✝¹ : PropertyCluster) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqPropertyCluster : BEq PropertyCluster

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqPropertyCluster = { beq := Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqPropertyCluster.beq }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqPropertyCluster.beq : PropertyCluster → PropertyCluster → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqPropertyCluster.beq x✝¹ x✝ = false

def Phenomena.ArgumentStructure.Studies.Siloni2012.instReprPropertyCluster.repr : PropertyCluster → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instReprPropertyCluster : Repr PropertyCluster

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instReprPropertyCluster = { reprPrec := Phenomena.ArgumentStructure.Studies.Siloni2012.instReprPropertyCluster.repr }

def Phenomena.ArgumentStructure.Studies.Siloni2012.lexicalProperties : PropertyCluster

Predicted cluster for lexically-formed reciprocal verbs. Symmetric verbs: closed class, singular event, can be frozen or drifted, derive event nominals, head idioms, license discontinuity. Cannot form ECM reciprocals or retain accusative on dative targets.

Equations

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

def Phenomena.ArgumentStructure.Studies.Siloni2012.syntacticProperties : PropertyCluster

Predicted cluster for syntactically-formed reciprocal verbs. Productive, allow ECM and sub-events, can retain accusative on dative targets. Cannot be frozen, drift, head idioms, derive event nominals, or license discontinuity.

Equations

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

def Phenomena.ArgumentStructure.Studies.Siloni2012.predictedProperties : Typology.RecipFormation → PropertyCluster

Derive the predicted property cluster from formation locus.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Siloni2012.predictedProperties Phenomena.ArgumentStructure.Typology.RecipFormation.lexical = Phenomena.ArgumentStructure.Studies.Siloni2012.lexicalProperties

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.properties_complementary : lexicalProperties.singularEvent = !syntacticProperties.singularEvent ∧ lexicalProperties.productive = !syntacticProperties.productive ∧ lexicalProperties.ecmReciprocals = !syntacticProperties.ecmReciprocals ∧ lexicalProperties.frozenInput = !syntacticProperties.frozenInput ∧ lexicalProperties.semanticDrift = !syntacticProperties.semanticDrift ∧ lexicalProperties.retainsAccOnDativeSuppression = !syntacticProperties.retainsAccOnDativeSuppression ∧ lexicalProperties.eventNominals = !syntacticProperties.eventNominals ∧ lexicalProperties.phrasalIdioms = !syntacticProperties.phrasalIdioms ∧ lexicalProperties.discontinuous = !syntacticProperties.discontinuous

The two clusters are perfectly complementary: every property that holds for lexical reciprocal verbs fails for syntactic ones, and vice versa. This is the central empirical finding of the paper.

def Phenomena.ArgumentStructure.Studies.Siloni2012.isSymmetricVerb : Typology.RecipFormation → Bool

Lexical reciprocal verbs are symmetric verbs: their reciprocity involves a singular atomic event in which both participants are identically involved (§2.3). Intransitive kiss and collide are symmetric — "John and Mary kissed" denotes one event of mutual kissing, not two directional sub-events.

The VerbDistributivity class in Events/StratifiedReference.lean axiomatizes the same property: meet has ¬ SDR_univ agentOf meet — it does not distribute over atomic agents, because the event is necessarily collective/atomic.

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.isSymmetricVerb Phenomena.ArgumentStructure.Typology.RecipFormation.lexical = true
• Phenomena.ArgumentStructure.Studies.Siloni2012.isSymmetricVerb Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic = false

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.symmetric_iff_singular (f : Typology.RecipFormation) : isSymmetricVerb f = (predictedProperties f).singularEvent

structure Phenomena.ArgumentStructure.Studies.Siloni2012.BundledRole : Type

A bundled θ-role: two entailment profiles merged into a single complex role assigned to one argument. Lexical reciprocalization bundles the external (agent-like) and internal (theme-like) roles of a transitive verb:

V(ACC) [θ_i] [θ_j] → V_SYM [θ_i · θ_j]

The subject of the resulting symmetric verb bears both the agent and theme entailments of the base transitive.

• external : Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

  The external (agent-like) component

• internal : Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

  The internal (theme-like) component

def Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqBundledRole.decEq (x✝ x✝¹ : BundledRole) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqBundledRole : DecidableEq BundledRole

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqBundledRole = Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqBundledRole.decEq

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole : BEq BundledRole

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole = { beq := Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole.beq }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole.beq : BundledRole → BundledRole → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole.beq { external := a, internal := a_1 } { external := b, internal := b_1 } = (a == b && a_1 == b_1)
• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqBundledRole.beq x✝¹ x✝ = false

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instReprBundledRole : Repr BundledRole

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instReprBundledRole = { reprPrec := Phenomena.ArgumentStructure.Studies.Siloni2012.instReprBundledRole.repr }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instReprBundledRole.repr : BundledRole → ℕ → Std.Format

Equations

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

def Phenomena.ArgumentStructure.Studies.Siloni2012.reciprocalBundle (subjectProfile objectProfile : Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile) : BundledRole

Lexical reciprocalization: bundle a transitive verb's two roles.

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.reciprocalBundle subjectProfile objectProfile = { external := subjectProfile, internal := objectProfile }

def Phenomena.ArgumentStructure.Studies.Siloni2012.BundledRole.componentCount (_b : BundledRole) : ℕ

A bundled role carries exactly two component profiles — this is what makes the subject of a reciprocal verb bear both Agent and Theme properties (depictive adjective case in Czech §3.1, comparative ellipsis §3.2).

Equations

• _b.componentCount = 2

The "I" reading of embedded reciprocals (@cite{higginbotham-1980}):

"John and Paul said they defeated each other in the final."

(we) John and Paul said: "we defeated each other."
(I)  John said he defeated Paul, and Paul said he defeated John.

The "I" reading requires TWO conditions (§4.3, p. 287):
(1) the embedded verb allows the sub-event reading, AND
(2) the embedded subject is associated with exactly one θ-role.

The puzzle: syntactic reciprocal verbs satisfy (1) — they DO have
the sub-event reading — yet still lack the "I" reading. Condition
(1) is necessary but not sufficient. The resolution: both types of
reciprocal verb fail condition (2), because both associate the
subject with two θ-roles (bundled or parasitic).

Only periphrastic reciprocals satisfy both conditions: the sub-event
reading is available (via the plural operator on *each other*), and
the subject bears exactly one role (Agent). 

def Phenomena.ArgumentStructure.Studies.Siloni2012.RecipClass.allowsIReading (c : RecipClass) : Bool

The "I" reading requires both sub-event availability AND a sole θ-role on the subject.

Equations

• c.allowsIReading = (c.allowsSubEventReading && c.subjectRoleCount == 1)

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.I_reading_iff_periphrastic (c : RecipClass) : c.allowsIReading = (c == RecipClass.periphrastic)

The "I" reading is available iff the construction is periphrastic.

• Periphrastic: sub-events ✓, sole role ✓ → "I" reading ✓
• Lexical verb: sub-events ✗, sole role ✗ → "I" reading ✗
• Syntactic verb: sub-events ✓, sole role ✗ → "I" reading ✗

The syntactic case is the puzzle: sub-events are present (condition 1 met) but the sole-role requirement fails (condition 2 unmet).

structure Phenomena.ArgumentStructure.Studies.Siloni2012.LangRecipVerb : Type

Per-language formation locus from the ten-language sample.

• language : String
• iso : String
• formation : Typology.RecipFormation

def Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqLangRecipVerb.decEq (x✝ x✝¹ : LangRecipVerb) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqLangRecipVerb : DecidableEq LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqLangRecipVerb = Phenomena.ArgumentStructure.Studies.Siloni2012.instDecidableEqLangRecipVerb.decEq

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqLangRecipVerb : BEq LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqLangRecipVerb = { beq := Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqLangRecipVerb.beq }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqLangRecipVerb.beq : LangRecipVerb → LangRecipVerb → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Siloni2012.instBEqLangRecipVerb.beq x✝¹ x✝ = false

instance Phenomena.ArgumentStructure.Studies.Siloni2012.instReprLangRecipVerb : Repr LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.instReprLangRecipVerb = { reprPrec := Phenomena.ArgumentStructure.Studies.Siloni2012.instReprLangRecipVerb.repr }

def Phenomena.ArgumentStructure.Studies.Siloni2012.instReprLangRecipVerb.repr : LangRecipVerb → ℕ → Std.Format

Equations

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

def Phenomena.ArgumentStructure.Studies.Siloni2012.hebrew : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.hebrew = { language := "Hebrew", iso := "heb", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.lexical }

def Phenomena.ArgumentStructure.Studies.Siloni2012.russian : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.russian = { language := "Russian", iso := "rus", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.lexical }

def Phenomena.ArgumentStructure.Studies.Siloni2012.hungarian : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.hungarian = { language := "Hungarian", iso := "hun", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.lexical }

def Phenomena.ArgumentStructure.Studies.Siloni2012.english : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.english = { language := "English", iso := "eng", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.lexical }

def Phenomena.ArgumentStructure.Studies.Siloni2012.french : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.french = { language := "French", iso := "fra", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.italian : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.italian = { language := "Italian", iso := "ita", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.spanish : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.spanish = { language := "Spanish", iso := "spa", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.czech : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.czech = { language := "Czech", iso := "ces", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.romanian : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.romanian = { language := "Romanian", iso := "ron", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.serboCroatian : LangRecipVerb

Equations

• Phenomena.ArgumentStructure.Studies.Siloni2012.serboCroatian = { language := "Serbo-Croatian", iso := "hbs", formation := Phenomena.ArgumentStructure.Typology.RecipFormation.syntactic }

def Phenomena.ArgumentStructure.Studies.Siloni2012.siloniSample : List LangRecipVerb

Equations

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

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.sample_size : siloniSample.length = 10

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.lexical_count : (List.filter (fun (x : LangRecipVerb) => x.formation == Typology.RecipFormation.lexical) siloniSample).length = 4

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.syntactic_count : (List.filter (fun (x : LangRecipVerb) => x.formation == Typology.RecipFormation.syntactic) siloniSample).length = 6

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.lexical_are_symmetric : ((List.filter (fun (x : LangRecipVerb) => x.formation == Typology.RecipFormation.lexical) siloniSample).all fun (l : LangRecipVerb) => isSymmetricVerb l.formation) = true

All lexical-formation languages produce symmetric verbs.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.syntactic_not_symmetric : ((List.filter (fun (x : LangRecipVerb) => x.formation == Typology.RecipFormation.syntactic) siloniSample).all fun (l : LangRecipVerb) => !isSymmetricVerb l.formation) = true

All syntactic-formation languages produce non-symmetric verbs.

The paper's core argument is a derivation chain, not a conjunction of independent facts. Formation locus determines interpretive possibilities step by step.

Generalization (29) from §3.5: "Plural events are not part of the
lexicon's inventory." Since the lexicon has no access to plural
operators, lexical operations cannot produce plural events. This
forces lexical reciprocals to be symmetric verbs (singular events),
which in turn blocks the sub-event reading.

Both verb types converge on "no 'I' reading" but via different
derivation paths:
- Lexical:   singular event → no sub-events → condition 1 fails
- Syntactic: sub-events present, BUT dual role → condition 2 fails

Cross-module connections:
- `meetProfile.agentSDR = false` in Champollion2017: same insight
- `meet_agent_not_sdr` in StratifiedReference: axiomatizes it 

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.recip_verb_dual_role (f : Typology.RecipFormation) : (toRecipClass f).subjectRoleCount = 2

Step 1: Both reciprocal verb types give the subject two θ-roles (lexical via bundling §4.1, syntactic via parasitic assignment §4.2).

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.singular_event_no_subevents (f : Typology.RecipFormation) (h : (predictedProperties f).singularEvent = true) : (toRecipClass f).allowsSubEventReading = false

Step 2: Singular-event verbs lack the sub-event reading (§2.2–2.3). Bridges PropertyCluster.singularEvent to RecipClass.allowsSubEventReading.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.subevents_necessary_for_I (c : RecipClass) (h : c.allowsSubEventReading = false) : c.allowsIReading = false

Step 3a: Sub-event availability is NECESSARY for the "I" reading (condition 1 of §4.3). Blocks via the first conjunct of &&.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.sole_role_necessary_for_I (c : RecipClass) (h : c.subjectRoleCount ≠ 1) : c.allowsIReading = false

Step 3b: A sole θ-role on the subject is NECESSARY for the "I" reading (condition 2 of §4.3). Blocks via the second conjunct.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.lexical_no_I_reading : (toRecipClass Typology.RecipFormation.lexical).allowsIReading = false

Lexical derivation (§3.5 → §2.2 → §4.3): singular event → no sub-events → condition 1 fails → no "I" reading.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.syntactic_no_I_reading : (toRecipClass Typology.RecipFormation.syntactic).allowsIReading = false

Syntactic derivation (§4.2 → §4.3): dual role → condition 2 fails → no "I" reading.

This resolves the PUZZLE: syntactic reciprocals HAVE sub-events (condition 1 met) but LACK the sole role (condition 2 unmet).

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.no_I_reading_either_formation (f : Typology.RecipFormation) : (toRecipClass f).allowsIReading = false

Both paths converge: neither verb type allows the "I" reading.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.hungarian_agrees : Typology.rp_hungarian.formation = some hungarian.formation

Hungarian formation agrees with Typology.lean.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.french_agrees : Typology.rp_french.formation = some french.formation

French formation agrees with Typology.lean.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.czech_agrees : Typology.rp_czech.formation = some czech.formation

Czech formation agrees with Typology.lean.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.swahili_consistent : Typology.rp_swahili.formation = some Typology.RecipFormation.lexical

Swahili is classified as lexical in Typology.lean (Nordlinger 2023). Siloni (2012) does not discuss Swahili directly, but the prediction is consistent: Swahili has verb-marked reciprocals (-ana) that license discontinuous constructions — a lexical property.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.greek_consistent : Typology.rp_greek.formation = some Typology.RecipFormation.lexical

Greek is classified as lexical in Typology.lean. Consistent: Greek allows discontinuous reciprocals with me.

theorem Phenomena.ArgumentStructure.Studies.Siloni2012.discontinuity_bridge (f : Typology.RecipFormation) : (predictedProperties f).discontinuous = f.allowsDiscontinuous

The discontinuity prediction from predictedProperties agrees with RecipFormation.allowsDiscontinuous in Typology.lean.