Keenan & Comrie (1977) [KC77]

Noun Phrase Accessibility and Universal Grammar. Linguistic Inquiry 8(1): 63–99.

Formalizes the three Hierarchy Constraints (HCs) and the derived Primary Relativization Constraint (PRC) from [KC77], verified against a subset of the paper's Table 1 data (pp. 76-79).

Architecture

This file derives K&C's typological theorems directly from Fragments.{Lang}.relMarkers : List Marker, the per-language data layer encoding actual linguistic markers (particles, pronouns, verbal suffixes). No intermediate KCProfile/StrategyEntry schema — predicates and aggregations are stated over List Marker directly, projecting through Marker.{positions, bearsCaseMarking, rcPosition} as needed.

The Fragment files cite [KC79] (the per-language exemplification appendix originally intended for publication with K&C 1977 — Language 55(2): 333–351) inline where its sentence-level examples back the descriptive marker data.

Hierarchy Constraints

The paper proposes three constraints on how languages form relative clauses, building on the Accessibility Hierarchy (AH):

SU > DO > IO > OBL > GEN > OCOMP

• HC₁ (p. 67): A language must be able to relativize subjects.
• HC₂ (Continuity) (p. 67): Any RC-forming strategy must apply to a continuous segment of the AH.
• HC₃ (Cut-off) (p. 67): Strategies that apply at one point may cease at any lower point.

From HC₁ + HC₂, the Primary Relativization Constraint (p. 68) follows: if a language's primary strategy (one that covers subjects) can apply to a low position N, it can apply to all positions above N. Non-primary strategies need not satisfy this — they may cover a continuous segment that excludes subjects (e.g., the +case strategy covering IO–OCOMP but not SU–DO in Welsh and Arabic, p. 70 + Table 1 p. 76).

Multi-Strategy Profiles

The paper's key empirical contribution is showing that languages typically have multiple relativization strategies, each covering a different contiguous segment of the AH. The ±case distinction (whether the relative element bears case marking) is the primary parameter distinguishing strategies.

Sample

Nine languages cover the key patterns: gap-to-resumptive split (Welsh, Hebrew, Arabic, Toba Batak), multi-strategy with prenominal RCs (Korean, Finnish), single-strategy (Malagasy), and per-position strategy split with serial-verb-mediated obliques (Yoruba).

def KeenanComrie1977.SatisfiesHC1 (markers : List RelativeClause.Marker) : Prop

HC₁: a language can relativize subjects iff some marker covers SU.

Equations

• KeenanComrie1977.SatisfiesHC1 markers = ∃ m ∈ markers, m.Covers RelativeClause.AHPosition.subject

