Hartmann and Zimmermann (2007): In place — out of place? Focus strategies in Hausa

Hartmann and Zimmermann's argument that Hausa is a counterexample to two universalist claims: that focus is always marked, and that the position of a focus determines its pragmatic interpretation. Focus is realized in situ or ex situ, and the paper's §3.2 matrix crosses the two strategies with four pragmatic uses, new-information, corrective, contrastive and selective, every cell of which is licensed (hzMatrix); strategy_does_not_determine_pragType refutes the Meaning-Structure Mapping Hypothesis of (21), the label following Vallduví and Vilkuna, stated as a failure of Function.FactorsThrough on the licensed utterances, so that the Hungarian and Hausa verdicts differ on one predicate. In-situ new-information focus carries no morphosyntactic reflex, and the §5 pilot finds no prosodic one either, so hausa_falsifies_UniversalBFR refutes the Basic Focus Rule of Selkirk; focused subjects, by contrast, always front (§2.2.2). Exhaustivity is not structural: the particle kawài 'only' exhaustifies over the resolved contrast set in either position.

Implementation notes

The §1.2 control taxonomy of uses and its factor-through theorems live in Semantics/Focus/Control.lean, and each cell's pragmatic type is computed from its controlling context rather than tagged. Subject foci in TAMs lacking a Relative form (future, habitual, subjunctive) are syntactically and morphologically unmarked, which the paper analyses as string-vacuous fronting, so the licensing predicate bans in-situ subjects unconditionally and the future subject focus of (8) is licensed yet reflex-free. The paper counts the subjunctive with the future and the habitual, but Newman excludes it from Rel environments, and the fragment's licensing, which is his, rejects a fronted subjunctive (not_licensed_exSitu_subjunctive). Which TAMs show Relative morphology is not stipulated: a licensed fronted focus changes the TAM exactly when the TAM does not occur in Rel environments (Hausa.FocusConfig.pacTAM_ne_iff), the completive and continuous of the paper's data. The §3.3 corpus tendencies stay in prose: answers to wh-questions are mostly in situ (99 against 25) and selective, corrective and contrastive foci mostly ex situ (154 against 12), but no use is categorically excluded from either position, and only that categorical claim is a theorem. Locators follow the authors' prepublication manuscript of the chapter.

TODO

• The like-for-like contrast with Hungarian: kawài against the exhaustification over Kiss1998.alternatives that the identificational position performs.
• §2.3 multiple foci: one ex-situ focus with in-situ foci (18a–c).
• §4 focus pied-piping and partial focus movement, and the final Ex-Situ Generalisation of their (47), which need a structured-meaning overlap predicate.
• §5 prosodic pilot data and §6.1 emphasis motivation are quantitative tendencies, in prose only.

References

• [HZ07c]
• [New00]
• [Uhm91]
• [Sel95]
• [VV98]

What is focused (§2.2.2)

inductive HartmannZimmermann2007.Focused : Type

Hausa singles out subjects as what is focused (§2.2.2); everything else collapses to nonSubject.

• subject : Focused
• nonSubject : Focused

@[instance_reducible]

instance HartmannZimmermann2007.instDecidableEqFocused : DecidableEq Focused

Equations

• HartmannZimmermann2007.instDecidableEqFocused x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HartmannZimmermann2007.instReprFocused.repr : Focused → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HartmannZimmermann2007.instReprFocused : Repr Focused

Equations

• HartmannZimmermann2007.instReprFocused = { reprPrec := HartmannZimmermann2007.instReprFocused.repr }

@[instance_reducible]

instance HartmannZimmermann2007.instInhabitedFocused : Inhabited Focused

Equations

• HartmannZimmermann2007.instInhabitedFocused = { default := HartmannZimmermann2007.instInhabitedFocused.default }

Tagged focus utterances and Hausa licensing

structure HartmannZimmermann2007.FocusUtterance : Type

A FocusConfig tagged with its pragmatic use and focused constituent.

• cfg : Hausa.FocusConfig
• pragType : Focus.Use
• focused : Focused

def HartmannZimmermann2007.instReprFocusUtterance.repr : FocusUtterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HartmannZimmermann2007.instReprFocusUtterance : Repr FocusUtterance

Equations

• HartmannZimmermann2007.instReprFocusUtterance = { reprPrec := HartmannZimmermann2007.instReprFocusUtterance.repr }

def HartmannZimmermann2007.FocusUtterance.IsHausaLicensed (u : FocusUtterance) : Prop

