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

This file formalizes [Hoh92]'s analysis of verum focus: the accent on a German finite verb in initial position, or on a subordinating particle such as daß, that highlights a meaning element VERUM paraphrasable as "it is true that", as in Karl SCHREIBT ein Drehbuch replying to the claim that Karl is writing a screenplay. The paper's argument runs from assumption (13), that VERUM is assigned to the accented word and highlighted as a semantic focus, to a rejection of the reading of VERUM as an illocution-type operator: verum focus occurs in embedded verb-second clauses and on complementizers, and in er HÖRT ihr nicht zu VERUM lies in the scope of the negation, so it must be a truth predicate whose scope follows from the syntax.

The scope rule (60) lets the meaning element of a constituent K₁ lie in the scope of that of K₂ iff K₁ stands in a structural relation SR to K₂; SR reads it as c-command with reconstruction of a fronted finite verb to its trace. On the peripheral structure of (76), a clause [Φ Π] whose position Φ is filled by a complementizer or by a finite verb binding a trace in Π, the negation in Π c-commands the verb's trace but not Φ, so Scoping.negOverVerum is admissible for verum focus on the finite verb and not for verum focus on daß. The felicity condition is that the background thought, the argument of VERUM, is known from the context (Appropriate); this derives the contrast of (55): after ich hoffe, daß Karl ihr zuhört, the verb-second reply is appropriate and the daß reply is not. IntroducesVerum is the non-segmental rule (97) of the final section, which introduces VERUM over any bare Π next to a non-empty sister; it decides which accents yield verum focus across complementizers, fronted verbs, relative and interrogative pronouns without a particle, and verb-final verbs.

Implementation notes

• Clauses are PhraseStructure.Trees over the labels of (76) and (97), with Π flat inside; the trace bindings that reconstruction respects are given as an explicit list, footnote 7's pseudo-reconstruction, and Höhle's relation SR is left open in the paper.
• VERUM is the identity on propositions, so the two scopings of (56) have the same content (content_focusBackground) and differ only in what is background.
• "Known from the context" is membership in a set of propositions the context makes known; the question under discussion plays no role.
• The assumption of §7 that there is no verum focus on a verb-final finite verb, and the copula and full-verb judgments of (71) and (72), are recorded in the example rows only.

References

• [Hoh92]

The peripheral structure of (76)

inductive Hohle1992.Node : Type

The constituent labels are the clause, the position in front of Φ holding a Vorfeld constituent or a relative or interrogative phrase, the peripheral position Φ of (76), its complement Π (Mittelfeld, verbal complex and Nachfeld), and inside Π the negation particle, the verb position and other material.

• clause : Node
• front : Node
• phi : Node
• pi : Node
• neg : Node
• verb : Node
• other : Node

@[instance_reducible]

instance Hohle1992.instDecidableEqNode : DecidableEq Node

Equations

• Hohle1992.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hohle1992.instReprNode : Repr Node

Equations

• Hohle1992.instReprNode = { reprPrec := Hohle1992.instReprNode.repr }

def Hohle1992.instReprNode.repr : Node → ℕ → Std.Format

Equations

• Hohle1992.instReprNode.repr Hohle1992.Node.clause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.clause")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.front prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.front")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.phi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.phi")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.pi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.pi")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.neg")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.verb")).group prec✝
• Hohle1992.instReprNode.repr Hohle1992.Node.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hohle1992.Node.other")).group prec✝

def Hohle1992.fClause : PhraseStructure.Tree Node String

In (55a) er HÖRT ihr nicht zu the finite verb fills Φ and binds a trace in Π.

Equations

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

def Hohle1992.cClause : PhraseStructure.Tree Node String

In (55b) daß er ihr nicht zuhört the complementizer fills Φ and binds nothing.

Equations

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

def Hohle1992.whClause : PhraseStructure.Tree Node String

In (81) WER hat den Hund getreten an interrogative pronoun precedes a filled Φ.

Equations

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

def Hohle1992.rwClause : PhraseStructure.Tree Node String

In (82a) DER das Buch gelesen hat a relative pronoun precedes an empty Φ (91ii).

Equations

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

def Hohle1992.woClause : PhraseStructure.Tree Node String

In (77a) and (80a) der WO das Buch gelesen hat a relative pronoun stands in front of a Φ filled by the dialectal relative particle.

Equations

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

def Hohle1992.finalClause : PhraseStructure.Tree Node String

In (68b) daß sie damit aufHÖRT the finite verb stays in final position inside Π.

Equations

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

The scope rule (60)

def Hohle1992.SR (t : PhraseStructure.Tree Node String) (binds : List (Core.Order.TreePath × Core.Order.TreePath)) (k₁ k₂ : Core.Order.TreePath) : Prop

The relation SR of (60), read as c-command with reconstruction (footnote 7). k₁ stands in SR to k₂ in t when k₂ c-commands k₁ or a trace that k₁ binds.

Equations

