Keenan and Stavi (1986): A Semantic Characterization of Natural Language Determiners

This file formalizes Keenan and Stavi's Conservativity Theorem: the possible determiner denotations, the Boolean closure of the denotations of a few simple determiners, are exactly the conservative functions, those with f R T ↔ f R (R ⊓ T). The generators are the Appendix's two individual-anchored determiners Sₐ and Eₐ, John's one or more and John's zero or more when a is all John possesses, here derived as restrictions of some and every by the singleton property of a (someOf, allOf); every conservative function is the join of the atoms atom p q at the pairs where it holds, the atoms of the algebra are exactly these (isAtom_iff), each atom is a meet of generators and their complements, and so the Boolean subalgebra the generators generate is the conservative algebra (closure_generators). The algebra is complete and atomic (the instance is in Quantification/Lattice.lean), so it is isomorphic to the power set of its atoms; sorting the individuals into three cells counts the atoms, and with n individuals there are 2 ^ 3 ^ n conservative functions among the 2 ^ 2 ^ 2n functions from properties to sets of properties (card_consGQ, card_gq, PROP 4), 512 among 65,536 for two individuals.

Section 3.3 characterizes the determiners of existential-there sentences as the existential functions, f R T ↔ f (R ⊓ T) ⊤: at least n is one, every and the n are not, and the class is closed under the Boolean operations (PROP 13). Section 3.4 isolates the cardinal functions, deciding by the number of individuals in restrictor and scope: they are closed under the Boolean operations and properly included in the existential functions (PROP 14), which are in turn isomorphic as a Boolean algebra to the type ⟨1⟩ quantifiers through f ↦ f(1) (PROP 15, existentialOrderIso), so number 2 ^ 2 ^ n; the cardinal functions are the sets of cardinalities up to n (cardinalOrderIso), so number 2 ^ (n + 1), and no ... but John is existential without being cardinal. Section 3.5 defines the logical determiners as the permutation-invariant conservative functions (114); they depend only on the sizes of the restrictor and of its meet with the scope, form the algebra of sets of nested pairs of cardinalities (logicalOrderIso), and number 2 ^ ((n + 1)(n + 2)/2) (PROP 19), 64 among the 512 conservative functions on two individuals. Footnote 10's characterization closes the circle: on a finite universe the cardinal functions are exactly the existential logical ones (cardinalSubalgebra_eq_inf).

Implementation notes

Conservativity, the existential property and quantity invariance are the substrate's Conservative, Existential and QuantityInvariant, the conservative algebra is ConsGQ with its CompleteAtomicBooleanAlgebra instance, and the counts are Nat.cards over a Fintype universe derived from mathlib's representation theorem CompleteAtomicBooleanAlgebra.toSetOfIsAtom. Cardinal is stated with Nat.card, which is by definition the Set.ncard the counting quantifiers count with. Canonical witnesses of each size are initial segments of a fixed enumeration (segment), which nest, unlike arbitrarily chosen subsets. BooleanSubalgebra.closure is finitary, so closure_generators carries [Finite α]; the paper closes under arbitrary meets and joins, and on an infinite universe the finitary closure is strictly smaller than the conservative algebra.

TODO

• Footnote 10(b): on an infinite universe CARD ⊊ E-Det ⊓ LOG, witnessed by the paper's f₀.
• The (In)effability Theorems of Section 3.6, which quantify over the English determiner expressions.

References

• [KS86]

The Conservativity Theorem (Section 2.5 and the Appendix)

def KeenanStavi1986.someOf {α : Type u_1} (a : α) : Quantifier.GQ α

Sₐ restricts some by the singleton property of a; it is the Appendix's denotation of John's one or more when a is all John possesses.

Equations

• KeenanStavi1986.someOf a = Quantifier.GQ.some.adjRestrict (Quantifier.NP.ident a)

@[simp]

theorem KeenanStavi1986.someOf_apply {α : Type u_1} (a : α) (R T : α → Prop) : someOf a R T ↔ R a ∧ T a

def KeenanStavi1986.allOf {α : Type u_1} (a : α) : Quantifier.GQ α

Eₐ restricts every by the singleton property of a; it is the Appendix's denotation of John's zero or more.

Equations

• KeenanStavi1986.allOf a = Quantifier.GQ.every.adjRestrict (Quantifier.NP.ident a)

@[simp]

