Dutch verbs

This file defines the Dutch verb as a lexical entry: the root Verb with the simplex verb it is formed on and its formation, simplex, with a separable particle or with an inseparable prefix, from which its infinitive and past participle follow. Broekhuis and Corver's grammar forms the past participle with the circumfix ge-…-d, ge-…-t or ge-…-en: gestraft 'punished'. A verb with an unstressed prefix, be-, ver-, ont- or her-, never realizes the ge- part, ontdekt 'discovered', while a particle precedes it, opgebeld 'called up' and not geopbeld, which shows that the particle does not form a morphological unit with the verb; under verb second the particle is stranded, Jan belde Marie gisteren op 'Jan called Marie yesterday'.

The perfect auxiliary follows from the verb on a frame (Dutch.Verbs.perfectAuxiliary). Transitive and intransitive verbs take hebben, and unaccusative verbs take zijn when they are telic and hebben when they are atelic; a directional phrase makes a verb of motion unaccusative and, if it bounds the path, telic, so De jongen heeft gewandeld 'the boy walked' but De jongen is naar Groningen gewandeld 'the boy walked to Groningen'. Blijven 'stay', whose state continues, takes zijn. Each entry records the auxiliaries its perfect takes, and the rule is tested against them.

Main definitions

• Dutch.Verbs.Verb: the entry.
• Dutch.Verbs.Verb.pastParticiple: the past participle, from the formation.
• Dutch.Verbs.Verb.withPath: the entry with a path phrase.
• Dutch.Verbs.perfectAuxiliary: the auxiliary of the perfect of a verb on a frame.
• Dutch.Verbs.inventory: the entries.

Main results

• Dutch.Verbs.pastParticiple_particle, Dutch.Verbs.pastParticiple_prefix: a particle precedes the ge- of the participle and a prefix replaces it.
• Dutch.Verbs.opgebeld, Dutch.Verbs.ontdekt: the grammar's examples.
• Dutch.Verbs.perfect_withPath_intransitive: a bounded directional phrase gives a dynamic intransitive verb zijn.
• Dutch.Verbs.perfectAuxiliary_mem: the rule gives every entry an auxiliary its perfect takes.

Implementation notes

• The participle of the simplex verb is stored without its ge-, as German.Conjugation.Stem stores it, and the entry does not conjugate further. The syntax of the particle, which the grammar and den Dikken analyse, is left to the studies.

References

• H. Broekhuis and N. Corver, Syntax of Dutch, Volume I: Verbs and Verb Phrases 1: Characterization, Classification and Lexical Projection (2026)
• [LRH95]
• [Sor00]

inductive Dutch.Verbs.Formation : Type

A verb is formed on a simplex verb either not at all, with a separable particle, which precedes the ge- of the past participle, or with an unstressed inseparable prefix, whose past participle has no ge-.

• simplex : Formation
• particle (form : String) : Formation
• prefix (form : String) : Formation

def Dutch.Verbs.instDecidableEqFormation.decEq (x✝ x✝¹ : Formation) : Decidable (x✝ = x✝¹)

Equations