• Hohle1992.SR t binds k₁ k₂ = ((k₂, k₁) ∈ RoseTree.cCommand t ∨ ∃ b ∈ binds, b.1 = k₁ ∧ (k₂, b.2) ∈ RoseTree.cCommand t)

@[instance_reducible]

instance Hohle1992.instDecidableSR (t : PhraseStructure.Tree Node String) (binds : List (Core.Order.TreePath × Core.Order.TreePath)) (k₁ k₂ : Core.Order.TreePath) : Decidable (SR t binds k₁ k₂)

Equations

• Hohle1992.instDecidableSR t binds k₁ k₂ = id inferInstance

structure Hohle1992.Configuration : Type

A negated clause with verum focus records its tree, the trace bindings, the position of the accented word carrying VERUM and the position of the negation particle.

• tree : PhraseStructure.Tree Node String
• binds : List (Core.Order.TreePath × Core.Order.TreePath)
• focus : Core.Order.TreePath
• neg : Core.Order.TreePath

def Hohle1992.negatedF : Configuration

In (55a) verum focus is on the fronted finite verb, reconstructed to its trace.

Equations

• Hohle1992.negatedF = { tree := Hohle1992.fClause, binds := [({ toList := [1, 0] }, { toList := [1, 1, 3] })], focus := { toList := [1, 0] }, neg := { toList := [1, 1, 1] } }

def Hohle1992.negatedC : Configuration

In (55b) verum focus is on the complementizer.

Equations

• Hohle1992.negatedC = { tree := Hohle1992.cClause, binds := [], focus := { toList := [0] }, neg := { toList := [1, 2] } }

inductive Hohle1992.Scoping : Type

The two scopings of VERUM relative to the negation, paraphrased in (56a) and (56b).

• negOverVerum : Scoping
• verumOverNeg : Scoping

@[instance_reducible]

instance Hohle1992.instDecidableEqScoping : DecidableEq Scoping

Equations

• Hohle1992.instDecidableEqScoping x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hohle1992.Scoping.Admissible (c : Configuration) : Scoping → Prop

Applied to VERUM and the negation, (60) says that VERUM may lie in the scope of the negation iff the accented constituent stands in SR to the negation particle, and conversely.

Equations

• Hohle1992.Scoping.Admissible c Hohle1992.Scoping.negOverVerum = Hohle1992.SR c.tree c.binds c.focus c.neg
• Hohle1992.Scoping.Admissible c Hohle1992.Scoping.verumOverNeg = Hohle1992.SR c.tree c.binds c.neg c.focus

@[instance_reducible]

instance Hohle1992.instDecidableAdmissible (c : Configuration) (s : Scoping) : Decidable (Scoping.Admissible c s)

Equations

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

theorem Hohle1992.negOverVerum_admissible_negatedF : Scoping.Admissible negatedF Scoping.negOverVerum

The negation of (55a) c-commands the trace of the fronted verb, so VERUM may lie in its scope.

theorem Hohle1992.verumOverNeg_admissible_negatedF : Scoping.Admissible negatedF Scoping.verumOverNeg

theorem Hohle1992.not_negOverVerum_admissible_negatedC : ¬Scoping.Admissible negatedC Scoping.negOverVerum

The complementizer of (55b) neither is c-commanded by the negation nor binds a trace, so VERUM cannot lie in the negation's scope.

theorem Hohle1992.verumOverNeg_admissible_negatedC : Scoping.Admissible negatedC Scoping.verumOverNeg

Focus–background structure and appropriateness

inductive Hohle1992.WF : Type

Höhle's class WF of meaning elements by which a speaker signals an attitude to the truth of a thought, each occurring as E(p) and recursively embeddable; the scope data use VERUM, a truth predicate, and the negation.

• verum : WF
• neg : WF

def Hohle1992.WF.apply {W : Type u_1} : WF → Set W → Set W

The extension of a WF element. VERUM, a truth predicate, maps a thought to itself.

Equations

• Hohle1992.WF.verum.apply x✝ = x✝
• Hohle1992.WF.neg.apply x✝ = x✝ᶜ

structure Hohle1992.FocusBackground (W : Type u_2) : Type u_2

A focus–background structure consists of the highlighted chain of WF elements, outermost first, and the background thought they apply to.

• focus : List WF
• background : Set W

def Hohle1992.FocusBackground.content {W : Type u_1} (s : FocusBackground W) : Set W

The content expressed by a focus–background structure.

Equations

• s.content = List.foldr Hohle1992.WF.apply s.background s.focus

def Hohle1992.Scoping.focusBackground {W : Type u_1} (p : Set W) : Scoping → FocusBackground W

By (56), with VERUM in the scope of the negation, the negation joins the highlighted part and the background is the thought p itself; with VERUM above the negation, the background is the negated thought.

Equations

• Hohle1992.Scoping.focusBackground p Hohle1992.Scoping.negOverVerum = { focus := [Hohle1992.WF.neg, Hohle1992.WF.verum], background := p }
• Hohle1992.Scoping.focusBackground p Hohle1992.Scoping.verumOverNeg = { focus := [Hohle1992.WF.verum], background := pᶜ }