theorem KeenanStavi1986.allOf_apply {α : Type u_1} (a : α) (R T : α → Prop) : allOf a R T ↔ R a → T a

theorem KeenanStavi1986.conservative_someOf {α : Type u_1} (a : α) : (someOf a).Conservative

theorem KeenanStavi1986.conservative_allOf {α : Type u_1} (a : α) : (allOf a).Conservative

theorem KeenanStavi1986.existential_someOf {α : Type u_1} (a : α) : (someOf a).Existential

The generators are themselves existential, an instance of PROP 16.

def KeenanStavi1986.generators (α : Type u_2) : Set (Quantifier.GQ α)

The generators of the conservative algebra are the Sₐ and Eₐ for every individual.

Equations

• KeenanStavi1986.generators α = Set.range KeenanStavi1986.someOf ∪ Set.range KeenanStavi1986.allOf

theorem KeenanStavi1986.conservative_of_mem_generators {α : Type u_1} {q : Quantifier.GQ α} (hq : q ∈ generators α) : q.Conservative

Every generator is conservative, the base case of PROP 1.

def KeenanStavi1986.atom {α : Type u_1} (p q : α → Prop) : Quantifier.GQ α

The Appendix's atom f_{pq} of the conservative algebra holds at the restrictor p and exactly the scopes meeting p in q.

Equations

• KeenanStavi1986.atom p q R T = (R = p ∧ R ⊓ T = q)

theorem KeenanStavi1986.conservative_atom {α : Type u_1} (p q : α → Prop) : (atom p q).Conservative

theorem KeenanStavi1986.atom_le_iff {α : Type u_1} {f : Quantifier.GQ α} (hf : f.Conservative) {p q : α → Prop} (h : q ≤ p) : atom p q ≤ f ↔ f p q

atom p q lies below a conservative f exactly when f holds at (p, q).

theorem KeenanStavi1986.isAtom_atom {α : Type u_1} {p q : α → Prop} (h : q ≤ p) : IsAtom ⟨atom p q, ⋯⟩

Each atom p q with q ≤ p is an atom of the conservative algebra; isAtom_iff adds the converse.

theorem KeenanStavi1986.isAtom_iff {α : Type u_1} {f : ↥(Quantifier.GQ.ConsGQ α)} : IsAtom f ↔ ∃ (p : α → Prop), ∃ q ≤ p, ↑f = atom p q

The atoms of the conservative algebra are exactly the atom p q with q ≤ p (the Appendix).

theorem KeenanStavi1986.eq_iSup_atom {α : Type u_1} {f : Quantifier.GQ α} (hf : f.Conservative) : f = ⨆ pq ∈ {pq : (α → Prop) × (α → Prop) | f pq.1 pq.2}, atom pq.1 pq.2

Every conservative function is the join of the atoms at the pairs where it holds, so the conservative algebra is atomistic; this is the indexed form the Appendix uses.

theorem KeenanStavi1986.atom_eq_iInf {α : Type u_1} (p q : α → Prop) : atom p q = ((⨅ a ∈ {a : α | q a}, someOf a) ⊓ ⨅ a ∈ {a : α | p a ∧ ¬q a}, (someOf a)ᶜ ⊓ (allOf a)ᶜ) ⊓ ⨅ a ∈ {a : α | ¬p a}, (someOf a)ᶜ ⊓ allOf a

The Appendix decomposes an atom into generators, meeting Sₐ over the individuals in q, the complements of Sₐ and Eₐ over those in p but not in q, and the complement of Sₐ with Eₐ over those outside p.

theorem KeenanStavi1986.atom_mem_closure {α : Type u_1} [Finite α] (p q : α → Prop) : atom p q ∈ BooleanSubalgebra.closure (generators α)

theorem KeenanStavi1986.closure_generators {α : Type u_1} [Finite α] : BooleanSubalgebra.closure (generators α) = Quantifier.GQ.conservativeSubalgebra

The Conservativity Theorem says that the Boolean algebra generated by the Sₐ and Eₐ is the algebra of conservative functions.

Counting the conservative functions (Section 2.7 and the Appendix)

@[reducible, inline]

abbrev KeenanStavi1986.Nested (α : Type u_2) : Type u_2

The atoms are indexed by the restrictor–scope pairs with the scope inside the restrictor.

Equations

