Type ⟨1⟩ quantifiers

The API for Quantifier α, the denotation type of a quantified noun phrase. Existential closure A turns a property into a quantifier and predicative content BE turns one back; BE ∘ A is the identity, and on the upward-closed quantifiers that [BC81] take natural-language determiners to denote, the two form a GaloisCoinsertion. Sending a quantifier through BE and back preserves truth conditions exactly when it is a principal ultrafilter: a proper name survives the round trip, every student does not. Ty.det names the determiner type ⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩, and the shifts relating Quantifier to the other noun-phrase types are [Par87]'s, in Semantics.Composition.TypeShifting.

The continuation identification

These are rfl: the carrier definitionally coincides with the continuation monad at answer type Prop, first exploited for natural language by [Bar02a] (see Studies/Barker2002.lean).

theorem Quantification.quantifier_eq_cont {E : Type} : Quantifier E = Cont Prop E

The quantifier type is the continuation type: a quantifier is a computation handed its own scope.

theorem Quantification.individual_eq_pure {E : Type} (a : E) : individual a = pure a

Montague lift is the continuation monad's unit.

theorem Quantification.individual_eq_T {E : Type} (a : E) : individual a = Combinator.T a

Montague lift is combinatory logic's type-raising combinator T.

Predicative content and existential closure

def Quantification.BE {E : Type} (Q : Quantifier E) : E → Prop

Predicative content of a quantifier: BE(Q) = λx. Q(λy. y = x).

Equations

• Quantification.BE Q x = Q fun (y : E) => y = x

def Quantification.A {E : Type} (domain : List E) (P : E → Prop) : Quantifier E

Existential closure: A(P) = λQ. ∃x ∈ domain. P(x) ∧ Q(x).

Equations

• Quantification.A domain P Q = ∃ x ∈ domain, P x ∧ Q x

BE as a bounded-lattice homomorphism

theorem Quantification.BE_conj {E : Type} (Q₁ Q₂ : Quantifier E) : (BE fun (P : E → Prop) => Q₁ P ∧ Q₂ P) = fun (x : E) => BE Q₁ x ∧ BE Q₂ x

BE(Q₁ ∧ Q₂) = BE(Q₁) ∧ BE(Q₂)

theorem Quantification.BE_disj {E : Type} (Q₁ Q₂ : Quantifier E) : (BE fun (P : E → Prop) => Q₁ P ∨ Q₂ P) = fun (x : E) => BE Q₁ x ∨ BE Q₂ x

BE(Q₁ ∨ Q₂) = BE(Q₁) ∨ BE(Q₂)

theorem Quantification.BE_neg {E : Type} (Q : Quantifier E) : (BE fun (P : E → Prop) => ¬Q P) = fun (x : E) => ¬BE Q x

BE(¬Q) = ¬BE(Q)

def Quantification.BE_hom (E : Type) : BoundedLatticeHom (Quantifier E) (E → Prop)

BE preserves meets, joins, ⊤ and ⊥ ([Par87]).

Equations

