Docs / Semantics / Genericity / MeaningPreservation

Meaning Preservation

import Linglib.Semantics.Genericity.MeaningPreservation

This file defines Meaning Preservation, the ranking of covert type shifts that decides which of the shifts available to a bare nominal it takes. Chierchia restricts covert type shifting in two ways: the Blocking Principle bars a shift that a determiner of the language lexicalizes, and Meaning Preservation ranks the shifts, so that a bare nominal takes the highest-ranked of those available to it. Both rankings in the literature have two tiers, and a two-tier ranking is the predicate of its upper tier, Prop ordered by implication. A shift applies when it is MaximalFor the ranking among the available shifts, that is, when it is available and in the upper tier unless no available shift is.

Chierchia ranks ∩ alone above ι and ∃, (39b) in Dayal's rendering, so his ranking is (· = .down). Dayal revises it to {∩, ι} > ∃, (39c), on Chierchia's own rationale that ∩ is preferred because it changes the type without introducing quantificational force, which holds of ι as well, so hers is (· ≠ .exists). The two rankings choose alike wherever no definite shift is available, as in a language whose definite article blocks ι and ι^x, and part ways where ι is available: under Dayal's ranking ι applies whenever it is unblocked, under Chierchia's only where ∩ is undefined.

Main definitions

Determiner.Inventory.Available: the covert shifts available to a bare nominal, those defined for it and not blocked.

Main results

CovertShift.maximalFor_eq_down_iff, CovertShift.maximalFor_ne_exists_iff: which available shifts each ranking selects.
CovertShift.maximalFor_available_ne_exists_down, …_iota, …_exists: under Dayal's ranking ∩ and ι apply wherever available and ∃ only as a last resort.
CovertShift.maximalFor_available_eq_down_down, …_iota, …_exists: under Chierchia's ranking ι and ∃ apply only where ∩ is undefined.
CovertShift.maximalFor_available_eq_down_iff_ne_exists: the rankings agree where no definite shift is available.

Implementation notes

ι^x, the anaphoric definite of Jenks, postdates both rankings, and Moroney is the first to make it a covert shift. It introduces no quantificational force, so Dayal's ranking puts it with ∩ and ι, and Chierchia's with ι.

References

Chierchia 1998, Reference to Kinds across Language formalized
Dayal 2004, Number Marking and (In)definiteness in Kind Terms formalized
Jenks 2018, Articulated Definiteness without Articles formalized
Moroney 2021, Definiteness and quantification: Evidence from Shan formalized

Declarations

A covert shift is available to a bare nominal of number num in a language with the determiners ds when it is defined for the nominal, ∩ only where down holds (for Chierchia's ∩, Kind.down P ∈ K), and no determiner blocks it for that number. ∩ is undefined for a singular count noun and for a property anchored to particular entities such as parts of this machine (Dayal 2004's fn. 1).

def Determiner.Inventory.Available L61–67

(ds : Inventory) (num : Number) (down : Prop) (τ : Genericity.CovertShift) :

Prop

ds.Available num down τ = ((τ = Genericity.CovertShift.down → down) ∧ ¬ds.Blocks num τ)

Used by Determiner.Inventory.instDecidablePredCovertShiftAvailableOfDecidable, Determiner.Inventory.available_iff_of_ne_down, Genericity.CovertShift.maximalFor_available_ne_exists_down, Genericity.CovertShift.maximalFor_available_ne_exists_iota, Genericity.CovertShift.maximalFor_available_ne_exists_exists, Genericity.CovertShift.maximalFor_available_eq_down_down, Genericity.CovertShift.maximalFor_available_eq_down_iota, Genericity.CovertShift.maximalFor_available_eq_down_exists, Genericity.CovertShift.maximalFor_available_eq_down_iff_ne_exists

Used in Dayal2004, Moroney2021

L69–71

L75–77

Under Chierchia's ranking an available shift applies when it is ∩ or ∩ is unavailable.

theorem Genericity.CovertShift.maximalFor_eq_down_iff L90–95

{A : CovertShift → Prop} {τ : CovertShift} :

MaximalFor A (fun (x : CovertShift) => x = down) τ ↔ A τ ∧ (τ = down ∨ ¬A down)

Under Dayal's ranking an available shift applies when it is not ∃ or only ∃ is available.

theorem Genericity.CovertShift.maximalFor_ne_exists_iff L97–100

{A : CovertShift → Prop} {τ : CovertShift} :

MaximalFor A (fun (x : CovertShift) => x ≠ «exists») τ ↔ A τ ∧ (τ ≠ «exists» ∨ ∀ (σ : CovertShift), A σ → σ = «exists»)

L102–103

L105–106

Under Dayal's ranking ∩ applies wherever it is defined, since no determiner blocks it.

@[simp] theorem Genericity.CovertShift.maximalFor_available_ne_exists_down L112–115

{ds : Determiner.Inventory} {num : Number} {down : Prop} :

MaximalFor (ds.Available num down) (fun (x : CovertShift) => x ≠ «exists») CovertShift.down ↔ down

Built from

L117–119

L121–130

Under Chierchia's ranking, too, ∩ applies wherever it is defined.

@[simp] theorem Genericity.CovertShift.maximalFor_available_eq_down_down L132–135

{ds : Determiner.Inventory} {num : Number} {down : Prop} :

MaximalFor (ds.Available num down) (fun (x : CovertShift) => x = CovertShift.down) CovertShift.down ↔ down

Built from

L137–139

L141–143

Where the determiners block ι and ι^x, as a definite article used anaphorically does, the two rankings select the same shifts.

theorem Genericity.CovertShift.maximalFor_available_eq_down_iff_ne_exists L145–154

{τ : CovertShift} {ds : Determiner.Inventory} {num : Number} {down : Prop} (hι : ds.Blocks num iota) (hx : ds.Blocks num iotaAnaphoric) :

MaximalFor (ds.Available num down) (fun (x : CovertShift) => x = CovertShift.down) τ ↔ MaximalFor (ds.Available num down) (fun (x : CovertShift) => x ≠ «exists») τ

Built from