@[implicit_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC1 (markers : List RelativeClause.Marker) : Decidable (SatisfiesHC1 markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC1 markers = id inferInstance

def KeenanComrie1977.SatisfiesHC2 (markers : List RelativeClause.Marker) : Prop

HC₂: every marker covers a contiguous segment of the AH.

Equations

• KeenanComrie1977.SatisfiesHC2 markers = ∀ m ∈ markers, m.IsContinuous

@[implicit_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC2 (markers : List RelativeClause.Marker) : Decidable (SatisfiesHC2 markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC2 markers = id inferInstance

def KeenanComrie1977.SatisfiesPRC (markers : List RelativeClause.Marker) : Prop

PRC: every primary marker is upward-closed on the AH. If marker m is primary and covers position pos, then m covers every position above pos. This is the paper's Primary Relativization Constraint (p. 68), which follows from HC₂ for primary strategies (see prc_from_hc2 below for the general derivation).

Equations

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

@[implicit_reducible]

instance KeenanComrie1977.instDecidableSatisfiesPRC (markers : List RelativeClause.Marker) : Decidable (SatisfiesPRC markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesPRC markers = id inferInstance

def KeenanComrie1977.lowestCovered (markers : List RelativeClause.Marker) : RelativeClause.AHPosition

The lowest AH position covered by any marker in the list (i.e., the deepest the language can reach). Returns .subject if even SU is uncovered (vacuously, since HC₁ would be violated).

Equations

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

Per-language abbrevs over Fragment marker lists. The original 8-language sample from the paper plus Yoruba (added later via [Awo78] + [KC79]).

@[reducible, inline]

abbrev KeenanComrie1977.english : List RelativeClause.Marker

Equations

• KeenanComrie1977.english = English.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.welsh : List RelativeClause.Marker

Equations

• KeenanComrie1977.welsh = Welsh.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.arabic : List RelativeClause.Marker

Equations

• KeenanComrie1977.arabic = [Arabic.ModernStandard.relAlladhi, Arabic.ModernStandard.relResumptive]

@[reducible, inline]

abbrev KeenanComrie1977.hebrew : List RelativeClause.Marker

Equations

• KeenanComrie1977.hebrew = Hebrew.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.tobaBatak : List RelativeClause.Marker

Equations

• KeenanComrie1977.tobaBatak = TobaBatak.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.korean : List RelativeClause.Marker

Equations

• KeenanComrie1977.korean = Korean.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.finnish : List RelativeClause.Marker

Equations

• KeenanComrie1977.finnish = Finnish.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.malagasy : List RelativeClause.Marker

Equations

• KeenanComrie1977.malagasy = Malagasy.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.yoruba : List RelativeClause.Marker

Equations

• KeenanComrie1977.yoruba = Yoruba.relMarkers

def KeenanComrie1977.originalSample : List (List RelativeClause.Marker)

The 8-language sub-sample from the original paper Table 1 (pp. 76-79).

Equations

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

def KeenanComrie1977.allSamples : List (List RelativeClause.Marker)

The original 8-language sample plus Yoruba (the only post-1977 addition; refutes one of the paper's implicit ±case generalizations — see yoruba_refutes_minus_case_covers_subjects below).

Equations

• KeenanComrie1977.allSamples = KeenanComrie1977.originalSample ++ [KeenanComrie1977.yoruba]

theorem KeenanComrie1977.sample_size : allSamples.length = 9

theorem KeenanComrie1977.hc1_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesHC1 markers

HC₁ holds: every language in the sample can relativize subjects.

theorem KeenanComrie1977.hc2_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesHC2 markers

HC₂ holds: every marker in every sampled language covers a contiguous AH segment.

theorem KeenanComrie1977.prc_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesPRC markers

PRC holds: every primary marker satisfies upward closure on the AH.

theorem KeenanComrie1977.every_language_has_primary (markers : List RelativeClause.Marker) : markers ∈ allSamples → ∃ m ∈ markers, m.IsPrimary

Restating HC₁ in terms of Marker.IsPrimary: every language has at least one primary marker.

theorem KeenanComrie1977.isUpperSet_of_satisfiesPRC {markers : List RelativeClause.Marker} (h : SatisfiesPRC markers) {m : RelativeClause.Marker} (hm : m ∈ markers) (hp : m.IsPrimary) : IsUpperSet {p : RelativeClause.AHPosition | m.Covers p}

The PRC is order upward-closure: in any PRC-satisfying language, a primary marker's coverage is an IsUpperSet on the AHPosition scale order. Keenan & Comrie's Primary Relativization Constraint is the order-theoretic "upper set" property — the same IsUpperSet that Core.Order.Markedness uses for differential-marking cutoffs — rather than a bespoke rank predicate.

theorem KeenanComrie1977.minus_case_covers_subjects_in_original_sample (markers : List RelativeClause.Marker) : markers ∈ originalSample → ∀ m ∈ markers, m.bearsCaseMarking = false → m.Covers RelativeClause.AHPosition.subject

In the original 8-language sub-sample, every -case marker covers subjects. The -case (gap/deletion) strategy is always primary when present in those languages.

REFUTED by Yoruba — see yoruba_refutes_minus_case_covers_subjects below: Yoruba has gap markers for DO and OBL that do not cover SU because subject relativization independently uses pronoun retention (ó, per [Awo78] §6.19).

theorem KeenanComrie1977.yoruba_refutes_minus_case_covers_subjects : ∃ m ∈ yoruba, m.bearsCaseMarking = false ∧ ¬m.Covers RelativeClause.AHPosition.subject

[KC79] effectively documents Yoruba as a refutation of the gap-implies-subject correlation. Yoruba's IO/OBL relativization is mediated by serial-verb DO recasting (K&C 1979 p. 349), producing -case markers that do not cover SU. SU relativization independently uses pronoun retention (ó, K&C 1979 p. 350 analyzes as verb agreement; descriptive surface form per [Awo78] §6.19).

theorem KeenanComrie1977.most_have_multiple_strategies : (List.filter (fun (x : List RelativeClause.Marker) => decide (x.length > 1)) allSamples).length ≥ 5

Most languages in the sample use more than one marker, with markers covering different segments.

theorem KeenanComrie1977.plus_case_secondary_excludes_su (markers : List RelativeClause.Marker) : markers ∈ allSamples → ∀ m ∈ markers, m.bearsCaseMarking = true → ¬m.IsPrimary → ¬m.Covers RelativeClause.AHPosition.subject

+case markers that are non-primary (don't cover SU) never cover SU in our sample. This reflects the typological generalization that pronoun retention is used for lower, not higher, AH positions. Holds across all 9 languages including Yoruba.

theorem KeenanComrie1977.toba_batak_do_gap (m : RelativeClause.Marker) : m ∈ tobaBatak → ¬m.Covers RelativeClause.AHPosition.directObject

Toba Batak has a genuine gap at DO: neither marker can relativize direct objects. This is consistent with the HCs because each individual marker is contiguous — the gap exists between markers, not within one. The paper notes this explicitly (p. 68-69: "direct objects cannot be relativized using this or any other strategy in Toba").

theorem KeenanComrie1977.toba_batak_hc2 : SatisfiesHC2 tobaBatak

Despite the DO gap, Toba Batak satisfies HC₂: both individual markers are contiguous (SU alone; IO–GEN alone).

theorem KeenanComrie1977.english_full_coverage : List.map (fun (x : RelativeClause.Marker) => x.positions.length) english = [2, 4]

English (Table 1 p. 76): -case that/∅ covers SU/DO (2 positions); +case who/whom covers IO/OBL/GEN/OCOMP (4 positions).

theorem KeenanComrie1977.welsh_strategy_split : welsh.length = 2 ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) welsh = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) welsh = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.indirectObject)) welsh = [false, true] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.objComparison)) welsh = [false, true]

Welsh (Table 1 p. 76; paper §1.3.2 p. 70): markers split at DO/IO. -case (particle a) covers SU/DO; +case (particle y + resumptive) covers IO/OBL/GEN/OCOMP.

theorem KeenanComrie1977.arabic_primary_su_only : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) arabic = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) arabic = [false, true]

