Kamp (1975): Two theories about adjectives

Kamp's first theory treats an adjective as a function from properties to properties, constrained by meaning postulates that make it predicative, privative or affirmative, with alleged satisfying none; extensionality is a separate dimension. His second theory, for vague adjectives, gives them partial extensions and, after van Fraassen, derives the comparative from quantification over the admissible completions: one object is at least as A as another when every completion that puts the second in the extension puts the first in. A rival definition, which compares the measures of the completion sets, makes any two objects comparable, which Kamp rejects for adjectives with several criteria such as clever; for one-dimensional adjectives the two agree. Before this, Kamp argues that no many-valued logic handles borderline cases.

Main statements

• intersective_at_world, subsective_at_world: fixing a world sends the intensional classes to the classes of single-world predicates.
• kleene_dilemma: no truth-functional conjunction is both idempotent at the borderline value and false on borderline contradictions.
• kampMeasureLe_total, clever_incomparable: the measured comparative is total, while the completion comparative leaves Smith and Jones incomparable in cleverness.
• kampPreorder_le_iff_kampMeasureLe: for one-dimensional adjectives the two comparatives agree.
• gray_intersective, fake_privative, skillful_subsective, skillful_not_extensional, alleged_not_subsective: each class has a member, and extensionality is independent of subsectivity.

Implementation notes

• The measure of (13) is specialized to atomic ℚ weights over a finite set of completions; only the ordering matters, so the weights need not sum to one.
• The Smith and Jones witness is symmetric, one criterion each; the paper's scenario is asymmetric, and the witness shows the incomparability and the forced verdict, not the paper's specific outcome.

References

• [Kam75]
• [VF69]
• [Lew70]
• [Kle80]
• [Par10]

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 (Semantics.Property W E)} (h : adj.IsIntersective) (w : W) : Modifier.IsIntersective fun (N : E → Prop) => adj (fun (x : W) => N) w

At a fixed world an intersective modifier of intensional properties is an intersective modifier of predicates, N ↦ adj (fun _ ↦ N) w.

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

At a fixed world a subsective modifier of intensional properties is a subsective modifier of predicates.

The many-valued dilemma

theorem Kamp1975.kleene_dilemma : ¬∃ (meet : SignType → SignType → SignType), meet 0 0 = 0 ∧ meet 0 (-0) = -1

No truth-functional conjunction is both idempotent at the borderline value and false on borderline contradictions, since with -0 = 0 both demands constrain the same pair of inputs. Kamp states the dilemma (pp. 130–131) for every linearly ordered n-valued logic, of which SignType is the smallest.

The completion comparative

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) of § 4, is the preorder in which u₁ ≤ u₂ when every completion in S that puts u₂ in the extension also puts u₁ in, so that ≤ reads at least as A as. Kamp credits (12) to [Lew70], who attributes it 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 completion comparative is antitone in the set of completions, since more completions make ≤ harder to satisfy.

Completion and 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

The measured comparative, definition (13) of § 4, holds of u₁ and u₂ when the completions putting u₂ in the extension weigh at most as much as those putting u₁ in.

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₁

The measured comparative makes any two objects comparable, Kamp's objection to it in § 5, which the completion comparative escapes (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₂

For nonnegative weights the completion comparative implies the measured one.

Smith and Jones

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.

inductive Kamp1975.Crit : Type

The two criteria of cleverness, problem solving and quick wit.

• problemSolving : Crit
• quickWit : Crit

@[instance_reducible]

instance Kamp1975.instDecidableEqCrit : DecidableEq Crit

Equations

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

inductive Kamp1975.P2 : Type

Smith and Jones.

• smith : P2
• jones : P2

@[instance_reducible]

instance Kamp1975.instDecidableEqP2 : DecidableEq P2

Equations

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

def Kamp1975.cleverExt : Crit → P2 → Prop

Smith is clever by the first criterion and Jones by the second.

Equations

• Kamp1975.cleverExt Kamp1975.Crit.problemSolving Kamp1975.P2.smith = True
• Kamp1975.cleverExt Kamp1975.Crit.quickWit Kamp1975.P2.jones = True
• Kamp1975.cleverExt x✝¹ x✝ = False

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

By the completion comparative Smith and Jones are incomparable in cleverness, which Kamp takes to capture the comparative correctly for adjectives with several criteria.

One-dimensionality

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

An adjective is one-dimensional, as heavy, tall and hot are in § 5, when the completion sets of any two entities are comparable by inclusion. The condition is Kamp's (18), stated in § 6.

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 a one-dimensional adjective and strictly positive weights the two comparatives agree, Kamp's observation in § 5 that "for this special case the two definitions are equivalent", strict positivity rendering his proviso that the measure be correctly specified.

A member of 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 (Semantics.Property W2 E3)

gray is predicative, Kamp's definition (4), since it conjoins a fixed property 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 (Semantics.Property W2 E3)

fake is privative, Kamp's definition (5), so fake gun entails not a gun. Kamp doubts that any English adjective is privative "in all of its possible uses".

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 (Semantics.Property W2 E3)

skillful is affirmative, Kamp's definition (6), but not extensional. A skillful surgeon is a surgeon, yet skill depends on the noun's intension and not just its current extension, as in the case of cobblers and darts players that Kamp credits to 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 : ¬ModalLogic.IsExtensional skillfulAdj

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

alleged satisfies no meaning postulate, Kamp's opening example (1) being that every alleged thief is a thief is no logical truth.

Equations

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

theorem Kamp1975.alleged_extensional : ModalLogic.IsExtensional allegedAdj

alleged ignores the noun, so it is extensional; with skillful_not_extensional this shows that extensionality is independent of subsectivity.

theorem Kamp1975.alleged_not_subsective : ¬allegedAdj.IsSubsective

alleged N does not entail N.

theorem Kamp1975.alleged_not_privative : ¬allegedAdj.IsPrivative

alleged N does not entail not N.