Benz (2025): Structure and Interpretation Across Categories

@cite{benz-2025}

Structure and Interpretation Across Categories. PhD dissertation, University of Pennsylvania.

Overview

This file formalizes three interconnected contributions from @cite{benz-2025}:

1. Content nominalizations (Ch. 3): German -ung nominalizations are systematically three-ways ambiguous (event/result/content), derived from allosemy of v and n in the structure [nP n [vP v [√Root]]].

2. Co-occurrence restrictions (Ch. 4): German preverbal elements (prefixes, particles, RSPs) show a striking co-occurrence paradigm explained by the conjunction of phrase-structural and interpretive constraints.

3. Allosemy and locality (Ch. 2, Ch. 4): RSPs are always interpreted transparently (outside v's locality domain), while prefixes and particles can receive non-transparent interpretations (inside v's complex head).

Architecture

• Morphology.DM.Allosemy: general framework + v/n/Voice allosemy
• Features.Acceptability: Acceptability type

structure Benz2025.NominalizationDatum : Type

A German nominalization datum with reading and diagnostic properties.

• form : String

  The nominalized form.

• baseVerb : String

  Base verb.

• suffix : String

  Nominalizing suffix.

• reading : Morphology.DM.Allosemy.NominalizationReading

  The reading exhibited in this example.

• sentence : String

  Example sentence.

• translation : String

  Translation.

• temporalModifiers : Bool

  Accepts temporal modifiers?

• pluralizable : Bool

  Can be pluralized?

• takesCPComplement : Bool

  Takes CP complement?

def Benz2025.instReprNominalizationDatum.repr : NominalizationDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benz2025.instReprNominalizationDatum : Repr NominalizationDatum

Equations

• Benz2025.instReprNominalizationDatum = { reprPrec := Benz2025.instReprNominalizationDatum.repr }

def Benz2025.instBEqNominalizationDatum.beq : NominalizationDatum → NominalizationDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Benz2025.instBEqNominalizationDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Benz2025.instBEqNominalizationDatum : BEq NominalizationDatum

Equations

• Benz2025.instBEqNominalizationDatum = { beq := Benz2025.instBEqNominalizationDatum.beq }

def Benz2025.beobachtung_CEN : NominalizationDatum

Beobachtung ('observation') — the running example in Ch. 3. All three readings are available for this single form.

Equations

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

def Benz2025.beobachtung_RN : NominalizationDatum

Equations

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

def Benz2025.beobachtung_CCN : NominalizationDatum

Equations

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

def Benz2025.allBeobachtungReadings : List NominalizationDatum

Equations

• Benz2025.allBeobachtungReadings = [Benz2025.beobachtung_CEN, Benz2025.beobachtung_RN, Benz2025.beobachtung_CCN]

theorem Benz2025.beobachtung_three_readings : (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.complexEvent) = true ∧ (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.simpleEntity) = true ∧ (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.content) = true

All three readings are attested for Beobachtung.

theorem Benz2025.cen_temporal : beobachtung_CEN.temporalModifiers = true

CENs accept temporal modifiers.

theorem Benz2025.rn_plural : beobachtung_RN.pluralizable = true

RNs are pluralizable.

theorem Benz2025.ccn_cp : beobachtung_CCN.takesCPComplement = true

CCNs take CP complements.

theorem Benz2025.cen_no_plural : beobachtung_CEN.pluralizable = false

CENs resist pluralization (event readings are mass-like).

theorem Benz2025.rn_no_temporal : beobachtung_RN.temporalModifiers = false

RNs lack temporal modifiers.

def Benz2025.readingAllosemePair : Morphology.DM.Allosemy.NominalizationReading → Morphology.DM.Allosemy.VAlloseme × Morphology.DM.Allosemy.NAlloseme

Map each reading to its alloseme pair.

Equations

• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.complexEvent = (Morphology.DM.Allosemy.VAlloseme.eventive, Morphology.DM.Allosemy.NAlloseme.sortal)
• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEvent = (Morphology.DM.Allosemy.VAlloseme.zero, Morphology.DM.Allosemy.NAlloseme.simpleEvent)
• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.result = (Morphology.DM.Allosemy.VAlloseme.eventive, Morphology.DM.Allosemy.NAlloseme.result)
• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleState = (Morphology.DM.Allosemy.VAlloseme.zero, Morphology.DM.Allosemy.NAlloseme.state)
• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEntity = (Morphology.DM.Allosemy.VAlloseme.zero, Morphology.DM.Allosemy.NAlloseme.sortal)
• Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.content = (Morphology.DM.Allosemy.VAlloseme.eventive, Morphology.DM.Allosemy.NAlloseme.content)

theorem Benz2025.alloseme_derivation_CEN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent

The alloseme pair correctly derives each reading.

theorem Benz2025.alloseme_derivation_RN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.zero Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity

theorem Benz2025.alloseme_derivation_CCN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.content = some Morphology.DM.Allosemy.NominalizationReading.content

theorem Benz2025.alloseme_roundtrip (r : Morphology.DM.Allosemy.NominalizationReading) : match readingAllosemePair r with | (v, n) => Morphology.DM.Allosemy.readingFromAllosemes v n = some r