Arabic (MSA) (Table 1 p. 76): the relative pronoun alladhī/allatii used alone (-case strategy) covers SU only; alladhī/allatii with a resumptive pronoun (+case strategy) covers DO–OCOMP.

theorem KeenanComrie1977.malagasy_su_only : malagasy.length = 1 ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) malagasy = [true] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) malagasy = [false]

Malagasy (Table 1 p. 78; paper §1.3.1 p. 69-70): single marker, SU only.

theorem KeenanComrie1977.korean_primary_su_to_obl : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) korean = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.oblique)) korean = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.genitive)) korean = [false, true]

Korean (Table 1 p. 78; paper §1.3.4 p. 74): -case adnominal verb suffix covers SU/DO/IO/OBL but not GEN; +case genitive marker covers GEN only.

theorem KeenanComrie1977.finnish_plus_case_is_primary : List.map (fun (x : RelativeClause.Marker) => x.bearsCaseMarking) finnish = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide m.IsPrimary) finnish = [true, true]

Finnish (Table 1 p. 76; paper §1.3.2 p. 70-71): the +case marker joka is the broader/primary one (covers SU–GEN); the -case participial marker also covers SU but is narrower (SU/DO only).

theorem KeenanComrie1977.yoruba_strategy_breakdown : yoruba.length = 4 ∧ List.map (fun (x : RelativeClause.Marker) => x.bearsCaseMarking) yoruba = [false, false, false, true] ∧ List.map (fun (m : RelativeClause.Marker) => decide m.IsPrimary) yoruba = [true, false, false, false]

Yoruba: 4 per-position markers. relTiSubject (-case, primary, only SU); relTiObject (-case, NOT primary, only DO); relTiOblique (-case, NOT primary, IO/OBL); relTiGenitive (+case, NOT primary, GEN only). All 4 individually contiguous on the AH, so HC₂ holds.

K&C 1977 Table 1's per-position coverage and each language's WALS-derived Relativization.lowestRelativizable encode complementary views of the same data. Bridge theorems below verify agreement on the lowest position covered, language by language. K&C's Table 1 is strictly more detailed than WALS Ch 122/123 (which only ask about subjects and obliques), so the K&C lowestCovered is at least as deep as the WALS lowestRelativizable.

theorem KeenanComrie1977.english_kc_matches_wals : lowestCovered english = RelativeClause.AHPosition.objComparison ∧ English.Relativization.lowestRelativizable = RelativeClause.AHPosition.objComparison

theorem KeenanComrie1977.welsh_kc_covers_deeper_than_wals : lowestCovered welsh = RelativeClause.AHPosition.objComparison ∧ Welsh.Relativization.lowestRelativizable = RelativeClause.AHPosition.oblique ∧ RelativeClause.AHPosition.oblique.moreAccessible RelativeClause.AHPosition.objComparison

theorem KeenanComrie1977.korean_kc_covers_deeper_than_wals : lowestCovered korean = RelativeClause.AHPosition.genitive ∧ Korean.Relativization.lowestRelativizable = RelativeClause.AHPosition.oblique

theorem KeenanComrie1977.malagasy_kc_matches_wals : lowestCovered malagasy = RelativeClause.AHPosition.subject ∧ Malagasy.Relativization.lowestRelativizable = RelativeClause.AHPosition.subject

theorem KeenanComrie1977.finnish_kc_matches_wals : lowestCovered finnish = RelativeClause.AHPosition.genitive ∧ Finnish.Relativization.lowestRelativizable = RelativeClause.AHPosition.oblique

