Hausa focus strategies and pragmatic types

Formalises the [HZ07] argument that Hausa is a counterexample to the universalist claims that focus marking is obligatory and that focus position determines pragmatic interpretation.

Implementation notes

The paper states the hypothesis it refutes as (21) "Meaning-Structure Mapping Hypothesis" (§3.1), the label following [VV98]'s phrase "the meaning-structure mapping"; the shared schema is Function.FactorsThroughOn (Core.Logic.FactorsThroughOn), making the Hungarian/Hausa contrast a difference of verdict on a single set-theoretic predicate. The §1.2 control taxonomy (Antecedent, Use) and its factor-through theorems live in Semantics/Focus/Control.lean.

Subject foci in TAMs lacking a Relative form (future, habitual, subjunctive) are "syntactically and morphologically unmarked" (p. 4); the paper analyses them as string-vacuously ex-situ, so IsHausaLicensed bans in-situ subjects unconditionally and exSitu_subject_subjunctive is licensed yet reflex-free.

§3.3's corpus tendencies stay prose: answers to wh-questions are mostly in-situ (99 vs 25) while selective/corrective/contrastive foci are >90% ex-situ (154 vs 12), but "none of the discussed instances of focus is categorically excluded from occurring either in situ or ex situ" — only the categorical no-determination claim is a theorem.

TODO

• The Kiss-side semantic interpretation of FocusType.IsExhaustive (obligatory covert onlyVia) for the like-for-like §3.2.5 contrast — needs a semantic layer in Kiss1998.lean.
• §2.3 multiple foci: co-occurrence of one ex-situ focus with in-situ foci (18a-c).
• §4 focus pied-piping / partial focus movement and the (47) "Ex-Situ Generalisation, final version" need a structured-meaning overlap predicate.
• §5 prosodic pilot data and §6.1 emphasis motivation are quantitative tendencies, currently in docstring prose only.

References

• [HZ07], [New00], [Uhm91], [Sel95], [VV98].

What is focused (§2.2.2)

inductive HartmannZimmermann2007.Focused : Type

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

• subject : Focused
• nonSubject : Focused

@[implicit_reducible]

instance HartmannZimmermann2007.instDecidableEqFocused : DecidableEq Focused

Equations

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

@[implicit_reducible]

instance HartmannZimmermann2007.instReprFocused : Repr Focused

Equations

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

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

Equations

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

@[implicit_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 : Semantics.Focus.Use
• focused : Focused

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

Equations

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

@[implicit_reducible]

instance HartmannZimmermann2007.instReprFocusUtterance : Repr FocusUtterance

Equations

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

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

Morphosyntactic licensing (FocusConfig.Licensed) plus the §2.2.2 ban on in-situ subject focus. The ban is unconditional: 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 = Hausa.Strategy.exSitu))

@[implicit_reducible]

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

Equations

• HartmannZimmermann2007.instDecidableIsHausaLicensed u = HartmannZimmermann2007.instDecidableIsHausaLicensed._aux_1 u

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 AltMeaning = ⟨none⟩).

inductive HartmannZimmermann2007.Alt : Type

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

• ans : Alt
• alt : Alt

theorem HartmannZimmermann2007.ctx_resolves (u : Semantics.Focus.Use) : (HartmannZimmermann2007.ctx✝ u).Resolves HartmannZimmermann2007.answer✝.oValue HartmannZimmermann2007.answer✝.aSet

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.5)

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.

theorem HartmannZimmermann2007.exhAnswer_eq (u : Semantics.Focus.Use) : HartmannZimmermann2007.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 — the §3.2.5 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 Semantics.Focus.Antecedent, not a tag.

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 ((27), Examples.ex27); the paper's 4sg impersonal akèe is approximated with the 3sg.M Relative continuous.

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.cmp_1sg_G Gender.masculine true (HartmannZimmermann2007.ctx✝ Semantics.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.fut_1sg Gender.masculine true (HartmannZimmermann2007.ctx✝ Semantics.Focus.Use.selective)

def HartmannZimmermann2007.inSitu_contrastive : FocusUtterance

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

Equations

• HartmannZimmermann2007.inSitu_contrastive = HartmannZimmermann2007.mkInSituUtt✝ Hausa.fut_1sg Gender.masculine true (HartmannZimmermann2007.ctx✝ Semantics.Focus.Use.contrastive)

def HartmannZimmermann2007.hzMatrix : List FocusUtterance

The 8-cell matrix of §3.2: both strategies × 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.FactorsThroughOn FocusUtterance.pragType (fun (u : FocusUtterance) => u.cfg.strategy) {u : FocusUtterance | u.IsHausaLicensed}

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

theorem HartmannZimmermann2007.strategy_underdetermines_pragType_inSitu : ¬Function.FactorsThroughOn FocusUtterance.pragType (fun (u : FocusUtterance) => u.cfg.strategy) {u : FocusUtterance | u.IsHausaLicensed ∧ u.cfg.strategy = Hausa.Strategy.inSitu}

The refutation persists restricted to in-situ utterances: (23) vs (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 = Hausa.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_subjunctive : FocusUtterance

Subject focus in a TAM with no Relative form (the (8) pattern, Examples.ex8): string-vacuous fronting with no overt reflex — see exSitu_subject_subjunctive_no_reflex.

Equations

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

theorem HartmannZimmermann2007.exSitu_subject_subjunctive_IsHausaLicensed : exSitu_subject_subjunctive.IsHausaLicensed

Universalist Basic Focus Rule (§5, §6.2)

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

An overt reflex of focus: non-vacuous fronting (subjects front string-vacuously), Relative-form morphology, or a stabilizer.

Equations

• u.HasMorphosyntacticReflex = (u.focused = HartmannZimmermann2007.Focused.nonSubject ∧ u.cfg.strategy = Hausa.Strategy.exSitu ∨ u.cfg.pac.mode = Hausa.Mode.relative ∨ u.cfg.hasStab = true)

@[implicit_reducible]

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

Equations

• HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex u = HartmannZimmermann2007.instDecidableHasMorphosyntacticReflex._aux_1 u

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_subjunctive_no_reflex : ¬exSitu_subject_subjunctive.HasMorphosyntacticReflex

The subject-side counterexample (the (8) pattern).

def HartmannZimmermann2007.FocusUtterance.reflexes (u : FocusUtterance) : List (Semantics.Focus.Reflex Focused)

The overt reflexes of a focus utterance in the shared Semantics.Focus.Realization vocabulary: non-vacuous fronting, Relative-form morphology, and the stabilizer.

Equations

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

theorem HartmannZimmermann2007.hasMorphosyntacticReflex_iff (u : FocusUtterance) : u.HasMorphosyntacticReflex ↔ { focus := u.focused, reflexes := u.reflexes }.IsOvert

The disjunctive reflex predicate coincides with overtness of the reflex list.

theorem HartmannZimmermann2007.hausa_refutes_perceptibility : ¬Semantics.Focus.EveryFocusPerceptible fun (u : { u : FocusUtterance // u.IsHausaLicensed }) => { focus := (↑u).focused, reflexes := (↑u).reflexes }

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

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

Stabilizer.toneAfter is Hausa.polarOf; the minimal pair below is (3a, 3b).

Data linkage

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

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

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

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

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