Round-trip: each reading maps to allosemes that reconstruct it.

theorem Benz2025.zero_content_impossible : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.zero Morphology.DM.Allosemy.NAlloseme.content = none

The impossible combination: zero v + content n yields no reading. Content requires an underlying event.

theorem Benz2025.cen_simpleEntity_mirror : (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.complexEvent).1 = Morphology.DM.Allosemy.VAlloseme.eventive ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEntity).1 = Morphology.DM.Allosemy.VAlloseme.zero ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.complexEvent).2 = Morphology.DM.Allosemy.NAlloseme.sortal ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEntity).2 = Morphology.DM.Allosemy.NAlloseme.sortal

CEN and simple entity RN are "mirror images" of the division of semantic labor: in CEN, v does the work (introducing the event variable) while n merely nominalizes; in simple entity RN, v is null (zero) and the referential/object interpretation comes from the nominalization context. Both use the same n alloseme (sortal) — it's v that varies.

inductive Benz2025.PreverbalElement : Type

The three types of German preverbal elements.

Ch. 4: prefixes are inseparable and attach as heads; particles are separable and attach as phrases; RSPs are adjectival phrases that form complex predicates with the verb.

• pfx : PreverbalElement
• prt : PreverbalElement
• rsp : PreverbalElement

@[implicit_reducible]

instance Benz2025.instDecidableEqPreverbalElement : DecidableEq PreverbalElement

Equations

• Benz2025.instDecidableEqPreverbalElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Benz2025.instReprPreverbalElement : Repr PreverbalElement

Equations

• Benz2025.instReprPreverbalElement = { reprPrec := Benz2025.instReprPreverbalElement.repr }

def Benz2025.instReprPreverbalElement.repr : PreverbalElement → ℕ → Std.Format

Equations

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

def Benz2025.PreverbalElement.isHead : PreverbalElement → Bool

Syntactic status: head or phrase.

§4.3.1: following Wurmbrand (1998) and Zeller (2001a), prefixes are heads (inseparable under V2 movement) while particles are phrases (obligatorily stranded under V2). RSPs are unambiguously phrasal (they can be modified: total flach gehämmert).

Equations

• Benz2025.PreverbalElement.pfx.isHead = true
• Benz2025.PreverbalElement.prt.isHead = false
• Benz2025.PreverbalElement.rsp.isHead = false

def Benz2025.PreverbalElement.alwaysSpecifiesResult : PreverbalElement → Bool

Does this element always specify a result state that conflicts with other delimiters?

§4.1: prefixes and RSPs always contribute a (potentially conflicting) result state specification. Particles can have non-delimiting readings (directional, completive) that don't necessarily conflict — this is why PRT-pfx combinations like aus-er-wählen are interpretively acceptable.

Equations

• Benz2025.PreverbalElement.pfx.alwaysSpecifiesResult = true
• Benz2025.PreverbalElement.prt.alwaysSpecifiesResult = false
• Benz2025.PreverbalElement.rsp.alwaysSpecifiesResult = true

def Benz2025.inseparablePrefixes : List String

German inseparable prefixes (closed class).

Table 4. The prefix ge- is the rare non-participial prefix (as in ge-bären, ge-denken).

Equations

• Benz2025.inseparablePrefixes = ["be", "ent", "er", "ge", "miss", "ver", "zer"]

def Benz2025.separableParticles : List String

German separable particles (open class, representative sample).

Table 4. Elements like durch-, über-, um- are ambiguous between prefix and particle uses.

Equations

• Benz2025.separableParticles = ["ab", "an", "auf", "aus", "bei", "ein", "los", "nach", "vor", "zu"]

def Benz2025.ambiguousElements : List String

Ambiguous preverbal elements: prefix or particle depending on verb.

Equations

• Benz2025.ambiguousElements = ["durch", "hinter", "über", "um", "unter", "wider"]

structure Benz2025.CooccurrenceDatum : Type

A co-occurrence pair: two preverbal elements in order (outer, inner), where the inner element is closer to the root.

• outer : PreverbalElement
• inner : PreverbalElement
• allowed : Bool
• structurePredicts : Bool

  Structure (head/phrase) predicts this restriction?

• interpretationPredicts : Bool

  Interpretation (delimitation) predicts this restriction?

• exampleStr : String

@[implicit_reducible]

instance Benz2025.instReprCooccurrenceDatum : Repr CooccurrenceDatum

Equations

• Benz2025.instReprCooccurrenceDatum = { reprPrec := Benz2025.instReprCooccurrenceDatum.repr }

def Benz2025.instReprCooccurrenceDatum.repr : CooccurrenceDatum → ℕ → Std.Format

Equations

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

def Benz2025.instBEqCooccurrenceDatum.beq : CooccurrenceDatum → CooccurrenceDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Benz2025.instBEqCooccurrenceDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Benz2025.instBEqCooccurrenceDatum : BEq CooccurrenceDatum

Equations

• Benz2025.instBEqCooccurrenceDatum = { beq := Benz2025.instBEqCooccurrenceDatum.beq }

