Hartmann & Zimmermann (2007) — Focus in Hausa

@cite{hartmann-zimmermann-2007} @cite{newman-2000}

@cite{hartmann-zimmermann-2007} argue that Hausa is a counterexample to the universalist claim that focus marking is obligatory and that focus position determines pragmatic interpretation. The empirical claims formalised in this study file are:

• Two focus strategies (§2): ex-situ (fronted, with relative TAM and optional stabilizer nē/cē) and in-situ (base position, no morphosyntactic reflex). Already encoded in Fragments/Hausa/Focus.lean's Strategy/FocusConfig.
• Subject-focus generalization (§2.2.2). Hausa subjects are forced ex-situ only when the TAM admits a relative form (the paper notes this "applies only in the perfective and continuous"); the future, habitual, and subjunctive don't show the asymmetry. The conditional form is exactly FocusUtterance.IsHausaLicensed below.
• Pragmatic uses of focus (§3.2). Four uses of one semantic focus — new-information, corrective, selective, contrastive — that all attest on both strategies, refuting the position-determines-interpretation Meaning-Structure Mapping Hypothesis.
• Meaning-Structure Mapping Hypothesis (eq. 21). Generalised polymorphically over arbitrary FocusUtterance → α interpretation functions; the pragmatic-type instance is the one Hausa refutes.
• Polar tone of nē/cē (§2.1): the stabilizer surfaces with the opposite tone of the immediately preceding syllable. This is exactly Stabilizer.toneAfter from Fragments/Hausa/Focus.lean §8, which delegates to Tone.polarOf.
• Universalist Basic Focus Rule fails on Hausa (§5, §6.2). Defined as a structural predicate (UniversalBFR) requiring every Hausa-licensed utterance to carry a morphosyntactic reflex of focus (ex-situ position or stabilizer); refuted by the in-situ new-information cell, which carries neither.

Out of scope: §3.2.5 exhaustivity against @cite{kiss-1998} requires an alternatives-semantics exhaustivity operator and a derivation that projects ex-situ to non-exhaustive readings — needs more infrastructure than PragType tags can carry, deferred to a study file with proper exhaustivity semantics. §4 focus pied-piping / partial focus movement and the eq. (47) "Ex-Situ Generalisation, final version" need a structured-meaning overlap predicate the current Fragment doesn't expose. The §5 prosodic pilot study and §6.1 emphasis motivation are quantitative tendencies / functional pressures rather than categorical claims and live in docstring prose only.

inductive Phenomena.Focus.Studies.HartmannZimmermann2007.PragType : Type

The four pragmatic uses of focus distinguished in @cite{hartmann-zimmermann-2007} §1.2 (eq. 1a–d), built on a single Roothian alternative-set semantics. The paper emphasises that these are pragmatic uses of one semantic focus, not distinct semantic types — so the type carries no semantic load, only a label for discourse role. The §3.2.5 exhaustive case is omitted: it would require an alternatives-semantics exhaustivity projection to be load-bearing rather than a tag.

• newInfo : PragType
• corrective : PragType
• selective : PragType
• contrastive : PragType

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableEqPragType : DecidableEq PragType

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableEqPragType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instReprPragType : Repr PragType

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instReprPragType = { reprPrec := Phenomena.Focus.Studies.HartmannZimmermann2007.instReprPragType.repr }

def Phenomena.Focus.Studies.HartmannZimmermann2007.instReprPragType.repr : PragType → ℕ → Std.Format

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedPragType.default : PragType

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedPragType.default = Phenomena.Focus.Studies.HartmannZimmermann2007.PragType.newInfo

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedPragType : Inhabited PragType

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedPragType = { default := Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedPragType.default }

inductive Phenomena.Focus.Studies.HartmannZimmermann2007.Focused : Type

A coarse classification of the focused constituent. Hausa singles out subjects as the cell where in-situ focus is unavailable in the perfective/continuous (paper §2.2.2); everything else (object, adverbial, predicate, clause) collapses to nonSubject.

• subject : Focused
• nonSubject : Focused

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableEqFocused : DecidableEq Focused

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocused.repr : Focused → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocused : Repr Focused

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocused = { reprPrec := Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocused.repr }

def Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedFocused.default : Focused

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedFocused.default = Phenomena.Focus.Studies.HartmannZimmermann2007.Focused.subject

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedFocused : Inhabited Focused

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedFocused = { default := Phenomena.Focus.Studies.HartmannZimmermann2007.instInhabitedFocused.default }

structure Phenomena.Focus.Studies.HartmannZimmermann2007.FocusUtterance : Type

A focus utterance bundles a FocusConfig (morphosyntax, from Fragments/Hausa/Focus.lean) with its pragmatic interpretation and a tag for what the focused constituent is. The Focus Fragment is deliberately agnostic about pragmatic type and constituent identity; this study file is where those tags get attached to specific paper examples.

• cfg : Fragments.Hausa.Focus.FocusConfig
• pragType : PragType
• focused : Focused

def Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocusUtterance.repr : FocusUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocusUtterance : Repr FocusUtterance

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocusUtterance = { reprPrec := Phenomena.Focus.Studies.HartmannZimmermann2007.instReprFocusUtterance.repr }

def Phenomena.Focus.Studies.HartmannZimmermann2007.FocusUtterance.IsHausaLicensed (u : FocusUtterance) : Prop

A focus utterance is Hausa-licensed iff it satisfies both the morphosyntactic licensing condition (FocusConfig.Licensed, encoding the relative-TAM requirement on ex-situ focus) and the @cite{hartmann-zimmermann-2007} §2.2.2 subject-focus generalization, conditional on the TAM admitting a relative form. Per the paper (p. 4): "subject foci are syntactically and morphologically unmarked in the future, habitual and subjunctive aspects". The asymmetry is therefore tied to TAM.HasRelativeForm, not to focus per se — making the licensing predicate derive from a structural fact about the TAM rather than stipulate a global subject ban.

Equations

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

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableIsHausaLicensed (u : FocusUtterance) : Decidable u.IsHausaLicensed

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableIsHausaLicensed u = Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableIsHausaLicensed._aux_1 u

def Phenomena.Focus.Studies.HartmannZimmermann2007.exSitu_newInfo : FocusUtterance

Ex-situ + new-information focus (paper eq. 22): Kiifii nèe Kandè takèe dafàawaa 'Kande is cooking the FISH.' PAC: 3sg.F relative continuous takèe (subject-marker for Kande).

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.exSitu_corrective : FocusUtterance

Ex-situ + corrective focus on a feminine subject (paper eq. 24): màataŕ-sa cèe ta mutù 'No, it was HIS WIFE who died.' PAC: 3sg.F relative completive ta.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.exSitu_selective : FocusUtterance

Ex-situ + selective focus (paper eq. 29): Gùdaa nakèe sô! 'I want a WHOLE.' PAC: 1sg relative continuous nakèe.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.exSitu_contrastive : FocusUtterance

Ex-situ + contrastive focus (paper eq. 27): cî kawài akèe ta yî 'it is only EATING that is going on.' Approximated with 3sg.M relative completive — paper uses the 4sg impersonal akèe which Features.Person.Category does not yet expose.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_newInfo : FocusUtterance

In-situ + new-information focus (paper eq. 23): Naa tahoo dàgà Bířnin Kwànni 'I came from BIRNIN KONNI.' PAC: 1sg general completive naa.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_corrective : FocusUtterance

In-situ + corrective focus (paper eq. 25): zân biyaa shâ bìyař̀ nèe 'No, I will pay FIFTEEN.' PAC: 1sg future zân (no G/R contrast).

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_selective : FocusUtterance

In-situ + selective focus (paper eq. 30): Zân shaa shaayìi 'I will drink TEA.' PAC: 1sg future zân.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_contrastive : FocusUtterance

In-situ + contrastive focus (paper eq. 26): ...baa àa bî ta gàbansà '...you shouldn't pass IN FRONT of him.' Approximated with 3sg.M general completive — paper uses the 4sg impersonal àa.

Equations

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

def Phenomena.Focus.Studies.HartmannZimmermann2007.hzMatrix : List FocusUtterance

The 8-cell empirical matrix from paper §3.2. Every cell is Hausa-licensed; together they witness the failure of the MSMH (§5 below).

Equations

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

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

Every cell of the H&Z matrix is Hausa-licensed. Both strategies attest each pragmatic type; the only subject-focus cell (exSitu_corrective, eq. 24) is ex-situ in a relative-form TAM, consistent with the §2.2.2 generalization.

def Phenomena.Focus.Studies.HartmannZimmermann2007.HausaMSMH : Prop

MSMH instantiated for Hausa. Specialises the polymorphic Theories.Semantics.Focus.MSMH.MeaningStructureMapping with FocusUtterance.IsHausaLicensed as the admissibility filter, cfg.strategy as the structural projection, and pragType as the interpretation projection. The Hungarian study file (Kiss1998.lean) instantiates the same polymorphic predicate with Hungarian-specific projections and proves it holds — making the typological contrast a difference of verdict on a single shared hypothesis.

Equations

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

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.hausa_falsifies_MSMH : ¬HausaMSMH

Hausa falsifies the MSMH (paper §3.2). Witness: exSitu_newInfo (eq. 22) and exSitu_corrective (eq. 24) are both ex-situ Hausa-licensed utterances differing in pragmatic type. The 8-cell matrix supplies many further same-strategy / different-pragType pairs.

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.hausa_falsifies_MSMH_inSitu : ∃ (u₁ : FocusUtterance) (u₂ : FocusUtterance), u₁.IsHausaLicensed ∧ u₂.IsHausaLicensed ∧ u₁.cfg.strategy = u₂.cfg.strategy ∧ u₁.pragType ≠ u₂.pragType

