Höhle (1992): Verum-Fokus im Deutschen

@cite{hohle-1992} @cite{romero-han-2004} @cite{rooth-1992} @cite{repp-2013} @cite{gutzmann-hartmann-matthewson-2020} @cite{martinez-vera-2026}

Höhle's seminal proposal: pitch accent on the finite verb (or negation particle) in German is verum focus — focus on the assertion operator, emphasising the polarity/truth of the prejacent rather than its content.

The classic minimal pair (Höhle 1992: 116):

• "Karl HAT das Buch gelesen." — VF on auxiliary, emphatic affirmation
• "Karl hat das BUCH gelesen." — content focus on object

The two share truth-conditional content but differ in what they contribute to the discourse: VF requires a salient ¬p (or salient suspension of p) and serves to settle that prior issue.

What this study formalises

• A minimal verumFocusOp on BiLayered W that highlights the prejacent's polarity in the context's salient set (the Höhle move: focus on the assertion operator).
• A felicity condition aligning with the cross-linguistic generalisation: VF is licensed exactly when the prejacent's negation is highlighted in the prior context.

Relation to other studies

This file used to live at Phenomena/Polarity/Studies/Hohle1992.lean as a 158-LOC file of bare def data records (sentences and tags) with no actual analysis of Höhle's verum-focus operator. Re-homed here as part of the Verum directory landing, replacing the data-only content with the formal operator and its felicity profile. The German prosodic data (auxiliary stress, negation stress) is illustrative of the substrate, not stipulated as primitive — see Phenomena/Verum/Basic for the cross-linguistic verum-marker inventory.

Adjacent studies the substrate is shared with:

• Phenomena/Verum/Studies/MartinezVera2026.lean — the same highlighting + ⟨A, N⟩ machinery applied to Saraguro Kichwa =mi. Höhle's German VF and Martínez Vera's =mi exemplify the same paper-(60) prediction about the focus-account of verum.
• Phenomena/Questions/Studies/RomeroHan2004.lean — VERUM as a CG operator (rather than as focus on the assertion operator). R&H's forSureCG is the alternative-line analysis that Höhle's focus-account contrasts with (paper §6's FAT vs. LOT debate).

def Phenomena.Verum.Studies.Hohle1992.verumFocusOp {W : Type u_1} (β : Semantics.Composition.Layered.BiLayered W) : Semantics.Composition.Layered.BiLayered W

Höhle's verum-focus operator. Applied to a prejacent β, it returns the same at-issue content (β.atIssue) — VF is truth-conditionally transparent — and adds a not-at-issue conjunct that the prejacent's polarity is the highlighted one. The not-at-issue contribution is Höhle's reading of pitch accent on the finite verb / negation as targeting the assertion operator rather than the propositional content.

Equations

• Phenomena.Verum.Studies.Hohle1992.verumFocusOp β = { atIssue := β.atIssue, notAtIssue := fun (w : W) => β.notAtIssue w ∧ β.atIssue w }

@[simp]

theorem Phenomena.Verum.Studies.Hohle1992.verumFocusOp_atIssue {W : Type u_1} (β : Semantics.Composition.Layered.BiLayered W) : (verumFocusOp β).atIssue = β.atIssue

VF preserves the at-issue layer (truth-conditional transparency).

@[simp]

theorem Phenomena.Verum.Studies.Hohle1992.verumFocusOp_notAtIssue {W : Type u_1} (β : Semantics.Composition.Layered.BiLayered W) : (verumFocusOp β).notAtIssue = fun (w : W) => β.notAtIssue w ∧ β.atIssue w

def Phenomena.Verum.Studies.Hohle1992.verumFelicitous {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) : Prop

Höhle's licensing condition: a verum-focus utterance is felicitous in context c iff the prejacent's negation is highlighted in c.

This is the cross-linguistic verum signature: the marker requires that ¬p be salient (asserted earlier, contextually inferable, or raised by a biased question). Without this, VF is infelicitous out-of-the-blue (Höhle 1992; @cite{romero-han-2004}; @cite{gutzmann-hartmann-matthewson-2020}).

Equations

• Phenomena.Verum.Studies.Hohle1992.verumFelicitous c β = Semantics.Highlighting.Highlighted c {w : W | ¬β.atIssue w}

theorem Phenomena.Verum.Studies.Hohle1992.verumFelicitous_after_highlighting_neg {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) (h : Semantics.Highlighting.AddressesQUD c.qud {w : W | ¬β.atIssue w}) : verumFelicitous (Semantics.Highlighting.addSalient c {w : W | ¬β.atIssue w}) β

VF is felicitous after a context that has highlighted ¬p. The witness: addSalient c {w | ¬ β.atIssue w} makes ¬p salient; if the QUD is set up to be addressed by ¬p (as it is in the standard biased-question or asserted-¬p discourse), then Highlighted holds.

def Phenomena.Verum.Studies.Hohle1992.hohleAsVerumOperator {W : Type u_1} : Basic.VerumOperator W

Höhle's verum-focus operator packaged as a VerumOperator, so that cross-paper bridge / refutation theorems can be stated against other inhabitants of the same shared structure.

Equations

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

@[simp]

theorem Phenomena.Verum.Studies.Hohle1992.hohleAsVerumOperator_apply {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) : hohleAsVerumOperator.felicitous c β = verumFelicitous c β