The Person Case Constraint

The PCC restricts which ⟨IO-person, DO-person⟩ combinations a clitic cluster can realize — the classic ban of French me lui. This file defines the descriptive typology of PCC varieties (strong, ultra-strong, weak, super-strong, me-first, and the predicted PG1–PG3). Prominence thresholds are cuts on the entailment chain [author] ⟹ [participant] ⟹ [proximate], denoting the person predicates Person.IncludesSpeaker and Person.IsSAP, so the person hierarchy enters as a theorem (inherentlyMetBy_antitone) rather than a stipulation. Grammars are preordered by inclusion of their licit regions (licitFinset).

Which mechanism enforces the constraint is left open here: a morphological filter, φ-Agree, and perspectival semantics have all been proposed. The rival accounts are formalized in their study files and compared cell-by-cell against this typology (Deal2024.strong_matches_pz, PanchevaZubizarreta2018.isLicit_iff_exists_appl_satisfying).

References

• [Bon91]: the original formulation, as a morphological filter
• [Nev07]: the strong/weak/ultra-strong/me-first taxonomy and the feature calculus
• [PZ18]: the four-parameter grammar (their (11)–(12)) formalized here
• [BR09], [CK21], [Dea24]: φ-Agree rivals, compared in Studies/

Prominence thresholds: cuts on the [author] ⟹ [participant] ⟹ [proximate] chain

inductive PCC.ProminenceThreshold : Type

The prominence a grammar requires of its IO: proximate (the default), participant, or author.

• proximate : ProminenceThreshold
• participant : ProminenceThreshold
• author : ProminenceThreshold

@[instance_reducible]

instance PCC.instDecidableEqProminenceThreshold : DecidableEq ProminenceThreshold

Equations

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

@[instance_reducible]

instance PCC.instReprProminenceThreshold : Repr ProminenceThreshold

Equations

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

def PCC.instReprProminenceThreshold.repr : ProminenceThreshold → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PCC.instFintypeProminenceThreshold : Fintype ProminenceThreshold

Equations

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

@[instance_reducible]

instance PCC.instLinearOrderProminenceThreshold : LinearOrder ProminenceThreshold

The restrictiveness chain proximate < participant < author.

Equations

• PCC.instLinearOrderProminenceThreshold = LinearOrder.lift' (fun (x : PCC.ProminenceThreshold) => x.ctorIdx) PCC.instLinearOrderProminenceThreshold._proof_1

def PCC.ProminenceThreshold.InherentlyMetBy : ProminenceThreshold → Person → Prop

A person meets a prominence threshold by its own features: speech-act participants meet proximate and participant, the speaker meets author. A 3P meets proximate only contextually (IOSatisfiesProminence).

Equations

• PCC.ProminenceThreshold.proximate.InherentlyMetBy = Person.IsSAP
• PCC.ProminenceThreshold.participant.InherentlyMetBy = Person.IsSAP
• PCC.ProminenceThreshold.author.InherentlyMetBy = Person.IncludesSpeaker

@[instance_reducible]

instance PCC.instDecidablePredPersonInherentlyMetBy (t : ProminenceThreshold) : DecidablePred t.InherentlyMetBy

Equations

• PCC.instDecidablePredPersonInherentlyMetBy PCC.ProminenceThreshold.proximate = PCC.instDecidablePredPersonInherentlyMetBy._aux_1
• PCC.instDecidablePredPersonInherentlyMetBy PCC.ProminenceThreshold.participant = PCC.instDecidablePredPersonInherentlyMetBy._aux_3
• PCC.instDecidablePredPersonInherentlyMetBy PCC.ProminenceThreshold.author = PCC.instDecidablePredPersonInherentlyMetBy._aux_5

theorem PCC.ProminenceThreshold.inherentlyMetBy_antitone (p : Person) : Antitone fun (x : ProminenceThreshold) => x.InherentlyMetBy p

Prominence is an order-ideal on the person prominence chain: raising the threshold only shrinks the set of persons that inherently meet it.

The PCC grammar

structure PCC.Grammar : Type

A PCC grammar is a setting of the four P-Constraint parameters: the prominence threshold, P-Uniqueness, P-Primacy, and the domain restriction. P-Primacy presupposes P-Uniqueness (primacy_le_uniqueness); field defaults are the paper's defaults, so {} is the strong PCC.

• prominence : ProminenceThreshold

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

• uniqueness : Bool

  P-Uniqueness: at most one DP may bear the required prominence.

• primacy : Bool

  P-Primacy: a [+author] IO wins a tie.

• restrictedDomain : Bool

  Restricted domain: the constraint applies only where a prominence-bearing DP is present.

• primacy_le_uniqueness : self.primacy ≤ self.uniqueness

  P-Primacy presupposes active P-Uniqueness.

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

def PCC.strongGrammar : Grammar

Strong PCC: all defaults; the DO must be 3P.

Equations

• PCC.strongGrammar = { primacy_le_uniqueness := PCC.strongGrammar._proof_1 }

def PCC.ultraStrongGrammar : Grammar

Ultra-strong PCC: adds P-Primacy; ⟨1,2⟩ licit, ⟨2,1⟩ not.

Equations