In-situ also falsifies the MSMH. The same-strategy / different-pragType pattern is not unique to ex-situ: inSitu_newInfo (eq. 23) and inSitu_corrective (eq. 25) are both in-situ Hausa-licensed utterances differing in pragmatic type.

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.subject_focus_only_exSitu (u : FocusUtterance) (h : u.IsHausaLicensed) (hSubj : u.focused = Focused.subject) (hRel : u.cfg.pac.tam.HasRelativeForm) : u.cfg.strategy = Fragments.Hausa.Focus.Strategy.exSitu

Subject-focus generalization (paper §2.2.2). Hausa subjects can only be focused via the ex-situ strategy when the TAM admits a relative form (perfective/continuous). The theorem unpacks the second conjunct of IsHausaLicensed.

def Phenomena.Focus.Studies.HartmannZimmermann2007.starred_inSitu_subject : FocusUtterance

The paper's ungrammatical in-situ subject focus (§2.2.2): *Daudàa ya-nàa kirà-ntà — 3sg.M subject, in-situ, continuous (cont_3sm_G — yanā). Continuous has a relative form, so the licensing predicate fires and rejects this.

Equations

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

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.starred_inSitu_subject_not_IsHausaLicensed : ¬starred_inSitu_subject.IsHausaLicensed

The starred in-situ subject focus is not Hausa-licensed. Its morphosyntactic licensing succeeds (in-situ is vacuously licensed by FocusConfig.Licensed) but the subject-focus conjunct fails: a subject constituent paired with inSitu strategy in a TAM with a relative form contradicts the §2.2.2 generalization.

def Phenomena.Focus.Studies.HartmannZimmermann2007.licensed_exSitu_subject : FocusUtterance

The paper's grammatical ex-situ subject focus (§2.2.2): Daudàa (nee) ya-kèe kirà-ntà. PAC: 3sg.M relative continuous yake.

Equations

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

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.licensed_exSitu_subject_IsHausaLicensed : licensed_exSitu_subject.IsHausaLicensed

The grammatical ex-situ subject focus IS Hausa-licensed. The minimal pair with starred_inSitu_subject is the empirical content of the §2.2.2 generalization.

def Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_subject_subjunctive : FocusUtterance

In-situ subject focus IS licensed when the TAM has no relative form. The paper's qualification (p. 4): "subject foci are syntactically and morphologically unmarked in the future, habitual and subjunctive aspects". A 3sg.M subjunctive subject in-situ is Hausa-licensed because subj_3sm.tam.HasRelativeForm is False, so the second conjunct of IsHausaLicensed is vacuous.

Equations

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

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.inSitu_subject_subjunctive_IsHausaLicensed : inSitu_subject_subjunctive.IsHausaLicensed

def Phenomena.Focus.Studies.HartmannZimmermann2007.FocusUtterance.HasMorphosyntacticReflex (u : FocusUtterance) : Prop

A focus utterance carries a morphosyntactic reflex of focus iff it fronts the focus (exSitu) or surfaces a stabilizer. This is the structural property the universalist Basic Focus Rule says every focused utterance must exhibit.

Equations

• u.HasMorphosyntacticReflex = (u.cfg.strategy = Fragments.Hausa.Focus.Strategy.exSitu ∨ u.cfg.hasStab = true)

@[implicit_reducible]

instance Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex (u : FocusUtterance) : Decidable u.HasMorphosyntacticReflex

Equations

• Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex u = Phenomena.Focus.Studies.HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex._aux_1 u

def Phenomena.Focus.Studies.HartmannZimmermann2007.UniversalBFR : Prop

Universalist Basic Focus Rule. The strong claim — implicit in Selkirk's BFR and the broader prosodic-marking universalist tradition — that every grammatically focused utterance carries some structural reflex of focus (movement, particle, stress, …). Restricted to morphosyntactic reflexes here because Hausa refutes even this weaker version.

Equations

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

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.hausa_falsifies_UniversalBFR : ¬UniversalBFR

Hausa falsifies the universalist BFR. Witness: inSitu_newInfo (paper eq. 23, Naa tahoo dàgà Bířnin Kwànni) is Hausa-licensed yet carries neither ex-situ position nor a stabilizer. The §5 prosodic-pilot finding (no significant pitch/duration/intensity reflex either) is documented in docstring prose only — even the morphosyntactic-only weakening already refutes the universal.

Paper §2.1: the focus-sensitive particle nē/cē surfaces "with low tone if the immediately preceding syllable is high, and with high tone if the preceding syllable is low" — i.e. polar tone. This is exactly Stabilizer.toneAfter from Fragments/Hausa/Focus.lean §8, which delegates to Tone.polarOf from Fragments/Hausa/Tone.lean. The two minimal-pair examples below are paper eq. (3a, 3b).

theorem Phenomena.Focus.Studies.HartmannZimmermann2007.polar_tone_from_polarOf (s : Fragments.Hausa.Focus.Stabilizer) (host : Phonology.Autosegmental.RegisterTier.TRN) : s.toneAfter host = Fragments.Hausa.Tone.polarOf host

The polar-tone description is structural, not stipulative. Re-derives stabilizer_tone_is_polar from the cross-fragment bridge as a one-liner, anchoring the H&Z §2.1 generalization in the same Tone.polarOf operator that handles the genitive linker -n and other Hausa polarity phenomena.