The P-Constraint

@cite{pancheva-zubizarreta-2018}

A parametric theory of person-sensitivity in clitic clusters, due to @cite{pancheva-zubizarreta-2018}. The P-Constraint is triggered by an interpretable person feature on Appl, which marks the indirect object as a point-of-view center (a logophoric pivot/self/source in the sense of @cite{sells-1987}).

Architecture

Empirical predictions for the eight named grammar instances, and the correspondence P&Z draw between P-Prominence settings and Sells's logophoric roles (§6.2), live in the study file Phenomena/Agreement/Studies/PanchevaZubizarreta2018.lean. This file holds only the framework-neutral parametric API — no commitment to any particular theory of logophoric roles:

• PProminence — what the IO must satisfy (proximate, participant, author)
• PCCGrammar — a Fintype parameter space (24 grammars total)
• The four parametric clauses as named Prop predicates with Decidable instances: DomainExempt, IOSatisfiesProminence, UniquenessSatisfied, PrimacyRescues
• IsLicit — the main predicate, defined as the disjunction implementing the algorithm of (12)
• licitFinset, licitCount — empirical-prediction enumeration via Finset.filter
• ApplDomain and PConstraintSatisfied — a minimal semantic model in which IsLicit is derived from selecting the IO as POV center
• Preorder PCCGrammar — entailment by licit-set containment

Convention deviation

IsLicit is the canonical Prop-valued predicate. The earlier pccLicit : ... → Bool API has been removed. Use IsLicit g io do_ and its Decidable instance directly; for proofs about specific cells, prefer by decide.

inductive Minimalist.PConstraint.PProminence : Type

P-Prominence settings. The interpretable person feature on Appl requires a DP at the phase edge to bear one of these positive specifications. The settings are framework-neutral feature specifications; @cite{pancheva-zubizarreta-2018} §6.2 give them a logophoric reading (proximate↔pivot, participant↔self, author↔source) that lives in the study file.

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

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableEqPProminence : DecidableEq PProminence

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instReprPProminence : Repr PProminence

Equations

• Minimalist.PConstraint.instReprPProminence = { reprPrec := Minimalist.PConstraint.instReprPProminence.repr }

def Minimalist.PConstraint.instReprPProminence.repr : PProminence → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instFintypePProminence : Fintype PProminence

Equations

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

structure Minimalist.PConstraint.PCCGrammar : Type

A PCC grammar, parameterized by the four binary settings of the P-Constraint (@cite{pancheva-zubizarreta-2018} (12)).

The 24-element parameter space (3 prominence values × 2³ Bool flags) is enumerated by the Fintype instance below.

• prominence : PProminence

  P-Prominence: what feature value the IO must inherit at the phase edge. Default: .proximate.

• uniqueness : Bool

  P-Uniqueness: at most one DP can agree with the interpretable person feature on Appl. Default: true (active).

• primacy : Bool

  P-Primacy: when both DPs satisfy P-Prominence, the [+author] DP takes priority. Conditional on P-Uniqueness. Default: false.

• restrictedDomain : Bool

  Domain: whether the interpretable person feature is present on ALL Appl heads (false = default), or only when a [+author] DP is present (true = restricted).

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableEqPCCGrammar : DecidableEq PCCGrammar

Equations

• Minimalist.PConstraint.instDecidableEqPCCGrammar = Minimalist.PConstraint.instDecidableEqPCCGrammar.decEq

def Minimalist.PConstraint.instDecidableEqPCCGrammar.decEq (x✝ x✝¹ : PCCGrammar) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.PConstraint.instReprPCCGrammar.repr : PCCGrammar → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instReprPCCGrammar : Repr PCCGrammar

Equations

• Minimalist.PConstraint.instReprPCCGrammar = { reprPrec := Minimalist.PConstraint.instReprPCCGrammar.repr }

def Minimalist.PConstraint.PCCGrammar.equivQuadruple : PCCGrammar ≃ PProminence × Bool × Bool × Bool

PCCGrammar is in bijection with PProminence × Bool × Bool × Bool.

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instFintypePCCGrammar : Fintype PCCGrammar