• PCC.ultraStrongGrammar = { primacy := true, primacy_le_uniqueness := PCC.ultraStrongGrammar._proof_1 }

def PCC.weakGrammar : Grammar

Weak PCC: drops P-Uniqueness; SAPs may co-occur.

Equations

• PCC.weakGrammar = { uniqueness := false, primacy_le_uniqueness := PCC.weakGrammar._proof_1 }

def PCC.superStrongGrammar : Grammar

Super-strong PCC: participant prominence; the IO must be a SAP, ⟨3,3⟩ banned.

Equations

• PCC.superStrongGrammar = { prominence := PCC.ProminenceThreshold.participant, primacy_le_uniqueness := PCC.strongGrammar._proof_1 }

def PCC.meFirstGrammar : Grammar

Me-first PCC: author prominence on a restricted domain.

Equations

• PCC.meFirstGrammar = { prominence := PCC.ProminenceThreshold.author, restrictedDomain := true, primacy_le_uniqueness := PCC.strongGrammar._proof_1 }

def PCC.pg1Grammar : Grammar

PG1 (predicted): participant prominence with P-Primacy.

Equations

• PCC.pg1Grammar = { prominence := PCC.ProminenceThreshold.participant, primacy := true, primacy_le_uniqueness := PCC.ultraStrongGrammar._proof_1 }

def PCC.pg2Grammar : Grammar

PG2 (predicted): participant prominence without P-Uniqueness.

Equations

• PCC.pg2Grammar = { prominence := PCC.ProminenceThreshold.participant, uniqueness := false, primacy_le_uniqueness := PCC.weakGrammar._proof_1 }

def PCC.pg3Grammar : Grammar

PG3 (predicted): author prominence on the unrestricted domain.

Equations

• PCC.pg3Grammar = { prominence := PCC.ProminenceThreshold.author, primacy_le_uniqueness := PCC.strongGrammar._proof_1 }

Subpredicates — the four clauses of (12)

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

(12b) The IO meets P-Prominence: inherently, or — under a proximate threshold only — by contextual marking when paired with another non-proximate 3P.

Equations

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

@[instance_reducible]

instance PCC.instDecidableIOSatisfiesProminence (g : Grammar) (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 : Grammar) (do_ : Person) : Prop

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

Equations

• PCC.UniquenessSatisfied g do_ = ¬g.prominence.InherentlyMetBy do_

@[instance_reducible]

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

Equations

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

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

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

The rescue checks only the IO, so primacy-active grammars license ⟨1,1⟩, where the paper's descriptive statement (14d) — the DO must be 2P or 3P — would forbid it (the paper never walks the mechanism through ⟨1,1⟩ for the [+proximate] family). The permissive reading is deliberate: rival probe-based accounts part ways with the P-Constraint at exactly this cell (Deal2024.sd_ultra_discrepancy_1_1).

Equations

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

@[instance_reducible]

instance PCC.instDecidablePrimacyRescues (g : Grammar) (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; a 3P is proximate only contextually.

Equations

• PCC.IsInherentlyProximate p = PCC.ProminenceThreshold.proximate.InherentlyMetBy p

@[instance_reducible]

instance PCC.instDecidablePredPersonIsInherentlyProximate : DecidablePred IsInherentlyProximate

Equations

• PCC.instDecidablePredPersonIsInherentlyProximate p = PCC.instDecidablePredPersonIsInherentlyProximate._aux_1 p

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

(12a) Domain-exempt: restricted domain with no DP bearing the prominence feature. The restriction presupposes an argument matching the P-Prominence value ([PZ18] §4.5: the restricted application "matches the feature value set in P-Prominence"; for me-first, ApplPs with a [+author] argument).

Equations

• PCC.DomainExempt g io do_ = (g.restrictedDomain = true ∧ ¬g.prominence.InherentlyMetBy io ∧ ¬g.prominence.InherentlyMetBy do_)

@[instance_reducible]

instance PCC.instDecidableDomainExempt (g : Grammar) (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 : Grammar) (io do_ : Person) : Prop

⟨IO, DO⟩ is licit under g: the domain restriction exempts the pair, or the IO meets P-Prominence and — when P-Uniqueness is active — the DO does not compete or P-Primacy rescues the tie.

Equations

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

@[instance_reducible]

instance PCC.instDecidableIsLicit (g : Grammar) (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 : Grammar) : Finset (Person × Person)

The person combinations g predicts licit.

Equations

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

@[simp]

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

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

Only a preorder: distinct parameter settings can share a licit set (e.g. the restricted-domain [+participant] grammar surfaces as the strong PCC, PanchevaZubizarreta2018.restricted_participant_surfaces_as_strong), so antisymmetry fails.

@[instance_reducible]

instance PCC.instPreorderGrammar : Preorder Grammar

Equations

• PCC.instPreorderGrammar = Preorder.lift PCC.licitFinset

@[instance_reducible]

instance PCC.instDecidableLeGrammar (g₁ g₂ : Grammar) : Decidable (g₁ ≤ g₂)

Equations

• PCC.instDecidableLeGrammar g₁ g₂ = (PCC.licitFinset g₁).instDecidableLE (PCC.licitFinset g₂)

theorem PCC.le_iff_isLicit_imp (g₁ g₂ : Grammar) : 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₂.