German Clause Types

German clause-type taxonomy: five clause types distinguished by verb position (V2 vs verb-last) and complementizer presence (dass vs not), encoded as an indexed refinement of the framework-agnostic Features.ClauseForm. Descriptive German syntax; the sentence-mood analysis built on this taxonomy ([Gut15], Ch 5: which mood operators each clause type composes) lives in Studies/Gutzmann2015.lean.

Clause type	Example
dass-VL	"Dass du kommst!"
V2-declarative	"Jim wohnt in Berlin."
VL-interrogative	"Wann Peter kommt?"
V2-interrogative	"Kommt Peter?"
Imperative	"Tritt zurück!"

GermanClauseType as ClauseForm-indexed inductive

GermanClauseType distinguishes clauses by both verb position (V2 vs VL) and complementizer presence (dass vs not), where ClauseForm only records the matrix-vs-embedded question / declarative word-order distinction. We encode the refinement structurally as an indexed inductive GermanClauseType : ClauseForm → Type:

GermanClauseType	ClauseForm
dassVL	declarative
v2Declarative	declarative
v2Interrogative	matrixQuestion
vlInterrogative	embeddedQuestion
imperative	declarative

Two consequences fall out of the indexing rather than requiring separate proof:

1. No bridge function. The "projection to ClauseForm" is the type-level index — (ct : GermanClauseType f) witnesses both the refined value and its ClauseForm projection f simultaneously.
2. (ct : GermanClauseType .matrixQuestion) is exactly the v2Interrogative case. cases ct on this type produces a single branch, capturing the structural fact that "matrix-question German clause" picks out v2Interrogative without auxiliary filtering.

inductive German.ClauseTypes.GermanClauseType : Features.ClauseForm → Type

German clause types distinguished by verb position and complementizer, indexed by their Features.ClauseForm projection.

• dassVL : GermanClauseType Features.ClauseForm.declarative

  dass-VL: complementizer clause, verb-last. Form-level: declarative.

• v2Declarative : GermanClauseType Features.ClauseForm.declarative

  V2-declarative: finite verb in C⁰. Form-level: declarative.

• v2Interrogative : GermanClauseType Features.ClauseForm.matrixQuestion

  V2-interrogative: verb-second. Form-level: matrix question.

• vlInterrogative : GermanClauseType Features.ClauseForm.embeddedQuestion

  VL-interrogative: verb-last. Form-level: embedded question.

• imperative : GermanClauseType Features.ClauseForm.declarative

  Imperative. Form-level: declarative (no SAI inversion).

def German.ClauseTypes.instDecidableEqGermanClauseType.decEq {a✝ : Features.ClauseForm} (x✝ x✝¹ : GermanClauseType a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance German.ClauseTypes.instDecidableEqGermanClauseType {a✝ : Features.ClauseForm} : DecidableEq (GermanClauseType a✝)

Equations

• German.ClauseTypes.instDecidableEqGermanClauseType = German.ClauseTypes.instDecidableEqGermanClauseType.decEq

@[implicit_reducible]

instance German.ClauseTypes.instReprGermanClauseType {a✝ : Features.ClauseForm} : Repr (GermanClauseType a✝)

Equations

• German.ClauseTypes.instReprGermanClauseType = { reprPrec := German.ClauseTypes.instReprGermanClauseType.repr }

def German.ClauseTypes.instReprGermanClauseType.repr {a✝ : Features.ClauseForm} : GermanClauseType a✝ → Nat → Std.Format

Equations

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

Structural consequences of the indexing

theorem German.ClauseTypes.matrix_question_is_v2_interrog (ct : GermanClauseType Features.ClauseForm.matrixQuestion) : ct = GermanClauseType.v2Interrogative

A matrix-question German clause type is exactly v2Interrogative. Pattern matching on GermanClauseType .matrixQuestion produces a single constructor by the indexing.

theorem German.ClauseTypes.embedded_question_is_vl_interrog (ct : GermanClauseType Features.ClauseForm.embeddedQuestion) : ct = GermanClauseType.vlInterrogative

An embedded-question German clause type is exactly vlInterrogative.