Accessibility Hierarchy: Ordering and Contiguity

@cite{keenan-comrie-1977}

Defines the rank function and contiguity predicate for the Accessibility Hierarchy. Mirrors Core.Case.Hierarchy for Blake's case hierarchy.

def Core.AHPosition.rank : AHPosition → Nat

Numeric rank of a position on the Accessibility Hierarchy. Higher rank = more accessible = more languages can relativize it.

Equations

• Core.AHPosition.subject.rank = 6
• Core.AHPosition.directObject.rank = 5
• Core.AHPosition.indirectObject.rank = 4
• Core.AHPosition.oblique.rank = 3
• Core.AHPosition.genitive.rank = 2
• Core.AHPosition.objComparison.rank = 1

def Core.AHPosition.atLeastAsAccessible (p1 p2 : AHPosition) : Prop

Position p1 is at least as accessible as p2 on the hierarchy.

Equations

• p1.atLeastAsAccessible p2 = (p1.rank ≥ p2.rank)

@[implicit_reducible]

instance Core.instDecidableAtLeastAsAccessible (p1 p2 : AHPosition) : Decidable (p1.atLeastAsAccessible p2)

Equations

• Core.instDecidableAtLeastAsAccessible p1 p2 = Core.instDecidableAtLeastAsAccessible._aux_1 p1 p2

def Core.AHPosition.moreAccessible (p1 p2 : AHPosition) : Prop

Position p1 is strictly more accessible than p2.

Equations

• p1.moreAccessible p2 = (p1.rank > p2.rank)

@[implicit_reducible]

instance Core.instDecidableMoreAccessible (p1 p2 : AHPosition) : Decidable (p1.moreAccessible p2)

Equations

• Core.instDecidableMoreAccessible p1 p2 = Core.instDecidableMoreAccessible._aux_1 p1 p2

def Core.AHPosition.all : List AHPosition

All AH positions in descending order of accessibility.

Equations

• Core.AHPosition.all = [Core.AHPosition.subject, Core.AHPosition.directObject, Core.AHPosition.indirectObject, Core.AHPosition.oblique, Core.AHPosition.genitive, Core.AHPosition.objComparison]

def Core.hasAHRank (positions : List AHPosition) (r : Nat) : Bool

Whether a list of AH positions contains at least one position at rank r.

Equations

• Core.hasAHRank positions r = positions.any fun (p : Core.AHPosition) => p.rank == r

def Core.contiguousOnAH (positions : List AHPosition) : Bool

A set of AH positions forms a contiguous segment on the hierarchy: for every pair of positions in the set, every intermediate rank is also represented.

Mirrors Core.validInventory for the case hierarchy (@cite{blake-1994}).

This formalizes HC₂ of @cite{keenan-comrie-1977}: "Any RC-forming strategy must apply to a continuous segment of the AH."

Equations

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

def Core.ContiguousOnAH (positions : List AHPosition) : Prop

Prop wrapper around contiguousOnAH. The Bool-shaped definition is structural and load-bearing for the PRC general-proof case-analysis in Phenomena/Relativization/Studies/KeenanComrie1977.lean; this Prop version is the canonical user-facing predicate.

Equations

• Core.ContiguousOnAH positions = (Core.contiguousOnAH positions = true)

@[implicit_reducible]

instance Core.instDecidableContiguousOnAH (positions : List AHPosition) : Decidable (ContiguousOnAH positions)

Equations

• Core.instDecidableContiguousOnAH positions = Core.instDecidableContiguousOnAH._aux_1 positions

def Core.RelClauseMarker.IsContinuous (m : RelClauseMarker) : Prop

A marker's positions form a contiguous segment of the AH.

Equations

• m.IsContinuous = Core.ContiguousOnAH m.positions

@[implicit_reducible]

instance Core.instDecidableIsContinuous (m : RelClauseMarker) : Decidable m.IsContinuous

Equations

• Core.instDecidableIsContinuous m = Core.instDecidableIsContinuous._aux_1 m

def Core.RelClauseMarker.IsPrimary (m : RelClauseMarker) : Prop

A marker is primary (in K&C 1977's sense, p. 67-68) if it can be used to relativize subjects. HC₁ requires every language to have at least one primary marker.

Equations

• m.IsPrimary = m.Covers Core.AHPosition.subject

@[implicit_reducible]

instance Core.instDecidableIsPrimary (m : RelClauseMarker) : Decidable m.IsPrimary

Equations

• Core.instDecidableIsPrimary m = Core.instDecidableIsPrimary._aux_1 m

def Core.RelClauseMarker.isPrimary (m : RelClauseMarker) : Bool

Bool version of IsPrimary, retained as a transitional shim for Bool-list equality theorems ((markers.map (·.isPrimary)) = [true, ...]).

Equations

• m.isPrimary = m.covers Core.AHPosition.subject

def Core.RelClauseMarker.isContinuous (m : RelClauseMarker) : Bool

Bool version of RelClauseMarker.IsContinuous, retained as a transitional shim while StrategyEntry (slated for deletion in the K&C study refactor) still consumes Bool-shaped contiguity.

Equations

• m.isContinuous = Core.contiguousOnAH m.positions

@[simp]

theorem Core.RelClauseMarker.isContinuous_eq (m : RelClauseMarker) : m.isContinuous = contiguousOnAH m.positions

theorem Core.ah_rank_injective (a b : AHPosition) (h : a.rank = b.rank) : a = b

The hierarchy rank is injective — no two positions share a rank. Combined with the natural order on ℕ, this makes the AH a total order.

theorem Core.ah_rank_bounded (p : AHPosition) : 1 ≤ p.rank ∧ p.rank ≤ 6

All ranks are between 1 and 6.

theorem Core.ah_reflexive (p : AHPosition) : p.atLeastAsAccessible p

Accessibility is reflexive (follows from ≥ on ℕ).

theorem Core.ah_transitive (a b c : AHPosition) (h1 : a.atLeastAsAccessible b) (h2 : b.atLeastAsAccessible c) : a.atLeastAsAccessible c

Accessibility is transitive (follows from ≥ on ℕ).

The K&C-anchored contiguity examples and the Primary Relativization Constraint general proof live in Phenomena/Relativization/Studies/KeenanComrie1977.lean.