Benz (2025): Structure and interpretation across categories

Three case studies on the syntax–LF interface in German run on the contextual-allosemy substrate of DistributedMorphology.Allosemy ([Ben25]). One nominalization structure yields the event, referential and content readings of Beobachtung, the variation lying in the allosemes of v and n (Ch. 3, after [Woo23]). The co-occurrence restrictions among inseparable prefixes, separable particles and resultative secondary predicates follow from a phrase-structural factor, that the inner element be a head, together with an event-structural one, [Ten94]'s Single Delimiting Constraint (Ch. 4), and the particle "structure problem" of [Lud01] is solved differently by the three nominalization types, whose distribution of preverbal elements follows from their solutions, while -ung further demands the complex change-of-state structure of [RK10] (Ch. 5).

Implementation notes

Alloseme selection is the substrate's own engine: allosemes are Vocabulary Items over neighborhoods, applicability is the Subset Principle, and the canonical choice is Elsewhere competition. The readings are derived from typed denotations, and the co-occurrence and nominalization paradigms are predicted cell by cell against the example rows, the Table 3 combinations, the resultative data of [Cre20] and the -ung and Ge-…-e forms of Ch. 5, with the base verbs read from the German fragment.

References

• [Ben25]
• [Woo23]
• [Ten94]
• [Lud01]
• [RK10]
• [Wil15]
• [Cre20]

def Benz2025.entryOf (form : String) : Option German.Verb

The fragment entry of a verb form named in a row.

Equations

• Benz2025.entryOf form = List.find? (fun (x : German.Verb) => decide (x.form = form)) German.Verbs.allVerbs

Content nominalizations (Ch. 3)

def Benz2025.beobachtungRows : List Datum

The (32) stimulus rows, in margin-label order Event, RN, Content.

Equations

• Benz2025.beobachtungRows = [Benz2025.Examples.ex32a, Benz2025.Examples.ex32b, Benz2025.Examples.ex32c]

def Benz2025.readingOf (e : Datum) : Option DistributedMorphology.Allosemy.NominalizationReading

The reading a stimulus row exemplifies, from its reading feature. The paper's loose "RN" label is rendered as the simple entity reading.

Equations

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

Readings from allosemes

def Benz2025.adoptedAllosemes : DistributedMorphology.Allosemy.NominalizationReading → DistributedMorphology.Allosemy.Verbalizer.Alloseme × DistributedMorphology.Allosemy.Nominalizer.Alloseme

The alloseme pair deriving each reading on the adopted analysis, where v is semantically vacuous on all readings but the CEN (§3.5, following [Woo23]). By adopted_roundtrip and adopted_unique, this is the unique derivation of each reading in which the two heads are not both contentful.

Equations

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

theorem Benz2025.adopted_roundtrip (r : DistributedMorphology.Allosemy.NominalizationReading) : DistributedMorphology.Allosemy.readingFromAllosemes (adoptedAllosemes r).1 (adoptedAllosemes r).2 = some r

Each reading is recovered from its adopted alloseme pair.

theorem Benz2025.adopted_unique (r : DistributedMorphology.Allosemy.NominalizationReading) (v : DistributedMorphology.Allosemy.Verbalizer.Alloseme) (n : DistributedMorphology.Allosemy.Nominalizer.Alloseme) (hr : DistributedMorphology.Allosemy.readingFromAllosemes v n = some r) (h : v.introducesEvent = false ∨ n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero) : (v, n) = adoptedAllosemes r

Among derivations in which the two heads are not both contentful, the adopted pair is the only one deriving the reading: economy of interpretation pins the analysis.