def Benz2025.cooccurrenceTable : List CooccurrenceDatum

The full co-occurrence paradigm from Table 3.

Equations

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

def Benz2025.structurallyCompatible (outer inner : PreverbalElement) : Bool

Structural compatibility: phrase can take headed complement; two heads can combine; head cannot wrap phrase; two phrases cannot stack.

§4.3.1, §4.4.

Equations

• Benz2025.structurallyCompatible outer inner = match outer.isHead, inner.isHead with | true, true => true | false, true => true | true, false => false | false, false => false

theorem Benz2025.structural_prediction_matches : List.map (fun (d : CooccurrenceDatum) => structurallyCompatible d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.structurePredicts) cooccurrenceTable

The structural prediction matches Table 3's "Structure Predicts" column.

def Benz2025.interpretivelyCompatible (outer inner : PreverbalElement) : Bool

Two elements that both always specify a result state cannot co-occur, as a single event cannot be delimited twice with conflicting endpoints.

§4.1: the interpretive constraint is about conflicting result state specifications. Particles escape this because they can have non-result (directional/completive) readings.

Equations

• Benz2025.interpretivelyCompatible outer inner = !(outer.alwaysSpecifiesResult && inner.alwaysSpecifiesResult)

theorem Benz2025.interpretive_prediction_matches : List.map (fun (d : CooccurrenceDatum) => interpretivelyCompatible d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.interpretationPredicts) cooccurrenceTable

The interpretive prediction matches Table 3's "Interpretation Predicts" column.

def Benz2025.predictedAllowed (outer inner : PreverbalElement) : Bool

A combination is allowed iff both structurally compatible AND interpretively compatible (no conflicting result states).

§4.4: both factors are needed; neither alone explains the full paradigm.

Equations

• Benz2025.predictedAllowed outer inner = (Benz2025.structurallyCompatible outer inner && Benz2025.interpretivelyCompatible outer inner)

theorem Benz2025.combined_prediction_matches : List.map (fun (d : CooccurrenceDatum) => predictedAllowed d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.allowed) cooccurrenceTable

The combined prediction matches Table 3's "Allowed" column.

theorem Benz2025.prt_pfx_uniquely_allowed : (List.filter (fun (x : CooccurrenceDatum) => x.allowed) cooccurrenceTable).length = 1

PRT-pfx is the unique allowed combination.

structure Benz2025.GermanResultativeDatum : Type

A German resultative datum with gloss and judgment.

• sentence : String
• gloss : String
• translation : String
• judgment : Features.Acceptability
• verbClass : String

def Benz2025.instReprGermanResultativeDatum.repr : GermanResultativeDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benz2025.instReprGermanResultativeDatum : Repr GermanResultativeDatum

Equations

• Benz2025.instReprGermanResultativeDatum = { reprPrec := Benz2025.instReprGermanResultativeDatum.repr }

def Benz2025.instBEqGermanResultativeDatum.beq : GermanResultativeDatum → GermanResultativeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Benz2025.instBEqGermanResultativeDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Benz2025.instBEqGermanResultativeDatum : BEq GermanResultativeDatum

Equations

• Benz2025.instBEqGermanResultativeDatum = { beq := Benz2025.instBEqGermanResultativeDatum.beq }

def Benz2025.germanRSPData : List GermanResultativeDatum

German RSP data from §4.2.

German allows obligatorily transitive, unaccusative, and inherently reflexive M predicates in resultatives — not just unergatives.

Equations

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

theorem Benz2025.german_allows_non_unergative_M : (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "obligatorily transitive") = true ∧ (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "unaccusative") = true ∧ (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "inherently reflexive") = true

German allows non-unergative M predicates in resultatives.

def Benz2025.rsp_pfx_contrasts : List (GermanResultativeDatum × GermanResultativeDatum)

RSPs are incompatible with prefixed verbs. Ch. 4: adding an RSP to a prefix verb is ungrammatical, but the same RSP with the simplex verb is fine.

Equations

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

theorem Benz2025.rsp_pfx_contrast_pattern : (rsp_pfx_contrasts.all fun (x : GermanResultativeDatum × GermanResultativeDatum) => match x with | (bad, good) => bad.judgment == Features.Acceptability.unacceptable && good.judgment == Features.Acceptability.ok) = true

Every RSP+pfx-verb contrast: pfx-verb ungrammatical, simplex OK.

def Benz2025.rsp_prt_contrasts : List (GermanResultativeDatum × GermanResultativeDatum)

RSPs are also incompatible with particles. Ch. 4: adding an RSP to a particle verb is ungrammatical, but the same RSP with the simplex verb is fine.

Equations

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

theorem Benz2025.rsp_prt_contrast_pattern : (rsp_prt_contrasts.all fun (x : GermanResultativeDatum × GermanResultativeDatum) => match x with | (bad, good) => bad.judgment == Features.Acceptability.unacceptable && good.judgment == Features.Acceptability.ok) = true

Every RSP+PRT-verb contrast: PRT-verb ungrammatical, simplex OK.

