Documentation

Linglib.Studies.Owusu2022

[Owu22]: Cross-Categorial Definiteness/Familiarity #

[Owu22] Ch 3 analyses the Akan (Kwa, Niger-Congo) indefinite bí as an unambiguous choice function (after [Kra98b]) whose situation pronoun ties the CF and the NP to a single index — entry (67): ⟦bí⟧ = λs.λP : CH(f_s). f_s(P(s)). The substrate type is SkolemCF S E := S → CF E (ChoiceFunction.lean). The nó chapters and the rival analyses in [Bom18], [Sch13], [AM13b] are left for future Studies files.

Main declarations #

Implementation notes #

Wide scope under negation (data §3.2.5 exx. (21)–(22); analysis §3.3): the CF variable is contextually given (speaker-anchored), and negation binds no situation variable, so the CF's referent is fixed before negation applies and ¬ > ∃ is underivable. The general lemma states what the ∃ > ¬ reading entails; the two-person model witnesses it on a model falsifying ¬ > ∃ — the case where the readings come apart. The operator-side derivation — extensional operators provably neutralize the situation pronoun's free/bound distinction, situation quantifiers provably separate it — lives in the substrate (Semantics/Quantification/ChoiceFunction: bound_free_collapse, bound_free_diverge_box). The narrow-scope readings in conditional antecedents (situation pronoun bound locally) and the opaque readings under intensional verbs (a skolem world index, §3.3.3, following Mirrazi's world-skolemized CFs — a 2019 ms., published as [Mir24]) need binding machinery beyond the fixed-situation fragment formalized here, as do the functional readings bound by individual quantifiers (the biara subject/object asymmetry via weak crossover on the individual skolem index).

Todo #

source
def Owusu2022.skolemDenot {S : Type u_1} {E : Type u_2} (f : Quantification.ChoiceFunction.SkolemCF S E) (s₀ : S) :
Akan.Determiners.Indefinite → Option (Intensional.Intension S (E → Prop) → E)

[Owu22]'s denotation table for the Akan indefinite contrast: bí applies a skolemized choice function to an intensional restrictor at the situation of its argument (entry (67); the same index feeds the CF and the restrictor — SkolemCF.applyIntension). The .bare cell is none — not CF-analyzed here, not undefined: bare NPs receive kind/indefinite readings (App. A) outside the CF analysis.

Equations
Instances For
    source
    @[simp]
    theorem Owusu2022.skolemDenot_bi {S : Type u_1} {E : Type u_2} (f : Quantification.ChoiceFunction.SkolemCF S E) (s₀ : S) :
    skolemDenot f s₀ Akan.Determiners.Indefinite.bi = some (f.applyIntension s₀)
    source
    @[simp]
    theorem Owusu2022.skolemDenot_bare {S : Type u_1} {E : Type u_2} (f : Quantification.ChoiceFunction.SkolemCF S E) (s₀ : S) :
    skolemDenot f s₀ Akan.Determiners.Indefinite.bare = none
    source
    theorem Owusu2022.bi_wide_scope_specific {S : Type u_1} {E : Type u_2} {f : Quantification.ChoiceFunction.SkolemCF S E} {s₀ : S} (hf : (f s₀).isCorrect) {P : Intensional.Intension S (E → Prop)} {VP : E → Prop} (hN : ∃ (x : E), P s₀ x) (d : Intensional.Intension S (E → Prop) → E) :
    d ∈ skolemDenot f s₀ Akan.Determiners.Indefinite.bi → ¬VP (d P) → ∃ (x : E), P s₀ x ∧ ¬VP x

    [Owu22]'s wide-scope-under-negation prediction (§3.2.5, §3.3) for the .bi denotation: the ∃ > ¬ reading is specific — if the CF-selected member of the (at s₀) non-empty restrictor fails VP, some restrictor member fails VP, witnessed by the CF's choice. It does not entail the narrow-scope ¬ > ∃ (see the model below).

    source
    theorem Owusu2022.tying_contentful :
    ∃ (S : Type) (E : Type) (f : Quantification.ChoiceFunction.SkolemCF S E) (P : Intensional.Intension S (E → Prop)) (s : S) (s' : S), f.applyIntension s P ≠ f s (P s') ∧ f.applyIntension s P ≠ f s' (P s)

    Entry (67)'s same-index tying is contentful in both coordinates: a single CF/restrictor pair where the tied denotation f_s(P(s)) differs from the restrictor-shifted variant f_s(P(s')) and from the CF-index-shifted variant f_s'(P(s)).

    A two-person model of ex. (21) #

    Onipa bí a-n-to dwom 'person INDEF PERF-NEG-sing song' = 'A certain person didn't sing' ([Owu22] §3.2.5 ex. (21), judged Indefinite ≫ Neg only). Two people — Kofi and Ama, common Twi day-names — exhaust the domain onipa 'person'; Kofi sang, Ama did not.

    source
    inductive Owusu2022.Onipa :
    Type

    onipa 'person' (Akan/Twi). The atomic restrictor type.

    Instances For
      source
      def Owusu2022.ToDwom :
      Onipa → Prop

      to dwom 'sing (a) song': Kofi sang, Ama did not.

      Equations
      Instances For
        source
        noncomputable def Owusu2022.preferAma :
        Quantification.ChoiceFunction.SkolemCF Unit Onipa

        A correct SkolemCF over the trivial situation Unit that selects Ama whenever the restrictor allows it, else Kofi.

        Equations
        Instances For
          source
          theorem Owusu2022.preferAma_correct :
          preferAma.isCorrect
          source
          theorem Owusu2022.bi_wide_scope_witnessed (d : Intensional.Intension Unit (Onipa → Prop) → Onipa) :
          d ∈ skolemDenot preferAma () Akan.Determiners.Indefinite.bi → ¬ToDwom (d (Intensional.Intension.rigid fun (x : Onipa) => True))

          The wide-scope (∃ > ¬) reading of ex. (21) is witnessed: the .bi denotation picks Ama from the (rigid, on this one-situation model) onipa domain, and she did not sing.

          source
          theorem Owusu2022.someone_sang :
          ∃ (x : Onipa), ToDwom x

          The narrow-scope (¬ > ∃) reading of ex. (21) — 'no person sang' — is false on this model: Kofi sang.