theorem Hohle1992.content_focusBackground {W : Type u_1} (p : Set W) (s : Scoping) : (Scoping.focusBackground p s).content = pᶜ

VERUM is truth-conditionally inert, so the two scopings of (56) express the same content and differ only in what is background.

def Hohle1992.Appropriate {W : Type u_1} (known : Set (Set W)) (c : Configuration) (p : Set W) : Prop

Höhle's condition on verum focus is that the background thought is known from the context. A negated clause expressing the thought p is appropriate when some scoping that (60) admits has its background among the propositions known from the context.

Equations

• Hohle1992.Appropriate known c p = ∃ (s : Hohle1992.Scoping), Hohle1992.Scoping.Admissible c s ∧ (Hohle1992.Scoping.focusBackground p s).background ∈ known

theorem Hohle1992.appropriate_negatedF_iff {W : Type u_1} (known : Set (Set W)) (p : Set W) : Appropriate known negatedF p ↔ p ∈ known ∨ pᶜ ∈ known

Verum focus on the fronted verb is appropriate whenever the thought or its negation is known.

theorem Hohle1992.appropriate_negatedC_iff {W : Type u_1} (known : Set (Set W)) (p : Set W) : Appropriate known negatedC p ↔ pᶜ ∈ known

Verum focus on the complementizer is appropriate only if the negated thought is known.

theorem Hohle1992.appropriate_negatedF_singleton {W : Type u_1} (p : Set W) : Appropriate {p} negatedF p

In (55a) after (55c), ich hoffe, daß Karl ihr zuhört makes the thought known, and the verb-second reply er HÖRT ihr nicht zu is appropriate.

theorem Hohle1992.not_appropriate_negatedC_singleton {W : Type u_1} [Nonempty W] (p : Set W) : ¬Appropriate {p} negatedC p

In (55b) after (55c), the reply daß er ihr nicht zuhört is inappropriate, since the negated thought its daß must take as background is not known.

The non-segmental introduction of VERUM (97)

def Hohle1992.PhonEmpty (t : PhraseStructure.Tree Node String) : Prop

A tree is phonologically empty when its yield is empty.

Equations

• Hohle1992.PhonEmpty t = (t.yield = [])

@[instance_reducible]

instance Hohle1992.instDecidablePhonEmpty (t : PhraseStructure.Tree Node String) : Decidable (PhonEmpty t)

Equations

• Hohle1992.instDecidablePhonEmpty t = id inferInstance

def Hohle1992.IsBarePi (t : PhraseStructure.Tree Node String) : Prop

A constituent of the form [σ Π σ] with σ phonologically empty is a Π itself, or a node among whose daughters is a Π and the others are phonologically empty.

Equations

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

@[instance_reducible]

instance Hohle1992.instDecidableIsBarePi (t : PhraseStructure.Tree Node String) : Decidable (IsBarePi t)

Equations

• Hohle1992.instDecidableIsBarePi t = id inferInstance

def Hohle1992.IntroducesVerum (t : PhraseStructure.Tree Node String) (kj : Core.Order.TreePath) : Prop

By (97), in a local tree [Kₖ Kⱼ Kᵢ] whose second daughter is a bare Π and whose first daughter is not phonologically empty, VERUM is introduced over the translation of Kᵢ; by (98ii) it is assigned to Kⱼ, so an accent on Kⱼ yields verum focus.

Equations

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

@[instance_reducible]

instance Hohle1992.instDecidableIntroducesVerum (t : PhraseStructure.Tree Node String) (kj : Core.Order.TreePath) : Decidable (IntroducesVerum t kj)

Equations

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

theorem Hohle1992.introducesVerum_fClause_phi : IntroducesVerum fClause { toList := [1, 0] }

The fronted finite verb of (55a) is the non-empty sister of Π.

theorem Hohle1992.introducesVerum_cClause_phi : IntroducesVerum cClause { toList := [0] }

The complementizer of (55b) is the non-empty sister of Π.

theorem Hohle1992.introducesVerum_woClause_phi : IntroducesVerum woClause { toList := [1, 0] }

In (77a) the relative particle wo filling Φ carries VERUM.

theorem Hohle1992.introducesVerum_rwClause_front : IntroducesVerum rwClause { toList := [0] }

In (82a) the relative pronoun in front of an empty Φ carries VERUM, the RW-verum focus of §9.

theorem Hohle1992.not_introducesVerum_woClause_front : ¬IntroducesVerum woClause { toList := [0] }

In (80a), with the particle wo filling Φ, the relative pronoun's sister is not a bare Π, so its accent yields no verum focus.

theorem Hohle1992.not_introducesVerum_whClause_front : ¬IntroducesVerum whClause { toList := [0] }

In (81) the interrogative pronoun in front of a fronted verb yields no verum focus.

theorem Hohle1992.not_introducesVerum_finalClause_verb : ¬IntroducesVerum finalClause { toList := [1, 3] }

In (68b) the verb-final finite verb inside Π yields no verum focus.