theorem Benz2025.reading_determines_contentful_head (v : DistributedMorphology.Allosemy.Verbalizer.Alloseme) (n : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : (DistributedMorphology.Allosemy.readingFromAllosemes v n = some DistributedMorphology.Allosemy.NominalizationReading.complexEvent → v.introducesEvent = true ∧ n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero) ∧ (DistributedMorphology.Allosemy.readingFromAllosemes v n = some DistributedMorphology.Allosemy.NominalizationReading.result → n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.result) ∧ (DistributedMorphology.Allosemy.readingFromAllosemes v n = some DistributedMorphology.Allosemy.NominalizationReading.content → n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.content)

The reading pins the division of labor (the "mirror image" claim of §3.5): an event reading arises only from contentful v with vacuous n, while a result or content reading forces the corresponding contentful n, whatever v contributes.

Alloseme selection in the nominalization structure

def Benz2025.vContext (eventive : Bool) : DistributedMorphology.Neighborhood (List DistributedMorphology.Allosemy.Feature)

vContext eventive is v's context in the nominalization structure [n [v √]], with the root, event-entailing or not, as its complement and n above it.

Equations

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

def Benz2025.nContext (eventive : Bool) : DistributedMorphology.Neighborhood (List DistributedMorphology.Allosemy.Feature)

nContext eventive is n's context in [n [v √]], with a verbal complement, eventive or not.

Equations

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

def Benz2025.availableReadings (eventive : Bool) : List DistributedMorphology.Allosemy.NominalizationReading

availableReadings eventive lists the readings derivable in the nominalization structure, those of any licensed v alloseme composed with any licensed n alloseme.

Equations

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

theorem Benz2025.v_allosemes_licensed : DistributedMorphology.Allosemy.licensed DistributedMorphology.Allosemy.Verbalizer.vocabulary (vContext true) = [DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive, DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero] ∧ DistributedMorphology.Allosemy.licensed DistributedMorphology.Allosemy.Verbalizer.vocabulary (vContext false) = [DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero]

Over an event-entailing root both v allosemes are licensed, the premise of the reading ambiguity, while a non-eventive root licenses only vacuous v.

theorem Benz2025.fromRootType_is_selectBy_winner (rt : Semantics.Root.ChangeType) : Option.map (fun (x : DistributedMorphology.VocabularyItem DistributedMorphology.Allosemy.Feature DistributedMorphology.Allosemy.Verbalizer.Alloseme) => x.exponent) (DistributedMorphology.winner? DistributedMorphology.Allosemy.Verbalizer.vocabulary (vContext (decide (rt = Semantics.Root.ChangeType.result)))) = some (DistributedMorphology.Allosemy.Verbalizer.Alloseme.fromRootType rt)

The canonical v alloseme of the root typology is the engine's Elsewhere winner: the more specified eventive entry beats vacuous v exactly when the root entails an event.

theorem Benz2025.beobachtung_readings_available (r : DistributedMorphology.Allosemy.NominalizationReading) : r ∈ List.filterMap readingOf beobachtungRows → r ∈ availableReadings true

Every attested Beobachtung reading ((32)) is available in the single structure: the engine licenses the allosemes and composition delivers the readings.

theorem Benz2025.nonEventive_readings : availableReadings false = [DistributedMorphology.Allosemy.NominalizationReading.content, DistributedMorphology.Allosemy.NominalizationReading.simpleEvent, DistributedMorphology.Allosemy.NominalizationReading.simpleState, DistributedMorphology.Allosemy.NominalizationReading.simpleEntity]

Without an event-entailing root neither the complex event nor the result reading is derivable; the content reading survives, since simple content nouns like Gerücht 'rumor' need no verbal source (Table 2).

Typed alloseme denotations (Ch. 3)

The denotations of the deverbal allosemes, after [Woo23] as taken over in Ch. 3: nominalization semantics runs over a domain in which eventualities are entities, and each n alloseme builds an entity predicate from what v hands it. The reading typology is then derived, not tabulated: readings exist exactly where the composition is defined (readingFromAllosemes_isSome_iff_denote), and the analytical options for the result and content readings compose to identical entity predicates (result_options_pred_agree, content_options_agree).

structure Benz2025.NominalizationModel (E : Type u_3) (S : Type u_4) : Type (max u_3 u_4)

A model for nominalization denotations embeds the eventualities into the entity domain, since a nominal can describe an event as an entity, and splits them into stative and dynamic; result relates an entity to the eventuality that produced it, and hasContent picks out the entities with propositional content.

• ev : S → E

  Eventualities as entities.

• ev_injective : Function.Injective self.ev
• stative : S → Prop

  Stative eventualities.

• result : E → S → Prop

  The entity is the result of the eventuality.

• hasContent : E → Prop

  The entity has propositional content (rumor, idea, claim).

structure Benz2025.RootMeaning (E : Type u_3) (S : Type u_4) : Type (max u_3 u_4)

A root contributes to nominalization semantics what it says of entities and of eventualities, and its Theme relation, which relates an eventuality of the root's kind to the entity it is predicated of.

• onEntities : E → Prop
• onEvents : S → Prop
• theme : E → S → Prop

inductive Benz2025.VerbalDenotation (E : Type u_3) (S : Type u_4) : Type (max u_3 u_4)

v hands to n verbal event content together with the Theme position it introduces under the eventive alloseme (§2.2), and the untouched root with no argument position under the zero alloseme, since v then introduces none (§3.5).

• eventive {E : Type u_3} {S : Type u_4} (p : S → Prop) (theme : E → S → Prop) : VerbalDenotation E S
• zero {E : Type u_3} {S : Type u_4} (ρ : RootMeaning E S) : VerbalDenotation E S

def Benz2025.denoteV {E : Type u_1} {S : Type u_2} (ρ : RootMeaning E S) : DistributedMorphology.Allosemy.Verbalizer.Alloseme → VerbalDenotation E S

denoteV ρ a applies the v alloseme a to the root ρ.

Equations

• Benz2025.denoteV ρ (some DistributedMorphology.Allosemy.Verbalizer.Contentful.eventive) = Benz2025.VerbalDenotation.eventive ρ.onEvents ρ.theme
• Benz2025.denoteV ρ none = Benz2025.VerbalDenotation.zero ρ

structure Benz2025.NominalDenotation (E : Type u_3) (S : Type u_4) : Type u_3

A nominal denotation is the entity predicate, together with the internal-argument relation when the nominal retains one. The relation is present exactly when v introduced the Theme position — no such position is part of the denotation unless v contributes it (§2.2, §3.5).

• pred : E → Prop

  What the nominal describes.

• internalArg : Option (E → E → Prop)

  internalArg y x holds when y saturates the Theme position of the nominal x (the observation of the sky).

def Benz2025.denoteN {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) : VerbalDenotation E S → DistributedMorphology.Allosemy.Nominalizer.Alloseme → Option (NominalDenotation E S)

denoteN m d a applies the n alloseme a to v's output d, and is none where the combination is uninterpretable. The CEN describes the events the verb describes and retains the Theme position v introduced; the SEN predicates the root's entity content of an event-entity; the result alloseme picks out what an event of the root's kind produced ([Woo23]'s denotation); the content alloseme ignores the verbal layer entirely. The non-deverbal allosemes have their semantics in Semantics/Possession/Relationalizer.lean.