theorem KeenanComrie1977.hebrew_kc_covers_deeper_than_wals : lowestCovered hebrew = RelativeClause.AHPosition.objComparison ∧ Hebrew.Relativization.lowestRelativizable = RelativeClause.AHPosition.oblique

theorem KeenanComrie1977.arabic_kc_covers_deeper_than_wals : lowestCovered arabic = RelativeClause.AHPosition.objComparison ∧ Arabic.ModernStandard.Relativization.lowestRelativizable = RelativeClause.AHPosition.oblique

theorem KeenanComrie1977.yoruba_kc_matches_wals : lowestCovered yoruba = RelativeClause.AHPosition.genitive ∧ Yoruba.Relativization.lowestRelativizable = RelativeClause.AHPosition.genitive

theorem KeenanComrie1977.kc_at_least_as_detailed_as_wals : (lowestCovered english).rank ≤ English.Relativization.lowestRelativizable.rank ∧ (lowestCovered welsh).rank ≤ Welsh.Relativization.lowestRelativizable.rank ∧ (lowestCovered korean).rank ≤ Korean.Relativization.lowestRelativizable.rank ∧ (lowestCovered malagasy).rank ≤ Malagasy.Relativization.lowestRelativizable.rank ∧ (lowestCovered finnish).rank ≤ Finnish.Relativization.lowestRelativizable.rank ∧ (lowestCovered hebrew).rank ≤ Hebrew.Relativization.lowestRelativizable.rank ∧ (lowestCovered arabic).rank ≤ Arabic.ModernStandard.Relativization.lowestRelativizable.rank ∧ (lowestCovered yoruba).rank ≤ Yoruba.Relativization.lowestRelativizable.rank

Systematic coverage agreement: K&C is at least as detailed as WALS for every sample language. The WALS profile never claims a language can relativize a position that K&C Table 1 doesn't cover.

HC₂ ("any RC-forming strategy must apply to a continuous segment of the AH") is a paper-anchored claim. The contiguity machinery (contiguousOnAH, AHPosition.rank) lives in Typology/RelativeClause/Basic.lean because it mirrors Features/Case/Basic.lean's IsValidInventory and is genuinely framework-agnostic. The specific contiguous-segment witnesses below exemplify HC₂ on the AH and are part of [KC77]'s core argumentation.

theorem KeenanComrie1977.full_ah_contiguous : RelativeClause.contiguousOnAH RelativeClause.AHPosition.all = true

The full hierarchy [SU, DO, IO, OBL, GEN, OCOMP] is contiguous.

theorem KeenanComrie1977.singleton_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject] = true

A single position is trivially contiguous.

theorem KeenanComrie1977.su_do_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject] = true

[SU, DO] is contiguous.

theorem KeenanComrie1977.io_obl_gen_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive] = true

[IO, OBL, GEN] is contiguous (a non-primary segment).

theorem KeenanComrie1977.su_do_obl_not_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.oblique] = false

[SU, DO, OBL] is NOT contiguous (skips IO at rank 4).

The PRC is the paper's main derivation: it follows from HC₁ + HC₂ rather than being an independent stipulation. The general proof lives here (paper content), not in Typology/RelativeClause/Basic.lean (substrate).

theorem KeenanComrie1977.prc_from_hc2 (positions : List RelativeClause.AHPosition) (h_contig : RelativeClause.contiguousOnAH positions = true) (h_su : (positions.any fun (x : RelativeClause.AHPosition) => x == RelativeClause.AHPosition.subject) = true) (p above : RelativeClause.AHPosition) (hp : (positions.any fun (x : RelativeClause.AHPosition) => x == p) = true) (habove : above.rank > p.rank) : (positions.any fun (x : RelativeClause.AHPosition) => x == above) = true

Primary Relativization Constraint (general proof).

If a list of AH positions is contiguous (HC₂) and contains .subject (i.e., the strategy is primary), then the list is upward-closed: for any covered position p, all positions above p on the AH are also covered.

This proves that the PRC is a logical consequence of HC₂ + being primary, not an independent constraint — the paper's core derivation ([KC77] p. 68: "PRC₂ follows directly from HC₂ and the definition of primary").

theorem KeenanComrie1977.prc_all_primary_segments : have segs := [[RelativeClause.AHPosition.subject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive, RelativeClause.AHPosition.objComparison]]; (segs.all fun (seg : List RelativeClause.AHPosition) => (RelativeClause.contiguousOnAH seg && seg.any fun (x : RelativeClause.AHPosition) => x == RelativeClause.AHPosition.subject) && seg.all fun (p : RelativeClause.AHPosition) => RelativeClause.AHPosition.all.all fun (above : RelativeClause.AHPosition) => if above.rank > p.rank then seg.any fun (x : RelativeClause.AHPosition) => x == above else true) = true

All 6 canonical primary strategy segments are upward-closed. These are the only possible contiguous segments containing .subject.