inductive Benz2025.InterpretiveTransparency : Type

Claim 2: RSPs are always transparent (outside v's locality domain for allosemy); prefixes and particles can be opaque (inside the complex head).

• transparent : InterpretiveTransparency
• nonTransparent : InterpretiveTransparency

@[implicit_reducible]

instance Benz2025.instDecidableEqInterpretiveTransparency : DecidableEq InterpretiveTransparency

Equations

• Benz2025.instDecidableEqInterpretiveTransparency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benz2025.instReprInterpretiveTransparency.repr : InterpretiveTransparency → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benz2025.instReprInterpretiveTransparency : Repr InterpretiveTransparency

Equations

• Benz2025.instReprInterpretiveTransparency = { reprPrec := Benz2025.instReprInterpretiveTransparency.repr }

def Benz2025.typicalTransparency : PreverbalElement → InterpretiveTransparency

Equations

• Benz2025.typicalTransparency Benz2025.PreverbalElement.rsp = Benz2025.InterpretiveTransparency.transparent
• Benz2025.typicalTransparency Benz2025.PreverbalElement.pfx = Benz2025.InterpretiveTransparency.nonTransparent
• Benz2025.typicalTransparency Benz2025.PreverbalElement.prt = Benz2025.InterpretiveTransparency.nonTransparent

theorem Benz2025.rsp_always_transparent : typicalTransparency PreverbalElement.rsp = InterpretiveTransparency.transparent

Complex predicate semantics

Following Williams (2015), adopted by §4.2: resultatives are complex predicates with semantics:

K(e₁, e₂, s) = Means(e₁, e₂) & End(e₁, s)

where e₁ is the complex event of change, e₂ is the means/manner subevent, and s is the result state. The M predicate is the verb; the R predicate is the RSP. This is NOT a causal relation — the means event can be concurrent with the change.

The End Theme Postulate links the Theme of the complex event to the end state: End(e₁, s) & Theme(e₁, x) |= Theme(s, x).

See also Semantics.Causation.Resultatives for the complementary analysis via causal dynamics, structural sufficiency, and CC-selection.

theorem Benz2025.claim1_two_factors : (cooccurrenceTable.any fun (d : CooccurrenceDatum) => d.structurePredicts && !d.interpretationPredicts && !d.allowed) = true ∧ (cooccurrenceTable.any fun (d : CooccurrenceDatum) => d.interpretationPredicts && !d.structurePredicts && !d.allowed) = true

Claim 1: Neither factor alone predicts the full co-occurrence paradigm. Structure alone is insufficient: some structurally OK combinations are blocked by interpretation (pfx-pfx, RSP-pfx). Interpretation alone is insufficient: some interpretively OK combinations are blocked by structure (pfx-PRT, PRT-PRT, RSP-PRT).

inductive Benz2025.NominalizationType : Type

German nominalization types discussed in Ch. 5.

• ung: -ung suffixation (Beobachtung, Erzählung). Requires the verb to project a full verbal shell including v; the entire vP is nominalized by n.
• ge_e: Ge-...-e circumfixation (Gerede, Gelaufe). Directly nominalizes the root without a full verbal projection; the root must be able to stand without obligatory internal arguments.
• nomInfinitive: Nominalized infinitive (das Beobachten, das Erzählen). The most permissive: the full verbal structure is preserved under nominalization.

• ung : NominalizationType
• ge_e : NominalizationType
• nomInfinitive : NominalizationType

@[implicit_reducible]

instance Benz2025.instDecidableEqNominalizationType : DecidableEq NominalizationType

Equations

• Benz2025.instDecidableEqNominalizationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benz2025.instReprNominalizationType.repr : NominalizationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benz2025.instReprNominalizationType : Repr NominalizationType

Equations

• Benz2025.instReprNominalizationType = { reprPrec := Benz2025.instReprNominalizationType.repr }

def Benz2025.peAcceptable : NominalizationType → PreverbalElement → Bool

Whether a preverbal element is acceptable in a given nominalization type.

Ch. 5: the distribution of preverbal elements across nominalization types reveals complementary distribution between prefixes and RSPs:

	pfx	prt	RSP
-ung	✓	✓	✗
Ge-...-e	✗	✓	✓
nom. inf.	✓	✓	✓

• -ung + RSP = ✗: RSPs are phrasal and cannot be trapped inside the complex head that -ung nominalization creates. The RSP would need to be inside the vP that n selects, but as a phrase it cannot incorporate.
• Ge-...-e + pfx = ✗: Ge-...-e directly nominalizes the root; it requires the root to be available without obligatory internal arguments. Prefixed verbs (where the prefix saturates argument structure) are incompatible because the prefix has already formed a complex head with the root, and the Ge-...-e circumfix cannot wrap around a complex head.
• Nom. inf.: maximally permissive because the full verbal projection (including any preverbal element) is preserved under nominalization.

Equations

• Benz2025.peAcceptable Benz2025.NominalizationType.ung Benz2025.PreverbalElement.pfx = true
• Benz2025.peAcceptable Benz2025.NominalizationType.ung Benz2025.PreverbalElement.prt = true
• Benz2025.peAcceptable Benz2025.NominalizationType.ung Benz2025.PreverbalElement.rsp = false
• Benz2025.peAcceptable Benz2025.NominalizationType.ge_e Benz2025.PreverbalElement.pfx = false
• Benz2025.peAcceptable Benz2025.NominalizationType.ge_e Benz2025.PreverbalElement.prt = true
• Benz2025.peAcceptable Benz2025.NominalizationType.ge_e Benz2025.PreverbalElement.rsp = true
• Benz2025.peAcceptable Benz2025.NominalizationType.nomInfinitive x✝ = true

theorem Benz2025.pfx_rsp_complementary_ung_ge : peAcceptable NominalizationType.ung PreverbalElement.pfx = true ∧ peAcceptable NominalizationType.ung PreverbalElement.rsp = false ∧ peAcceptable NominalizationType.ge_e PreverbalElement.pfx = false ∧ peAcceptable NominalizationType.ge_e PreverbalElement.rsp = true

Prefixes and RSPs show complementary distribution across -ung and Ge-...-e: pfx is accepted where RSP is rejected, and vice versa.

Ch. 5: this complementarity follows from the structural difference between head-level (pfx) and phrase-level (RSP) preverbal elements, interacting with the different structural requirements of -ung (requires full vP) vs Ge-...-e (directly nominalizes root).

theorem Benz2025.prt_accepted_in_both : peAcceptable NominalizationType.ung PreverbalElement.prt = true ∧ peAcceptable NominalizationType.ge_e PreverbalElement.prt = true

Particles are accepted in both -ung and Ge-...-e: they are structurally flexible enough to appear in both configurations.

theorem Benz2025.nom_inf_maximally_permissive (pe : PreverbalElement) : peAcceptable NominalizationType.nomInfinitive pe = true

Nominalized infinitives accept all three PE types.

theorem Benz2025.rsp_blocked_in_ung : peAcceptable NominalizationType.ung PreverbalElement.rsp = false

RSPs are blocked in -ung nominalizations — this connects to the co-occurrence restriction: RSPs as phrases cannot incorporate into the complex head structure that -ung creates.

theorem Benz2025.pfx_blocked_in_ge_e : peAcceptable NominalizationType.ge_e PreverbalElement.pfx = false

Prefixes are blocked in Ge-...-e nominalizations — the circumfix cannot wrap around a root that already has a prefix head.

theorem Benz2025.ung_head_phrase_pattern : peAcceptable NominalizationType.ung PreverbalElement.pfx = PreverbalElement.pfx.isHead ∧ peAcceptable NominalizationType.ung PreverbalElement.rsp = PreverbalElement.rsp.isHead

The head/phrase distinction predicts the -ung pattern: heads (pfx) are accepted, phrases (rsp) are not. Particles are the exception — separable but still accepted.

Benz's core theoretical argument (Chs. 4–5)

central claim is that the 9-cell co-occurrence paradigm (§6, Table 3) and the PE×nominalization distribution (§16, the table in Ch. 5) are not stipulated — they follow from the conjunction of two independently motivated principles:

1. Lexical Integrity (structural): a phrase cannot incorporate into a head. Only head+head or phrase+head are licit; head+phrase and phrase+phrase are not.

2. Result State Uniqueness (interpretive): an event can have at most one telos. Two elements that both obligatorily specify a result state cannot co-occur.

The types SynLevel and ResultStateSpec below formalize these two dimensions abstractly. The compatibility functions incorporationAllowed and resultStatesCompatible are defined purely over these abstract types, with no reference to PreverbalElement. Only then do we classify each PE into these dimensions and prove that the predicted paradigm matches.

inductive Benz2025.SynLevel : Type

The syntactic level of a morphological element: head (X⁰) or phrase (XP).

This distinction is standard in X-bar theory and is logically prior to the PE typology — it applies to any syntactic object, not just German preverbal elements.

• head : SynLevel
• phrase : SynLevel

@[implicit_reducible]

instance Benz2025.instDecidableEqSynLevel : DecidableEq SynLevel

Equations

• Benz2025.instDecidableEqSynLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benz2025.instReprSynLevel.repr : SynLevel → ℕ → Std.Format

Equations

• Benz2025.instReprSynLevel.repr Benz2025.SynLevel.head prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benz2025.SynLevel.head")).group prec✝
• Benz2025.instReprSynLevel.repr Benz2025.SynLevel.phrase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Benz2025.SynLevel.phrase")).group prec✝

@[implicit_reducible]

instance Benz2025.instReprSynLevel : Repr SynLevel

Equations

• Benz2025.instReprSynLevel = { reprPrec := Benz2025.instReprSynLevel.repr }

def Benz2025.incorporationAllowed (outer inner : SynLevel) : Bool

Lexical Integrity: a head can take a head complement (head-adjunction / incorporation), and a phrase can take a head complement (normal complementation), but a head cannot take a phrase complement in a word-internal structure, and two phrases cannot form a word.

This is a general principle of morphosyntactic structure, not specific to German preverbal elements. It follows from the ban on phrasal incorporation (§4.3.1, following Baker 1988).

Equations

• Benz2025.incorporationAllowed Benz2025.SynLevel.head Benz2025.SynLevel.head = true
• Benz2025.incorporationAllowed Benz2025.SynLevel.phrase Benz2025.SynLevel.head = true
• Benz2025.incorporationAllowed Benz2025.SynLevel.head Benz2025.SynLevel.phrase = false
• Benz2025.incorporationAllowed Benz2025.SynLevel.phrase Benz2025.SynLevel.phrase = false

inductive Benz2025.ResultStateSpec : Type

Whether an element obligatorily introduces a result state specification.

This is a semantic property that applies to any predicate-modifying element — it is not specific to German PEs. An element that always specifies a result state will conflict with another such element because a single event has at most one telos.

• specifies : ResultStateSpec
• neutral : ResultStateSpec

@[implicit_reducible]

instance Benz2025.instDecidableEqResultStateSpec : DecidableEq ResultStateSpec

Equations

• Benz2025.instDecidableEqResultStateSpec x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Benz2025.instReprResultStateSpec.repr : ResultStateSpec → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Benz2025.instReprResultStateSpec : Repr ResultStateSpec

Equations

• Benz2025.instReprResultStateSpec = { reprPrec := Benz2025.instReprResultStateSpec.repr }

def Benz2025.resultStatesCompatible (a b : ResultStateSpec) : Bool

Result State Uniqueness: two elements that both obligatorily specify a result state cannot co-occur, because a single event cannot be delimited by two conflicting endpoints.

This is an instance of a general thematic uniqueness constraint: just as an event has at most one agent (Carlson 1998), it has at most one telos. The constraint is purely interpretive — it says nothing about syntax.

Equations

• Benz2025.resultStatesCompatible Benz2025.ResultStateSpec.specifies Benz2025.ResultStateSpec.specifies = false
• Benz2025.resultStatesCompatible a b = true

def Benz2025.PreverbalElement.synLevel : PreverbalElement → SynLevel

Classify each PE by its syntactic level.

§4.3.1: prefixes are heads (inseparable under V2); particles and RSPs are phrases (stranded under V2, can be modified).

Equations

• Benz2025.PreverbalElement.pfx.synLevel = Benz2025.SynLevel.head
• Benz2025.PreverbalElement.prt.synLevel = Benz2025.SynLevel.phrase
• Benz2025.PreverbalElement.rsp.synLevel = Benz2025.SynLevel.phrase

def Benz2025.PreverbalElement.resultSpec : PreverbalElement → ResultStateSpec

Classify each PE by its result state specification.

§4.1: prefixes and RSPs obligatorily specify a result state. Particles are neutral — they can have non-delimiting readings (directional, completive) that do not introduce a result state.

Equations

• Benz2025.PreverbalElement.pfx.resultSpec = Benz2025.ResultStateSpec.specifies
• Benz2025.PreverbalElement.prt.resultSpec = Benz2025.ResultStateSpec.neutral
• Benz2025.PreverbalElement.rsp.resultSpec = Benz2025.ResultStateSpec.specifies

theorem Benz2025.synLevel_matches_isHead (pe : PreverbalElement) : (pe.synLevel == SynLevel.head) = pe.isHead

The abstract synLevel classification is equivalent to isHead.

theorem Benz2025.resultSpec_matches_alwaysSpecifies (pe : PreverbalElement) : (pe.resultSpec == ResultStateSpec.specifies) = pe.alwaysSpecifiesResult

The abstract resultSpec classification is equivalent to alwaysSpecifiesResult.

inductive Benz2025.Blocked : PreverbalElement → PreverbalElement → Prop

A blocking derivation: a proof that a PE combination violates one of Benz's two independently motivated principles.

Each constructor is a derivation rule whose premises are stated in terms of the abstract classification (SynLevel, ResultStateSpec), not PE-specific Booleans. A combination is blocked iff at least one derivation can be constructed.

byLexicalIntegrity (§4.3.1, Baker 1988): only heads can occupy the inner (closer-to-root) position in a word-internal combination. A phrasal inner element cannot incorporate.

byResultUniqueness (§4.1): an event has at most one telos. Two elements that both obligatorily specify a result state yield conflicting endpoints.

• byLexicalIntegrity {o i : PreverbalElement} : i.synLevel = SynLevel.phrase → Blocked o i
• byResultUniqueness {o i : PreverbalElement} : o.resultSpec = ResultStateSpec.specifies → i.resultSpec = ResultStateSpec.specifies → Blocked o i

theorem Benz2025.paradigm_from_principles (o i : PreverbalElement) : predictedAllowed o i = (incorporationAllowed o.synLevel i.synLevel && resultStatesCompatible o.resultSpec i.resultSpec)

Boolean decomposition lemma: predictedAllowed factors into the conjunction of the two abstract compatibility functions. Used as a stepping stone in the soundness proof below.

The derivation system (Blocked) is both sound and complete with respect to the empirical paradigm (predictedAllowed). Together with combined_prediction_matches (§9), this means the two principles exactly generate the data: every blocked cell has a derivation, every derivation corresponds to a blocked cell, and the unique allowed cell (PRT-pfx) has no derivation.

theorem Benz2025.blocked_sound {o i : PreverbalElement} (h : Blocked o i) : predictedAllowed o i = false

Soundness: every blocking derivation corresponds to a genuinely blocked combination. The theory does not over-generate.

• byLexicalIntegrity: a phrasal inner element makes incorporationAllowed return false regardless of the outer element's level.
• byResultUniqueness: two result-specifying elements make resultStatesCompatible return false regardless of structure.

theorem Benz2025.blocked_complete {o i : PreverbalElement} (h : predictedAllowed o i = false) : Blocked o i

Completeness: every blocked combination has a blocking derivation. The two principles account for ALL restrictions — nothing is left unexplained.

For each of the 8 blocked cells, an explicit derivation is constructed (6 by Lexical Integrity, 2 by Result State Uniqueness). For PRT-pfx, the hypothesis is contradictory.

theorem Benz2025.prt_pfx_no_derivation : ¬Blocked PreverbalElement.prt PreverbalElement.pfx

The allowed combination has no derivation. PRT-pfx is allowed precisely because neither principle applies:

• pfx is a head (not a phrase), so Lexical Integrity is satisfied
• prt is result-neutral (not specifying), so Result Uniqueness is satisfied

We examine each possible derivation and show its premises are contradicted by the PE classifications.

theorem Benz2025.pfx_pfx_only_by_result : Blocked PreverbalElement.pfx PreverbalElement.pfx ∧ PreverbalElement.pfx.synLevel ≠ SynLevel.phrase

pfx-pfx is blocked ONLY by Result State Uniqueness — Lexical Integrity cannot derive it (both are heads, so the inner is not phrasal). This shows the interpretive rule is not redundant.

theorem Benz2025.pfx_prt_only_by_structure : Blocked PreverbalElement.pfx PreverbalElement.prt ∧ PreverbalElement.prt.resultSpec ≠ ResultStateSpec.specifies

pfx-PRT is blocked ONLY by Lexical Integrity — Result State Uniqueness cannot derive it (PRT is result-neutral). This shows the structural rule is not redundant.

theorem Benz2025.incorporation_only_depends_on_inner (outer inner : SynLevel) : incorporationAllowed outer inner = (inner == SynLevel.head)

Incorporation depends only on the inner element's level: the outer element's level is irrelevant. This is a derived property of the incorporationAllowed function, not stipulated.

theorem Benz2025.ung_from_principles (pe : PreverbalElement) : peAcceptable NominalizationType.ung pe = (incorporationAllowed pe.synLevel pe.synLevel || resultStatesCompatible pe.resultSpec pe.resultSpec)

The nominalization theorem. -ung acceptability (Ch. 5) follows from the same two abstract principles applied reflexively: a PE is acceptable in -ung iff it can incorporate with itself (headedness) OR its result state does not conflict with itself (neutrality).

This connects Ch. 5 to Ch. 4: the PE×nominalization distribution is not an independent observation — it is a projection of the same two principles that generate the co-occurrence paradigm.

theorem Benz2025.ge_e_from_principles (pe : PreverbalElement) : peAcceptable NominalizationType.ge_e pe = (pe.synLevel == SynLevel.phrase)

Ge-...-e acceptability reduces to a single abstract principle: a PE is acceptable in Ge-...-e iff it is a phrase (not a head). The circumfix directly nominalizes the root, so only non-head elements are compatible.

theorem Benz2025.ung_ge_e_mirror (pe : PreverbalElement) (h : pe.synLevel = SynLevel.head) : peAcceptable NominalizationType.ung pe = true ∧ peAcceptable NominalizationType.ge_e pe = false

The -ung / Ge-...-e mirror: for heads, the two nominalization types give opposite results. This follows from ge_e_from_principles and the fact that heads satisfy incorporationAllowed reflexively.

These theorems chain through four independently defined modules: RootTypology.lean (root semantics) → Allosemy.lean (v alloseme selection) → Allosemy.lean (nominalization reading) → Benz2025.lean (PE distribution from abstract principles). No single module defines the full path.

theorem Benz2025.end_to_end_result_root : have v := Morphology.DM.Allosemy.VAlloseme.fromRootType RootType.result; v = Morphology.DM.Allosemy.VAlloseme.eventive ∧ Morphology.DM.Allosemy.readingFromAllosemes v Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent ∧ incorporationAllowed PreverbalElement.pfx.synLevel PreverbalElement.pfx.synLevel = true ∧ resultStatesCompatible PreverbalElement.rsp.resultSpec PreverbalElement.rsp.resultSpec = false

End-to-end for result roots: a result root selects eventive v, yielding CEN in -ung nominalizations. -ung accepts heads (pfx) and rejects phrases that specify results (RSP) — both predictions derived from the abstract principles, not from the peAcceptable table.

theorem Benz2025.end_to_end_pc_root : have v := Morphology.DM.Allosemy.VAlloseme.fromRootType RootType.propertyConcept; v = Morphology.DM.Allosemy.VAlloseme.zero ∧ Morphology.DM.Allosemy.readingFromAllosemes v Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity ∧ (PreverbalElement.rsp.synLevel == SynLevel.phrase) = true ∧ (PreverbalElement.pfx.synLevel == SynLevel.phrase) = false

Mirror chain for PC roots: zero v → simple entity reading → Ge-...-e, which accepts phrases (RSP) and rejects heads (pfx).

def Benz2025.canUngNominalize : Option Features.VendlerClass → Bool

Whether a verb can undergo -ung nominalization, based on its Vendler class.

Ch. 5, following Roßdeutscher & Kamp (2010): -ung requires complex change-of-state event structure. Only accomplishments and achievements (which contain a result state component) qualify. Activities and states do not.

Equations

• Benz2025.canUngNominalize (some Features.VendlerClass.accomplishment) = true
• Benz2025.canUngNominalize (some Features.VendlerClass.achievement) = true
• Benz2025.canUngNominalize x✝ = false

theorem Benz2025.activity_no_ung : canUngNominalize Fragments.German.Predicates.haemmern.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.malen.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.kuessen.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.fuehren.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.rauben.vendlerClass = false

Activity simplex verbs cannot form -ung nominalizations: *Hämmer-ung, *Mal-ung, *Küss-ung.

theorem Benz2025.complex_event_ung : canUngNominalize Fragments.German.Predicates.beobachten.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.einfuehren.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.verbinden.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.brechen.vendlerClass = true

Prefix/particle verbs with complex event structure CAN form -ung nominalizations: Beobacht-ung, Einführ-ung, Verbind-ung.

def Benz2025.isTransitiveVerb (v : Fragments.German.Predicates.GermanVerbEntry) : Bool

Transitivity derived from fragment fields (not from a raw string).

Equations

• Benz2025.isTransitiveVerb v = (v.complementType == Semantics.Lexical.ComplementType.np && !v.unaccusative)

theorem Benz2025.rsp_data_grounded_in_fragments : isTransitiveVerb Fragments.German.Predicates.haemmern = true ∧ isTransitiveVerb Fragments.German.Predicates.brechen = true ∧ Fragments.German.Predicates.frieren.unaccusative = true ∧ isTransitiveVerb Fragments.German.Predicates.frieren = false

The verb classifications in the RSP data (§10, encoded as raw strings) are derivable from the fragment entries' typed fields. Changing frieren's unaccusative field or hämmern's complementType would break this theorem without touching the RSP data.

theorem Benz2025.rootType_alloseme_divergence : Option.map Morphology.DM.Allosemy.VAlloseme.fromRootType Fragments.German.Predicates.brechen.rootType = some Morphology.DM.Allosemy.VAlloseme.eventive ∧ Option.map Morphology.DM.Allosemy.VAlloseme.fromRootType Fragments.German.Predicates.frieren.rootType = some Morphology.DM.Allosemy.VAlloseme.zero ∧ Option.map (fun (x : RootType) => (Morphology.DM.Allosemy.VAlloseme.fromRootType x).introducesEvent) Fragments.German.Predicates.brechen.rootType = some true ∧ Option.map (fun (x : RootType) => (Morphology.DM.Allosemy.VAlloseme.fromRootType x).introducesEvent) Fragments.German.Predicates.frieren.rootType = some false

brechen (result root) and frieren (PC root) yield opposite v allosemes. This connects three modules: the fragment entry's rootType (Predicates.lean), VAlloseme.fromRootType (Allosemy.lean), and VAlloseme.introducesEvent (Allosemy.lean).

theorem Benz2025.brechen_two_paths : (Fragments.German.Predicates.brechen.rootType.bind fun (rt : RootType) => Morphology.DM.Allosemy.readingFromAllosemes (Morphology.DM.Allosemy.VAlloseme.fromRootType rt) Morphology.DM.Allosemy.NAlloseme.sortal) = some Morphology.DM.Allosemy.NominalizationReading.complexEvent ∧ canUngNominalize Fragments.German.Predicates.brechen.vendlerClass = true

The allosemy-based CEN prediction and the event-structure-based -ung prediction agree for brechen: result root → eventive v → CEN reading → can -ung, and achievement vendlerClass → can -ung. Two independent paths to the same conclusion.

theorem Benz2025.frieren_canonical_vs_possible : (Fragments.German.Predicates.frieren.rootType.bind fun (rt : RootType) => Morphology.DM.Allosemy.readingFromAllosemes (Morphology.DM.Allosemy.VAlloseme.fromRootType rt) Morphology.DM.Allosemy.NAlloseme.sortal) = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity ∧ canUngNominalize Fragments.German.Predicates.frieren.vendlerClass = true ∧ Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent

The two paths DISAGREE for frieren: the canonical PC root → zero v → RN (not CEN), yet the achievement vendlerClass → can -ung. This is not a bug — it captures key insight that allosemy means BOTH v allosemes are available for any verb. The canonical alloseme is a default, not a constraint. Frieren CAN have eventive v and thus CAN form a CEN, even though its canonical alloseme is zero.