Documentation

Linglib.Semantics.Quantification.Individual

Individuals #

This file is about the Montagovian individuals, the type ⟨1⟩ quantifiers NP.individual a of the properties of an entity, and the type shifts they fix. The individuals generate NP E under complete Boolean operations: every quantifier is the join of the quantifiers true of one of its properties alone, and the quantifier true of R alone, every R and no non-R, is a meet of individuals and their complements. A complete homomorphism out of NP E is therefore fixed by its values on the individuals. The individuals are exactly the quantifiers that commute with negation and with arbitrary conjunction, Keenan and Faltz's characterization of proper-noun denotations, and an existential is one exactly when its restrictor is a singleton.

Predicative content BE is the complete homomorphism sending each individual to its singleton, and the existential determiner GQ.some, Partee's A, is a section of it, so BE ∘ A is the identity. On the monotone quantifiers the two form a Galois coinsertion, and a quantifier survives the round trip A ∘ BE exactly when it is existential, as an individual is.

Main definitions #

Main statements #

References #

Individuals #

source
theorem Quantifier.NP.sInter_individual {E : Type u_1} (a : E) :
⋂₀ individual a = {a}

The sets of a principal ultrafilter intersect to the singleton of its generator.

source
@[simp]
theorem Quantifier.NP.individual_compl {E : Type u_1} (a : E) (P : E → Prop) :
individual a Pᶜ ↔ ¬individual a P
source
@[simp]
theorem Quantifier.NP.individual_sInf {E : Type u_1} (a : E) (S : Set (E → Prop)) :
individual a (sInf S) ↔ ∀ P ∈ S, individual a P

Generation by the individuals #

Every, some and no at a restrictor are the meet, the join and the meet of the complements of the individuals of the restrictor, and every quantifier is a join of meets of individuals and their complements.

source
theorem Quantifier.NP.every_eq_iInf_individual {E : Type u_1} (R : E → Prop) :
GQ.every R = ⨅ (x : E), ⨅ (_ : R x), individual x
source
theorem Quantifier.NP.some_eq_iSup_individual {E : Type u_1} (R : E → Prop) :
GQ.some R = ⨆ (x : E), ⨆ (_ : R x), individual x
source
theorem Quantifier.NP.no_eq_iInf_compl_individual {E : Type u_1} (R : E → Prop) :
GQ.no R = ⨅ (x : E), ⨅ (_ : R x), (individual x)ᶜ
source
theorem Quantifier.NP.every_inf_no_compl_apply {E : Type u_1} {R S : E → Prop} :
(GQ.every R ⊓ GQ.no Rᶜ) S ↔ S = R

Every R and no non-R is the quantifier true of R alone.

source
theorem Quantifier.NP.eq_iSup_every_inf_no {E : Type u_1} (Q : NP E) :
Q = ⨆ (R : E → Prop), ⨆ (_ : Q R), GQ.every R ⊓ GQ.no Rᶜ

Every quantifier is the join of the quantifiers true of one of its properties alone.

source
theorem Quantifier.NP.completeLatticeHom_ext {E : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra β] {f g : CompleteLatticeHom (NP E) β} (h : ∀ (x : E), f (individual x) = g (individual x)) :
f = g

Complete homomorphisms out of NP E that agree on the individuals are equal, the individuals being complete generators.

Predicative content and existential closure #

source
def Quantifier.NP.BE {E : Type u_1} :
CompleteLatticeHom (NP E) (E → Prop)

BE Q is the predicative content of the quantifier Q, BE(Q) = λx. Q(λy. y = x), which preserves arbitrary meets and joins.

Equations
Instances For
    source
    @[simp]
    theorem Quantifier.NP.BE_apply {E : Type u_1} (Q : NP E) (x : E) :
    BE Q x = Q (ident x)
    source
    @[simp]
    theorem Quantifier.NP.BE_individual {E : Type u_1} (j : E) :
    BE (individual j) = ident j

    BE ∘ individual = ident.

    source
    @[simp]
    theorem Quantifier.NP.some_ident {E : Type u_1} (j : E) :
    GQ.some (ident j) = individual j

    A ∘ ident = individual.

    source
    @[simp]
    theorem Quantifier.NP.BE_some {E : Type u_1} (P : E → Prop) :
    BE (GQ.some P) = P

    BE ∘ A is the identity: be a man is man.

    source
    theorem Quantifier.NP.some_injective {E : Type u_1} :
    Function.Injective GQ.some
    source
    theorem Quantifier.NP.some_eq_individual_iff {E : Type u_1} {N : E → Prop} {a : E} :
    GQ.some N = individual a ↔ N = ident a

    An existential is a Montagovian individual exactly when its restrictor is a singleton.

    source
    theorem Quantifier.NP.some_BE_eq_self_iff {E : Type u_1} {Q : NP E} :
    GQ.some (BE Q) = Q ↔ ∃ (P : E → Prop), GQ.some P = Q

    A quantifier survives the round trip through BE and A exactly when it is existential.

    The Galois coinsertion on monotone quantifiers #

    source
    theorem Quantifier.NP.individual_le_iff {E : Type u_1} {Q : NP E} (hQ : Monotone Q) {x : E} :
    individual x ≤ Q ↔ BE Q x

    A monotone quantifier lies above the lift of x exactly when it holds of x's singleton.

    source
    theorem Quantifier.NP.some_le_iff {E : Type u_1} {Q : NP E} (hQ : Monotone Q) {P : E → Prop} :
    GQ.some P ≤ Q ↔ P ≤ BE Q
    source
    def Quantifier.NP.gciSomeBE {E : Type u_1} :
    GaloisCoinsertion (fun (P : E → Prop) => { toFun := GQ.some P, monotone' := ⋯ }) fun (Q : (E → Prop) →o Prop) => BE ⇑Q

    On the monotone quantifiers GQ.some and BE form a Galois coinsertion.

    Equations
    Instances For

      Individuals as complete homomorphisms #

      Keenan and Faltz define a proper-noun denotation as a set of properties satisfying the Meets, Joins and Complements Conditions and prove that these are exactly the individuals generated by atoms; the Joins Condition follows from the other two. Read as scope, the Complements Condition says that the quantifier commutes with negation and the Meets Condition that it commutes with universal quantification, so the scopeless quantifiers are the Montagovian individuals.

      source
      theorem Quantifier.NP.exists_eq_individual_iff {E : Type u_1} {Q : NP E} :
      (∃ (a : E), Q = individual a) ↔ (∀ (P : E → Prop), Q Pᶜ ↔ ¬Q P) ∧ ∀ (S : Set (E → Prop)), Q (sInf S) ↔ ∀ P ∈ S, Q P

      The quantifiers that commute with negation and with arbitrary conjunction are the Montagovian individuals, [KF85]'s Theorem 9 for the algebra E → Prop.