German Modal Particles

@cite{gutzmann-2015}

Lexical entries for German modal particles (Modalpartikeln), analyzed within the L_TU framework.

Two Kinds of Modal Particle (@cite{gutzmann-2015}, §6.5)

Modal particles fall into two categories with distinct types and restriction mechanisms:

Functional Expletive UCIs (ja, denn, halt, doch)

Type: ⟨⟨s,t⟩, u⟩. These take a proposition and return u-content. They are [+functional], [−2-dimensional], [−resource-sensitive]. Their mood restriction arises from use-conditional conflict: their independent u-content is incompatible with certain sentence moods.

UC-Modifiers (wohl)

Type: ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩. These take a UCI and return a modified UCI. wohl modifies the epistemic mood operator EPIS. Its mood restriction is selectional: imperatives lack EPIS, so wohl has no argument to modify — a type mismatch, not a pragmatic conflict.

Semantic Properties (derived from L_TU)

The special behavior of modal particles follows from their UCI type and L_TU's composition rules, without any special syntactic assumptions:

• Non-truth-conditionality: identity in t-dim (functional expletive)
• Scopelessness: u-content is stored by UE, inaccessible to higher operators
• Unfocusability: focus operator and MP end up in different dimensions
• Uncoordinatability: no LER extends use-conditional coordination to 3D

Mood Distribution (@cite{gutzmann-2015}, Table 6.1)

Particle	Declarative	Interrogative	Imperative	Kind	Restriction
ja	✓	✗	✗	UCI	conflict
denn	✗	✓	✗	UCI	conflict
wohl	✓	✓	✗	UC-modifier	selectional
halt	✓	✗	✗	UCI	conflict
doch	✓	✗	✓	UCI	conflict

structure Fragments.German.ModalParticles.ModalParticleEntry : Type

A German modal particle lexical entry.

Follows the pattern of QuestionParticles.QParticleEntry with per-sentence-type distribution booleans for direct per-datum verification.

• form : String

  Surface form

• exprKind : Semantics.UseConditional.UCExprKind

  Whether this is a UCI or a UC-modifier (@cite{gutzmann-2015}, §6.5)

• uciClass : Semantics.UseConditional.UCIClass

  UCI classification (only meaningful when exprKind = .uci)

• restrictionKind : Semantics.UseConditional.RestrictionKind

  How mood restriction arises

• declOk : Bool

  Licensed in declarative sentences

• interrogOk : Bool

  Licensed in interrogative sentences

• imperOk : Bool

  Licensed in imperative sentences

• glossEnglish : String

  English gloss

