German Clause Types

@cite{gutzmann-2015}

German clause-type taxonomy used by Gutzmann (2015) for the analysis of sentence mood operators (DEONT, EPIS, HKNOW). Five clause types distinguished by verb position (V2 vs verb-last) and complementizer presence (dass vs not), with their associated mood-operator inventories and clause-level mood compositions.

This file is the German fragment counterpart of the language-agnostic operators in Theories.Semantics.Mood.Gutzmann. The theory file defines DEONT, EPIS, the E modifier, and HKNOW; this file specifies which of those operators each German clause type composes.

German Clause Type Inventory (@cite{gutzmann-2015}, Ch 5)

Clause type	Mood operators	Example
dass-VL	DEONT only	"Dass du kommst!"
V2-declarative	DEONT(EPIS(p))	"Jim wohnt in Berlin."
VL-interrogative	DEONT(EPIS(p))	"Wann Peter kommt?"
V2-interrogative	DEONT(EPIS(p)) ⊙ HKNOW	"Kommt Peter?"
Imperative	DEONT only	"Tritt zurück!"

def Fragments.German.ClauseTypes.dassVLMood {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : Bool

dass-VL clause mood: DEONT only (@cite{gutzmann-2015}, (5.82)).

No [±wh] visible at LF (dass is semantically empty, so [−wh] is invisible per the visibility condition (5.41)). Therefore no epistemic interpretation is triggered. The root rule introduces DEONT.

"Dass du nicht zu spät kommst!" = The speaker wants [you not arrive late].

Equations

• Fragments.German.ClauseTypes.dassVLMood p c = Semantics.Mood.Gutzmann.deont p c

def Fragments.German.ClauseTypes.v2DeclMood {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : Bool

V2-declarative mood: DEONT(EPIS(p)) (@cite{gutzmann-2015}, (5.93)–(5.96)).

The finite verb moves to C⁰ (V-to-C triggered by [−wh] attached to an overt element at PF). The [−wh] is visible at LF, triggering epistemic interpretation. The root rule adds DEONT, and E modifies it to embed the epistemic predicate.

"Jim wohnt in Berlin." = The speaker wants the hearer to believe [Jim lives in Berlin].

Equations

• Fragments.German.ClauseTypes.v2DeclMood p c = Semantics.Mood.Gutzmann.episModifier Semantics.Mood.Gutzmann.deont p c

def Fragments.German.ClauseTypes.v2InterrogMood {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : Bool

V2-interrogative mood: DEONT(EPIS(p)) ⊙ HKNOW(p) (@cite{gutzmann-2015}, (5.100)).

V2-interrogatives have two [±wh] specifications: [+wh] in CP^spec and [−wh] in C⁰ (Brandt et al. 1992). The first triggers epistemic interpretation, the second (in C⁰) triggers an additional epistemic interpretation resolved to hearer knowledge. HKNOW is a separate functional expletive UCI whose u-content is conjoined (⊙) with the deontic/epistemic mood.

"Kommt Peter?" = The speaker wants to know [whether Peter comes] AND the addressee knows [whether Peter comes].

Equations

• Fragments.German.ClauseTypes.v2InterrogMood p c = (Semantics.Mood.Gutzmann.episModifier Semantics.Mood.Gutzmann.deont p c && Semantics.Mood.Gutzmann.hknow p c)

def Fragments.German.ClauseTypes.vlInterrogMood {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : Bool

VL-interrogative mood: DEONT(EPIS(p)) only — no HKNOW (@cite{gutzmann-2015}, p. 213).

VL-interrogatives (e.g., "Wann Peter nach Hause kommt?") lack the [−wh] in C⁰ that triggers HKNOW. Therefore they are felicitous even when the hearer does not know the answer (the Cuban cigar scenario).

Equations

• Fragments.German.ClauseTypes.vlInterrogMood p c = Semantics.Mood.Gutzmann.episModifier Semantics.Mood.Gutzmann.deont p c

theorem Fragments.German.ClauseTypes.dassVL_is_pure_deontic {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : dassVLMood p c = Semantics.Mood.Gutzmann.deont p c

dass-VL clauses have no epistemic component.

theorem Fragments.German.ClauseTypes.v2_vs_vl_interrog {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : v2InterrogMood p c = (vlInterrogMood p c && Semantics.Mood.Gutzmann.hknow p c)

V2-interrogatives differ from VL-interrogatives only in the HKNOW component (hearer knowledge use condition).

theorem Fragments.German.ClauseTypes.imperative_equals_dassVL {W : Type u_1} (p : W → Bool) (c : Semantics.Mood.Gutzmann.MoodContext W) : dassVLMood p c = Semantics.Mood.Gutzmann.deont p c

Imperatives and dass-VL clauses share the same mood structure: DEONT only, no epistemic. Both lack [±wh] visible at LF.

GermanClauseType as ClauseForm-indexed inductive

GermanClauseType is a Gutzmann-2015-specific refinement of the framework-agnostic Features.ClauseForm: it 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. Each constructor specifies the ClauseForm it refines:

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 Fragments.German.ClauseTypes.GermanClauseType : Features.ClauseForm → Type

German clause types distinguished by verb position and complementizer, indexed by their Features.ClauseForm projection. The verb-position/complementizer information determines mood operator inventory (@cite{gutzmann-2015}, Ch 5).

• dassVL : GermanClauseType Features.ClauseForm.declarative

  dass-VL: complementizer clause, verb-last. No [±wh] visible at LF. Form-level: declarative.

• v2Declarative : GermanClauseType Features.ClauseForm.declarative

  V2-declarative: finite verb in C⁰, [−wh] visible at LF. Form-level: declarative.

• v2Interrogative : GermanClauseType Features.ClauseForm.matrixQuestion

  V2-interrogative: verb-second, [+wh] in SpecCP + [−wh] in C⁰. Form-level: matrix question.

• vlInterrogative : GermanClauseType Features.ClauseForm.embeddedQuestion

  VL-interrogative: verb-last, [+wh] only (no [−wh] in C⁰). Form-level: embedded question.

• imperative : GermanClauseType Features.ClauseForm.declarative

  Imperative: no [±wh] visible at LF. Form-level: declarative (no SAI inversion).

def Fragments.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 Fragments.German.ClauseTypes.instDecidableEqGermanClauseType {a✝ : Features.ClauseForm} : DecidableEq (GermanClauseType a✝)

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

def Fragments.German.ClauseTypes.GermanClauseType.moodStructure {f : Features.ClauseForm} : GermanClauseType f → Semantics.Mood.Gutzmann.MoodStructure

The mood structure of each German clause type, derived from the theory of [±wh] visibility and the root rule.

Equations

• Fragments.German.ClauseTypes.GermanClauseType.dassVL.moodStructure = { hasDeontic := true, hasEpistemic := false, hasHearerKnowledge := false }
• Fragments.German.ClauseTypes.GermanClauseType.v2Declarative.moodStructure = { hasDeontic := true, hasEpistemic := true, hasHearerKnowledge := false }
• Fragments.German.ClauseTypes.GermanClauseType.v2Interrogative.moodStructure = { hasDeontic := true, hasEpistemic := true, hasHearerKnowledge := true }
• Fragments.German.ClauseTypes.GermanClauseType.vlInterrogative.moodStructure = { hasDeontic := true, hasEpistemic := true, hasHearerKnowledge := false }
• Fragments.German.ClauseTypes.GermanClauseType.imperative.moodStructure = { hasDeontic := true, hasEpistemic := false, hasHearerKnowledge := false }

theorem Fragments.German.ClauseTypes.every_clause_has_deont {f : Features.ClauseForm} (ct : GermanClauseType f) : ct.moodStructure.hasDeontic = true

Every matrix clause has a deontic operator (the root rule).

theorem Fragments.German.ClauseTypes.imperative_lacks_epis : GermanClauseType.imperative.moodStructure.hasEpistemic = false

Imperatives lack EPIS — the structural basis for selectional restrictions on UC-modifiers like wohl.

theorem Fragments.German.ClauseTypes.dassVL_matches_imperative : GermanClauseType.dassVL.moodStructure = GermanClauseType.imperative.moodStructure

dass-VL and imperatives share mood structure: deontic only.

theorem Fragments.German.ClauseTypes.v2_vl_differ_only_in_hknow : GermanClauseType.v2Interrogative.moodStructure.hasDeontic = GermanClauseType.vlInterrogative.moodStructure.hasDeontic ∧ GermanClauseType.v2Interrogative.moodStructure.hasEpistemic = GermanClauseType.vlInterrogative.moodStructure.hasEpistemic ∧ GermanClauseType.v2Interrogative.moodStructure.hasHearerKnowledge = true ∧ GermanClauseType.vlInterrogative.moodStructure.hasHearerKnowledge = false

V2-interrogatives differ from VL-interrogatives only in HKNOW.

Structural consequences of the indexing

These theorems exploit the indexed structure: instead of projecting via a forgetful function and filtering, the type-level index does the work.

theorem Fragments.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 Fragments.German.ClauseTypes.embedded_question_is_vl_interrog (ct : GermanClauseType Features.ClauseForm.embeddedQuestion) : ct = GermanClauseType.vlInterrogative

An embedded-question German clause type is exactly vlInterrogative.

theorem Fragments.German.ClauseTypes.hknow_iff_matrix_question {f : Features.ClauseForm} (ct : GermanClauseType f) : ct.moodStructure.hasHearerKnowledge = true ↔ f = Features.ClauseForm.matrixQuestion

HKNOW iff matrix question — restated structurally as a fact about the index. The HKNOW use condition tracks form-level matrix interrogativity (@cite{gutzmann-2015}, p. 213, Cuban cigar argument).

theorem Fragments.German.ClauseTypes.matrix_question_has_hknow (ct : GermanClauseType Features.ClauseForm.matrixQuestion) : ct.moodStructure.hasHearerKnowledge = true

Matrix-question German clauses always carry HKNOW.

theorem Fragments.German.ClauseTypes.declarative_fiber_underdetermines_mood : GermanClauseType.dassVL.moodStructure ≠ GermanClauseType.v2Declarative.moodStructure

The .declarative fiber is many-to-one — three German clause types inhabit it (dassVL, v2Declarative, imperative), and they are distinguishable only at the moodStructure level. The contrast below type-checks because both terms have type GermanClauseType .declarative.