Kamp (1975): Two Theories about Adjectives

[Kam75]

Theory 1 classifies adjective meanings (functions from properties to properties) by meaning postulates — the classification lives in Semantics/Modification/Classification.lean. Theory 2, building on [VF69]'s supervaluations, derives the comparative from quantification over completions of a partial model; we formalize its comparative core, leaving the model apparatus abstract.

Main results

• kleene_dilemma: no truth-functional conjunction is both idempotent at the borderline value and false on borderline contradictions.
• kampPreorder: the completion comparative, definition (12).
• kampMeasureLe: the measure comparative, definition (13); kampMeasureLe_total is Kamp's objection to it and clever_incomparable his Smith/Jones witness.
• kampPreorder_le_iff_kampMeasureLe: for one-dimensional adjectives, (12) and (13) coincide.
• grayAdj, fakeAdj, skillfulAdj, allegedAdj: witnesses for the four classes, shared by Partee2010.lean and DelPinal2015.lean.

Bridge to single-world predicates

The classification (Modifier.isIntersective, .isSubsective, …) is one order-theoretic definition instantiated at two carriers: the intensional Property W E = W → E → Prop and the single-world E → Prop. The bridge theorems below show that fixing a world sends the first instance to the second.

theorem Kamp1975.intersective_at_world {W : Type u_1} {E : Type u_2} {adj : Modifier (Modification.Property W E)} (h : adj.isIntersective) (w : W) : Modifier.isIntersective fun (N : E → Prop) => adj (fun (x : W) => N) w

Single-world specialization: given a fixed world, the intensional instance of Modifier.isIntersective reduces to the E → Prop instance on the rigidified single-world view N ↦ adj (fun _ => N) w.

theorem Kamp1975.subsective_at_world {W : Type u_1} {E : Type u_2} {adj : Modifier (Modification.Property W E)} (h : adj.isSubsective) (w : W) : Modifier.isSubsective fun (N : E → Prop) => adj (fun (x : W) => N) w

Single-world specialization of Modifier.isSubsective.

The many-valued dilemma

theorem Kamp1975.kleene_dilemma : ¬∃ (meet : Trivalent → Trivalent → Trivalent), meet Trivalent.indet Trivalent.indet = Trivalent.indet ∧ meet Trivalent.indet Trivalent.indet.neg = Trivalent.false

No truth-functional conjunction is both idempotent at the borderline value and false on borderline contradictions: with neg indet = indet, both demands constrain the same input pair. This is the dilemma of [Kam75], pp. 130–131, stated there for every linearly ordered n-valued logic; Trivalent is the minimal witness.

Kamp's completion comparative, definition (12)

Definition (12) (paper § 4): u₁ is at least as A as u₂ iff every admissible completion that puts u₂ in the extension also puts u₁ in it. [Kle80] § 5.3 states the strict comparative existentially over comparison classes; the bridge is Klein1980.kleinPreorder_eq_kampPreorder.

@[reducible]

def Kamp1975.kampPreorder {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) (S : Set C) : Preorder E

Kamp's completion comparative (definition (12), paper § 4) as a Preorder: le u₁ u₂ iff every completion in S that puts u₂ in the extension also puts u₁ in — le reads "u₁ is at least as A as u₂", Kamp's ≥. The S-restricted analogue of kleinPreorder in Delineation.lean. Kamp credits (12) to Lewis (1970), where it is attributed to Kaplan.

Equations