Equations

• Minimalist.PConstraint.instFintypePCCGrammar = Fintype.ofEquiv (Minimalist.PConstraint.PProminence × Bool × Bool × Bool) Minimalist.PConstraint.PCCGrammar.equivQuadruple.symm

def Minimalist.PConstraint.strongGrammar : PCCGrammar

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

Equations

• Minimalist.PConstraint.strongGrammar = { }

def Minimalist.PConstraint.ultraStrongGrammar : PCCGrammar

Ultra-strong PCC — adds P-Primacy. Allows ⟨1,2⟩ but not ⟨2,1⟩.

Equations

• Minimalist.PConstraint.ultraStrongGrammar = { primacy := true }

def Minimalist.PConstraint.weakGrammar : PCCGrammar

Weak PCC — drops P-Uniqueness. Allows SAP co-occurrence.

Equations

• Minimalist.PConstraint.weakGrammar = { uniqueness := false }

def Minimalist.PConstraint.superStrongGrammar : PCCGrammar

Super-strong PCC — [+participant] prominence. IO must be SAP.

Equations

• Minimalist.PConstraint.superStrongGrammar = { prominence := Minimalist.PConstraint.PProminence.participant }

def Minimalist.PConstraint.meFirstGrammar : PCCGrammar

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

Equations

• Minimalist.PConstraint.meFirstGrammar = { prominence := Minimalist.PConstraint.PProminence.author, restrictedDomain := true }

def Minimalist.PConstraint.pg1Grammar : PCCGrammar

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

Equations

• Minimalist.PConstraint.pg1Grammar = { prominence := Minimalist.PConstraint.PProminence.participant, primacy := true }

def Minimalist.PConstraint.pg2Grammar : PCCGrammar

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

Equations

• Minimalist.PConstraint.pg2Grammar = { prominence := Minimalist.PConstraint.PProminence.participant, uniqueness := false }

def Minimalist.PConstraint.pg3Grammar : PCCGrammar

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

Equations

• Minimalist.PConstraint.pg3Grammar = { prominence := Minimalist.PConstraint.PProminence.author }

def Minimalist.PConstraint.IsInherentlyProximate (p : Features.Prominence.PersonLevel) : Prop

A DP is inherently [+PROXIMATE] iff it is a SAP (@cite{pancheva-zubizarreta-2018} (11)). Third person can only be [+PROXIMATE] contextually.

Equations

• Minimalist.PConstraint.IsInherentlyProximate p = ((Minimalist.decomposePerson p).hasProximate = true)

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableIsInherentlyProximate (p : Features.Prominence.PersonLevel) : Decidable (IsInherentlyProximate p)

Equations

• Minimalist.PConstraint.instDecidableIsInherentlyProximate p = Minimalist.PConstraint.instDecidableIsInherentlyProximate._aux_1 p

def Minimalist.PConstraint.SatisfiesProminence (s : PProminence) (p : Features.Prominence.PersonLevel) : Prop

A DP inherently satisfies a P-Prominence setting.

Equations

• Minimalist.PConstraint.SatisfiesProminence Minimalist.PConstraint.PProminence.proximate p = ((Minimalist.decomposePerson p).hasProximate = true)
• Minimalist.PConstraint.SatisfiesProminence Minimalist.PConstraint.PProminence.participant p = ((Minimalist.decomposePerson p).hasParticipant = true)
• Minimalist.PConstraint.SatisfiesProminence Minimalist.PConstraint.PProminence.author p = ((Minimalist.decomposePerson p).hasAuthor = true)

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableSatisfiesProminence (s : PProminence) (p : Features.Prominence.PersonLevel) : Decidable (SatisfiesProminence s p)

Equations

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