Equations

• One or more equations did not get rendered due to their size.
• Benz2025.denoteN m (Benz2025.VerbalDenotation.eventive p theme) (some DistributedMorphology.Allosemy.Nominalizer.Contentful.content) = some { pred := m.hasContent }
• Benz2025.denoteN m (Benz2025.VerbalDenotation.zero ρ) (some DistributedMorphology.Allosemy.Nominalizer.Contentful.entity) = some { pred := ρ.onEntities }
• Benz2025.denoteN m (Benz2025.VerbalDenotation.zero ρ) (some DistributedMorphology.Allosemy.Nominalizer.Contentful.content) = some { pred := m.hasContent }
• Benz2025.denoteN m x✝¹ x✝ = none

theorem Benz2025.result_options_pred_agree {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) : Option.map (fun (x : NominalDenotation E S) => x.pred) (denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) DistributedMorphology.Allosemy.Nominalizer.Alloseme.result) = Option.map (fun (x : NominalDenotation E S) => x.pred) (denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero) DistributedMorphology.Allosemy.Nominalizer.Alloseme.result)

The event and result readings are mirror images at the entity-predicate level: the two analytical options for the result reading — eventive v with n's result alloseme, or vacuous v with the same — agree on what the nominal describes (§3.5, crediting [Woo23]).

theorem Benz2025.result_options_disagree_on_arguments {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) : (∃ (r : NominalDenotation E S), denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) DistributedMorphology.Allosemy.Nominalizer.Alloseme.result = some r ∧ r.internalArg.isSome = true) ∧ ∃ (r : NominalDenotation E S), denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero) DistributedMorphology.Allosemy.Nominalizer.Alloseme.result = some r ∧ r.internalArg = none

...but not on argument structure: on the both-heads-interpreted option the result nominal retains the internal-argument position v introduced, on the v-vacuous option it has none. Since result nominals cannot saturate an internal argument, this is the reason for adopting the vacuous option for the RN reading (§3.5, following [Woo23]).

theorem Benz2025.cen_retains_argument_structure {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) : ∃ (r : NominalDenotation E S), denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero = some r ∧ r.internalArg.isSome = true