def Fragments.German.ModalParticles.instDecidableEqModalParticleEntry.decEq (x✝ x✝¹ : ModalParticleEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.German.ModalParticles.instDecidableEqModalParticleEntry : DecidableEq ModalParticleEntry

Equations

• Fragments.German.ModalParticles.instDecidableEqModalParticleEntry = Fragments.German.ModalParticles.instDecidableEqModalParticleEntry.decEq

def Fragments.German.ModalParticles.instReprModalParticleEntry.repr : ModalParticleEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.German.ModalParticles.instReprModalParticleEntry : Repr ModalParticleEntry

Equations

• Fragments.German.ModalParticles.instReprModalParticleEntry = { reprPrec := Fragments.German.ModalParticles.instReprModalParticleEntry.repr }

def Fragments.German.ModalParticles.ModalParticleEntry.moodOk (mp : ModalParticleEntry) : Core.Mood.IllocutionaryMood → Bool

Check whether a modal particle is licensed in a given sentence type.

Equations

• mp.moodOk Core.Mood.IllocutionaryMood.declarative = mp.declOk
• mp.moodOk Core.Mood.IllocutionaryMood.interrogative = mp.interrogOk
• mp.moodOk Core.Mood.IllocutionaryMood.imperative = mp.imperOk
• mp.moodOk x✝ = false

def Fragments.German.ModalParticles.ModalParticleEntry.licensedInClause (mp : ModalParticleEntry) {f : Features.ClauseForm} : ClauseTypes.GermanClauseType f → Bool

Map a German clause type to the distribution field it tests.

Equations

• mp.licensedInClause Fragments.German.ClauseTypes.GermanClauseType.dassVL = false
• mp.licensedInClause Fragments.German.ClauseTypes.GermanClauseType.v2Declarative = mp.declOk
• mp.licensedInClause Fragments.German.ClauseTypes.GermanClauseType.v2Interrogative = mp.interrogOk
• mp.licensedInClause Fragments.German.ClauseTypes.GermanClauseType.vlInterrogative = mp.interrogOk
• mp.licensedInClause Fragments.German.ClauseTypes.GermanClauseType.imperative = mp.imperOk

def Fragments.German.ModalParticles.ja : ModalParticleEntry

ja — common-ground reminder particle.

Roughly: "as you may already know." Licensed only in declaratives; excluded from interrogatives and imperatives. Its use condition references the truth of its propositional argument, conflicting with the epistemic uncertainty of interrogatives and the non-epistemic nature of imperatives.

Restriction kind: use-conditional conflict.

Equations

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

def Fragments.German.ModalParticles.denn : ModalParticleEntry

denn — question-prompting particle.

Signals the question is prompted by contextual evidence; the interrogative counterpart of ja. Licensed only in interrogatives; excluded from declaratives, imperatives, and dass-VL clauses.

Restriction kind: use-conditional conflict.

Equations

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

def Fragments.German.ModalParticles.wohl : ModalParticleEntry

wohl — epistemic hedging particle.

Modifies the epistemic mood operator EPIS, introducing a degree of uncertainty. Licensed in declaratives and interrogatives (both of which involve EPIS), but excluded from imperatives (which lack EPIS).

This is a UC-modifier, not a functional expletive UCI. Its type is ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩ — it takes a UCI (like DEONT composed with EPIS) and modifies its epistemic component. The restriction is selectional: imperatives lack EPIS, so wohl has no argument to modify (type mismatch).

Equations

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

def Fragments.German.ModalParticles.halt : ModalParticleEntry

halt — resignation/acceptance particle.

Roughly: "that's just the way it is." Licensed only in declaratives.

Restriction kind: use-conditional conflict.

Equations

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

def Fragments.German.ModalParticles.doch : ModalParticleEntry

doch — contradiction/insistence particle.

Signals conflict with an expected or salient counterstance. Uniquely among common MPs, licensed in both declaratives and imperatives — its use condition (contradiction of a salient proposition) is compatible with both deontic-only and deontic/epistemic mood structures.

Restriction kind: use-conditional conflict.

Equations

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

def Fragments.German.ModalParticles.allModalParticles : List ModalParticleEntry

All modal particle entries.

Equations

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

def Fragments.German.ModalParticles.uciParticles : List ModalParticleEntry

The functional expletive UCI entries (excluding UC-modifiers).

Equations

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

theorem Fragments.German.ModalParticles.ja_decl_only : ja.declOk = true ∧ ja.interrogOk = false ∧ ja.imperOk = false

theorem Fragments.German.ModalParticles.denn_interrog_only : denn.declOk = false ∧ denn.interrogOk = true ∧ denn.imperOk = false

theorem Fragments.German.ModalParticles.wohl_decl_and_interrog : wohl.declOk = true ∧ wohl.interrogOk = true ∧ wohl.imperOk = false

theorem Fragments.German.ModalParticles.halt_decl_only : halt.declOk = true ∧ halt.interrogOk = false ∧ halt.imperOk = false

theorem Fragments.German.ModalParticles.doch_decl_and_imper : doch.declOk = true ∧ doch.interrogOk = false ∧ doch.imperOk = true

theorem Fragments.German.ModalParticles.uci_mps_functional_expletive (mp : ModalParticleEntry) : mp ∈ uciParticles → mp.exprKind = Semantics.UseConditional.UCExprKind.uci → mp.uciClass = Semantics.UseConditional.functionalExpletive

Every true UCI among these particles is a functional expletive.

theorem Fragments.German.ModalParticles.wohl_unique_uc_modifier (mp : ModalParticleEntry) : mp ∈ allModalParticles → mp.exprKind = Semantics.UseConditional.UCExprKind.ucModifier → mp.form = "wohl"

wohl is the only UC-modifier among these particles.

theorem Fragments.German.ModalParticles.restriction_tracks_kind (mp : ModalParticleEntry) : mp ∈ allModalParticles → (mp.exprKind = Semantics.UseConditional.UCExprKind.uci → mp.restrictionKind = Semantics.UseConditional.RestrictionKind.ucConflict) ∧ (mp.exprKind = Semantics.UseConditional.UCExprKind.ucModifier → mp.restrictionKind = Semantics.UseConditional.RestrictionKind.selectional)

Every UCI in this list has conflict-based restriction; the UC-modifier has selectional restriction.

theorem Fragments.German.ModalParticles.doch_unique_imperative (mp : ModalParticleEntry) : mp ∈ allModalParticles → mp.imperOk = true → mp.form = "doch"

doch is the only common MP licensed in imperatives.

theorem Fragments.German.ModalParticles.no_mp_universal (mp : ModalParticleEntry) : mp ∈ allModalParticles → ¬(mp.declOk = true ∧ mp.interrogOk = true ∧ mp.imperOk = true)

No MP is licensed in all three sentence types.

theorem Fragments.German.ModalParticles.wohl_iff_epis {f : Features.ClauseForm} (ct : ClauseTypes.GermanClauseType f) : wohl.licensedInClause ct = ct.moodStructure.hasEpistemic

wohl's licensing across ALL German clause types is exactly determined by the presence of EPIS in the clause type's mood structure.

This is the formal content of the selectional restriction analysis: wohl modifies EPIS, so it is licensed iff EPIS is present.

theorem Fragments.German.ModalParticles.all_excluded_from_dassVL (mp : ModalParticleEntry) : mp ∈ allModalParticles → mp.licensedInClause ClauseTypes.GermanClauseType.dassVL = false

Every MP is excluded from dass-VL clauses (subordinate, no matrix mood).

theorem Fragments.German.ModalParticles.ja_denn_complementary {f : Features.ClauseForm} (ct : ClauseTypes.GermanClauseType f) : ¬(ja.licensedInClause ct = true ∧ denn.licensedInClause ct = true)

ja and denn are in complementary distribution: for every clause type, at most one of them is licensed.