Gutzmann (2015): Sentence Mood as Use-Conditional Meaning

[Gut15]

Use-Conditional Meaning: Studies in Multidimensional Semantics (OUP). Self-contained study: the L_TU logic (the book's central formal contribution, a three-dimensional extension of [Pot05]'s L_CI), the sentence-mood operators DEONT/EPIS/HKNOW as use-conditional items, their composition in the German clause-type inventory, and the modal particle predictions. (L_TU and the mood operators live here rather than in the theory layer because this book is their only consumer; they graduate per the ≥ 2-studies rule if a second study consumes them.)

Key claims

1. Sentence mood operators (deontic, epistemic) are UCIs, not presuppositions
2. The epistemic interpretation of [±wh] does NOT pass standard presupposition tests (negation, disjunction)
3. V2-interrogatives carry a HKNOW condition absent from VL-interrogatives (the Cuban cigar argument)
4. Modal particles are functional expletive UCIs whose mood restrictions derive from interaction with sentence mood operators
5. wohl is a UC-modifier (not a UCI), with selectional restriction

Clause type predictions

Clause type	t-content	u-content
dass-VL	p	DEONT(p)
V2-declarative	p	DEONT(EPIS(p))
VL-interrogative	p	DEONT(EPIS(p))
V2-interrogative	p	DEONT(EPIS(p)) ⊙ HKNOW(p)
Imperative	p	DEONT(p)

The L_TU architecture

Every expression carries three meaning dimensions — t-dim (truth-conditional, world-indexed), s-dim (active use-conditional content being composed), u-dim (completed use-conditional propositions, context-indexed). Multidimensional application (MA) composes dimensions pointwise; use-conditional elimination (UE) stores a completed s-dim in the u-dim and resets. The non-interaction theorem (non_interaction) guarantees use-conditional meaning never leaks into truth conditions.

The L_TU logic

L_TU Type System

inductive Gutzmann2015.UCType : Type

The L_TU type system ([Gut15], (4.45)).

Basic types: e (entities), t (truth values), u (use-conditional propositions, opaque). A type is use-conditional iff it equals u or is a function type whose codomain is use-conditional.

• e : UCType
• t : UCType
• u : UCType
• func : UCType → UCType → UCType

@[instance_reducible]

instance Gutzmann2015.instDecidableEqUCType : DecidableEq UCType

Equations

• Gutzmann2015.instDecidableEqUCType = Gutzmann2015.instDecidableEqUCType.decEq