An utterance is Hausa-licensed when it is morphosyntactically licensed (FocusConfig.Licensed) and respects the §2.2.2 ban on in-situ subject focus. The ban is unconditional, since in TAMs without a Relative form the fronting is merely invisible (p. 4), not absent.

Equations

• u.IsHausaLicensed = (u.cfg.Licensed ∧ (u.focused = HartmannZimmermann2007.Focused.subject → u.cfg.strategy = Focus.Strategy.exSitu))

@[instance_reducible]

instance HartmannZimmermann2007.instDecidableIsHausaLicensed (u : FocusUtterance) : Decidable u.IsHausaLicensed

Equations

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

Controlling contexts of the §3.2 matrix

Every cell's mini-scenario has one shape: a two-point answer domain — the mentioned answer ans vs the contextual alternative alt — whose content (fish vs other dishes, fifteen vs twenty Naira, behind vs in front, …) lives in the cell's data row. The antecedent is the canonical Use.model of the row's context shape; the answer is composed by the engine (pairAnswer); ctx_resolves is the uniform full-resolution fact. Ex-situ variants are interpreted at the base structure (fronting is A'-movement for the paper, and alternatives do not distribute through abstraction: PredAbs WithAlternatives = ⟨none⟩).

inductive HartmannZimmermann2007.Alt : Type

The two-point answer domain of a cell's mini-scenario.

• ans : Alt
• alt : Alt

def HartmannZimmermann2007.ctx (u : Focus.Use) : Focus.Antecedent Alt

The canonical antecedent of a use over the two-point scenario.

Equations

• HartmannZimmermann2007.ctx u = Focus.Use.model {HartmannZimmermann2007.Alt.ans} {HartmannZimmermann2007.Alt.alt} u

def HartmannZimmermann2007.answer : WithAlternatives (Set Alt)

The composed answer of the two-point scenario.

Equations

• HartmannZimmermann2007.answer = Focus.pairAnswer HartmannZimmermann2007.Alt.ans HartmannZimmermann2007.Alt.alt

theorem HartmannZimmermann2007.ctx_resolves (u : Focus.Use) : (ctx u).Resolves answer.ordinary answer.alternatives

Every cell's context fully resolves against the composed answer — all squiggle clauses, plus the correction clause for the corrective cells. One semantics, four pragmatic uses.

Exhaustive focus (§3.2, (32))