• Kamp1975.kampPreorder ext S = { le := fun (u₁ u₂ : E) => ∀ c ∈ S, ext c u₂ → ext c u₁, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Kamp1975.kampPreorder_antitone {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) (u₁ u₂ : E) : Antitone fun (S : Set C) => u₁ ≤ u₂

The Kamp preorder is Antitone in S: enlarging S (more completions to quantify over) makes ≤ harder to satisfy.

(12) vs (13): definite vs measured comparatives

Kamp's second candidate, definition (13) (paper § 4), compares the measures of the completion sets rather than the sets themselves. His § 5 argues against (13) for multi-criteria adjectives: it makes any two entities comparable, while (12) leaves Smith and Jones incomparable in cleverness — for Kamp the right verdict. For one-dimensional adjectives (heavy, tall, hot) the two provably coincide.

def Kamp1975.kampMeasureLe {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) [(c : C) → (e : E) → Decidable (ext c e)] (S : Finset C) (p : C → ℚ) (u₁ u₂ : E) : Prop

[Kam75] definition (13) (paper § 4): the measure-based comparative — u₁ ≤ u₂ iff the measure of completions putting u₂ in the extension is at most that putting u₁ in (kampPreorder's orientation). Kamp's probability measure over a field of subsets is specialized to atomic ℚ weights over a finite completion set; only the ordering matters, so weights need not sum to 1.

Equations

• Kamp1975.kampMeasureLe ext S p u₁ u₂ = (∑ c ∈ S with ext c u₂, p c ≤ ∑ c ∈ S with ext c u₁, p c)

theorem Kamp1975.kampMeasureLe_total {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) [(c : C) → (e : E) → Decidable (ext c e)] (S : Finset C) (p : C → ℚ) (u₁ u₂ : E) : kampMeasureLe ext S p u₁ u₂ ∨ kampMeasureLe ext S p u₂ u₁

(13) is total: it makes any two objects comparable. This is Kamp's § 5 objection to (13); (12) does not share the property (clever_incomparable).

theorem Kamp1975.kampMeasureLe_of_kampPreorder_le {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) [(c : C) → (e : E) → Decidable (ext c e)] (S : Finset C) (p : C → ℚ) (hp : ∀ c ∈ S, 0 ≤ p c) {u₁ u₂ : E} (h : u₁ ≤ u₂) : kampMeasureLe ext S p u₁ u₂

Definite comparison entails measured comparison: (12) implies (13) for nonnegative weights.

The Smith/Jones incomparability witness (§ 5)

Two criteria for clever — problem-solving and quick-wittedness — as two completions; Smith passes one, Jones the other. Under (12) the two are incomparable, which Kamp argues is correct; (13) must issue a verdict (kampMeasureLe_total). Kamp's own scenario is asymmetric (Smith much better at problems, only slightly worse in wit, so (13) wrongly makes Smith cleverer); this symmetric toy witnesses the incomparability and the forced verdict, not that specific outcome.

@[instance_reducible]

instance Kamp1975.instDecidableEqCrit : DecidableEq Kamp1975.Crit✝

Equations

• Kamp1975.instDecidableEqCrit x✝ y✝ = if h : Kamp1975.Crit.ctorIdx✝ x✝ = Kamp1975.Crit.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Kamp1975.instDecidableEqP2 : DecidableEq Kamp1975.P2✝

Equations

• Kamp1975.instDecidableEqP2 x✝ y✝ = if h : Kamp1975.P2.ctorIdx✝ x✝ = Kamp1975.P2.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

theorem Kamp1975.clever_incomparable : ¬Kamp1975.P2.smith✝ ≤ Kamp1975.P2.jones✝ ∧ ¬Kamp1975.P2.jones✝ ≤ Kamp1975.P2.smith✝

Under (12), Smith and Jones are incomparable in cleverness — Kamp's argument that (12) "captures the comparative correctly" for multi-criteria adjectives, against (13)'s forced totality.

One-dimensionality

def Kamp1975.OneDimensional {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) (S : Finset C) : Prop

One-dimensional adjectives ([Kam75] § 5: heavy, tall, hot): any two entities' completion-sets are ⊆-comparable, so the extensions form a chain (threshold structure). The formal condition is Kamp's (18), stated in § 6 where it grounds the adjective/noun asymmetry.

Equations

• Kamp1975.OneDimensional ext S = ∀ (u₁ u₂ : E), (∀ c ∈ S, ext c u₁ → ext c u₂) ∨ ∀ c ∈ S, ext c u₂ → ext c u₁

theorem Kamp1975.kampPreorder_le_iff_kampMeasureLe {E : Type u_1} {C : Type u_2} (ext : C → E → Prop) [(c : C) → (e : E) → Decidable (ext c e)] (S : Finset C) (p : C → ℚ) (hp : ∀ c ∈ S, 0 < p c) (h18 : OneDimensional ext S) (u₁ u₂ : E) : u₁ ≤ u₂ ↔ kampMeasureLe ext S p u₁ u₂

For one-dimensional adjectives with strictly positive weights, the measured comparative (13) collapses to the definite comparative (12) — Kamp's § 5 observation that "for this special case the two definitions are equivalent", with strict positivity rendering his "provided p has been correctly specified".

Concrete Witnesses for Each Class

Each class in the hierarchy is non-empty: explicit denotations that provably satisfy each definition from Classification.lean, modeling the classic examples from the literature — "gray" (intersective), "fake" (privative), "skillful" (subsective but not extensional), "alleged" (non-subsective/modal).

[Par10] argues that the privative class should be eliminated in favor of subsective + noun coercion. The witness fakeAdj below models the traditional analysis; see Partee2010.lean for the coercion reanalysis.

inductive Kamp1975.W2 : Type

Two worlds suffice to distinguish extensional from non-extensional.

• w₁ : W2
• w₂ : W2

inductive Kamp1975.E3 : Type

Three entities suffice for all witness constructions.

• a : E3
• b : E3
• c : E3

def Kamp1975.grayAdj : Modifier (Modification.Property W2 E3)

"gray": an intersective adjective ([Kam75] definition (4), "predicative") — a fixed property conjoined with the noun, so "gray cat" entails both "gray" and "cat".

Equations

• Kamp1975.grayAdj N w Kamp1975.E3.a = (True ∧ N w Kamp1975.E3.a)
• Kamp1975.grayAdj N w x = (False ∧ N w x)

theorem Kamp1975.gray_intersective : grayAdj.isIntersective

def Kamp1975.fakeAdj : Modifier (Modification.Property W2 E3)

"fake": a privative adjective ([Kam75] definition (5); fake and false are his examples) — "fake gun" entails "not a gun". Kamp doubts any English adjective is privative "in all of its possible uses", anticipating [Par10]'s subsective-plus-coercion reanalysis; see Partee2010.lean.

Equations

• Kamp1975.fakeAdj N w Kamp1975.E3.b = (True ∧ ¬N w Kamp1975.E3.b)
• Kamp1975.fakeAdj N w x = (False ∧ ¬N w x)

theorem Kamp1975.fake_privative : fakeAdj.isPrivative

def Kamp1975.skillfulAdj : Modifier (Modification.Property W2 E3)

"skillful": subsective ([Kam75] definition (6), "affirmative") but not extensional — "skillful surgeon" entails "surgeon", yet skill depends on the noun's intension, not just its current extension (Kamp's example, crediting the cobblers/darts-players case to David Lewis).

Equations

• Kamp1975.skillfulAdj N w Kamp1975.E3.a = (N w Kamp1975.E3.a ∧ N Kamp1975.W2.w₁ Kamp1975.E3.a)
• Kamp1975.skillfulAdj N w x = (N w x ∧ False)

theorem Kamp1975.skillful_subsective : skillfulAdj.isSubsective

theorem Kamp1975.skillful_not_extensional : ¬Intensional.IsExtensional skillfulAdj

def Kamp1975.allegedAdj : Modifier (Modification.Property W2 E3)

"alleged": a non-subsective (modal) adjective — [Kam75]'s opening example (1), "Every alleged thief is a thief" is no logical truth. No meaning postulate relates the modified and unmodified extensions (likewise "potential", "putative").

Equations

• Kamp1975.allegedAdj _N x✝ Kamp1975.E3.a = True
• Kamp1975.allegedAdj _N x✝ x = False

theorem Kamp1975.alleged_extensional : Intensional.IsExtensional allegedAdj

"alleged" ignores the noun entirely, so it is trivially extensional — with skillful_not_extensional and skillful_subsective, this witnesses that extensionality is orthogonal to subsectivity.

theorem Kamp1975.alleged_not_subsective : ¬allegedAdj.isSubsective

"alleged N" does not entail "N" (not subsective).

theorem Kamp1975.alleged_not_privative : ¬allegedAdj.isPrivative

"alleged N" does not entail "not N" (not privative).