def Minimalist.PConstraint.DomainExempt (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Prop

Clause (12a) — Domain. When the domain is restricted and no [+author] DP is present, the P-Constraint does not apply.

Equations

• Minimalist.PConstraint.DomainExempt g io do_ = (g.restrictedDomain = true ∧ (Minimalist.decomposePerson io).hasAuthor = false ∧ (Minimalist.decomposePerson do_).hasAuthor = false)

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableDomainExempt (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Decidable (DomainExempt g io do_)

Equations

• Minimalist.PConstraint.instDecidableDomainExempt g io do_ = Minimalist.PConstraint.instDecidableDomainExempt._aux_1 g io do_

def Minimalist.PConstraint.IOSatisfiesProminence (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Prop

Clause (12b) — P-Prominence. The IO satisfies the prominence requirement, either inherently or — for .proximate only — by contextual marking when paired with another non-proximate 3P (@cite{pancheva-zubizarreta-2018} §4.1.4).

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableIOSatisfiesProminence (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Decidable (IOSatisfiesProminence g io do_)

Equations

• Minimalist.PConstraint.instDecidableIOSatisfiesProminence g io do_ = Minimalist.PConstraint.instDecidableIOSatisfiesProminence._aux_1 g io do_

def Minimalist.PConstraint.UniquenessSatisfied (g : PCCGrammar) (do_ : Features.Prominence.PersonLevel) : Prop

Clause (12c) — P-Uniqueness. The DO does not also inherently satisfy the prominence requirement. (Contextual proximate-marking on the IO does not propagate to the DO.)

Equations

• Minimalist.PConstraint.UniquenessSatisfied g do_ = ¬Minimalist.PConstraint.SatisfiesProminence g.prominence do_

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableUniquenessSatisfied (g : PCCGrammar) (do_ : Features.Prominence.PersonLevel) : Decidable (UniquenessSatisfied g do_)

Equations

• Minimalist.PConstraint.instDecidableUniquenessSatisfied g do_ = Minimalist.PConstraint.instDecidableUniquenessSatisfied._aux_1 g do_

def Minimalist.PConstraint.PrimacyRescues (g : PCCGrammar) (io : Features.Prominence.PersonLevel) : Prop

Clause (12d) — P-Primacy. When P-Uniqueness would block, a [+author] IO rescues.

Equations

• Minimalist.PConstraint.PrimacyRescues g io = (g.primacy = true ∧ (Minimalist.decomposePerson io).hasAuthor = true)

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidablePrimacyRescues (g : PCCGrammar) (io : Features.Prominence.PersonLevel) : Decidable (PrimacyRescues g io)

Equations

• Minimalist.PConstraint.instDecidablePrimacyRescues g io = Minimalist.PConstraint.instDecidablePrimacyRescues._aux_1 g io

def Minimalist.PConstraint.IsLicit (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Prop

The PCC verdict on a ⟨IO, DO⟩ person combination under grammar g.

Implements (12) compositionally:

• Domain-exempt configurations are vacuously licit.
• Otherwise, the IO must satisfy P-Prominence; and either P-Uniqueness is inactive, or it is satisfied, or P-Primacy rescues.

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableIsLicit (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : Decidable (IsLicit g io do_)

Equations

• Minimalist.PConstraint.instDecidableIsLicit g io do_ = Minimalist.PConstraint.instDecidableIsLicit._aux_1 g io do_

def Minimalist.PConstraint.licitFinset (g : PCCGrammar) : Finset (Features.Prominence.PersonLevel × Features.Prominence.PersonLevel)

The set of person combinations the grammar predicts to be licit.

Equations

• Minimalist.PConstraint.licitFinset g = {p : Features.Prominence.PersonLevel × Features.Prominence.PersonLevel | Minimalist.PConstraint.IsLicit g p.1 p.2}

def Minimalist.PConstraint.licitCount (g : PCCGrammar) : ℕ

Cardinality of the licit set (out of 9 total combinations).

Equations

• Minimalist.PConstraint.licitCount g = (Minimalist.PConstraint.licitFinset g).card

@[simp]

theorem Minimalist.PConstraint.mem_licitFinset (g : PCCGrammar) (p : Features.Prominence.PersonLevel × Features.Prominence.PersonLevel) : p ∈ licitFinset g ↔ IsLicit g p.1 p.2

def Minimalist.PConstraint.parameterDepartures (g : PCCGrammar) : ℕ

Number of parametric departures from the default (strong PCC). This is the markedness rank — strong = 0, ultra/weak/super/pg3 = 1, me-first/pg1/pg2 = 2 (@cite{pancheva-zubizarreta-2018} §4.5 (31)).

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instLEPCCGrammar : LE PCCGrammar

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instPreorderPCCGrammar : Preorder PCCGrammar

Equations

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

@[implicit_reducible]

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

Equations

• Minimalist.PConstraint.instDecidableLePCCGrammar g₁ g₂ = (Minimalist.PConstraint.licitFinset g₁).instDecidableRelSubset (Minimalist.PConstraint.licitFinset g₂)

theorem Minimalist.PConstraint.le_iff_isLicit_imp (g₁ g₂ : PCCGrammar) : g₁ ≤ g₂ ↔ ∀ (io do_ : Features.Prominence.PersonLevel), IsLicit g₁ io do_ → IsLicit g₂ io do_

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

structure Minimalist.PConstraint.ApplDomain : Type

A minimal model of the Appl phase: the two arguments and the chosen point-of-view center. The interpretable person feature on Appl (@cite{pancheva-zubizarreta-2018} (10)) marks one DP as the perspectival center; in the unmarked case this is the IO at the phase edge.

• io : Features.Prominence.PersonLevel

  The indirect-object argument introduced by Appl.

• do_ : Features.Prominence.PersonLevel

  The direct-object argument inside VP.

• povCenter : Features.Prominence.PersonLevel

  The DP selected as point-of-view center within the phase.

def Minimalist.PConstraint.instDecidableEqApplDomain.decEq (x✝ x✝¹ : ApplDomain) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidableEqApplDomain : DecidableEq ApplDomain

Equations

• Minimalist.PConstraint.instDecidableEqApplDomain = Minimalist.PConstraint.instDecidableEqApplDomain.decEq

def Minimalist.PConstraint.instReprApplDomain.repr : ApplDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instReprApplDomain : Repr ApplDomain

Equations

• Minimalist.PConstraint.instReprApplDomain = { reprPrec := Minimalist.PConstraint.instReprApplDomain.repr }

def Minimalist.PConstraint.ApplDomain.povIsIO (a : ApplDomain) : Prop

The IO is the canonical POV-center candidate (@cite{pancheva-zubizarreta-2018} page 1320).

Equations

• a.povIsIO = (a.povCenter = a.io)

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidablePovIsIO (a : ApplDomain) : Decidable a.povIsIO

Equations

• Minimalist.PConstraint.instDecidablePovIsIO a = Minimalist.PConstraint.instDecidablePovIsIO._aux_1 a

def Minimalist.PConstraint.PConstraintSatisfied (g : PCCGrammar) (a : ApplDomain) : Prop

The P-Constraint as a semantic predicate over an Appl domain. A domain satisfies the P-Constraint iff either it is exempt, or the POV center is the IO and the IO inherits the prominence value with uniqueness/primacy as required.

Equations

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

@[implicit_reducible]

instance Minimalist.PConstraint.instDecidablePConstraintSatisfied (g : PCCGrammar) (a : ApplDomain) : Decidable (PConstraintSatisfied g a)

Equations

• Minimalist.PConstraint.instDecidablePConstraintSatisfied g a = Minimalist.PConstraint.instDecidablePConstraintSatisfied._aux_1 g a

theorem Minimalist.PConstraint.isLicit_iff_exists_appl_satisfying (g : PCCGrammar) (io do_ : Features.Prominence.PersonLevel) : IsLicit g io do_ ↔ ∃ (a : ApplDomain), a.io = io ∧ a.do_ = do_ ∧ PConstraintSatisfied g a

Central derivation. A ⟨IO, DO⟩ combination is licit iff there exists an Appl domain over those arguments — with the IO chosen as POV center — that satisfies the P-Constraint. The four parametric clauses are not stipulated verdicts; they are the conditions under which IO-as-POV-center is consistent with the interpretable person feature on Appl.