Exhaustivity is not structurally encoded: it is induced by focus particles (kawài 'only'; nee/cee per the paper's fn. 3) over the resolved contrast set, in either strategy — (32a/b) attest in-situ and ex-situ only BOOKS alike.

def HartmannZimmermann2007.exhAnswer (u : Focus.Use) : Set Alt

The exhaustified answer is the exclusion asserted by only over the scenario's resolved contrast set.

Equations

• HartmannZimmermann2007.exhAnswer u = Exhaustification.excludes (HartmannZimmermann2007.ctx u).contrastSet HartmannZimmermann2007.answer.ordinary

theorem HartmannZimmermann2007.exhAnswer_eq (u : Focus.Use) : exhAnswer u = {Alt.ans}

The exhaustified answer computes to the bare true answer, uniformly across the four uses. Exhaustification consumes the resolved contrast set and prejacent, never the strategy, which is the §3.2 point that exhaustive readings are available in both positions.

The 8-cell empirical matrix (§3.2)

Each cell's pragmatic type is computed from its controlling context: the constructors take a Focus.Antecedent, not a tag.

def HartmannZimmermann2007.mkExSituUtt (tam pacTAM : Hausa.TAM) (cell : Agreement.Bundle) (g : Gender) (hasStab : Bool) {W : Type u_1} (ctl : Focus.Antecedent W) (foc : Focused := Focused.nonSubject) : FocusUtterance

Equations

• HartmannZimmermann2007.mkExSituUtt tam pacTAM cell g hasStab ctl foc = { cfg := Hausa.mkExSitu tam pacTAM cell (some g) hasStab, pragType := ctl.use, focused := foc }

def HartmannZimmermann2007.mkInSituUtt (tam : Hausa.TAM) (cell : Agreement.Bundle) (g : Gender) {W : Type u_1} (ctl : Focus.Antecedent W) (foc : Focused := Focused.nonSubject) (hasStab : Bool := false) : FocusUtterance

Equations

• HartmannZimmermann2007.mkInSituUtt tam cell g ctl foc hasStab = { cfg := Hausa.mkInSitu tam cell (some g) hasStab, pragType := ctl.use, focused := foc }

def HartmannZimmermann2007.s1 : Agreement.Bundle

The first person singular PAC cell.

Equations

• HartmannZimmermann2007.s1 = Agreement.Bundle.personNumber Person.first Number.singular

def HartmannZimmermann2007.s3m : Agreement.Bundle

The third person masculine singular PAC cell.

Equations

• HartmannZimmermann2007.s3m = Agreement.Bundle.set Agreement.Dimension.gender Gender.masculine (Agreement.Bundle.personNumber Person.third Number.singular)

def HartmannZimmermann2007.s3f : Agreement.Bundle

The third person feminine singular PAC cell.

Equations

• HartmannZimmermann2007.s3f = Agreement.Bundle.set Agreement.Dimension.gender Gender.feminine (Agreement.Bundle.personNumber Person.third Number.singular)

def HartmannZimmermann2007.p4 : Agreement.Bundle

The impersonal PAC cell.

Equations

• HartmannZimmermann2007.p4 = Hausa.impersonal

def HartmannZimmermann2007.exSitu_newInfo : FocusUtterance

Ex-situ new-information focus ((22), Examples.ex22).

Equations

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

def HartmannZimmermann2007.exSitu_corrective : FocusUtterance

Ex-situ corrective focus on a feminine subject ((24), Examples.ex24).

Equations

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

def HartmannZimmermann2007.exSitu_selective : FocusUtterance

Ex-situ selective focus, no stabilizer ((29), Examples.ex29).

Equations

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

def HartmannZimmermann2007.exSitu_contrastive : FocusUtterance

Ex-situ contrastive focus, no stabilizer, with the impersonal akèe ((27), Examples.ex27).

Equations

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

def HartmannZimmermann2007.inSitu_newInfo : FocusUtterance

In-situ new-information focus ((23), Examples.ex23).

Equations

• HartmannZimmermann2007.inSitu_newInfo = HartmannZimmermann2007.mkInSituUtt Hausa.TAM.completive HartmannZimmermann2007.s1 Gender.masculine (HartmannZimmermann2007.ctx Focus.Use.newInfo)

def HartmannZimmermann2007.inSitu_corrective : FocusUtterance

In-situ corrective focus with sentence-final nèe ((25), Examples.ex25).

Equations

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

def HartmannZimmermann2007.inSitu_selective : FocusUtterance

In-situ selective focus ((30), Examples.ex30).

Equations

• HartmannZimmermann2007.inSitu_selective = HartmannZimmermann2007.mkInSituUtt Hausa.TAM.future HartmannZimmermann2007.s1 Gender.masculine (HartmannZimmermann2007.ctx Focus.Use.selective)

def HartmannZimmermann2007.inSitu_contrastive : FocusUtterance

In-situ contrastive focus ((26), Examples.ex26).

Equations

• HartmannZimmermann2007.inSitu_contrastive = HartmannZimmermann2007.mkInSituUtt Hausa.TAM.future HartmannZimmermann2007.s1 Gender.masculine (HartmannZimmermann2007.ctx Focus.Use.contrastive)

def HartmannZimmermann2007.hzMatrix : List FocusUtterance

The 8-cell matrix of §3.2 crosses both strategies with all four pragmatic types.

Equations

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

theorem HartmannZimmermann2007.all_hzMatrix_IsHausaLicensed (u : FocusUtterance) : u ∈ hzMatrix → u.IsHausaLicensed

Every cell of the §3.2 matrix is Hausa-licensed.

Strategy does not determine pragmatic type (§3.2)

theorem HartmannZimmermann2007.strategy_does_not_determine_pragType : ¬Function.FactorsThrough (fun (u : { u : FocusUtterance // u.IsHausaLicensed }) => (↑u).pragType) fun (u : { u : FocusUtterance // u.IsHausaLicensed }) => (↑u).cfg.strategy

On Hausa-licensed utterances pragType does not factor through strategy, since (22) and (24) are both ex-situ with distinct pragmatic types.

theorem HartmannZimmermann2007.strategy_underdetermines_pragType_inSitu : ¬Function.FactorsThrough (fun (u : { u : FocusUtterance // u.IsHausaLicensed ∧ u.cfg.strategy = Focus.Strategy.inSitu }) => (↑u).pragType) fun (u : { u : FocusUtterance // u.IsHausaLicensed ∧ u.cfg.strategy = Focus.Strategy.inSitu }) => (↑u).cfg.strategy

The refutation persists when restricted to in-situ utterances, by (23) against (25).

Subject-focus generalization (§2.2.2)

theorem HartmannZimmermann2007.subject_focus_only_exSitu (u : FocusUtterance) (h : u.IsHausaLicensed) (hSubj : u.focused = Focused.subject) : u.cfg.strategy = Focus.Strategy.exSitu

Focused subjects front (§2.2.2); unpacks the second conjunct of IsHausaLicensed.

def HartmannZimmermann2007.starred_inSitu_subject : FocusUtterance

The starred in-situ subject focus ((17 A2), Examples.ex17a2).

Equations

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

theorem HartmannZimmermann2007.starred_inSitu_subject_not_IsHausaLicensed : ¬starred_inSitu_subject.IsHausaLicensed

def HartmannZimmermann2007.licensed_exSitu_subject : FocusUtterance

The grammatical ex-situ subject focus ((17 A1), Examples.ex17a1).

Equations

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

theorem HartmannZimmermann2007.licensed_exSitu_subject_IsHausaLicensed : licensed_exSitu_subject.IsHausaLicensed

def HartmannZimmermann2007.exSitu_subject_future : FocusUtterance

Subject focus in the future, which occurs in Rel environments unchanged ((8), Examples.ex8), is string-vacuous fronting with no overt reflex (exSitu_subject_future_no_reflex).

Equations

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

theorem HartmannZimmermann2007.exSitu_subject_future_IsHausaLicensed : exSitu_subject_future.IsHausaLicensed

theorem HartmannZimmermann2007.not_licensed_exSitu_subjunctive (t : Hausa.TAM) (c : Agreement.Bundle) (g : Option Gender) (hs : Bool) : ¬(Hausa.mkExSitu Hausa.TAM.subjunctive t c g hs).Licensed

No fronted subjunctive is licensed, since the subjunctive has no Rel counterpart.

Universalist Basic Focus Rule (§5, §6.2)

def HartmannZimmermann2007.FocusUtterance.reflexes (u : FocusUtterance) : Finset (Reflex Focused)

The overt reflexes of a focus utterance in the shared Reflex vocabulary are non-vacuous fronting (subjects front string-vacuously), the Rel form of the PAC where fronting changes the TAM, and the stabilizer.

Equations

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

def HartmannZimmermann2007.FocusUtterance.HasMorphosyntacticReflex (u : FocusUtterance) : Prop

A focus utterance has a morphosyntactic reflex when some reflex lies outside the phonological channel.

Equations

• u.HasMorphosyntacticReflex = ∃ ρ ∈ u.reflexes, ρ.modality.channel ≠ Reflex.Channel.phonological

@[instance_reducible]

instance HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex (u : FocusUtterance) : Decidable u.HasMorphosyntacticReflex

Equations

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

def HartmannZimmermann2007.UniversalBFR : Prop

The universalist claim — [Sel95]'s Basic Focus Rule and its tradition (§5, §6.2) — that every focused utterance carries some structural reflex, weakened to morphosyntax and quantified over Hausa utterances only.

Equations

• HartmannZimmermann2007.UniversalBFR = ∀ (u : HartmannZimmermann2007.FocusUtterance), u.IsHausaLicensed → u.HasMorphosyntacticReflex

theorem HartmannZimmermann2007.hausa_falsifies_UniversalBFR : ¬UniversalBFR

(23) is licensed and reflex-free; the §5 pilot finds no prosodic reflex either.

theorem HartmannZimmermann2007.exSitu_subject_future_no_reflex : ¬exSitu_subject_future.HasMorphosyntacticReflex

The subject-side counterexample, (8).

theorem HartmannZimmermann2007.hasMorphosyntacticReflex_iff (u : FocusUtterance) : u.HasMorphosyntacticReflex ↔ u.reflexes.Nonempty

Every Hausa focus reflex is morphosyntactic, so a morphosyntactic reflex is just an overt one.

theorem HartmannZimmermann2007.hausa_refutes_perceptibility : ¬∀ (u : { u : FocusUtterance // u.IsHausaLicensed }), (↑u).reflexes.Nonempty

Hausa refutes the universalist claim that every (licensed) focus receives an overt reflex — the same shape Tangale refutes in HartmannZimmermann2004.lean.

Polar tone of nē/cē (§2.1)

def HartmannZimmermann2007.toneTable : List (String × Tone.TRN)

The rows' tone labels.

Equations

• HartmannZimmermann2007.toneTable = [("H", Tone.TRN.H), ("L", Tone.TRN.L)]

theorem HartmannZimmermann2007.stab_tone_polar (e : Datum) : e ∈ [Examples.ex3a, Examples.ex3b] → e.parse? "stab_tone" toneTable = Option.map Hausa.polarOf (e.parse? "host_tone" toneTable)

In (3a) and (3b) the stabilizer's tone is polar to the host's final tone, high after Kandè and low after Kiifii.

Data linkage

Each cell's tags are pinned to the paperFeatures of its Data.Examples.HartmannZimmermann2007 row.

def HartmannZimmermann2007.strategyLabel : Focus.Strategy → String

Equations

• HartmannZimmermann2007.strategyLabel Focus.Strategy.inSitu = "inSitu"
• HartmannZimmermann2007.strategyLabel Focus.Strategy.exSitu = "exSitu"

def HartmannZimmermann2007.pragLabel : Focus.Use → String

Equations

• HartmannZimmermann2007.pragLabel Focus.Use.newInfo = "newInfo"
• HartmannZimmermann2007.pragLabel Focus.Use.corrective = "corrective"
• HartmannZimmermann2007.pragLabel Focus.Use.selective = "selective"
• HartmannZimmermann2007.pragLabel Focus.Use.contrastive = "contrastive"

def HartmannZimmermann2007.focusedLabel : Focused → String

Equations

• HartmannZimmermann2007.focusedLabel HartmannZimmermann2007.Focused.subject = "subject"
• HartmannZimmermann2007.focusedLabel HartmannZimmermann2007.Focused.nonSubject = "nonSubject"

def HartmannZimmermann2007.stabLabel (c : Hausa.FocusConfig) : String

Equations

• HartmannZimmermann2007.stabLabel c = match c.stab? with | some p => if p = Hausa.ce then "cee" else "nee" | none => "none"

def HartmannZimmermann2007.cellRows : List (FocusUtterance × Datum)

Equations

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

theorem HartmannZimmermann2007.cells_match_rows (p : FocusUtterance × Datum) : p ∈ cellRows → p.2.feature? "strategy" = some (strategyLabel p.1.cfg.strategy) ∧ p.2.feature? "pragType" = some (pragLabel p.1.pragType) ∧ p.2.feature? "focused" = some (focusedLabel p.1.focused) ∧ p.2.feature? "stabilizer" = some (stabLabel p.1.cfg)

Every cell's tags agree with its row's paperFeatures.

theorem HartmannZimmermann2007.ex8_matches_row : Examples.ex8.feature? "strategy" = some (strategyLabel exSitu_subject_future.cfg.strategy) ∧ Examples.ex8.feature? "focused" = some (focusedLabel exSitu_subject_future.focused) ∧ Examples.ex8.feature? "stabilizer" = some (stabLabel exSitu_subject_future.cfg)

(8) carries no pragmatic tag; its other tags agree with its cell.

def HartmannZimmermann2007.tamLabel : Hausa.TAM → String

Equations

• HartmannZimmermann2007.tamLabel Hausa.TAM.completive = "completive"
• HartmannZimmermann2007.tamLabel Hausa.TAM.preterite = "preterite"
• HartmannZimmermann2007.tamLabel Hausa.TAM.continuous = "continuous"
• HartmannZimmermann2007.tamLabel Hausa.TAM.relContinuous1 = "relContinuous1"
• HartmannZimmermann2007.tamLabel Hausa.TAM.relContinuous2 = "relContinuous2"
• HartmannZimmermann2007.tamLabel Hausa.TAM.future = "future"
• HartmannZimmermann2007.tamLabel Hausa.TAM.allative = "allative"
• HartmannZimmermann2007.tamLabel Hausa.TAM.potential = "potential"
• HartmannZimmermann2007.tamLabel Hausa.TAM.rhetorical = "rhetorical"
• HartmannZimmermann2007.tamLabel Hausa.TAM.habitual = "habitual"
• HartmannZimmermann2007.tamLabel Hausa.TAM.subjunctive = "subjunctive"

theorem HartmannZimmermann2007.tam_matches_rows (p : FocusUtterance × Datum) : p ∈ [(exSitu_subject_future, Examples.ex8), (licensed_exSitu_subject, Examples.ex17a1), (starred_inSitu_subject, Examples.ex17a2)] → p.2.feature? "tam" = some (tamLabel p.1.cfg.tam)

The rows that tag a TAM tag the clause's TAM, not its PAC's, as (17 A1) is continuous with a Rel-continuous PAC.

theorem HartmannZimmermann2007.starred_row_is_the_unlicensed_cell : Examples.ex17a2.judgment = Judgment.ungrammatical ∧ ¬starred_inSitu_subject.IsHausaLicensed

The row the paper stars is the cell the licensing predicate rejects.