• Dutch.Verbs.instDecidableEqFormation.decEq Dutch.Verbs.Formation.simplex Dutch.Verbs.Formation.simplex = isTrue ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq Dutch.Verbs.Formation.simplex (Dutch.Verbs.Formation.particle form) = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq Dutch.Verbs.Formation.simplex (Dutch.Verbs.Formation.prefix form) = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.particle form) Dutch.Verbs.Formation.simplex = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.particle a) (Dutch.Verbs.Formation.particle b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.particle form) (Dutch.Verbs.Formation.prefix form_1) = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.prefix form) Dutch.Verbs.Formation.simplex = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.prefix form) (Dutch.Verbs.Formation.particle form_1) = isFalse ⋯
• Dutch.Verbs.instDecidableEqFormation.decEq (Dutch.Verbs.Formation.prefix a) (Dutch.Verbs.Formation.prefix b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dutch.Verbs.instDecidableEqFormation : DecidableEq Formation

Equations

• Dutch.Verbs.instDecidableEqFormation = Dutch.Verbs.instDecidableEqFormation.decEq

@[instance_reducible]

instance Dutch.Verbs.instReprFormation : Repr Formation

Equations

• Dutch.Verbs.instReprFormation = { reprPrec := Dutch.Verbs.instReprFormation.repr }

def Dutch.Verbs.instReprFormation.repr : Formation → ℕ → Std.Format

Equations

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

def Dutch.Verbs.Formation.form : Formation → String

The particle or prefix of a formation, empty for a simplex verb.

Equations

• Dutch.Verbs.Formation.simplex.form = ""
• (Dutch.Verbs.Formation.particle p).form = p
• (Dutch.Verbs.Formation.prefix p).form = p

structure Dutch.Verbs.Verbextends Verb : Type

A Dutch verb is the root entry with the simplex verb it is formed on and its formation.

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

  The infinitive of the simplex verb.

• participle : String

  The past participle of the simplex verb without its ge-.

• formation : Formation

  The formation.

def Dutch.Verbs.instBEqVerb.beq : Verb → Verb → Bool

Equations

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

@[instance_reducible]

instance Dutch.Verbs.instBEqVerb : BEq Verb

Equations

• Dutch.Verbs.instBEqVerb = { beq := Dutch.Verbs.instBEqVerb.beq }

def Dutch.Verbs.Verb.infinitive (v : Verb) : String

The infinitive puts the particle or prefix before the simplex verb.

Equations

• v.infinitive = v.formation.form ++ v.base

def Dutch.Verbs.Verb.pastParticiple (v : Verb) : String

The past participle has ge- on the simplex verb, after a particle, and replaced by a prefix.

Equations

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

def Dutch.Verbs.Verb.IsSeparable (v : Verb) : Prop

A verb is separable when it is formed with a particle.

Equations

• v.IsSeparable = ∃ (p : String), v.formation = Dutch.Verbs.Formation.particle p

@[instance_reducible]

instance Dutch.Verbs.Verb.instDecidableIsSeparable (v : Verb) : Decidable v.IsSeparable

Equations

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

def Dutch.Verbs.simplex (inf pp : String) : Verb

simplex inf pp is the simplex transitive verb with the infinitive inf and the past participle pp, given with its ge-.

Equations

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

def Dutch.Verbs.particleVerb (p : String) (v : Verb) : Verb

particleVerb p v is the verb formed on v with the separable particle p.

Equations

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

def Dutch.Verbs.prefixVerb (p : String) (v : Verb) : Verb

prefixVerb p v is the verb formed on v with the inseparable prefix p.

Equations

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

theorem Dutch.Verbs.pastParticiple_particle (p : String) (v : Verb) : (particleVerb p v).pastParticiple = p ++ "ge" ++ v.participle

A particle precedes the ge- of the past participle.

theorem Dutch.Verbs.pastParticiple_prefix (p : String) (v : Verb) : (prefixVerb p v).pastParticiple = p ++ v.participle

A prefix replaces the ge- of the past participle.

theorem Dutch.Verbs.isSeparable_particleVerb_not_prefixVerb (p : String) (v : Verb) : (particleVerb p v).IsSeparable ∧ ¬(prefixVerb p v).IsSeparable

A verb formed with a particle is separable and one formed with a prefix is not.

Simplex verbs

def Dutch.Verbs.straffen : Verb

straffen 'punish', gestraft.

Equations

• Dutch.Verbs.straffen = Dutch.Verbs.simplex "straffen" "gestraft"

def Dutch.Verbs.kussen : Verb

kussen 'kiss', gekust.

Equations

• Dutch.Verbs.kussen = Dutch.Verbs.simplex "kussen" "gekust"

def Dutch.Verbs.bellen : Verb

bellen 'call', gebeld.

Equations

• Dutch.Verbs.bellen = Dutch.Verbs.simplex "bellen" "gebeld"

def Dutch.Verbs.voeren : Verb

voeren 'carry', gevoerd.

Equations

• Dutch.Verbs.voeren = Dutch.Verbs.simplex "voeren" "gevoerd"

def Dutch.Verbs.halen : Verb

halen 'fetch', gehaald.

Equations

• Dutch.Verbs.halen = Dutch.Verbs.simplex "halen" "gehaald"

def Dutch.Verbs.lezen : Verb

lezen 'read', gelezen.

Equations

• Dutch.Verbs.lezen = Dutch.Verbs.simplex "lezen" "gelezen"

def Dutch.Verbs.dekken : Verb

dekken 'cover', gedekt.

Equations

• Dutch.Verbs.dekken = Dutch.Verbs.simplex "dekken" "gedekt"

def Dutch.Verbs.dienen : Verb

dienen 'serve', gediend.

Equations

• Dutch.Verbs.dienen = Dutch.Verbs.simplex "dienen" "gediend"

Particle verbs

def Dutch.Verbs.opbellen : Verb

opbellen 'call up', formed on bellen with op, opgebeld.

Equations

• Dutch.Verbs.opbellen = Dutch.Verbs.particleVerb "op" Dutch.Verbs.bellen

def Dutch.Verbs.uitvoeren : Verb

uitvoeren 'carry out', formed on voeren with uit, uitgevoerd.

Equations

• Dutch.Verbs.uitvoeren = Dutch.Verbs.particleVerb "uit" Dutch.Verbs.voeren

def Dutch.Verbs.afhalen : Verb

afhalen 'pick up', formed on halen with af, afgehaald.

Equations

• Dutch.Verbs.afhalen = Dutch.Verbs.particleVerb "af" Dutch.Verbs.halen

Prefixed verbs

def Dutch.Verbs.ontdekken : Verb

ontdekken 'discover', formed on dekken with ont-, ontdekt.

Equations

• Dutch.Verbs.ontdekken = Dutch.Verbs.prefixVerb "ont" Dutch.Verbs.dekken

def Dutch.Verbs.bedekken : Verb

bedekken 'cover', formed on dekken with be-, bedekt.

Equations

• Dutch.Verbs.bedekken = Dutch.Verbs.prefixVerb "be" Dutch.Verbs.dekken

def Dutch.Verbs.verdienen : Verb

verdienen 'deserve, earn', formed on dienen with ver-, verdiend.

Equations

• Dutch.Verbs.verdienen = Dutch.Verbs.prefixVerb "ver" Dutch.Verbs.dienen

def Dutch.Verbs.herhalen : Verb

herhalen 'repeat', formed on halen with her-, herhaald.

Equations

• Dutch.Verbs.herhalen = Dutch.Verbs.prefixVerb "her" Dutch.Verbs.halen

Monadic verbs

The monadic verbs of [Sor00]'s Dutch examples and of the grammar's discussion of motion verbs, each with the auxiliaries of its perfect and, for an unaccusative verb, the voice the grammar's unaccusativity tests assign it (§2.1), which introduces no external argument.

def Dutch.Verbs.komen : Verb

komen 'come', kom - kwam - gekomen, an unaccusative verb of motion to a goal.

Equations

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

def Dutch.Verbs.sterven : Verb

sterven 'die' is an unaccusative verb denoting a transition, as in De oude man is gestorven.

Equations

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

def Dutch.Verbs.groeien : Verb

groeien 'grow', an unaccusative verb of change along a scale of size.

Equations

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

def Dutch.Verbs.stijgen : Verb

stijgen 'rise', an unaccusative verb of change along a scale of height.

Equations

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

def Dutch.Verbs.blijven : Verb

blijven 'stay' is an unaccusative verb expressing that a state continues to exist (§1.2), with the auxiliary zijn, as in Was dan ook wat langer gebleven! 'You should have stayed a bit longer!'.

Equations

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

def Dutch.Verbs.overblijven : Verb

overblijven 'remain, be left', formed on blijven with the particle over.

Equations

• Dutch.Verbs.overblijven = Dutch.Verbs.particleVerb "over" Dutch.Verbs.blijven

def Dutch.Verbs.duren : Verb

duren 'last', stative.

Equations

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

def Dutch.Verbs.staan : Verb

staan 'stand' is a stative verb of location, an atelic unaccusative verb with hebben, as in Jan heeft lang op het perron gestaan.

Equations

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

def Dutch.Verbs.bestaan : Verb

bestaan 'exist', formed on staan with the prefix be-.

Equations

• Dutch.Verbs.bestaan = Dutch.Verbs.prefixVerb "be" Dutch.Verbs.staan

def Dutch.Verbs.blazen : Verb

blazen 'blow', an intransitive activity with an agentive subject.

Equations

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

def Dutch.Verbs.werken : Verb

werken 'work', gewerkt, an intransitive activity with an agentive subject.

Equations

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

def Dutch.Verbs.lopen : Verb

lopen 'walk, run', loop - liep - gelopen, an agentive verb of manner of motion, intransitive ([LRH95] p. 148).

Equations

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

def Dutch.Verbs.wandelen : Verb

wandelen 'walk' is an intransitive verb of manner of motion, as in De jongen heeft gewandeld.

Equations

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

def Dutch.Verbs.rollen : Verb

rollen 'roll', a nonagentive verb of manner of motion, unaccusative ([LRH95] pp. 147–148) and atelic.

Equations

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

The perfect auxiliary

def Dutch.Verbs.Verb.withPath (v : Verb) (p : Adposition.SpatialReading) : Verb

The predicate the entry v forms with a path phrase of reading p.

Equations

• v.withPath p = { toVerb := v.withPath p, base := v.base, participle := v.participle, formation := v.formation }

@[simp]

theorem Dutch.Verbs.Verb.toVerb_withPath (v : Verb) (p : Adposition.SpatialReading) : (v.withPath p).toVerb = v.withPath p

def Dutch.Verbs.perfectAuxiliary (v : Verb) (fr : ArgumentFrame) : Verb.PerfectAuxiliary

The auxiliary of the perfect of v on the frame fr ([BC26b] §§2.1–2.2) is zijn on an intransitive frame when the verb is unaccusative and telic, or when a directional phrase gives the verb of motion a path and makes it telic, since the phrase makes it unaccusative; hebben otherwise, for transitive and intransitive verbs and for atelic unaccusative ones; and zijn for blijven, whose state continues.

Equations

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

theorem Dutch.Verbs.perfect_withPath_intransitive {v : Verb} {p : Adposition.SpatialReading} (hv : v.TakesSpatial) (hd : p.direction ≠ Spatial.Path.Direction.place) (hb : p.IsBounded) {c : Aspect.VendlerClass} (hc : v.vendlerClass = some c) (hdyn : c.dynamicity = Aspect.Dynamicity.dynamic) : perfectAuxiliary (v.withPath p) ArgumentFrame.intransitive = Verb.PerfectAuxiliary.be

A bounded directional phrase gives a dynamic intransitive verb zijn, as in De jongen is naar Groningen gewandeld (§2.2, (274b)).

The inventory

def Dutch.Verbs.inventory : List Verb

inventory lists the entries.

Equations

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

theorem Dutch.Verbs.perfectAuxiliary_mem (v : Verb) : v ∈ inventory → v.perfectAuxiliaries.Nonempty → perfectAuxiliary v (v.valency.frames.headD ArgumentFrame.intransitive) ∈ v.perfectAuxiliaries

The rule gives every entry on its basic frame an auxiliary its perfect takes.

theorem Dutch.Verbs.form_eq_infinitive (v : Verb) : v ∈ inventory → v.form = v.infinitive

Every entry is cited by its infinitive.

theorem Dutch.Verbs.takesSpatial_of_direction_eq_place (v : Verb) : v ∈ inventory → v.direction = some Spatial.Path.Direction.place → v.TakesSpatial

Every verb of manner of motion selects a directional phrase, so that all of them take zijn under one that bounds the path.

theorem Dutch.Verbs.opgebeld : opbellen.pastParticiple = "opgebeld" ∧ uitvoeren.pastParticiple = "uitgevoerd"

opgebeld and uitgevoerd, with the particle before ge-.

theorem Dutch.Verbs.ontdekt : ontdekken.pastParticiple = "ontdekt" ∧ verdienen.pastParticiple = "verdiend"

ontdekt and verdiend, without ge-.

theorem Dutch.Verbs.ge_after_formation_iff (v : Verb) : v ∈ inventory → (['g', 'e'] <+: List.drop v.formation.form.length v.pastParticiple.toList ↔ v.IsSeparable ∨ v.formation = Formation.simplex)

An entry's participle has ge- after its particle or prefix exactly when the entry is separable or simplex.