The Person Case Constraint (theory-neutral)

[PZ18] [nevins-2007] [Bon91]

The PCC restricts which ⟨IO-person, DO-person⟩ combinations a single probe can license in a clitic cluster. It is person-feature combinatorics, not a syntactic primitive: the licit region of each grammar is determined order-theoretically by the [author] ⟹ [participant] ⟹ [proximate] entailment chain (Nevins 2007's feature calculus, adopted by [PZ18] (11)), and the variants (strong/weak/ultra-strong/ …) are points in a parameter lattice. So it lives on the person feature, not in the syntax. The Minimalist application — the interpretable p-feature on Appl, the phase edge — is the consumer (PConstraintSatisfied), kept separately.

Formerly Syntax/Minimalist/PConstraint.lean.

Person prominence, derived from feature containment

Person.Features (Features/Person/Decomposition.lean) already carries the [±participant, ±author] decomposition with its containment order (author ⊏ participant). A person's prominence is read off it. Inherently [+proximate] = [+participant] (1P/2P are proximate, 3P is not); the proximate/participant grammars differ only in the contextual clause ([PZ18]: a 3P IO may count as proximate when paired with another 3P), encoded in IOSatisfiesProminence.

Theory-neutral person-feature accessors

def PCC.hasAuthor (p : Person) : Bool

[+author] of a person, via the theory-neutral decomposition.

Equations

• PCC.hasAuthor p = p.toFeatures.elim false fun (x : Person.Features) => x.hasAuthor

def PCC.hasParticipant (p : Person) : Bool

[+participant] of a person, via the theory-neutral decomposition.

Equations

• PCC.hasParticipant p = p.toFeatures.elim false fun (x : Person.Features) => x.hasParticipant

P-Prominence: a cut on the [author] ⟹ [participant] ⟹ [proximate] chain

inductive PCC.PProminence : Type

The value the interpretable p-feature on the head requires of the IO ([PZ18] (12b)). proximate is the default (least restrictive); participant and author are the marked, more restrictive thresholds.

• proximate : PProminence
• participant : PProminence
• author : PProminence

@[implicit_reducible]

instance PCC.instDecidableEqPProminence : DecidableEq PProminence

Equations

• PCC.instDecidableEqPProminence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PCC.instReprPProminence.repr : PProminence → ℕ → Std.Format

Equations

• PCC.instReprPProminence.repr PCC.PProminence.proximate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCC.PProminence.proximate")).group prec✝
• PCC.instReprPProminence.repr PCC.PProminence.participant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCC.PProminence.participant")).group prec✝
• PCC.instReprPProminence.repr PCC.PProminence.author prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCC.PProminence.author")).group prec✝

@[implicit_reducible]

instance PCC.instReprPProminence : Repr PProminence

Equations

• PCC.instReprPProminence = { reprPrec := PCC.instReprPProminence.repr }

@[implicit_reducible]

instance PCC.instFintypePProminence : Fintype PProminence

Equations

• PCC.instFintypePProminence = { elems := { val := ↑PCC.PProminence.enumList, nodup := PCC.PProminence.enumList_nodup }, complete := PCC.instFintypePProminence._proof_1 }

def PCC.PProminence.satisfiedInherentlyBy : PProminence → Person → Bool

A person inherently satisfies a prominence threshold. The sets nest by feature containment (prominence_inherent_nested): author ⊆ participant = proximate.

Equations

• PCC.PProminence.proximate.satisfiedInherentlyBy = PCC.hasParticipant
• PCC.PProminence.participant.satisfiedInherentlyBy = PCC.hasParticipant
• PCC.PProminence.author.satisfiedInherentlyBy = PCC.hasAuthor

theorem PCC.prominence_inherent_nested (p : Person) : (PProminence.author.satisfiedInherentlyBy p = true → PProminence.participant.satisfiedInherentlyBy p = true) ∧ (PProminence.participant.satisfiedInherentlyBy p = true ↔ PProminence.proximate.satisfiedInherentlyBy p = true)

Prominence is an order-ideal on the person prominence chain ([nevins-2007]'s [author] ⟹ [participant] ⟹ [proximate]): the author-satisfiers are contained in the participant-satisfiers, which equal the (inherent) proximate-satisfiers. The person hierarchy is thus a theorem of feature containment, not a stipulated primitive.

The PCC grammar — a constrained parameter lattice

A grammar is the four parameters of [PZ18] (12), with the dependency P-Primacy ⟹ P-Uniqueness (Primacy presupposes active Uniqueness) carried as a well-formedness invariant, so the impossible corner does not exist.

structure PCC.RawGrammar : Type

The raw four-parameter grammar ([PZ18] (12)).

• prominence : PProminence

  P-Prominence: the threshold the IO must meet (always active; default .proximate).

• uniqueness : Bool

  P-Uniqueness: at most one DP agrees with the p-feature (default active).

• primacy : Bool

  P-Primacy: a [+author] DP wins a tie; presupposes P-Uniqueness (default off).

• restrictedDomain : Bool

  Domain: p-feature on all Appl heads (default), or only with a relevant DP.

def PCC.instDecidableEqRawGrammar.decEq (x✝ x✝¹ : RawGrammar) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance PCC.instDecidableEqRawGrammar : DecidableEq RawGrammar

Equations

• PCC.instDecidableEqRawGrammar = PCC.instDecidableEqRawGrammar.decEq

@[implicit_reducible]

instance PCC.instReprRawGrammar : Repr RawGrammar

Equations

• PCC.instReprRawGrammar = { reprPrec := PCC.instReprRawGrammar.repr }

def PCC.instReprRawGrammar.repr : RawGrammar → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance PCC.instFintypeRawGrammar : Fintype RawGrammar

Equations

• PCC.instFintypeRawGrammar = Fintype.ofEquiv ((_ : PCC.PProminence) × (_ : Bool) × (_ : Bool) × Bool) PCC.RawGrammar.proxyTypeEquiv

def PCC.RawGrammar.WellFormed (g : RawGrammar) : Prop

Well-formedness: P-Primacy presupposes active P-Uniqueness.

Equations

• g.WellFormed = (g.primacy = true → g.uniqueness = true)

@[implicit_reducible]

instance PCC.instDecidableWellFormed (g : RawGrammar) : Decidable g.WellFormed

Equations

• PCC.instDecidableWellFormed g = PCC.instDecidableWellFormed._aux_1 g

def PCC.PCCGrammar : Type

A PCC grammar: the four parameters subject to primacy ⟹ uniqueness. The impossible (Primacy-on, Uniqueness-off) corner is excluded by construction.

Equations

• PCC.PCCGrammar = { g : PCC.RawGrammar // g.WellFormed }

@[implicit_reducible]

instance PCC.instDecidableEqPCCGrammar : DecidableEq PCCGrammar

Equations

• PCC.instDecidableEqPCCGrammar = Subtype.instDecidableEq

@[implicit_reducible]

instance PCC.instFintypePCCGrammar : Fintype PCCGrammar

Equations

• PCC.instFintypePCCGrammar = Subtype.fintype PCC.RawGrammar.WellFormed

def PCC.mkGrammar (prominence : PProminence := PProminence.proximate) (uniqueness : Bool := true) (primacy restrictedDomain : Bool := false) (h : { prominence := prominence, uniqueness := uniqueness, primacy := primacy, restrictedDomain := restrictedDomain }.WellFormed := by decide) : PCCGrammar

Build a PCCGrammar, discharging well-formedness by decide.

Equations

• PCC.mkGrammar prominence uniqueness primacy restrictedDomain h = ⟨{ prominence := prominence, uniqueness := uniqueness, primacy := primacy, restrictedDomain := restrictedDomain }, h⟩

def PCC.PCCGrammar.prominence (g : PCCGrammar) : PProminence

Accessor: the prominence threshold.

Equations

• g.prominence = (↑g).prominence

def PCC.PCCGrammar.uniqueness (g : PCCGrammar) : Bool

Accessor: P-Uniqueness.

Equations

• g.uniqueness = (↑g).uniqueness

def PCC.PCCGrammar.primacy (g : PCCGrammar) : Bool

Accessor: P-Primacy.

Equations

• g.primacy = (↑g).primacy

def PCC.PCCGrammar.restrictedDomain (g : PCCGrammar) : Bool

Accessor: restricted domain.

Equations

• g.restrictedDomain = (↑g).restrictedDomain

Named grammars ([PZ18] (31)–(34))

def PCC.strongGrammar : PCCGrammar

Strong PCC — all defaults. DO must be 3P.

Equations

• PCC.strongGrammar = PCC.mkGrammar PCC.PProminence.proximate true false false PCC.strongGrammar._proof_1

def PCC.ultraStrongGrammar : PCCGrammar

Ultra-strong PCC — adds P-Primacy (allows ⟨1,2⟩, not ⟨2,1⟩).

Equations

• PCC.ultraStrongGrammar = PCC.mkGrammar PCC.PProminence.proximate true true false PCC.ultraStrongGrammar._proof_1

def PCC.weakGrammar : PCCGrammar

Weak PCC — drops P-Uniqueness (allows SAP co-occurrence).

Equations

• PCC.weakGrammar = PCC.mkGrammar PCC.PProminence.proximate false false false PCC.weakGrammar._proof_1

def PCC.superStrongGrammar : PCCGrammar

Super-strong PCC — [+participant] prominence (IO must be SAP, bans ⟨3,3⟩).

Equations

• PCC.superStrongGrammar = PCC.mkGrammar PCC.PProminence.participant true false false PCC.superStrongGrammar._proof_1

def PCC.meFirstGrammar : PCCGrammar

Me-first PCC — [+author] prominence, restricted domain.

Equations

• PCC.meFirstGrammar = PCC.mkGrammar PCC.PProminence.author true false true PCC.meFirstGrammar._proof_1

def PCC.pg1Grammar : PCCGrammar

PG1 (predicted): [+participant] + P-Primacy.

Equations

• PCC.pg1Grammar = PCC.mkGrammar PCC.PProminence.participant true true false PCC.pg1Grammar._proof_1

def PCC.pg2Grammar : PCCGrammar

PG2 (predicted): [+participant], no P-Uniqueness.

Equations

• PCC.pg2Grammar = PCC.mkGrammar PCC.PProminence.participant false false false PCC.pg2Grammar._proof_1

def PCC.pg3Grammar : PCCGrammar

PG3 (predicted): [+author], unrestricted domain.

Equations

• PCC.pg3Grammar = PCC.mkGrammar PCC.PProminence.author true false false PCC.pg3Grammar._proof_1

Subpredicates — the four clauses of (12)

def PCC.IOSatisfiesProminence (g : PCCGrammar) (io do_ : Person) : Prop

(12b) The IO satisfies P-Prominence, inherently or — for .proximate only — by contextual marking when paired with another non-proximate 3P.

Equations

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

@[implicit_reducible]

instance PCC.instDecidableIOSatisfiesProminence (g : PCCGrammar) (io do_ : Person) : Decidable (IOSatisfiesProminence g io do_)

Equations

• PCC.instDecidableIOSatisfiesProminence g io do_ = PCC.instDecidableIOSatisfiesProminence._aux_1 g io do_

def PCC.UniquenessSatisfied (g : PCCGrammar) (do_ : Person) : Prop

(12c) The DO does not also inherently satisfy P-Prominence.

Equations

• PCC.UniquenessSatisfied g do_ = ¬g.prominence.satisfiedInherentlyBy do_ = true

@[implicit_reducible]

instance PCC.instDecidableUniquenessSatisfied (g : PCCGrammar) (do_ : Person) : Decidable (UniquenessSatisfied g do_)

Equations

• PCC.instDecidableUniquenessSatisfied g do_ = PCC.instDecidableUniquenessSatisfied._aux_1 g do_

def PCC.PrimacyRescues (g : PCCGrammar) (io : Person) : Prop

(12d) A [+author] IO rescues an otherwise-blocking configuration when P-Primacy is on.

Equations

• PCC.PrimacyRescues g io = (g.primacy = true ∧ PCC.hasAuthor io = true)

@[implicit_reducible]

instance PCC.instDecidablePrimacyRescues (g : PCCGrammar) (io : Person) : Decidable (PrimacyRescues g io)

Equations

• PCC.instDecidablePrimacyRescues g io = PCC.instDecidablePrimacyRescues._aux_1 g io

def PCC.IsInherentlyProximate (p : Person) : Prop

A person is inherently [+proximate] iff it is a speech-act participant ([PZ18] (11)); a 3P is proximate only contextually.

Equations

• PCC.IsInherentlyProximate p = (PCC.hasParticipant p = true)

@[implicit_reducible]

instance PCC.instDecidableIsInherentlyProximate (p : Person) : Decidable (IsInherentlyProximate p)

Equations

• PCC.instDecidableIsInherentlyProximate p = PCC.instDecidableIsInherentlyProximate._aux_1 p

def PCC.DomainExempt (g : PCCGrammar) (io do_ : Person) : Prop

(12a) Domain-exempt: restricted domain with no [+author] DP present.

Equations

• PCC.DomainExempt g io do_ = (g.restrictedDomain = true ∧ PCC.hasAuthor io = false ∧ PCC.hasAuthor do_ = false)

@[implicit_reducible]

instance PCC.instDecidableDomainExempt (g : PCCGrammar) (io do_ : Person) : Decidable (DomainExempt g io do_)

Equations

• PCC.instDecidableDomainExempt g io do_ = PCC.instDecidableDomainExempt._aux_1 g io do_

Licit person combinations

def PCC.IsLicit (g : PCCGrammar) (io do_ : Person) : Prop

The PCC verdict on ⟨IO, DO⟩ under g, composing the four clauses of (12).

Equations

• PCC.IsLicit g io do_ = (PCC.DomainExempt g io do_ ∨ PCC.IOSatisfiesProminence g io do_ ∧ (g.uniqueness = false ∨ PCC.UniquenessSatisfied g do_ ∨ PCC.PrimacyRescues g io))

@[implicit_reducible]

instance PCC.instDecidableIsLicit (g : PCCGrammar) (io do_ : Person) : Decidable (IsLicit g io do_)

Equations

• PCC.instDecidableIsLicit g io do_ = PCC.instDecidableIsLicit._aux_1 g io do_

def PCC.cliticPairs : Finset (Person × Person)

The prediction domain: the 1/2/3 person tripartition.

Equations

• PCC.cliticPairs = {Person.first, Person.second, Person.third} ×ˢ {Person.first, Person.second, Person.third}

def PCC.licitFinset (g : PCCGrammar) : Finset (Person × Person)

The person combinations g predicts licit.

Equations

• PCC.licitFinset g = {p ∈ PCC.cliticPairs | PCC.IsLicit g p.1 p.2}

def PCC.licitCount (g : PCCGrammar) : ℕ

Cardinality of the licit set (out of 9).

Equations

• PCC.licitCount g = (PCC.licitFinset g).card

def PCC.parameterDepartures (g : PCCGrammar) : ℕ

Markedness rank: parametric departures from the default (strong PCC) ([PZ18] §4.5 (31)) — strong = 0.

Equations

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

@[simp]

theorem PCC.mem_licitFinset (g : PCCGrammar) (p : Person × Person) : p ∈ licitFinset g ↔ p ∈ cliticPairs ∧ IsLicit g p.1 p.2

The typology as a partial order (entailment by licit-set inclusion)

@[implicit_reducible]

instance PCC.instLEPCCGrammar : LE PCCGrammar

Equations

• PCC.instLEPCCGrammar = { le := fun (g₁ g₂ : PCC.PCCGrammar) => PCC.licitFinset g₁ ⊆ PCC.licitFinset g₂ }

@[implicit_reducible]

instance PCC.instPreorderPCCGrammar : Preorder PCCGrammar

Equations

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

@[implicit_reducible]

instance PCC.instDecidableLePCCGrammar (g₁ g₂ : PCCGrammar) : Decidable (g₁ ≤ g₂)

Equations

• PCC.instDecidableLePCCGrammar g₁ g₂ = (PCC.licitFinset g₁).instDecidableRelSubset (PCC.licitFinset g₂)

theorem PCC.le_iff_isLicit_imp (g₁ g₂ : PCCGrammar) : g₁ ≤ g₂ ↔ ∀ (io do_ : Person), (io, do_) ∈ cliticPairs → IsLicit g₁ io do_ → IsLicit g₂ io do_

Entailment unfolded: every licit cell of g₁ is licit in g₂.

theorem PCC.proximate_family_chain : strongGrammar ≤ ultraStrongGrammar ∧ ultraStrongGrammar ≤ weakGrammar

Within the proximate family the licit sets form a chain ([PZ18]): strong ⊆ ultra-strong ⊆ weak — monotone removal of P-Primacy then P-Uniqueness only enlarges the licit region. (Cross-family the typology is a lattice, not a chain: me-first/super-strong are incomparable.)