CENs retain argument structure: the complex event nominal carries the Theme position v introduced (the observation of the sky), which is what separates it from every zero-v reading (zero_v_no_argument_structure).

theorem Benz2025.zero_v_no_argument_structure {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) (n : DistributedMorphology.Allosemy.Nominalizer.Alloseme) {r : NominalDenotation E S} (h : denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero) n = some r) : r.internalArg = none

No zero-v reading has an internal-argument position: none is introduced by v, so none is part of the denotation (§3.5).

theorem Benz2025.content_options_agree {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) : denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) DistributedMorphology.Allosemy.Nominalizer.Alloseme.content = denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero) DistributedMorphology.Allosemy.Nominalizer.Alloseme.content

The content reading likewise ignores the verbal layer: both v options compose to hasContent, which is how simple content nouns can have the reading with no verbal source at all (§3.5).

theorem Benz2025.readingFromAllosemes_isSome_iff_denote {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) (v : DistributedMorphology.Allosemy.Verbalizer.Alloseme) (n : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : (DistributedMorphology.Allosemy.readingFromAllosemes v n).isSome = true ↔ (denoteN m (denoteV ρ v) n).isSome = true

The reading typology tracks denotational definedness: a (v, n) pair has a reading exactly when its composed denotation is defined.

theorem Benz2025.cen_denotes_events {E : Type u_1} {S : Type u_2} (m : NominalizationModel E S) (ρ : RootMeaning E S) {r : NominalDenotation E S} (h : denoteN m (denoteV ρ DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero = some r) (x : E) : r.pred x → ∃ (e : S), x = m.ev e

A complex event nominal holds only of event-entities: the ground of its event reading (temporal modification, aspectual behavior).

Prefixes, particles, and resultatives (Ch. 4)

inductive Benz2025.PreverbalElement : Type

A German preverbal element is an inseparable prefix (be-, ent-, er-, ver-, zer-), a separable particle (ab-, an-, auf-, aus-, ein-) or a resultative secondary predicate (platt, tot, kaputt).

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

@[instance_reducible]

instance Benz2025.instDecidableEqPreverbalElement : DecidableEq PreverbalElement

Equations

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

@[instance_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.

@[instance_reducible]

instance Benz2025.instFintypePreverbalElement : Fintype PreverbalElement

Equations

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

inductive Benz2025.SynLevel : Type

A head, which can sit inside a complex head, or a phrase, which cannot incorporate.

• head : SynLevel
• phrase : SynLevel

@[instance_reducible]

instance Benz2025.instDecidableEqSynLevel : DecidableEq SynLevel

Equations

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

@[instance_reducible]

instance Benz2025.instReprSynLevel : Repr SynLevel

Equations

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

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✝

def Benz2025.PreverbalElement.synLevel : PreverbalElement → SynLevel

Prefixes are heads forming a complex head with the root, inseparable under V2 movement; particles and resultatives are phrasal, stranded under V2 ([Wur98], [Zel01]).

Equations

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

inductive Benz2025.ResultStateSpec : Type

An element either obligatorily specifies a result state, as prefixes and resultatives do, or does not, as particles with their non-delimiting directional and completive readings (§4.4).

• specifies : ResultStateSpec
• neutral : ResultStateSpec

@[instance_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.

@[instance_reducible]

instance Benz2025.instReprResultStateSpec : Repr ResultStateSpec

Equations

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

def Benz2025.PreverbalElement.resultSpec : PreverbalElement → ResultStateSpec

Equations

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

The two factors

def Benz2025.IncorporationAllowed (_outer inner : SynLevel) : Prop

The inner element, closer to the root, must be a head: a head outside a phrase cannot form a complex head with the root, and a phrasal outer element competes with a phrasal inner one for the verb's single complement position (§4.4).

Equations

• Benz2025.IncorporationAllowed _outer inner = (inner = Benz2025.SynLevel.head)

@[instance_reducible]

instance Benz2025.instDecidableIncorporationAllowed (outer inner : SynLevel) : Decidable (IncorporationAllowed outer inner)

Equations

• Benz2025.instDecidableIncorporationAllowed outer inner = Benz2025.instDecidableIncorporationAllowed._aux_1 outer inner

def Benz2025.ResultStatesCompatible (a b : ResultStateSpec) : Prop

Two obligatory result-state specifiers conflict, since the end state of a complex event is specified once: [Ten94]'s Single Delimiting Constraint, (159).

Equations

• Benz2025.ResultStatesCompatible a b = ¬(a = Benz2025.ResultStateSpec.specifies ∧ b = Benz2025.ResultStateSpec.specifies)

@[instance_reducible]

instance Benz2025.instDecidableResultStatesCompatible (a b : ResultStateSpec) : Decidable (ResultStatesCompatible a b)

Equations

• Benz2025.instDecidableResultStatesCompatible a b = { decide := !decide (a = Benz2025.ResultStateSpec.specifies ∧ b = Benz2025.ResultStateSpec.specifies), reflects_decide := ⋯ }

def Benz2025.StructurallyCompatible (outer inner : PreverbalElement) : Prop

Equations

• Benz2025.StructurallyCompatible outer inner = Benz2025.IncorporationAllowed outer.synLevel inner.synLevel

def Benz2025.InterpretivelyCompatible (outer inner : PreverbalElement) : Prop

Equations

• Benz2025.InterpretivelyCompatible outer inner = Benz2025.ResultStatesCompatible outer.resultSpec inner.resultSpec

def Benz2025.Allowed (outer inner : PreverbalElement) : Prop

A combination is predicted possible iff both factors permit it (§4.4).

Equations

• Benz2025.Allowed outer inner = (Benz2025.StructurallyCompatible outer inner ∧ Benz2025.InterpretivelyCompatible outer inner)

@[instance_reducible]

instance Benz2025.instDecidableStructurallyCompatible (outer inner : PreverbalElement) : Decidable (StructurallyCompatible outer inner)

Equations

• Benz2025.instDecidableStructurallyCompatible outer inner = Benz2025.instDecidableStructurallyCompatible._aux_1 outer inner

@[instance_reducible]

instance Benz2025.instDecidableInterpretivelyCompatible (outer inner : PreverbalElement) : Decidable (InterpretivelyCompatible outer inner)

Equations

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

@[instance_reducible]

instance Benz2025.instDecidableAllowed (outer inner : PreverbalElement) : Decidable (Allowed outer inner)

Equations

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

theorem Benz2025.allowed_iff (outer inner : PreverbalElement) : Allowed outer inner ↔ outer = PreverbalElement.prt ∧ inner = PreverbalElement.pfx

The particle-over-prefix order is the one allowed combination ((84) aus-er-wählen, an-ver-trauen, vor-ent-halten).

theorem Benz2025.two_factors_needed : (StructurallyCompatible PreverbalElement.pfx PreverbalElement.pfx ∧ ¬Allowed PreverbalElement.pfx PreverbalElement.pfx) ∧ InterpretivelyCompatible PreverbalElement.pfx PreverbalElement.prt ∧ ¬Allowed PreverbalElement.pfx PreverbalElement.prt

Neither factor alone predicts the paradigm: structure permits prefix over prefix, which the constraint excludes, and the constraint permits prefix over particle, which structure excludes.

theorem Benz2025.prt_rsp_particle_dependent : ¬StructurallyCompatible PreverbalElement.prt PreverbalElement.rsp ∧ InterpretivelyCompatible PreverbalElement.prt PreverbalElement.rsp

The printed Table 3 marks the merged pfx/PRT-RSP row's interpretation cell excluded, but on the account's own classification only the prefix half is: for a particle over a resultative the structural factor does the work, and only some such verbs are also ruled out semantically (§4.4).

Blocking derivations

inductive Benz2025.Blocked : PreverbalElement → PreverbalElement → Prop

A derivation that a combination violates one of the two principles.

• byPhrasalInner {o i : PreverbalElement} : i.synLevel = SynLevel.phrase → Blocked o i

  A phrasal element cannot occupy the inner position (§4.4).

• bySingleDelimiting {o i : PreverbalElement} : o.resultSpec = ResultStateSpec.specifies → i.resultSpec = ResultStateSpec.specifies → Blocked o i

  Two obligatory result-state specifiers conflict ((159)).

theorem Benz2025.blocked_iff (outer inner : PreverbalElement) : Blocked outer inner ↔ ¬Allowed outer inner

The two principles generate exactly the paradigm: a combination has a blocking derivation iff it is not allowed.

The paradigm against the examples

def Benz2025.elementOf : String → Option PreverbalElement

Equations

• Benz2025.elementOf "pfx" = some Benz2025.PreverbalElement.pfx
• Benz2025.elementOf "prt" = some Benz2025.PreverbalElement.prt
• Benz2025.elementOf "rsp" = some Benz2025.PreverbalElement.rsp
• Benz2025.elementOf x✝ = none

def Benz2025.CellAcceptable (e : Datum) : Prop

CellAcceptable e holds when the combination the row tests is acceptable, the combination being the row's alternative where it gives one ((87) and (88) pair a resultative baseline with the blocked prefixed or particle form) and the row itself otherwise.

Equations

• Benz2025.CellAcceptable e = match e.alternatives with | [] => e.judgment = Judgment.acceptable | a :: tail => a.2 = Judgment.acceptable

@[instance_reducible]

instance Benz2025.instDecidableCellAcceptable (e : Datum) : Decidable (CellAcceptable e)

Equations

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

theorem Benz2025.allowed_rows (e : Datum) : e ∈ Examples.all → ∀ o ∈ (e.feature? "outer").bind elementOf, ∀ i ∈ (e.feature? "inner").bind elementOf, Allowed o i ↔ CellAcceptable e

Table 3 agrees with its examples ((81)–(84), (86)–(88)): a combination is acceptable exactly when both factors allow it.

German resultative data (§4.2)

Complex predicate semantics after [Wil15], adopted at (158): the M(eans) predicate is the verb, the R(esult) predicate the resultative, and the End Theme Postulate (108) links the complex event's Theme to the end state.

def Benz2025.rspRows : List Datum

The resultative stimulus rows ((89), (115); the (115) rows are due to [Cre20]).

Equations

• Benz2025.rspRows = [Benz2025.Examples.ex89a, Benz2025.Examples.ex89b, Benz2025.Examples.ex115a, Benz2025.Examples.ex115e, Benz2025.Examples.ex115f]

theorem Benz2025.rsp_rows_have_entries (e : Datum) : e ∈ rspRows → ((e.feature? "m_predicate").bind entryOf).isSome = true

Every resultative row names a means predicate with a fragment entry.

theorem Benz2025.rsp_verb_classes (e : Datum) : e ∈ rspRows → ∀ v ∈ (e.feature? "m_predicate").bind entryOf, e.feature? "verb_class" = some "unaccusative" ↔ v.IsUnaccusative

The rows' verb-class labels follow the fragment entries of their means predicates.

theorem Benz2025.unaccusative_means : ∃ e ∈ rspRows, ∃ v ∈ (e.feature? "m_predicate").bind entryOf, v.IsUnaccusative

German allows non-unergative means predicates in resultatives ((115e) frieren), against weak-resultative reanalyses of the whole class.

Prefixes in nominalizations (Ch. 5)

inductive Benz2025.NominalizationType : Type

German nominalizes by -ung suffixation, by Ge-…-e circumfixation, and by the nominalized infinitive.

• ung : NominalizationType
• geE : NominalizationType
• infinitive : NominalizationType

@[instance_reducible]

instance Benz2025.instDecidableEqNominalizationType : DecidableEq NominalizationType

Equations

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

@[instance_reducible]

instance Benz2025.instReprNominalizationType : Repr NominalizationType

Equations

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

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

Equations

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

inductive Benz2025.StructureSolution : Type

A solution to the particle structure problem ([Lud01]), how a phrasal particle ends up inside a derived nominal: the nominalizer takes phrasal structure, the particle attaches low as a head, or the particle attaches outside the nominalizer.

• phrasalInput : StructureSolution
• particleAsHead : StructureSolution
• outerAttachment : StructureSolution

@[instance_reducible]

instance Benz2025.instDecidableEqStructureSolution : DecidableEq StructureSolution

Equations

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

def Benz2025.instReprStructureSolution.repr : StructureSolution → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Benz2025.instReprStructureSolution : Repr StructureSolution

Equations

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

def Benz2025.NominalizationType.solution : NominalizationType → StructureSolution

The solution each type favors (§5.2–5.4): nominalized infinitives take phrasal inputs, -ung particles as heads, Ge-…-e outer attachment ((223)), since its eventive semantics without an internal argument conflicts with prefix verbs' argument-structural demands.

Equations

• Benz2025.NominalizationType.infinitive.solution = Benz2025.StructureSolution.phrasalInput
• Benz2025.NominalizationType.ung.solution = Benz2025.StructureSolution.particleAsHead
• Benz2025.NominalizationType.geE.solution = Benz2025.StructureSolution.outerAttachment

def Benz2025.PreverbalElement.CanAttachAsHead : PreverbalElement → Prop

The element can attach as a non-phrasal head: prefixes always, particles low (§5.3), and resultatives never ((205)–(206)).

Equations

• Benz2025.PreverbalElement.rsp.CanAttachAsHead = False
• x✝.CanAttachAsHead = True

@[instance_reducible]

instance Benz2025.instDecidablePredPreverbalElementCanAttachAsHead : DecidablePred PreverbalElement.CanAttachAsHead

Equations

• Benz2025.instDecidablePredPreverbalElementCanAttachAsHead Benz2025.PreverbalElement.pfx = { decide := true, reflects_decide := Benz2025.instDecidablePredPreverbalElementCanAttachAsHead._proof_1 }
• Benz2025.instDecidablePredPreverbalElementCanAttachAsHead Benz2025.PreverbalElement.prt = { decide := true, reflects_decide := Benz2025.instDecidablePredPreverbalElementCanAttachAsHead._proof_2 }
• Benz2025.instDecidablePredPreverbalElementCanAttachAsHead Benz2025.PreverbalElement.rsp = { decide := false, reflects_decide := Benz2025.instDecidablePredPreverbalElementCanAttachAsHead._proof_3 }

def Benz2025.StructureSolution.Admits : StructureSolution → PreverbalElement → Prop

s.Admits pe holds when the solution s accommodates the element pe: phrasal inputs admit everything, particles-as-heads the head-attachers, outer attachment the phrasal elements, since a prefix is a verbal head and cannot attach outside a noun.

Equations

• Benz2025.StructureSolution.phrasalInput.Admits x✝ = True
• Benz2025.StructureSolution.particleAsHead.Admits x✝ = x✝.CanAttachAsHead
• Benz2025.StructureSolution.outerAttachment.Admits x✝ = (x✝.synLevel = Benz2025.SynLevel.phrase)

@[instance_reducible]

instance Benz2025.instDecidableAdmits (s : StructureSolution) (pe : PreverbalElement) : Decidable (s.Admits pe)

Equations

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

def Benz2025.CanUngNominalize (v : German.Verb) : Prop

-ung requires complex change-of-state event structure ([RK10], endorsed at §5.3.1), the accomplishments of the fragment.

Equations

• Benz2025.CanUngNominalize v = (v.vendlerClass = some Aspect.VendlerClass.accomplishment)

@[instance_reducible]

instance Benz2025.instDecidableCanUngNominalize (v : German.Verb) : Decidable (CanUngNominalize v)

Equations

• Benz2025.instDecidableCanUngNominalize v = Benz2025.instDecidableCanUngNominalize._aux_1 v

def Benz2025.typeOf : String → Option NominalizationType

Equations

• Benz2025.typeOf "ung" = some Benz2025.NominalizationType.ung
• Benz2025.typeOf "geE" = some Benz2025.NominalizationType.geE
• Benz2025.typeOf "infinitive" = some Benz2025.NominalizationType.infinitive
• Benz2025.typeOf x✝ = none

def Benz2025.nominalizationOf (e : Datum) : Option NominalizationType

A row's nominalization type.

Equations

• Benz2025.nominalizationOf e = (e.feature? "nominalization").bind Benz2025.typeOf

def Benz2025.Predicted (e : Datum) : Prop

Predicted e holds when the account predicts the nominalization row e: the type's solution accommodates the preverbal element, and an -ung form has a base with complex change-of-state structure.

Equations

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

@[instance_reducible]

instance Benz2025.instDecidablePredicted (e : Datum) : Decidable (Predicted e)

Equations

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

theorem Benz2025.nominalization_rows_have_entries (e : Datum) : e ∈ Examples.all → (nominalizationOf e).isSome = true → ((e.feature? "verb").bind entryOf).isSome = true

Every nominalization row names a verb with a fragment entry.

theorem Benz2025.nominalization_rows (e : Datum) : e ∈ Examples.all → (nominalizationOf e).isSome = true → (Predicted e ↔ e.judgment = Judgment.acceptable)

The Ch. 5 distribution ((193), (197), (198), (204), (212), (216), (218)): a nominalization is acceptable exactly when the account predicts it.