• Quantification.BE_hom E = { toFun := Quantification.BE, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

Truth-conditional transparency of the round trip

A type-shift is truth-conditionally transparent when the shifted meaning produces the same sentential truth value as the original. For a quantifier Q, the round trip A(BE(Q)) preserves truth conditions exactly when Q is a principal ultrafilter — when Q = individual j for some entity j. Proper names, pronouns and definites shift transparently; every student shifts to some student, and a numeral to its lower-bounded reading. Where the round trip is not transparent, both meanings are live interpretive alternatives.

def Quantification.isPrincipalUltrafilter {E : Type} (domain : List E) (Q : Quantifier E) : Prop

A quantifier is a principal ultrafilter when it is some entity's Montagovian individual.

Equations

• Quantification.isPrincipalUltrafilter domain Q = ∃ j ∈ domain, Q = Quantification.individual j

theorem Quantification.roundtrip_preserves_principal {E : Type} (domain : List E) (j : E) (hj : j ∈ domain) (P : E → Prop) : A domain (BE (individual j)) P = individual j P

The round trip is the identity on principal ultrafilters: A(BE(individual j))(P) = individual j P.

theorem Quantification.BE_A_id {E : Type} (domain : List E) (P : E → Prop) (hcomplete : ∀ (x : E), x ∈ domain) : BE (A domain P) = P

BE ∘ A = id on properties ([Par87]): existential closure followed by predicative content recovers the original property, so A is a section of BE. Partee argues on this basis that A (with some) is the most natural determiner-type functor.

BE(A(P))(x) = A(P)(λy. y = x) = ∃z ∈ domain. P(z) ∧ z = x = P(x).

theorem Quantification.roundtrip_changes_nonprincipal : (Quantification.twoEvery✝ fun (x : Bool) => True) ∧ ¬A Quantification.twoDomain✝ (BE Quantification.twoEvery✝) fun (x : Bool) => True

For non-principal quantifiers the round trip changes truth conditions: every(⊤) is true but A(BE(every))(⊤) is not, since BE(every) asks which entity equals every entity and on a two-element domain none does.

Section and retraction

theorem Quantification.BE_leftInverse_A {E : Type} (domain : List E) (hcomplete : ∀ (x : E), x ∈ domain) : Function.LeftInverse BE (A domain)

BE is a left inverse of A.

theorem Quantification.BE_surjective {E : Type} (domain : List E) (hcomplete : ∀ (x : E), x ∈ domain) : Function.Surjective BE

BE is surjective: every property is the predicative content of some quantifier.

theorem Quantification.A_injective {E : Type} (domain : List E) (hcomplete : ∀ (x : E), x ∈ domain) : Function.Injective (A domain)

A is injective: distinct properties yield distinct quantifiers under existential closure — different common nouns mean different things as indefinites.

Galois coinsertion on monotone quantifiers

On the full Boolean algebra of quantifiers A ⊣ BE fails: for non-monotone Q such as λR. ¬R(a), the counit A(BE(Q)) ≤ Q does not hold. Restricted to the upward-closed quantifiers — [BC81]'s constraint on what natural language determiners denote — it does hold, because a singleton {x} ≤ R whenever R(x), and monotonicity lifts this to Q({x}) ≤ Q(R). So the monotonicity constraint is exactly the condition making A and BE an adjunction.

def Quantification.UpwardGQ (E : Type) : Type

Upward-closed (monotone) quantifiers: Q(P) and P ≤ P' imply Q(P').

Equations

• Quantification.UpwardGQ E = { Q : Quantification.Quantifier E // Monotone Q }

@[instance_reducible]

instance Quantification.instPartialOrderUpwardGQ {E : Type} : PartialOrder (UpwardGQ E)

Equations

• Quantification.instPartialOrderUpwardGQ = Subtype.partialOrder fun (Q : Quantification.Quantifier E) => Monotone Q

theorem Quantification.A_monotone_gq {E : Type} (domain : List E) (P : E → Prop) : Monotone (A domain P)

A(P) is always upward-closed.

def Quantification.A_up {E : Type} (domain : List E) (P : E → Prop) : UpwardGQ E

A into the UpwardGQ subtype.

Equations

• Quantification.A_up domain P = ⟨Quantification.A domain P, ⋯⟩

def Quantification.BE_up {E : Type} (Q : UpwardGQ E) : E → Prop

BE out of the UpwardGQ subtype.

Equations

• Quantification.BE_up Q = Quantification.BE ↑Q

theorem Quantification.A_up_mono {E : Type} (domain : List E) : Monotone (A_up domain)

A is monotone as a map from properties to quantifiers.

theorem Quantification.BE_up_mono {E : Type} : Monotone BE_up

BE is monotone on UpwardGQ.

theorem Quantification.A_BE_le_of_mono {E : Type} (domain : List E) (Q : UpwardGQ E) : A_up domain (BE_up Q) ≤ Q

Counit inequality: A(BE(Q)) ≤ Q for upward-closed Q. This is what fails for non-monotone Q such as λR. ¬R(a), where Q({a}) is false but Q(∅) is true.

def Quantification.galoisCoinsertion {E : Type} (domain : List E) (hcomplete : ∀ (x : E), x ∈ domain) : GaloisCoinsertion (A_up domain) BE_up

A and BE form a GaloisCoinsertion on the upward-closed quantifiers: BE ∘ A = id on properties, and A(BE(Q)) ≤ Q for monotone Q.

Equations

• Quantification.galoisCoinsertion domain hcomplete = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem Quantification.gc_A_BE {E : Type} (domain : List E) (hcomplete : ∀ (x : E), x ∈ domain) : GaloisConnection (A_up domain) BE_up

The Galois connection: A(P) ≤ Q ↔ P ≤ BE(Q) for monotone Q.

Semantic-type alias

def Quantification.Quantifier.Ty.det : Intensional.Ty

The determiner type ⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩.

Equations

• Quantification.Quantifier.Ty.det = ((Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ Intensional.Ty.t)

theorem Quantification.Quantifier.A_eq_some_sem (E : Type) (domain : List E) (hComplete : ∀ (x : E), x ∈ domain) : A domain = some_sem

Existential closure over a complete finite domain is ⟦some⟧: both compute λR.λS. ∃x. R(x) ∧ S(x).