Hungarian preverbal/postverbal focus contrast

Formalises [EK98]: identificational focus moves to the immediately preverbal Spec,FP and expresses exhaustive identification; information focus stays postverbal and carries no exhaustivity. Position determines focus type on licensed configurations, and the §3 distributional restrictions (universals, csak-phrases, valami/valaki) follow from class–type compatibility.

Implementation notes

The apparatus (Position, FocusType, ConstituentClass, FocusConfig) is Kiss's analytical classification, not consensus typology, so it lives here rather than in a Fragment.

Kiss's exhaustivity claim has been substantially revised in later work (Onea & Beaver 2011, Horváth 2010, Wedgwood 2005); the theorems formalise the 1998 position without adjudicating.

The factor-through schema (Function.FactorsThroughOn) is instantiated for Hausa in HartmannZimmermann2007.lean, where it is refuted.

TODO

• §4 scope (identificational focus binds variables).
• §5.2 cleft realisation in English.
• §9 cross-linguistic feature typology for Italian, Romanian, Catalan, Greek, Arabic, Finnish.
• §7 focus iteration and projection (eq. 51-53).

Structural position and focus type (§1, §2)

inductive Kiss1998.Position : Type

The two structural positions for focused constituents in Hungarian: preverbal = Spec,FP (the identificational slot), postverbal = VP-internal in situ.

• preverbal : Position
• postverbal : Position

@[implicit_reducible]

instance Kiss1998.instDecidableEqPosition : DecidableEq Position

Equations

• Kiss1998.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiss1998.instReprPosition : Repr Position

Equations

• Kiss1998.instReprPosition = { reprPrec := Kiss1998.instReprPosition.repr }

def Kiss1998.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Kiss1998.instReprPosition.repr Kiss1998.Position.preverbal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiss1998.Position.preverbal")).group prec✝

@[implicit_reducible]

instance Kiss1998.instInhabitedPosition : Inhabited Position

Equations

• Kiss1998.instInhabitedPosition = { default := Kiss1998.instInhabitedPosition.default }

inductive Kiss1998.FocusType : Type

The two focus types: identificational carries an exhaustivity entailment, information does not.

• identificational : FocusType
• information : FocusType

@[implicit_reducible]

instance Kiss1998.instDecidableEqFocusType : DecidableEq FocusType

Equations

• Kiss1998.instDecidableEqFocusType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kiss1998.instReprFocusType.repr : FocusType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiss1998.instReprFocusType : Repr FocusType

Equations

• Kiss1998.instReprFocusType = { reprPrec := Kiss1998.instReprFocusType.repr }

@[implicit_reducible]

instance Kiss1998.instInhabitedFocusType : Inhabited FocusType

Equations

• Kiss1998.instInhabitedFocusType = { default := Kiss1998.instInhabitedFocusType.default }

def Kiss1998.FocusType.IsExhaustive : FocusType → Prop

Whether the focus type carries an exhaustivity entailment (§2, the Szabolcsi–Farkas test).

Equations

• Kiss1998.FocusType.identificational.IsExhaustive = True
• Kiss1998.FocusType.information.IsExhaustive = False

@[implicit_reducible]

instance Kiss1998.instDecidableIsExhaustive (t : FocusType) : Decidable t.IsExhaustive

Equations

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

Constituent classes and licensing (§3)

inductive Kiss1998.ConstituentClass : Type

Coarse classification of the focused constituent for the §3 distributional facts: regular DPs occur as either type; universal covers the minden / X+is / még…is class barred from identificational focus (17b–d); onlyPhrase is csak X, obligatorily identificational; someIndef is valami/valaki, barred from both (17e).

• regular : ConstituentClass
• universal : ConstituentClass
• onlyPhrase : ConstituentClass
• someIndef : ConstituentClass

@[implicit_reducible]

instance Kiss1998.instDecidableEqConstituentClass : DecidableEq ConstituentClass

Equations