def Gutzmann2015.instDecidableEqUCType.decEq (x✝ x✝¹ : UCType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.e Gutzmann2015.UCType.e = isTrue ⋯
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.e Gutzmann2015.UCType.t = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_1
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.e Gutzmann2015.UCType.u = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_2
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.e (a.func a_1) = isFalse ⋯
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.t Gutzmann2015.UCType.e = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_4
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.t Gutzmann2015.UCType.t = isTrue ⋯
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.t Gutzmann2015.UCType.u = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_5
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.t (a.func a_1) = isFalse ⋯
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.u Gutzmann2015.UCType.e = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_7
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.u Gutzmann2015.UCType.t = isFalse Gutzmann2015.instDecidableEqUCType.decEq._proof_8
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.u Gutzmann2015.UCType.u = isTrue ⋯
• Gutzmann2015.instDecidableEqUCType.decEq Gutzmann2015.UCType.u (a.func a_1) = isFalse ⋯
• Gutzmann2015.instDecidableEqUCType.decEq (a.func a_1) Gutzmann2015.UCType.e = isFalse ⋯
• Gutzmann2015.instDecidableEqUCType.decEq (a.func a_1) Gutzmann2015.UCType.t = isFalse ⋯
• Gutzmann2015.instDecidableEqUCType.decEq (a.func a_1) Gutzmann2015.UCType.u = isFalse ⋯

def Gutzmann2015.instReprUCType.repr : UCType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Gutzmann2015.instReprUCType.repr Gutzmann2015.UCType.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gutzmann2015.UCType.e")).group prec✝
• Gutzmann2015.instReprUCType.repr Gutzmann2015.UCType.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gutzmann2015.UCType.t")).group prec✝
• Gutzmann2015.instReprUCType.repr Gutzmann2015.UCType.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gutzmann2015.UCType.u")).group prec✝

@[instance_reducible]

instance Gutzmann2015.instReprUCType : Repr UCType

Equations

• Gutzmann2015.instReprUCType = { reprPrec := Gutzmann2015.instReprUCType.repr }

def Gutzmann2015.UCType.IsUCType : UCType → Prop

A type is use-conditional iff it is u or a function into a use-conditional type. This determines which dimension an expression's content targets during composition.

Equations

• Gutzmann2015.UCType.u.IsUCType = True
• (a.func τ).IsUCType = τ.IsUCType
• x✝.IsUCType = False

@[instance_reducible]

instance Gutzmann2015.UCType.decIsUCType : DecidablePred IsUCType

Equations

• Gutzmann2015.UCType.e.decIsUCType = isFalse ⋯
• Gutzmann2015.UCType.t.decIsUCType = isFalse ⋯
• Gutzmann2015.UCType.u.decIsUCType = isTrue trivial
• (a.func a_1).decIsUCType = a_1.decIsUCType

theorem Gutzmann2015.u_is_uc : UCType.u.IsUCType

theorem Gutzmann2015.t_is_not_uc : ¬UCType.t.IsUCType

theorem Gutzmann2015.func_into_u_is_uc : (UCType.e.func UCType.u).IsUCType

UCI Typology

structure Gutzmann2015.UCIClass : Type

UCI classification by three binary features ([Gut15], Ch 2).

• functional: takes a truth-conditional argument (vs isolated)
• twoDimensional: contributes to both t-dim and s-dim (vs expletive)
• resourceSensitive: argument is consumed/shunted (vs passed through)

• functional : Bool
• twoDimensional : Bool
• resourceSensitive : Bool

def Gutzmann2015.instDecidableEqUCIClass.decEq (x✝ x✝¹ : UCIClass) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Gutzmann2015.instDecidableEqUCIClass : DecidableEq UCIClass

Equations

• Gutzmann2015.instDecidableEqUCIClass = Gutzmann2015.instDecidableEqUCIClass.decEq

@[instance_reducible]

instance Gutzmann2015.instReprUCIClass : Repr UCIClass

Equations

• Gutzmann2015.instReprUCIClass = { reprPrec := Gutzmann2015.instReprUCIClass.repr }

def Gutzmann2015.instReprUCIClass.repr : UCIClass → ℕ → Std.Format

Equations

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

def Gutzmann2015.isolatedExpletive : UCIClass

Isolated expletive: no argument, only use-conditional content. Example: damn in "the damn dog."

Equations

• Gutzmann2015.isolatedExpletive = { functional := false, twoDimensional := false, resourceSensitive := false }

def Gutzmann2015.isolatedMixed : UCIClass

Isolated mixed: no argument, contributes to both dimensions. Example: ethnic slurs with descriptive + expressive content.

Equations

• Gutzmann2015.isolatedMixed = { functional := false, twoDimensional := true, resourceSensitive := false }

def Gutzmann2015.functionalExpletive : UCIClass

Functional expletive: takes an argument, only use-conditional output. Example: German modal particles ja, denn; sentence mood operators.

Equations

• Gutzmann2015.functionalExpletive = { functional := true, twoDimensional := false, resourceSensitive := false }

def Gutzmann2015.functionalShunting : UCIClass

Functional shunting: takes an argument that is consumed (not returned). Example: [Pot05]'s comma feature for appositives.

Equations

• Gutzmann2015.functionalShunting = { functional := true, twoDimensional := false, resourceSensitive := true }

def Gutzmann2015.functionalMixed : UCIClass

Functional mixed: takes an argument, contributes to both dimensions. Example: some honorific systems.

Equations

• Gutzmann2015.functionalMixed = { functional := true, twoDimensional := true, resourceSensitive := false }

Use-Conditional Expressions

inductive Gutzmann2015.UCExprKind : Type

How a use-conditional expression interacts with composition ([Gut15], §6.5).

A UCI is a use-conditional item: it contributes u-content by taking truth-conditional arguments. A UC-modifier takes another UCI as its argument and modifies its use-conditional behavior.

This distinction drives two different mechanisms for mood restriction:

• UCIs are restricted by use-conditional conflict (their independent u-content is incompatible with certain mood operators)
• UC-modifiers are restricted selectionally (the mood operator they modify is absent from certain clause types)

• uci : UCExprKind

  Use-conditional item: maps truth-conditional content to u-content. Type: ⟨⟨s,t⟩, u⟩ (functional) or u (isolated).

• ucModifier : UCExprKind

  Use-conditional modifier: maps UCIs to UCIs. Type: ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩. Modifies an existing mood operator (e.g., German wohl modifies EPIS).

@[instance_reducible]

instance Gutzmann2015.instDecidableEqUCExprKind : DecidableEq UCExprKind

Equations

• Gutzmann2015.instDecidableEqUCExprKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gutzmann2015.instReprUCExprKind.repr : UCExprKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gutzmann2015.instReprUCExprKind : Repr UCExprKind

Equations

• Gutzmann2015.instReprUCExprKind = { reprPrec := Gutzmann2015.instReprUCExprKind.repr }

inductive Gutzmann2015.RestrictionKind : Type

How an expression's mood restriction arises ([Gut15], §6.5).

The two mechanisms are empirically distinguishable: selectional restrictions produce type-mismatch infelicity, while use-conditional conflict produces pragmatic deviance.

• selectional : RestrictionKind

  The expression modifies a mood operator that is absent from certain clause types — a type mismatch. Example: German wohl modifies EPIS, which is absent from imperatives.

• ucConflict : RestrictionKind

  The expression's independent u-content is incompatible with certain sentence moods. Example: German ja's common-ground reminder conflicts with the epistemic uncertainty of interrogatives.

@[instance_reducible]

instance Gutzmann2015.instDecidableEqRestrictionKind : DecidableEq RestrictionKind

Equations

• Gutzmann2015.instDecidableEqRestrictionKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gutzmann2015.instReprRestrictionKind : Repr RestrictionKind

Equations

• Gutzmann2015.instReprRestrictionKind = { reprPrec := Gutzmann2015.instReprRestrictionKind.repr }

def Gutzmann2015.instReprRestrictionKind.repr : RestrictionKind → ℕ → Std.Format

Equations

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

Three-Dimensional Meanings

structure Gutzmann2015.ThreeDimMeaning (C : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A three-dimensional meaning in L_TU ([Gut15], (4.46)).

C is the context type (for use-conditional propositions, sets of contexts), W is the world type (for truth-conditional propositions, sets of worlds).

The crucial type distinction: uDim is C → Bool while tDim/sDim are W → Bool. Use-conditional propositions constrain the context of utterance, not the described world — matching Kaplan's character/content distinction.

• tDim : W → Prop

  Truth-conditional content: the at-issue proposition

• sDim : W → Prop

  Active use-conditional content being composed

• uDim : C → Prop

  Completed use-conditional propositions (stored, inaccessible to further truth-conditional composition)

def Gutzmann2015.multidimApp {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) : ThreeDimMeaning C W

Multidimensional application ([Gut15], (4.46)).

The full MA rule applies functions intradimensionally: dimension 1 applies σ(β₁), dimension 2 applies ρ(β₂), and u-dimensions merge via ⊙ (conjunction). At the propositional level — where both inputs are already of type ⟨s,t⟩ — function application reduces to pointwise conjunction, which is what this definition implements. The sub-propositional case (where dims 1-2 are genuine function applications) is not formalized.

Equations

• Gutzmann2015.multidimApp f a = { tDim := fun (w : W) => f.tDim w ∧ a.tDim w, sDim := fun (w : W) => f.sDim w ∧ a.sDim w, uDim := fun (c : C) => f.uDim c ∧ a.uDim c }

def Gutzmann2015.ucElim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : ThreeDimMeaning C W

Use-conditional elimination ([Gut15], (4.54)).

When the s-dimension reaches type u (its content is a completed use-conditional proposition), UE:

1. Shifts s-dim content to u-dim (conjoining with existing u-content)
2. Resets s-dim to a copy of t-dim

The eval parameter bridges the world-indexed s-dim to the context-indexed u-dim, typically by projecting the world from the context.

Equations

• Gutzmann2015.ucElim m eval = { tDim := m.tDim, sDim := m.tDim, uDim := fun (c : C) => m.uDim c ∧ eval m.sDim c }

def Gutzmann2015.ofTruthConditional {C : Type u_1} {W : Type u_2} (p : W → Prop) : ThreeDimMeaning C W

Lift a truth-conditional proposition to a three-dimensional meaning.

Both t-dim and s-dim carry the propositional content. u-dim is trivially satisfied (no use-conditional content yet). Corresponds to a pure truth-conditional lexical item before LER extension.

Equations

• Gutzmann2015.ofTruthConditional p = { tDim := p, sDim := p, uDim := fun (x : C) => True }

def Gutzmann2015.ofUCI {C : Type u_1} {W : Type u_2} (ucContent : W → Prop) : ThreeDimMeaning C W

Lift a use-conditional function to a three-dimensional meaning.

t-dim is trivially true (UCIs do not contribute truth conditions). s-dim carries the active UCI content. u-dim is trivially true until ucElim fires.

Equations

• Gutzmann2015.ofUCI ucContent = { tDim := fun (x : W) => True, sDim := ucContent, uDim := fun (x : C) => True }

Bridge to TwoDimProp

def Gutzmann2015.toTwoDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (evalU : (C → Prop) → W → Prop) : Pragmatics.Expressives.TwoDimProp W

Project a three-dimensional meaning to a TwoDimProp (final interpretation).

After all composition and UE steps, the final meaning of a sentence has t-dim = truth-conditional content and u-dim = accumulated use-conditional propositions. The s-dim equals t-dim (reset by UE) and is discarded.

The evalU function projects the context-indexed u-dim (C → Bool) to a world-indexed CI content (W → Bool) for the TwoDimProp.ci field. This corresponds to [Gut15]'s lowering operator ⇓_c which converts u-propositions to world sets by fixing context parameters except the world.

Equations

• Gutzmann2015.toTwoDim m evalU = { atIssue := m.tDim, ci := evalU m.uDim }

Key Theorems

theorem Gutzmann2015.ucElim_preserves_tDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : (ucElim m eval).tDim = m.tDim

UE does not affect truth conditions.

This is the formal guarantee of non-interaction: storing use-conditional content in the u-dimension never changes what a sentence says about the world.

theorem Gutzmann2015.ucElim_resets_sDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : (ucElim m eval).sDim = m.tDim

After UE, the s-dimension is reset to the t-dimension.

theorem Gutzmann2015.multidimApp_merges_uDim {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) (c : C) : (multidimApp f a).uDim c ↔ f.uDim c ∧ a.uDim c

MA merges u-dimensions via conjunction. Completed use-conditional propositions from both constituents are preserved.

theorem Gutzmann2015.ofTruthConditional_trivial_uDim {C : Type u_1} {W : Type u_2} (p : W → Prop) (c : C) : (ofTruthConditional p).uDim c

A pure truth-conditional expression has trivial use conditions.

theorem Gutzmann2015.ofUCI_trivial_tDim {C : Type u_1} {W : Type u_2} (ucContent : W → Prop) (w : W) : (ofUCI ucContent).tDim w

A UCI has trivial truth conditions.

Non-Interaction (General)

inductive Gutzmann2015.LTUDeriv (C : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A derivation in the propositional fragment of L_TU.

Derivation trees encode the composition history: which expressions were combined via MA, and where UE was applied. This lets us state and prove properties of all possible derivations, not just specific ones.

• leaf {C : Type u_1} {W : Type u_2} : ThreeDimMeaning C W → LTUDeriv C W

  A lexical item (leaf of the derivation tree)

• app {C : Type u_1} {W : Type u_2} : LTUDeriv C W → LTUDeriv C W → LTUDeriv C W

  Multidimensional application of two sub-derivations

• elim {C : Type u_1} {W : Type u_2} : LTUDeriv C W → ((W → Prop) → C → Prop) → LTUDeriv C W

  Use-conditional elimination applied to a sub-derivation

def Gutzmann2015.LTUDeriv.eval {C : Type u_1} {W : Type u_2} : LTUDeriv C W → ThreeDimMeaning C W

Evaluate a derivation to its three-dimensional meaning.

Equations

• (Gutzmann2015.LTUDeriv.leaf m).eval = m
• (d₁.app d₂).eval = Gutzmann2015.multidimApp d₁.eval d₂.eval
• (d.elim f).eval = Gutzmann2015.ucElim d.eval f

def Gutzmann2015.LTUDeriv.stripUC {C : Type u_1} {W : Type u_2} : LTUDeriv C W → LTUDeriv C W

Strip all use-conditional content from a derivation's leaves, replacing s-dim with t-dim and u-dim with trivial content. This produces a "truth-conditional shadow" of the derivation.

Equations

• (Gutzmann2015.LTUDeriv.leaf m).stripUC = Gutzmann2015.LTUDeriv.leaf { tDim := m.tDim, sDim := m.tDim, uDim := fun (x : C) => True }
• (d₁.app d₂).stripUC = d₁.stripUC.app d₂.stripUC
• (d.elim f).stripUC = d.stripUC.elim f

theorem Gutzmann2015.non_interaction {C : Type u_1} {W : Type u_2} (d : LTUDeriv C W) (w : W) : d.eval.tDim w ↔ d.stripUC.eval.tDim w

Non-interaction theorem ([Gut15]).

For ANY derivation built from multidimensional application and use-conditional elimination, the truth-conditional content of the result depends ONLY on the truth-conditional content of the inputs.

Stripping all use-conditional content from the leaves does not change the final t-dimension. Use-conditional meaning can never leak into truth conditions — not through MA, not through UE, not through any combination of the two. This is the fundamental architectural guarantee of L_TU.

theorem Gutzmann2015.non_interaction_ext {C : Type u_1} {W : Type u_2} (d : LTUDeriv C W) : d.eval.tDim = d.stripUC.eval.tDim

Non-interaction at the function level (extensional form).

UCI Non-Contribution

theorem Gutzmann2015.multidimApp_uci_tDim {C : Type u_1} {W : Type u_2} (tc uci : ThreeDimMeaning C W) (h : ∀ (w : W), uci.tDim w) (w : W) : (multidimApp tc uci).tDim w ↔ tc.tDim w

Composing with a UCI does not change truth conditions.

When a functional expletive UCI (with trivial t-dim) is composed with truth-conditional content via MA, the t-dim of the result equals the t-dim of the truth-conditional input. This is the formal content of "UCIs do not contribute truth conditions."

theorem Gutzmann2015.multidimApp_tc_preserves_uci_tDim {C : Type u_1} {W : Type u_2} (uci tc : ThreeDimMeaning C W) (h : ∀ (w : W), uci.tDim w) (w : W) : (multidimApp uci tc).tDim w ↔ tc.tDim w

Composing with truth-conditional content does not change truth conditions of an expression whose t-dim is already trivial.

Bridge Compositionality

theorem Gutzmann2015.toTwoDim_multidimApp {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) (evalU : (C → Prop) → W → Prop) (hConj : ∀ (p q : C → Prop) (w : W), evalU (fun (c : C) => p c ∧ q c) w ↔ evalU p w ∧ evalU q w) : toTwoDim (multidimApp f a) evalU = (toTwoDim f evalU).and (toTwoDim a evalU)

The 3D→2D bridge commutes with MA when the lowering operator distributes over conjunction.

If evalU preserves conjunctive structure (i.e., lowering a conjunction of u-propositions equals the conjunction of lowered u-propositions), then projecting a composed 3D meaning to 2D is the same as composing the individual 2D projections.

This is the formal guarantee that L_TU's 3D composition "collapses" correctly into [Pot05]'s 2D framework.

Sentence-mood operators as UCIs

Mood Context

structure Gutzmann2015.MoodContext (W : Type u_1) : Type u_1

A context of utterance for sentence mood evaluation.

Captures the context parameters that sentence mood operators quantify over: c_S (speaker), c_A (addressee), c_W (world of the context).

Simplification: [Gut15] defines DEONT via existential quantification over a set D of contextually suitable deontic predicates (wants, wishes, orders, ...). The full definition is: ⟦DEONT⟧ = λp.{c : ∃ d ∈ D, d suitable for p in c ∧ d(c_S, p, c_W)}. We simplify this to a fixed speakerWants function, which suffices for the core derivation theorems but does not capture the context-dependent selection among different deontic attitudes.

• world : W

  The world of the utterance context

• speakerWants : Bool → Bool

  Whether the speaker wants p to hold (given p's truth value at world)

• addresseeKnows : Bool → Bool

  Whether the addressee knows whether p (given p's truth value at world)

Sentence Mood Operators

def Gutzmann2015.deont {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

Deontic sentence mood operator ([Gut15], (5.85)).

⟦DEONT⟧ = λp. {c : there is a d ∈ D such that d is suitable for p in c and d holds for p in c_W}

Simplified: the speaker wants p to hold in the utterance world.

Introduced by the root rule (5.43): every matrix clause gets a deontic interpretation, expressing a volition on the part of the speaker.

Equations

• Gutzmann2015.deont p c = c.speakerWants (p c.world)

def Gutzmann2015.epis {W : Type u_1} (p : W → Bool) : W → Bool

Epistemic sentence mood operator ([Gut15], (5.90)).

⟦EPIS⟧ = λp. {w : EPIS(p)(w) in w} = λp. {w : there is an e ∈ E suitable for p in w and e holds for p in w}

Simplified: at the world level, epistemic embedding preserves truth. The epistemic contribution is in the use-conditional dimension, mediated by the E modifier.

Equations

• Gutzmann2015.epis p = p

def Gutzmann2015.episModifier {W : Type u_1} (d : (W → Bool) → MoodContext W → Bool) : (W → Bool) → MoodContext W → Bool

The E operator: epistemic modifier on UCIs ([Gut15], (5.91)).

E = λDλp. D(EPIS(p))

This is a use-conditional modifier of type ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩. It takes a UCI (like DEONT) that maps propositions to use-conditional propositions, and pre-composes it with EPIS. The result is that DEONT applies to the epistemically embedded proposition rather than the raw propositional content.

Equations

• Gutzmann2015.episModifier d p c = d (Gutzmann2015.epis p) c

def Gutzmann2015.hknow {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

Hearer knowledge operator ([Gut15], (5.99)).

⟦HKNOW⟧ = λp. {c : c_A knows whether p in c_W}

A functional expletive UCI that adds a "free-floating" use condition: the addressee knows the answer to the question. Present only in V2-interrogatives (triggered by [−wh] in C⁰), absent from VL-interrogatives — accounting for the Cuban cigar scenario.

Equations

• Gutzmann2015.hknow p c = c.addresseeKnows (p c.world)

Mood Operator Inventory

structure Gutzmann2015.MoodStructure : Type

Which sentence mood operators are present in a clause type ([Gut15], Table 5.1).

Language-agnostic predicate over a (possibly language-specific) clause type, recording which of DEONT, EPIS, and HKNOW the clause composes. Used by per-language clause-type fragments to declare their mood inventories (e.g., German.ClauseTypes.GermanClauseType.moodStructure).

• hasDeontic : Bool
• hasEpistemic : Bool
• hasHearerKnowledge : Bool

@[instance_reducible]

instance Gutzmann2015.instDecidableEqMoodStructure : DecidableEq MoodStructure

Equations

• Gutzmann2015.instDecidableEqMoodStructure = Gutzmann2015.instDecidableEqMoodStructure.decEq

def Gutzmann2015.instDecidableEqMoodStructure.decEq (x✝ x✝¹ : MoodStructure) : Decidable (x✝ = x✝¹)

Equations

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

def Gutzmann2015.instReprMoodStructure.repr : MoodStructure → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gutzmann2015.instReprMoodStructure : Repr MoodStructure

Equations

• Gutzmann2015.instReprMoodStructure = { reprPrec := Gutzmann2015.instReprMoodStructure.repr }

Operator-level theorems

theorem Gutzmann2015.epis_preserves_truth {W : Type u_1} (p : W → Bool) (w : W) : epis p w = p w

Epistemic embedding preserves truth at the world level. The epistemic contribution is purely use-conditional, not truth-conditional.

The German clause-type mood compositions

German clause-type mood compositions

def Gutzmann2015.dassVLMood {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

dass-VL clause mood: DEONT only ([Gut15], (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

• Gutzmann2015.dassVLMood p c = Gutzmann2015.deont p c

def Gutzmann2015.v2DeclMood {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

V2-declarative mood: DEONT(EPIS(p)) ([Gut15], (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

• Gutzmann2015.v2DeclMood p c = Gutzmann2015.episModifier Gutzmann2015.deont p c

def Gutzmann2015.v2InterrogMood {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

V2-interrogative mood: DEONT(EPIS(p)) ⊙ HKNOW(p) ([Gut15], (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

• Gutzmann2015.v2InterrogMood p c = (Gutzmann2015.episModifier Gutzmann2015.deont p c && Gutzmann2015.hknow p c)

def Gutzmann2015.vlInterrogMood {W : Type u_1} (p : W → Bool) (c : MoodContext W) : Bool

VL-interrogative mood: DEONT(EPIS(p)) only — no HKNOW ([Gut15], 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

• Gutzmann2015.vlInterrogMood p c = Gutzmann2015.episModifier Gutzmann2015.deont p c

Mood-operator theorems for the German clause-type compositions

theorem Gutzmann2015.dassVL_is_pure_deontic {W : Type u_1} (p : W → Bool) (c : MoodContext W) : dassVLMood p c = deont p c

dass-VL clauses have no epistemic component.

theorem Gutzmann2015.v2_vs_vl_interrog {W : Type u_1} (p : W → Bool) (c : MoodContext W) : v2InterrogMood p c = (vlInterrogMood p c && hknow p c)

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

Mood structures of the German clause types

def German.ClauseTypes.GermanClauseType.moodStructure : GermanClauseType → Gutzmann2015.MoodStructure

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

Equations

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

theorem Gutzmann2015.every_clause_has_deont (ct : German.ClauseTypes.GermanClauseType) : ct.moodStructure.hasDeontic = true

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

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

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

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

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

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

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

theorem Gutzmann2015.hknow_iff_v2_interrogative (ct : German.ClauseTypes.GermanClauseType) : ct.moodStructure.hasHearerKnowledge = true ↔ ct = German.ClauseTypes.GermanClauseType.v2Interrogative

HKNOW holds of exactly the V2-interrogative — the matrix question. The HKNOW use condition tracks matrix interrogativity ([Gut15], p. 213, Cuban cigar argument).

theorem Gutzmann2015.dassVL_v2Decl_differ_in_mood : German.ClauseTypes.GermanClauseType.dassVL.moodStructure ≠ German.ClauseTypes.GermanClauseType.v2Declarative.moodStructure

dass-VL and V2-declaratives are distinguished only at the mood-structure level.

Mood-structure predictions

theorem Gutzmann2015.cuban_cigar : German.ClauseTypes.GermanClauseType.v2Interrogative.moodStructure.hasHearerKnowledge = true ∧ German.ClauseTypes.GermanClauseType.vlInterrogative.moodStructure.hasHearerKnowledge = false

The Cuban cigar argument: V2- and VL-interrogatives differ ONLY in the hearer knowledge condition. This explains why VL-interrogatives are felicitous even when the hearer clearly does not know the answer (the Cuban cigar scenario), while V2-interrogatives are not.

theorem Gutzmann2015.imperative_matches_dassVL : German.ClauseTypes.GermanClauseType.imperative.moodStructure = German.ClauseTypes.GermanClauseType.dassVL.moodStructure

Imperatives share dass-VL mood structure (deontic only): both lack [±wh] at LF, so neither triggers epistemic interpretation.

theorem Gutzmann2015.dassVL_no_epis : German.ClauseTypes.GermanClauseType.dassVL.moodStructure.hasEpistemic = false

dass-VL clauses have no epistemic component.

theorem Gutzmann2015.v2Decl_epis_no_hknow : German.ClauseTypes.GermanClauseType.v2Declarative.moodStructure.hasEpistemic = true ∧ German.ClauseTypes.GermanClauseType.v2Declarative.moodStructure.hasHearerKnowledge = false

V2-declaratives have epistemic but not hearer knowledge.

Modal particle–mood interaction

def Gutzmann2015.uciParticles : List Particle

Gutzmann's L_TU classification (§6.5): ja/denn/halt/doch are functional-expletive UCIs of type ⟨⟨s,t⟩, u⟩, restricted via use-conditional conflict. (Formerly fragment fields; the typing is this book's analysis.)

Equations

• Gutzmann2015.uciParticles = [German.Particles.ja, German.Particles.denn, German.Particles.halt, German.Particles.doch]

def Gutzmann2015.ucModifiers : List Particle

wohl is Gutzmann's sole UC-modifier among the common MPs: type ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩, modifying EPIS, restricted selectionally.

Equations

• Gutzmann2015.ucModifiers = [German.Particles.wohl]

def Gutzmann2015.restrictionKind (p : Particle) : RestrictionKind

Restriction kind per Gutzmann: UCIs restrict via use-conditional conflict, UC-modifiers selectionally (imperatives lack EPIS — a type mismatch, not a pragmatic conflict).

Equations

• Gutzmann2015.restrictionKind p = if p ∈ Gutzmann2015.ucModifiers then Gutzmann2015.RestrictionKind.selectional else Gutzmann2015.RestrictionKind.ucConflict

theorem Gutzmann2015.wohl_iff_epis (ct : German.ClauseTypes.GermanClauseType) : German.Particles.licensedInClause German.Particles.wohl ct = ct.moodStructure.hasEpistemic

wohl's licensing across German clause types is exactly the presence of EPIS in the clause type's mood structure — the formal content of the selectional restriction analysis.

theorem Gutzmann2015.ja_declarative_restriction : German.Particles.ja.LicensedIn Particle.ClauseType.declarative ∧ ¬German.Particles.ja.LicensedIn Particle.ClauseType.polar

ja is restricted to declaratives, matching the clause type with deontic + epistemic mood but without the hearer knowledge condition.

theorem Gutzmann2015.denn_interrogative_restriction : ¬German.Particles.denn.LicensedIn Particle.ClauseType.declarative ∧ German.Particles.denn.LicensedIn Particle.ClauseType.polar

denn is the interrogative counterpart of ja.

theorem Gutzmann2015.ja_denn_partition (ct : German.ClauseTypes.GermanClauseType) : ¬(German.Particles.licensedInClause German.Particles.ja ct = true ∧ German.Particles.licensedInClause German.Particles.denn ct = true)

ja and denn partition clause types: they are never both licensed in the same clause type.