The Person Case Constraint

The Person Case Constraint restricts which combinations of indirect and direct object person a clitic cluster can realize, the classic ban of French me lui. A combination is a scenario (Clause.Scenario) of the indirect over the direct object. This file defines the four-parameter P-Constraint grammars that generate the varieties (strong, ultra-strong, weak, super-strong, me-first, and the predicted PG1–PG3), whose prominence thresholds are cuts on the entailment chain [author] ⟹ [participant] ⟹ [proximate], denoting Person.IncludesSpeaker and Person.IsSAP, so the person hierarchy enters as a theorem (inherentlyMetBy_antitone). 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 these grammars.

Main declarations

• PCC.Grammar, PCC.IsLicit: the P-Constraint grammars and the combinations they license.
• PCC.cliticPairs, PCC.distinctPairs: the combinations of the person tripartition, with and without the reflexive diagonal.

References

• [Bon91]
• [Nev07]
• [PZ18]
• [BR09]
• [CK21]
• [Dea24]

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

inductive PCC.ProminenceThreshold : Type

The prominence a grammar requires of its IO is 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 meeting proximate and participant and the speaker 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

Raising the threshold only shrinks the set of persons that inherently meet it.

The PCC grammar

structure PCC.Grammar : Type

A PCC grammar sets 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

  The threshold of P-Prominence, which the IO must meet.

• uniqueness : Bool

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

• primacy : Bool

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

• restrictedDomain : Bool

  On a 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

The strong PCC keeps all defaults, so the DO must be 3P.

Equations

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

def PCC.ultraStrongGrammar : Grammar

The ultra-strong PCC adds P-Primacy, so ⟨1,2⟩ is licit and ⟨2,1⟩ not.

Equations

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

def PCC.weakGrammar : Grammar

The weak PCC drops P-Uniqueness, so SAPs may co-occur.

Equations

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

def PCC.superStrongGrammar : Grammar

The super-strong PCC has participant prominence, so the IO must be a SAP and ⟨3,3⟩ is banned.

Equations

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

def PCC.meFirstGrammar : Grammar

The me-first PCC has 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

The predicted PG1 has 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

The predicted PG2 has 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

The predicted PG3 has 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) (s : Clause.Scenario 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.instDecidablePredScenarioPersonIOSatisfiesProminence (g : Grammar) : DecidablePred (IOSatisfiesProminence g)

Equations

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

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_ = { decide := !decide (g.prominence.InherentlyMetBy do_), reflects_decide := ⋯ }

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), that 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, which [Dea24]'s table (1) leaves out.

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 = { decide := decide (g.primacy = true) && decide io.IncludesSpeaker, reflects_decide := ⋯ }

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) (s : Clause.Scenario Person) : Prop

(12a) A combination is domain-exempt on a restricted domain when no DP bears 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 s = (g.restrictedDomain = true ∧ ¬g.prominence.InherentlyMetBy s.high ∧ ¬g.prominence.InherentlyMetBy s.low)

@[instance_reducible]

instance PCC.instDecidablePredScenarioPersonDomainExempt (g : Grammar) : DecidablePred (DomainExempt g)

Equations

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

Licit person combinations

def PCC.IsLicit (g : Grammar) (s : Clause.Scenario Person) : Prop

A combination of IO over DO is licit under g when the domain restriction exempts it, 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 s = (PCC.DomainExempt g s ∨ PCC.IOSatisfiesProminence g s ∧ (g.uniqueness = true → PCC.UniquenessSatisfied g s.low ∨ PCC.PrimacyRescues g s.high))

@[instance_reducible]

instance PCC.instDecidablePredScenarioPersonIsLicit (g : Grammar) : DecidablePred (IsLicit g)

Equations

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

def PCC.persons : Finset Person

The persons of the tripartition, over which the typology is stated.

Equations

• PCC.persons = {Person.first, Person.second, Person.third}

def PCC.cliticPairs : Finset (Clause.Scenario Person)

The prediction domain is the combinations of the tripartition.

Equations

• PCC.cliticPairs = Finset.map Clause.Scenario.equivProd.symm.toEmbedding (PCC.persons ×ˢ PCC.persons)

def PCC.distinctPairs : Finset (Clause.Scenario Person)

The combinations of distinct persons, without the reflexive diagonal.

Equations

• PCC.distinctPairs = Finset.map Clause.Scenario.equivProd.symm.toEmbedding PCC.persons.offDiag

def PCC.licitFinset (g : Grammar) : Finset (Clause.Scenario Person)

The person combinations g predicts licit.

Equations

• PCC.licitFinset g = {s ∈ PCC.cliticPairs | PCC.IsLicit g s}

@[simp]

theorem PCC.mem_licitFinset (g : Grammar) (s : Clause.Scenario Person) : s ∈ licitFinset g ↔ s ∈ cliticPairs ∧ IsLicit g s

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

The order is only a preorder, since distinct parameter settings can share a licit set: the restricted-domain [+participant] grammar surfaces as the strong PCC (PanchevaZubizarreta2018.restricted_participant_surfaces_as_strong).

@[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

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

theorem PCC.le_iff_isLicit_imp (g₁ g₂ : Grammar) : g₁ ≤ g₂ ↔ ∀ s ∈ cliticPairs, IsLicit g₁ s → IsLicit g₂ s

One grammar entails another when every combination licit in the first is licit in the second.