Documentation

Studies.Kiss1998

É. Kiss (1998): Identificational Focus versus Information Focus #

This file formalizes [EK98]'s distinction between identificational focus, which in Hungarian moves to the immediately preverbal position and expresses exhaustive identification, and information focus, which stays in situ after the verb and merely marks its content as new. Identificational focus exhaustifies the prejacent over the alternatives evoked by the contextually given set, the Exhaustification.exh of [Chi06], and information focus asserts the bare prejacent. The paper's characterisation of exhaustive identification, that the focus "is identified as the exhaustive subset of this set for which the predicate phrase actually holds", is the theorem exh_Ici, and the coordination test and the dialogue test by which the paper diagnoses exhaustivity come out as theorems on the hat-and-coat scenario of its examples (szabolcsi_test, farkas_test). The distributional restrictions of §3 follow from the same semantics, exhaustive identification being exclusion by identification. A universal quantifier identifies without excluding (exh_Ici_restrictor), a some-phrase excludes without identifying (exh_nonempty_eq_empty), and an additive also or even phrase contradicts its own presupposition unless the given set has been narrowed by a prior identification, the paper's (18) (disjoint_exh_additive, additive_exh_of_notMem).

Implementation notes #

TODO #

References #

def Kiss1998.alternatives {ι : Type u_1} (A : Set ι) :
Set (Set (Set ι))

The alternatives evoked by a focus over the given set A, one for each given element, saying that the predicate phrase holds of it.

Equations
Instances For
    theorem Kiss1998.alternatives_eq {ι : Type u_1} (A : Set ι) (a : ι) :
    alternatives A = ((fun (i : ι) => Set.Ici {i}) <$> { ordinary := a, alternatives := A }).alternatives

    Hamblin composition of the predicate phrase with a focused argument ranging over the given set evokes exactly these alternatives.

    Exhaustive identification (§2) #

    theorem Kiss1998.exh_Ici {ι : Type u_1} (A s : Set ι) :
    Exhaustification.exh (alternatives A) (Set.Ici s) = Set.Icc s (s ∪ Aᶜ)

    Exhaustively identifying the group s over the given set A asserts that the predicate holds of s and of no other given element, the paper's (9).

    theorem Kiss1998.exh_Ici_univ {ι : Type u_1} (s : Set ι) :
    Exhaustification.exh (alternatives Set.univ) (Set.Ici s) = {s}

    Over the whole domain, exhaustively identifying s asserts that the predicate holds of s and of nothing else.

    theorem Kiss1998.szabolcsi_test {ι : Type u_1} {A : Set ι} {a b : ι} (hb : b ∈ A) (hab : a ≠ b) :
    Disjoint (Exhaustification.exh (alternatives A) (Set.Ici {a, b})) (Exhaustification.exh (alternatives A) (Set.Ici {a})) ∧ Set.Ici {a, b} ⊆ Set.Ici {a}

    Szabolcsi's coordination test, (12) against (13). The identificational a hat contradicts the identificational a hat and a coat, while the information-focus a hat follows from the information-focus a hat and a coat.

    theorem Kiss1998.farkas_test {ι : Type u_1} {A : Set ι} {a b : ι} (hb : b ∈ A) (hab : a ≠ b) :
    {a, b} ∉ Exhaustification.exh (alternatives A) (Set.Ici {a}) ∧ {a, b} ∈ Set.Ici {a}

    Farkas's dialogue test, (15). Where Mary picked a coat too, the identificational claim is false, so No, she picked a coat, too denies its exhaustivity, while the information-focus claim is true and the denial is out of place.

    theorem Kiss1998.not_monotone_exh {ι : Type u_1} {A : Set ι} {a b : ι} (hb : b ∈ A) (hab : a ≠ b) :

    Exhaustive identification is not monotone in the prejacent, which is what the coordination test detects.

    Distributional restrictions (§3) #

    Exhaustive identification is exclusion by identification. An identificational focus names the given elements the predicate holds of and excludes the rest, and the constituents barred from the identificational position, (17b–e), are those for which one half fails.

    theorem Kiss1998.exh_Ici_restrictor {ι : Type u_1} (A : Set ι) :
    Exhaustification.exh (alternatives A) (Set.Ici A) = Set.Ici A

    A universal quantifier identifies without excluding (17b), since exhaustifying every hat over its restrictor is vacuous.

    theorem Kiss1998.exh_nonempty_eq_empty {ι : Type u_1} {A : Set ι} (hA : A.Nontrivial) :
    Exhaustification.exh (alternatives A) {w : Set ι | (w ∩ A).Nonempty} = ∅

    A some-phrase cannot be exhaustively identified (17e), since exhaustifying something over a given set with two elements is contradictory.

    def Kiss1998.additive {ι : Type u_1} (A : Set ι) (a : ι) :
    Set (Set ι)

    The presupposition of the additive also a and even a, that the predicate holds of some other given element.

    Equations
    Instances For
      theorem Kiss1998.disjoint_exh_additive {ι : Type u_1} (A : Set ι) (a : ι) :
      Disjoint (Exhaustification.exh (alternatives A) (Set.Ici {a})) (additive A a)

      An additive phrase identifies without excluding (17c, 17d), since its presupposition contradicts the exhaustification of its prejacent.

      theorem Kiss1998.additive_exh_of_notMem {ι : Type u_1} {A : Set ι} {a b : ι} (hb : b ∉ A) (hab : b ≠ a) :
      {a, b} ∈ Exhaustification.exh (alternatives A) (Set.Ici {a}) ∩ additive (insert b A) a

      In the cleft also-phrase of (18), a prior identification has removed b from the given set, so it was also a identifies a in addition, excluding everybody but a and b.