German modal particles

This file defines the German modal particles ja, denn, wohl, halt and doch and the combination doch wohl as Particle entries, each with the sentence types of a main clause in which Durrell describes it. A modal particle stands in the middle of the clause and adds the speaker's attitude to what is said. Ja appeals for agreement in statements, expresses surprise in exclamations and intensifies a command, often as a warning and especially when stressed. Denn is used in questions only, polar and constituent questions alike. Wohl signals probability in statements and uncertainty in questions. Halt occurs in statements and commands. Doch marks disagreement in statements, urgency in commands, a request for confirmation in constituent questions and surprise in exclamations; unstressed, it can turn a statement into a question expecting the answer yes, and with wohl it hopes that something is the case. A sentence type the grammar says nothing about is left unrecorded.

The polarity particles ja, nein and doch, answering and responding, are German.PolarityParticle; the response doch is also used as a separate utterance before a Verum focus correction (TurcoBraunDimroth2014). The analyses of the modal particles are with the studies of them: Gutzmann's typing of ja, denn and wohl with his own examples, Theiler's denn, Seeliger and Repp's doch wohl.

References

• [Dur11]
• [Gut15]
• [The21]
• [SR18]

def German.Particles.inMatrix (yes no : List Clause.SentenceType) : Clause.Distribution

inMatrix yes no records a particle as optional in the main-clause sentence types yes and excluded from those in no, and records nothing else.

Equations

• German.Particles.inMatrix yes no x✝ Clause.EmbeddingContext.matrix = if x✝ ∈ yes then some Clause.Occurrence.optional else if x✝ ∈ no then some Clause.Occurrence.excluded else none
• German.Particles.inMatrix yes no x✝¹ x✝ = none

def German.Particles.ja : Particle

Ja appeals for agreement in statements, expresses surprise in exclamations and intensifies a command.

Equations

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

def German.Particles.denn : Particle

Denn is used in questions only, polar and constituent.

Equations

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

def German.Particles.wohl : Particle

Wohl signals probability in statements and uncertainty in questions.

Equations

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

def German.Particles.halt : Particle

Halt occurs in statements and commands.

Equations

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

def German.Particles.doch : Particle

Doch occurs in statements, commands, constituent questions and exclamations.

Equations

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

def German.Particles.dochWohl : Particle

Doch wohl, also wohl doch, occurs in statements and hopes that something is the case.

Equations

• German.Particles.dochWohl = { form := "doch wohl", position := some Particle.Position.clauseMedial, distribution := German.Particles.inMatrix [Clause.SentenceType.declarative] [] }

def German.Particles.modalParticles : List Particle

The modal particles.

Equations

• German.Particles.modalParticles = [German.Particles.ja, German.Particles.denn, German.Particles.wohl, German.Particles.halt, German.Particles.doch]

inductive German.PolarityParticle : Type

The German polarity particles.

• ja : PolarityParticle

  ja 'yes'.

• nein : PolarityParticle

  nein 'no'.

• doch : PolarityParticle

  doch 'yes', contradicting a negative: Kommt er nicht? — Doch, he is coming.

@[instance_reducible]

instance German.instDecidableEqPolarityParticle : DecidableEq PolarityParticle

Equations

• German.instDecidableEqPolarityParticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def German.instReprPolarityParticle.repr : PolarityParticle → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance German.instReprPolarityParticle : Repr PolarityParticle

Equations

• German.instReprPolarityParticle = { reprPrec := German.instReprPolarityParticle.repr }

@[instance_reducible]

instance German.instFintypePolarityParticle : Fintype PolarityParticle

Equations

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

def German.PolarityParticle.form : PolarityParticle → String

The spelling of a polarity particle.

Equations

• German.PolarityParticle.ja.form = "ja"
• German.PolarityParticle.nein.form = "nein"
• German.PolarityParticle.doch.form = "doch"