• Kiss1998.instDecidableEqConstituentClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiss1998.instReprConstituentClass : Repr ConstituentClass

Equations

• Kiss1998.instReprConstituentClass = { reprPrec := Kiss1998.instReprConstituentClass.repr }

def Kiss1998.instReprConstituentClass.repr : ConstituentClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiss1998.instInhabitedConstituentClass : Inhabited ConstituentClass

Equations

• Kiss1998.instInhabitedConstituentClass = { default := Kiss1998.instInhabitedConstituentClass.default }

structure Kiss1998.FocusConfig : Type

A Hungarian focused-clause configuration; Licensed enforces the position–type and class–type pairings.

• position : Position

  The structural position of the focused constituent.

• focusType : FocusType

  The focus type (identificational vs information).

• cclass : ConstituentClass

  The lexical class of the focused constituent.

def Kiss1998.instDecidableEqFocusConfig.decEq (x✝ x✝¹ : FocusConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Kiss1998.instDecidableEqFocusConfig : DecidableEq FocusConfig

Equations

• Kiss1998.instDecidableEqFocusConfig = Kiss1998.instDecidableEqFocusConfig.decEq

def Kiss1998.instReprFocusConfig.repr : FocusConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Kiss1998.instReprFocusConfig : Repr FocusConfig

Equations

• Kiss1998.instReprFocusConfig = { reprPrec := Kiss1998.instReprFocusConfig.repr }

@[implicit_reducible]

instance Kiss1998.instInhabitedFocusConfig : Inhabited FocusConfig

Equations

• Kiss1998.instInhabitedFocusConfig = { default := Kiss1998.instInhabitedFocusConfig.default }

def Kiss1998.positionFor : FocusType → Position

The canonical position for a focus type (§2): identificational moves to Spec,FP, information stays postverbal.

Equations

• Kiss1998.positionFor Kiss1998.FocusType.identificational = Kiss1998.Position.preverbal
• Kiss1998.positionFor Kiss1998.FocusType.information = Kiss1998.Position.postverbal

def Kiss1998.ConstituentClass.compatibleWith : ConstituentClass → FocusType → Prop

Class–type compatibility (§3): universal is barred from identificational focus (17b–d); onlyPhrase is "obligatorily realized as identificational" (§3); someIndef is barred from both — starred identificationally (17e) and "cannot function as information foci, either" (§3).

Equations

• Kiss1998.ConstituentClass.regular.compatibleWith x✝ = True
• Kiss1998.ConstituentClass.universal.compatibleWith Kiss1998.FocusType.identificational = False
• Kiss1998.ConstituentClass.universal.compatibleWith Kiss1998.FocusType.information = True
• Kiss1998.ConstituentClass.onlyPhrase.compatibleWith Kiss1998.FocusType.identificational = True
• Kiss1998.ConstituentClass.onlyPhrase.compatibleWith Kiss1998.FocusType.information = False
• Kiss1998.ConstituentClass.someIndef.compatibleWith x✝ = False

@[implicit_reducible]

instance Kiss1998.instDecidableCompatibleWith (c : ConstituentClass) (t : FocusType) : Decidable (c.compatibleWith t)

Equations

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

def Kiss1998.FocusConfig.Licensed (c : FocusConfig) : Prop

A configuration is licensed iff its position is canonical for its focus type (§2) and its constituent class is compatible with that type (§3).

Equations

• c.Licensed = (c.position = Kiss1998.positionFor c.focusType ∧ c.cclass.compatibleWith c.focusType)

@[implicit_reducible]

instance Kiss1998.instDecidableLicensed (c : FocusConfig) : Decidable c.Licensed

Equations

• Kiss1998.instDecidableLicensed c = Kiss1998.instDecidableLicensed._aux_1 c

def Kiss1998.mkIdentificational (cc : ConstituentClass) (_h : cc.compatibleWith FocusType.identificational) : FocusConfig

A preverbal identificational focus over a compatible class.

Equations

• Kiss1998.mkIdentificational cc _h = { position := Kiss1998.Position.preverbal, focusType := Kiss1998.FocusType.identificational, cclass := cc }

def Kiss1998.mkInformation (cc : ConstituentClass) (_h : cc.compatibleWith FocusType.information) : FocusConfig

A postverbal information focus over a compatible class.

Equations

• Kiss1998.mkInformation cc _h = { position := Kiss1998.Position.postverbal, focusType := Kiss1998.FocusType.information, cclass := cc }

theorem Kiss1998.mkIdentificational_licensed (cc : ConstituentClass) (h : cc.compatibleWith FocusType.identificational) : (mkIdentificational cc h).Licensed

theorem Kiss1998.mkInformation_licensed (cc : ConstituentClass) (h : cc.compatibleWith FocusType.information) : (mkInformation cc h).Licensed

theorem Kiss1998.licensed_position_determines_type (c : FocusConfig) (h : c.Licensed) : c.position = Position.preverbal ↔ c.focusType = FocusType.identificational

Position determines focus type on licensed configurations — the biconditional behind the Meaning-Structure Mapping verdict for Hungarian.

theorem Kiss1998.onlyPhrase_forces_identificational (c : FocusConfig) (h : c.Licensed) (hcc : c.cclass = ConstituentClass.onlyPhrase) : c.focusType = FocusType.identificational

csak-phrases must be identificational foci (§3).

theorem Kiss1998.someIndef_never_licensed (c : FocusConfig) (h : c.Licensed) : c.cclass ≠ ConstituentClass.someIndef

valami/valaki can never be focused (17e): no licensed configuration has a someIndef constituent.

Cells (§1, eq. 5a/5b, 8a/8b, 17b, 19b)

def Kiss1998.preverbal_identificational : FocusConfig

Eq. (5a): Tegnap este Marinak mutattam be Pétert 'It was to MARY that I introduced Peter last night.' Identificational/preverbal: of the relevant set of persons, it was Mary and no one else that I introduced Peter to.

Equations

• Kiss1998.preverbal_identificational = Kiss1998.mkIdentificational Kiss1998.ConstituentClass.regular True.intro

def Kiss1998.postverbal_information : FocusConfig

Eq. (5b): Tegnap este be mutattam Pétert MARINAK 'Last night I introduced Peter TO MARY.' Information/postverbal: presents Mary as nonpresupposed information, without suggesting Mary was the only one.

Equations

• Kiss1998.postverbal_information = Kiss1998.mkInformation Kiss1998.ConstituentClass.regular True.intro

def Kiss1998.preverbal_hat : FocusConfig

Eq. (8a): Mari egy kalapot nézett ki magának 'It was a HAT that Mary picked for herself.' Identificational/preverbal of a regular DP.

Equations

• Kiss1998.preverbal_hat = Kiss1998.mkIdentificational Kiss1998.ConstituentClass.regular True.intro

def Kiss1998.postverbal_hat : FocusConfig

Eq. (8b): Mari ki nézett magának EGY KALAPOT 'Mary picked for herself A HAT.' Information/postverbal of a regular DP — non-exhaustive.

Equations

• Kiss1998.postverbal_hat = Kiss1998.mkInformation Kiss1998.ConstituentClass.regular True.intro

def Kiss1998.starred_universal_identificational : FocusConfig

Eq. (17b — starred): *Mari minden kalapot nézett ki magának 'It was every hat that Mary picked for herself.' Universal quantifier in identificational focus position is ungrammatical (paper §3). Constructed directly to demonstrate the distributional restriction has bite.

Equations

• Kiss1998.starred_universal_identificational = { position := Kiss1998.Position.preverbal, focusType := Kiss1998.FocusType.identificational, cclass := Kiss1998.ConstituentClass.universal }

def Kiss1998.universal_information : FocusConfig

Eq. (19b): Minden kollégámat meg hívtam 'I invited EVERY COLLEAGUE OF MINE.' Universal quantifier as postverbal information focus — grammatical, demonstrating that minden is barred only from identificational position, not from focus altogether.

Equations

• Kiss1998.universal_information = Kiss1998.mkInformation Kiss1998.ConstituentClass.universal True.intro

Position determines focus type (paper §2)

Among licensed configurations, focusType factors through position. The same schema is instantiated for Hausa in HartmannZimmermann2007.lean (with cfg.strategy and pragType) and refuted there — a difference of verdict on one shared predicate.

def Kiss1998.typeOfPosition : Position → FocusType

The factor witnessing §2: focus type as a function of position.

Equations

• Kiss1998.typeOfPosition Kiss1998.Position.preverbal = Kiss1998.FocusType.identificational
• Kiss1998.typeOfPosition Kiss1998.Position.postverbal = Kiss1998.FocusType.information

theorem Kiss1998.focusType_eqOn_typeOfPosition : Set.EqOn FocusConfig.focusType (typeOfPosition ∘ FocusConfig.position) {c : FocusConfig | c.Licensed}

On licensed configurations the focus type is literally typeOfPosition of the position — the §2 claim in factored form.

theorem Kiss1998.position_determines_focusType : Function.FactorsThroughOn FocusConfig.focusType FocusConfig.position {c : FocusConfig | c.Licensed}

Position determines focus type on licensed configurations: Kiss's §2 structural claim, derived from the explicit factor.

theorem Kiss1998.preverbal_iff_exhaustive (c : FocusConfig) (h : c.Licensed) : c.position = Position.preverbal ↔ c.focusType.IsExhaustive

Position equivalence with exhaustivity: composition of the position-type and type-exhaustivity equivalences. The semantic payoff of Kiss's §2 structural distinction.

Distributional restrictions (paper §3, eq. 17)

theorem Kiss1998.starred_universal_identificational_not_licensed : ¬starred_universal_identificational.Licensed

Universal quantifiers cannot be identificational foci (17b): starred_universal_identificational fails licensing.

theorem Kiss1998.universal_information_licensed : universal_information.Licensed

Universal quantifiers can be information foci (19b): the class barred preverbally is admissible postverbally.

theorem Kiss1998.only_information_not_licensed : ¬{ position := Position.postverbal, focusType := FocusType.information, cclass := ConstituentClass.onlyPhrase }.Licensed

The csak X construction is obligatorily identificational (§3): the information-focus alternative is ill-licensed.

theorem Kiss1998.someIndef_neither_licensed : ¬{ position := Position.preverbal, focusType := FocusType.identificational, cclass := ConstituentClass.someIndef }.Licensed ∧ ¬{ position := Position.postverbal, focusType := FocusType.information, cclass := ConstituentClass.someIndef }.Licensed

Indefinite valami/valaki is barred from both focus types (17e).

Cell properties

theorem Kiss1998.preverbal_identificational_licensed : preverbal_identificational.Licensed

theorem Kiss1998.postverbal_information_licensed : postverbal_information.Licensed

theorem Kiss1998.minimal_pair_distinct_types : preverbal_hat.focusType ≠ postverbal_hat.focusType

The eq. (5a/5b) minimal pair: same constituent, different positions, different focus types — both licensed.

Exhaustive identification semantics (§2)

The hat/coat model of the paper's own test sentences ((8), (12)–(15)). Identificational focus is the prejacent exhaustified over the resolved alternatives — covert obligatory Semantics.Focus.onlyVia — while information focus is the bare prejacent. Szabolcsi's coordination test and Farkas's dialogue test come out as theorems, and position determines whether exhaustification applies: the like-for-like counterpart of HartmannZimmermann2007.exhAnswer_eq, where exhaustification is strategy-blind.

inductive Kiss1998.HatWorld : Type

Worlds tracking what Mary picked for herself.

• hatOnly : HatWorld
• coatOnly : HatWorld
• both : HatWorld
• neither : HatWorld

@[implicit_reducible]

instance Kiss1998.instDecidableEqHatWorld : DecidableEq HatWorld

Equations

• Kiss1998.instDecidableEqHatWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kiss1998.instReprHatWorld : Repr HatWorld

Equations

• Kiss1998.instReprHatWorld = { reprPrec := Kiss1998.instReprHatWorld.repr }

def Kiss1998.instReprHatWorld.repr : HatWorld → ℕ → Std.Format

Equations

• Kiss1998.instReprHatWorld.repr Kiss1998.HatWorld.hatOnly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiss1998.HatWorld.hatOnly")).group prec✝
• Kiss1998.instReprHatWorld.repr Kiss1998.HatWorld.coatOnly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiss1998.HatWorld.coatOnly")).group prec✝
• Kiss1998.instReprHatWorld.repr Kiss1998.HatWorld.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiss1998.HatWorld.both")).group prec✝
• Kiss1998.instReprHatWorld.repr Kiss1998.HatWorld.neither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiss1998.HatWorld.neither")).group prec✝

def Kiss1998.pickedHat : Set HatWorld

'Mary picked a hat' (at least).

Equations

• Kiss1998.pickedHat = {Kiss1998.HatWorld.hatOnly, Kiss1998.HatWorld.both}

def Kiss1998.pickedCoat : Set HatWorld

'Mary picked a coat' (at least).

Equations

• Kiss1998.pickedCoat = {Kiss1998.HatWorld.coatOnly, Kiss1998.HatWorld.both}

def Kiss1998.hatAlts : Semantics.Focus.Interpretation.PropFocusValue HatWorld

The resolved atomic alternatives for the picking scenario.

Equations

• Kiss1998.hatAlts = {Kiss1998.pickedHat, Kiss1998.pickedCoat}

def Kiss1998.identificational (p : Set HatWorld) : Set HatWorld

Identificational focus: the prejacent exhaustified over the resolved alternatives (§2's "exhaustive subset of the relevant set").

Equations

• Kiss1998.identificational p = p ∩ Semantics.Focus.onlyVia Kiss1998.hatAlts p

theorem Kiss1998.identificational_hat_eq : identificational pickedHat = {HatWorld.hatOnly}

The identificational meaning of (8a)/(12b) computes to picked-exactly-a-hat.

theorem Kiss1998.szabolcsi_test : identificational pickedHat ∩ (pickedHat ∩ pickedCoat) = ∅ ∧ pickedHat ∩ pickedCoat ⊆ pickedHat

Szabolcsi's coordination test ((12) vs (13)): the identificational a hat contradicts the hat-and-coat content, while the information-focus a hat is entailed by it.

theorem Kiss1998.farkas_test : HatWorld.both ∉ identificational pickedHat ∧ HatWorld.both ∈ pickedHat

Farkas's dialogue test ((15)): in the situation where Mary picked a coat too, the identificational claim is false (so B's "No, she picked a coat, too" is a coherent denial of exhaustivity), while the information-focus claim is true (so the denial is infelicitous).

def Kiss1998.semanticsOf : FocusType → Set HatWorld

The two focus types' denotations for the hat prejacent.

Equations

• Kiss1998.semanticsOf Kiss1998.FocusType.identificational = Kiss1998.identificational Kiss1998.pickedHat
• Kiss1998.semanticsOf Kiss1998.FocusType.information = Kiss1998.pickedHat

theorem Kiss1998.position_determines_exhaustification : semanticsOf (typeOfPosition Position.preverbal) = {HatWorld.hatOnly} ∧ semanticsOf (typeOfPosition Position.postverbal) = pickedHat

Position determines the semantics: the preverbal slot's meaning is exhaustified, the postverbal one's is plain — Kiss's §2 claim cashed out through the factor typeOfPosition. The Hausa counterpart (HartmannZimmermann2007.exhAnswer_eq) shows exhaustification strategy-blind: the two-verdict contrast at the level of one semantic operator.