• KeenanStavi1986.Nested α = { pq : (α → Prop) × (α → Prop) // pq.2 ≤ pq.1 }

theorem KeenanStavi1986.atom_injective {α : Type u_1} : Function.Injective fun (pq : Nested α) => atom (↑pq).1 (↑pq).2

Distinct nested pairs give distinct atoms.

noncomputable def KeenanStavi1986.atomEquiv {α : Type u_1} : Nested α ≃ { f : ↥(Quantifier.GQ.ConsGQ α) // IsAtom f }

The paper's index pairs are exactly mathlib's atoms of the conservative algebra.

Equations

• KeenanStavi1986.atomEquiv = Equiv.ofBijective (fun (pq : KeenanStavi1986.Nested α) => ⟨⟨KeenanStavi1986.atom (↑pq).1 (↑pq).2, ⋯⟩, ⋯⟩) ⋯

noncomputable def KeenanStavi1986.nestedEquivFin3 {α : Type u_1} : Nested α ≃ (α → Fin 3)

A pair q ≤ p sorts each individual into one of three cells, in q, in p but not q, or outside p, and any sorting arises (the Appendix's coding g_pq).

Equations

• One or more equations did not get rendered due to their size.

theorem KeenanStavi1986.card_nested {α : Type u_1} [Fintype α] : Nat.card (Nested α) = 3 ^ Fintype.card α

theorem KeenanStavi1986.card_isAtom {α : Type u_1} [Fintype α] : Nat.card { f : ↥(Quantifier.GQ.ConsGQ α) // IsAtom f } = 3 ^ Fintype.card α

The conservative algebra has 3 ^ n atoms, three cells per individual.

theorem KeenanStavi1986.card_consGQ {α : Type u_1} [Fintype α] : Nat.card ↥(Quantifier.GQ.ConsGQ α) = 2 ^ 3 ^ Fintype.card α

With n individuals there are 2 ^ 3 ^ n conservative functions, through the power set of the atoms (PROP 4).

theorem KeenanStavi1986.mk_consGQ {α : Type u_1} : Cardinal.mk ↥(Quantifier.GQ.ConsGQ α) = 2 ^ 3 ^ Cardinal.mk α

PROP 4 in its cardinal-valued form, covering the infinite universes the paper allows.

theorem KeenanStavi1986.card_gq {α : Type u_1} [Fintype α] : Nat.card (Quantifier.GQ α) = 2 ^ 2 ^ (2 * Fintype.card α)

Among 2 ^ 2 ^ 2n functions from properties to sets of properties (PROP 4).

Canonical witnesses of each size

Initial segments of a fixed enumeration of the universe, nested by construction, standing in for the paper's freely chosen sets of k individuals.

def KeenanStavi1986.segment {α : Type u_1} [Fintype α] (k : ℕ) : α → Prop

segment k holds of the first k individuals under a fixed enumeration of the universe.

Equations

• KeenanStavi1986.segment k x = (↑((Fintype.equivFin α) x) < k)

theorem KeenanStavi1986.segment_mono {α : Type u_1} [Fintype α] {k m : ℕ} (h : k ≤ m) : segment k ≤ segment m

theorem KeenanStavi1986.card_segment {α : Type u_1} [Fintype α] {k : ℕ} (hk : k ≤ Fintype.card α) : Nat.card { x : α // segment k x } = k

theorem KeenanStavi1986.card_segment_inter {α : Type u_1} [Fintype α] {m k : ℕ} (h : m ≤ k) (hm : m ≤ Fintype.card α) : Nat.card { x : α // segment k x ∧ segment m x } = m

theorem KeenanStavi1986.card_subtype_le_card {α : Type u_1} [Fintype α] (P : α → Prop) : Nat.card { x : α // P x } ≤ Fintype.card α

A subtype of a finite carrier has at most Fintype.card α elements.

theorem KeenanStavi1986.card_inter_le_card_left {α : Type u_1} [Fintype α] (R T : α → Prop) : Nat.card { x : α // R x ∧ T x } ≤ Nat.card { x : α // R x }

The meet cell is no larger than the restrictor cell.

Existential determiners (Section 3.3)

def KeenanStavi1986.existentialSubalgebra {α : Type u_1} : BooleanSubalgebra (Quantifier.GQ α)

The existential functions are closed under the Boolean operations (PROP 13).

Equations

• KeenanStavi1986.existentialSubalgebra = { carrier := {f : Quantifier.GQ α | f.Existential}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem KeenanStavi1986.mem_existentialSubalgebra {α : Type u_1} {f : Quantifier.GQ α} : f ∈ existentialSubalgebra ↔ f.Existential

theorem KeenanStavi1986.existential_iSup {α : Type u_1} {ι : Sort u_2} {f : ι → Quantifier.GQ α} (hf : ∀ (i : ι), (f i).Existential) : (⨆ (i : ι), f i).Existential

An indexed join of existential functions is existential (PROP 13(b) in its infinitary form).

theorem KeenanStavi1986.existential_iInf {α : Type u_1} {ι : Sort u_2} {f : ι → Quantifier.GQ α} (hf : ∀ (i : ι), (f i).Existential) : (⨅ (i : ι), f i).Existential

An indexed meet of existential functions is existential (PROP 13(b) in its infinitary form).

theorem KeenanStavi1986.existentialSubalgebra_le {α : Type u_1} : existentialSubalgebra ≤ Quantifier.GQ.conservativeSubalgebra

Existential functions are conservative, so E-Det lies in DDet.

theorem KeenanStavi1986.existential_atLeast {α : Type u_1} (n : ℕ) : (Quantifier.GQ.atLeast n).Existential

At least n is existential ((99)–(100)).

theorem KeenanStavi1986.not_existential_every {α : Type u_1} [Nonempty α] : ¬Quantifier.GQ.every.Existential

every is not existential, since with a scope lacking one individual everything is T fails while every T-thing is an individual holds (the two-lawyer argument of Section 3.3).

def KeenanStavi1986.theN {α : Type u_1} (n : ℕ) : Quantifier.GQ α

the n is the universal on a restrictor of exactly n individuals ((43)); both is theN 2.

Equations

• KeenanStavi1986.theN n = Quantifier.GQ.every ⊓ fun (R x : α → Prop) => {x : α | R x}.ncard = n

theorem KeenanStavi1986.theN_apply {α : Type u_1} (n : ℕ) (R T : α → Prop) : theN n R T ↔ Quantifier.GQ.every R T ∧ {x : α | R x}.ncard = n

theorem KeenanStavi1986.theN_two_eq_both {α : Type u_1} [Finite α] : theN 2 = Quantifier.GQ.both

the two is each of the two.

theorem KeenanStavi1986.not_existential_theN {α : Type u_1} [Fintype α] {n : ℕ} (hn : n < Fintype.card α) : ¬(theN n).Existential

the n is not existential below the universe size, since the n things are the first n fails while the n first-n things are individuals holds (Section 3.3's argument for the two, at every n).

def KeenanStavi1986.noBut {α : Type u_1} (a : α) : Quantifier.GQ α

no ... but J holds when restrictor and scope meet in exactly the individual a ((42)).

Equations

• KeenanStavi1986.noBut a R T = (R ⊓ T = Quantifier.NP.ident a)

theorem KeenanStavi1986.existential_noBut {α : Type u_1} (a : α) : (noBut a).Existential

no ... but John is existential ((103)).

noncomputable def KeenanStavi1986.existentialOrderIso {α : Type u_1} : ↥existentialSubalgebra ≃o Quantifier.NP α

An existential function is determined by its set of properties f(1), and the correspondence is an isomorphism onto the type ⟨1⟩ quantifiers, the possible NP denotations (PROP 15).

Equations

• One or more equations did not get rendered due to their size.

theorem KeenanStavi1986.card_existential {α : Type u_1} [Fintype α] : Nat.card ↥existentialSubalgebra = 2 ^ 2 ^ Fintype.card α

With n individuals there are 2 ^ 2 ^ n existential functions (PROP 15(a)).

Cardinal determiners (Section 3.4)

def KeenanStavi1986.Cardinal {α : Type u_1} (f : Quantifier.GQ α) : Prop

A cardinal function decides by the number of individuals in restrictor and scope ((102)).

Equations

• KeenanStavi1986.Cardinal f = ∀ (R T R' T' : α → Prop), Nat.card { x : α // R x ∧ T x } = Nat.card { x : α // R' x ∧ T' x } → (f R T ↔ f R' T')

def KeenanStavi1986.cardinalSubalgebra {α : Type u_1} : BooleanSubalgebra (Quantifier.GQ α)

The cardinal functions are closed under the Boolean operations (PROP 14(a)).

Equations

• KeenanStavi1986.cardinalSubalgebra = { carrier := {f : Quantifier.GQ α | KeenanStavi1986.Cardinal f}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem KeenanStavi1986.mem_cardinalSubalgebra {α : Type u_1} {f : Quantifier.GQ α} : f ∈ cardinalSubalgebra ↔ Cardinal f

theorem KeenanStavi1986.Cardinal.existential {α : Type u_1} {f : Quantifier.GQ α} (hf : Cardinal f) : f.Existential

A cardinal function is existential (PROP 14(c)).

theorem KeenanStavi1986.Cardinal.quantityInvariant {α : Type u_1} {f : Quantifier.GQ α} (hf : Cardinal f) : f.QuantityInvariant

A cardinal function is quantity invariant, since a bijection preserves the count of the meet.

theorem KeenanStavi1986.cardinalSubalgebra_le {α : Type u_1} : cardinalSubalgebra ≤ existentialSubalgebra

theorem KeenanStavi1986.cardinal_atLeast {α : Type u_1} (n : ℕ) : Cardinal (Quantifier.GQ.atLeast n)

at least n is cardinal.

theorem KeenanStavi1986.cardinal_exactly {α : Type u_1} (n : ℕ) : Cardinal (Quantifier.GQ.exactly n)

exactly n is cardinal.

theorem KeenanStavi1986.cardinal_some {α : Type u_1} [Fintype α] : Cardinal Quantifier.GQ.some

some is cardinal, as at least one.

theorem KeenanStavi1986.not_cardinal_noBut {α : Type u_1} {a b : α} (hab : a ≠ b) : ¬Cardinal (noBut a)

no ... but John is not cardinal: it separates two singletons of equal size.

theorem KeenanStavi1986.not_cardinal_someOf {α : Type u_1} {a b : α} (hab : a ≠ b) : ¬Cardinal (someOf a)

The cardinal functions are not closed under adjectival restriction, since Sₐ restricts the cardinal some but is not itself cardinal (PROP 16's parenthetical).

theorem KeenanStavi1986.cardinalSubalgebra_lt {α : Type u_1} [Nontrivial α] : cardinalSubalgebra < existentialSubalgebra

The cardinal functions are a proper subclass of the existential ones once two individuals exist, witnessed by no ... but John (PROP 14(c)).

noncomputable def KeenanStavi1986.cardinalOrderIso {α : Type u_1} [Fintype α] : ↥cardinalSubalgebra ≃o Set (Fin (Fintype.card α + 1))

A cardinal function is a set K of cardinalities between 0 and n, holding at (R, T) exactly when |R ⊓ T| ∈ K, and the correspondence is an isomorphism onto the power set ((102), with PROP 14(b) the count).

Equations

• One or more equations did not get rendered due to their size.

theorem KeenanStavi1986.card_cardinal {α : Type u_1} [Fintype α] : Nat.card ↥cardinalSubalgebra = 2 ^ (Fintype.card α + 1)

With n individuals there are 2 ^ (n + 1) cardinal functions (PROP 14(b)).

theorem KeenanStavi1986.isAtom_cardinal_iff {α : Type u_1} [Fintype α] {f : ↥cardinalSubalgebra} : IsAtom f ↔ ∃ (k : Fin (Fintype.card α + 1)), ↑f = Quantifier.GQ.exactly ↑k

The atoms of the cardinal algebra are the exactly k, as the Appendix remarks.

Logical determiners (Section 3.5 and the Appendix)

def KeenanStavi1986.quantityInvariantSubalgebra {α : Type u_1} : BooleanSubalgebra (Quantifier.GQ α)

The quantity-invariant functions are closed under the Boolean operations (the Appendix's PI subalgebra).

Equations

• KeenanStavi1986.quantityInvariantSubalgebra = { carrier := {f : Quantifier.GQ α | f.QuantityInvariant}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem KeenanStavi1986.mem_quantityInvariantSubalgebra {α : Type u_1} {f : Quantifier.GQ α} : f ∈ quantityInvariantSubalgebra ↔ f.QuantityInvariant

def KeenanStavi1986.logicalSubalgebra {α : Type u_1} : BooleanSubalgebra (Quantifier.GQ α)

LOG, the algebra of logical determiners, collects the permutation-invariant members of the conservative algebra ((114)).

Equations

• KeenanStavi1986.logicalSubalgebra = Quantifier.GQ.conservativeSubalgebra ⊓ KeenanStavi1986.quantityInvariantSubalgebra

@[simp]

theorem KeenanStavi1986.mem_logicalSubalgebra {α : Type u_1} {f : Quantifier.GQ α} : f ∈ logicalSubalgebra ↔ f.Conservative ∧ f.QuantityInvariant

theorem KeenanStavi1986.logical_every {α : Type u_1} : Quantifier.GQ.every ∈ logicalSubalgebra

every is logical.

theorem KeenanStavi1986.not_cardinal_every {α : Type u_1} [Nonempty α] : ¬Cardinal Quantifier.GQ.every

On a nonempty universe every is not cardinal, since it is not existential.

theorem KeenanStavi1986.cardinalSubalgebra_le_logical {α : Type u_1} : cardinalSubalgebra ≤ logicalSubalgebra

Every cardinal function is logical.

theorem KeenanStavi1986.cardinalSubalgebra_lt_logical {α : Type u_1} [Nontrivial α] : cardinalSubalgebra < logicalSubalgebra

Beyond one individual the cardinal functions are a proper subclass of the logical ones, witnessed by every (Section 3.5).

theorem KeenanStavi1986.logical_congr {α : Type u_1} [Fintype α] {f : Quantifier.GQ α} (hf : f ∈ logicalSubalgebra) {R T R' T' : α → Prop} (hR : Nat.card { x : α // R x } = Nat.card { x : α // R' x }) (hRT : Nat.card { x : α // R x ∧ T x } = Nat.card { x : α // R' x ∧ T' x }) : f R T ↔ f R' T'

A logical function depends only on the sizes of the restrictor and of its meet with the scope, the two-number reduction behind PROP 19.

@[reducible, inline]

abbrev KeenanStavi1986.Triangle (n : ℕ) : Type

The logical atoms are indexed by nested pairs of cardinalities up to the universe size (the Appendix's F_{m',m} index).

Equations

• KeenanStavi1986.Triangle n = { mm : Fin (n + 1) × Fin (n + 1) // mm.2 ≤ mm.1 }

theorem KeenanStavi1986.card_triangle (n : ℕ) : Nat.card (Triangle n) = (n + 1) * (n + 2) / 2

noncomputable def KeenanStavi1986.logicalOrderIso {α : Type u_1} [Fintype α] : ↥logicalSubalgebra ≃o Set (Triangle (Fintype.card α))

A logical function is a set of nested pairs (|R|, |R ⊓ T|), read off the initial segments, and any set of pairs arises; the correspondence is an isomorphism onto the power set (the Appendix's representation of PI).

Equations

• One or more equations did not get rendered due to their size.

theorem KeenanStavi1986.card_logical {α : Type u_1} [Fintype α] : Nat.card ↥logicalSubalgebra = 2 ^ ((Fintype.card α + 1) * (Fintype.card α + 2) / 2)

With n individuals there are 2 ^ ((n + 1)(n + 2)/2) logical functions (PROP 19).

def KeenanStavi1986.exactlyOfThe {α : Type u_1} (m n : ℕ) : Quantifier.GQ α

exactly m of the n is the Appendix's atom F_{n,m} of the logical algebra.

Equations

• KeenanStavi1986.exactlyOfThe m n R T = (Nat.card { x : α // R x } = n ∧ Nat.card { x : α // R x ∧ T x } = m)

theorem KeenanStavi1986.isAtom_logical_iff {α : Type u_1} [Fintype α] {f : ↥logicalSubalgebra} : IsAtom f ↔ ∃ (mm : Triangle (Fintype.card α)), ↑f = exactlyOfThe ↑(↑mm).2 ↑(↑mm).1

The atoms of the logical algebra are the exactly m of the n, as the Appendix remarks.

theorem KeenanStavi1986.cardinalSubalgebra_eq_inf {α : Type u_1} [Fintype α] : cardinalSubalgebra = existentialSubalgebra ⊓ logicalSubalgebra

Footnote 10 characterizes the cardinal functions on a finite universe as exactly the existential logical ones.

The paper's worked universes

Two individuals: 512 conservative functions among 65,536, of which 8 are cardinal and 64 logical; three individuals: 16 cardinal among 256 existential functions.