Null-Subject Typology: Pro-Drop and Overt PRO

Framework-agnostic substrate for the pro-drop / overt-PRO typology ([Ost26]): the loci where a language decides between null and overt subjects, the coarse two-Boolean profile, and the implicational universal stated over both the coarse profile and the fine per-context SubjectAssignment interface. Anti-agreement loci follow [Bai18].

Theory-laden explanations of the parameter (rich-agreement licensing, the EPP, topic drop) belong in Syntax/<framework>/; theory-laden bridges (e.g. deriving hasOvertPRO from a Minimalist minimal-pronoun inventory) live with the theory they presuppose (Syntax/Minimalist/MinimalPronoun.lean).

Main declarations

• SubjectContext — a cell of the person × finiteness × clause-role × Ā-status cross-classification.
• ProDropProfile — the coarse two-Boolean typological observable; ProDropProfile.Satisfies is [Ost26]'s universal (overt PRO → no pro-drop).
• Typology — the four cells; overtPROProDrop is predicted absent.
• SubjectAssignment — the fine interface (SubjectContext → Exponent) a syntactic theory must provide; its Satisfies is defined via the projection toProDropProfile, so the universal is singly authored.

Per-person predicates (allowsProDropAt, hasOvertPROAt, licensesAntiAgreementAt) expose the grain that partial-pro-drop (Hebrew, Brazilian Portuguese, Finnish) and anti-agreement languages require.

Subject-context vocabulary

@[reducible, inline]

abbrev NullSubject.Person : Type

Grammatical person. Aliased to UD.Person for cross-linguistic compatibility with the rest of linglib's morphological feature system; constructors are .first, .second, .third, .zero.

Equations

• NullSubject.Person = UD.Person

def NullSubject.thematicPersons : List Person

The thematic persons (1st, 2nd, 3rd). .zero (impersonal) is excluded because the typological universals here are about thematic-subject realization; impersonal subjects are governed by a separate parameter (cf. expletive vs null-expletive).

Equations

• NullSubject.thematicPersons = [UD.Person.first, UD.Person.second, UD.Person.third]

inductive NullSubject.Finiteness : Type

Finiteness of the clause hosting the subject locus. Coarser than [Lan04a]'s scale — that finer-grained version belongs in a syntactic theory file, not here.

• finite : Finiteness

  Finite clause (independent T, agreement morphology).

• nonfinite : Finiteness

  Non-finite clause (control, raising, ECM, gerundive, ...).

@[implicit_reducible]

instance NullSubject.instDecidableEqFiniteness : DecidableEq Finiteness

Equations

• NullSubject.instDecidableEqFiniteness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NullSubject.instReprFiniteness.repr : Finiteness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance NullSubject.instReprFiniteness : Repr Finiteness

Equations

• NullSubject.instReprFiniteness = { reprPrec := NullSubject.instReprFiniteness.repr }

@[implicit_reducible]

instance NullSubject.instInhabitedFiniteness : Inhabited Finiteness

Equations

• NullSubject.instInhabitedFiniteness = { default := NullSubject.instInhabitedFiniteness.default }

inductive NullSubject.ClauseRole : Type

The structural role of the clause hosting the subject locus. The three values exhaust the loci where the pro-drop / overt-PRO typology actually distinguishes languages.

• matrix : ClauseRole

  Matrix clause subject.

• embeddedFinite : ClauseRole

  Subject of a finite embedded clause (relevant for embedded-pro-drop diagnostics).

• controlSubject : ClauseRole

  Subject of an obligatory-control clause (PRO position).

@[implicit_reducible]

instance NullSubject.instDecidableEqClauseRole : DecidableEq ClauseRole

Equations

• NullSubject.instDecidableEqClauseRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NullSubject.instReprClauseRole : Repr ClauseRole

Equations

• NullSubject.instReprClauseRole = { reprPrec := NullSubject.instReprClauseRole.repr }

def NullSubject.instReprClauseRole.repr : ClauseRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance NullSubject.instInhabitedClauseRole : Inhabited ClauseRole

Equations

• NullSubject.instInhabitedClauseRole = { default := NullSubject.instInhabitedClauseRole.default }

inductive NullSubject.ABarStatus : Type

Whether the subject is in situ or has undergone Ā-extraction. Distinguished here because anti-agreement effects (Tarifit, Fiorentino, Wolof; [Bai18]) license null subjects only under Ā-extraction.

• insitu : ABarStatus

  Subject in situ (no Ā-extraction).

• aBarExtracted : ABarStatus

  Subject has undergone Ā-extraction (relativized, wh-fronted, focus-fronted, topicalized).

@[implicit_reducible]

instance NullSubject.instDecidableEqABarStatus : DecidableEq ABarStatus

Equations

• NullSubject.instDecidableEqABarStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NullSubject.instReprABarStatus : Repr ABarStatus

Equations

• NullSubject.instReprABarStatus = { reprPrec := NullSubject.instReprABarStatus.repr }

def NullSubject.instReprABarStatus.repr : ABarStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance NullSubject.instInhabitedABarStatus : Inhabited ABarStatus

Equations

• NullSubject.instInhabitedABarStatus = { default := NullSubject.instInhabitedABarStatus.default }

structure NullSubject.SubjectContext : Type

A cell of the four-way cross-classification: a single locus at which a language must decide between a null and an overt subject exponent.

• person : Person
• finiteness : Finiteness
• clauseRole : ClauseRole
• aBarStatus : ABarStatus

@[implicit_reducible]

instance NullSubject.instDecidableEqSubjectContext : DecidableEq SubjectContext

Equations

• NullSubject.instDecidableEqSubjectContext = NullSubject.instDecidableEqSubjectContext.decEq

def NullSubject.instDecidableEqSubjectContext.decEq (x✝ x✝¹ : SubjectContext) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance NullSubject.instReprSubjectContext : Repr SubjectContext

Equations

• NullSubject.instReprSubjectContext = { reprPrec := NullSubject.instReprSubjectContext.repr }

def NullSubject.instReprSubjectContext.repr : SubjectContext → ℕ → Std.Format

Equations

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

inductive NullSubject.Exponent : Type

The exponent decision at a SubjectContext: null vs overt. The typology this file tracks reduces to a function SubjectContext → Exponent.

• null : Exponent

  Silent subject (pro / null PRO / dropped subject).

• overt : Exponent

  Overt subject (full pronoun, clitic, agreement-doubled pronoun, overt PRO).

@[implicit_reducible]

instance NullSubject.instDecidableEqExponent : DecidableEq Exponent

Equations

• NullSubject.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NullSubject.instReprExponent : Repr Exponent

Equations

• NullSubject.instReprExponent = { reprPrec := NullSubject.instReprExponent.repr }

def NullSubject.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• NullSubject.instReprExponent.repr NullSubject.Exponent.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NullSubject.Exponent.null")).group prec✝

@[implicit_reducible]

instance NullSubject.instInhabitedExponent : Inhabited Exponent

Equations

• NullSubject.instInhabitedExponent = { default := NullSubject.instInhabitedExponent.default }

def NullSubject.SubjectContext.matrixFinite (p : Person) : SubjectContext

Matrix finite subject of person p (in situ). The canonical locus for "is this language pro-drop?".

Equations

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

def NullSubject.SubjectContext.embeddedFinite (p : Person) : SubjectContext

Embedded finite subject of person p (in situ). Distinguished from matrixFinite so that embedded-pro-drop asymmetries (some languages drop only embedded subjects) can be stated.

Equations

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

def NullSubject.SubjectContext.controlled (p : Person) : SubjectContext

Subject of an obligatory-control clause (PRO position) of person p. The canonical locus for "does this language have overt PRO?".

Equations

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

def NullSubject.SubjectContext.matrixExtracted (p : Person) : SubjectContext

Ā-extracted matrix finite subject of person p. The canonical locus for the anti-agreement effect ([Bai18]).

Equations

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

The coarse profile and the implicational universal

structure NullSubject.ProDropProfile : Type

A language's pro-drop / overt-PRO profile. The two Booleans are the typological observables; [Ost26]'s implicational universal is a constraint on which combinations are predicted to occur.

• allowsProDrop : Bool

  Whether the language permits null thematic subjects in finite clauses (pro-drop).

• hasOvertPRO : Bool

  Whether the subject of an obligatory-control clause must be realized overtly (overt PRO).

@[implicit_reducible]

instance NullSubject.instDecidableEqProDropProfile : DecidableEq ProDropProfile

Equations

• NullSubject.instDecidableEqProDropProfile = NullSubject.instDecidableEqProDropProfile.decEq

def NullSubject.instDecidableEqProDropProfile.decEq (x✝ x✝¹ : ProDropProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance NullSubject.instReprProDropProfile : Repr ProDropProfile

Equations

• NullSubject.instReprProDropProfile = { reprPrec := NullSubject.instReprProDropProfile.repr }

def NullSubject.instReprProDropProfile.repr : ProDropProfile → ℕ → Std.Format

Equations

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

def NullSubject.ProDropProfile.Satisfies (p : ProDropProfile) : Prop

[Ost26]'s implicational universal as a Prop: overt PRO entails non-pro-drop. Stated as a Prop so it composes with other logical predicates; Decidable instance below makes it evaluable by decide.

Equations

• p.Satisfies = (p.hasOvertPRO = true → p.allowsProDrop = false)

@[implicit_reducible]

instance NullSubject.ProDropProfile.instDecidableSatisfies (p : ProDropProfile) : Decidable p.Satisfies

Equations

• p.instDecidableSatisfies = id inferInstance

theorem NullSubject.ProDropProfile.satisfies_of_not_overt_pro (p : ProDropProfile) (h : p.hasOvertPRO = false) : p.Satisfies

If PRO is null, the universal is satisfied vacuously (its antecedent is false).

theorem NullSubject.ProDropProfile.satisfies_of_overt_pro_no_prodrop (p : ProDropProfile) (hD : p.allowsProDrop = false) : p.Satisfies

If PRO is overt and the language is non-pro-drop, the universal's consequent already holds, so the implication does too.

theorem NullSubject.ProDropProfile.prodrop_excludes_overt_pro (p : ProDropProfile) (h : p.Satisfies) (hD : p.allowsProDrop = true) : p.hasOvertPRO = false

Contrapositive: a pro-drop language cannot have overt PRO. This is the practically useful direction of the universal — given that a language is pro-drop, it predicts the absence of overt PRO.

inductive NullSubject.Typology : Type

The four cells of the typology. The fourth (overt PRO + pro-drop) is predicted absent by [Ost26]'s universal. Names use mathlib-style camelCase.

• nullPRONoProDrop : Typology

  Null PRO + non-pro-drop (e.g., English).

• nullPROProDrop : Typology

  Null PRO + pro-drop (e.g., Italian).

• overtPRONoProDrop : Typology

  Overt PRO + non-pro-drop (e.g., SMPM, Gã, Büli).

• overtPROProDrop : Typology

  Overt PRO + pro-drop — predicted absent.

@[implicit_reducible]

instance NullSubject.instDecidableEqTypology : DecidableEq Typology

Equations

• NullSubject.instDecidableEqTypology x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NullSubject.instReprTypology : Repr Typology

Equations

• NullSubject.instReprTypology = { reprPrec := NullSubject.instReprTypology.repr }

def NullSubject.instReprTypology.repr : Typology → ℕ → Std.Format

Equations

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

def NullSubject.Typology.isAttested : Typology → Prop

Whether a typological cell is attested under the universal. The only forbidden cell is overtPROProDrop.

Equations

• NullSubject.Typology.overtPROProDrop.isAttested = False
• x✝.isAttested = True

@[implicit_reducible]

instance NullSubject.instDecidableIsAttested (t : Typology) : Decidable t.isAttested

Equations

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

def NullSubject.ProDropProfile.classify (p : ProDropProfile) : Typology

Classify a profile into one of the four typological cells.

Equations

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

theorem NullSubject.ProDropProfile.satisfies_iff_attested (p : ProDropProfile) : p.Satisfies ↔ p.classify.isAttested

A profile satisfies the universal iff its typological cell is attested. This is the typology-as-finite-enumeration restatement of Satisfies.

Universals over subject assignments

@[reducible, inline]

abbrev NullSubject.SubjectAssignment : Type

A language's null-vs-overt decision at every cell of the cross-classification. The abstract interface against which pro-drop / overt-PRO universals are stated: each framework provides its own projection from its inventory type to a SubjectAssignment, and the universals apply to all of them uniformly.

Equations

• NullSubject.SubjectAssignment = (NullSubject.SubjectContext → NullSubject.Exponent)

def NullSubject.SubjectAssignment.hasOvertPROAt (a : SubjectAssignment) (p : Person) : Prop

Per-person controlled-subject (PRO) overtness.

Equations

• a.hasOvertPROAt p = (a (NullSubject.SubjectContext.controlled p) = NullSubject.Exponent.overt)

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableHasOvertPROAt (a : SubjectAssignment) (p : Person) : Decidable (a.hasOvertPROAt p)

Equations

• a.instDecidableHasOvertPROAt p = NullSubject.SubjectAssignment.instDecidableHasOvertPROAt._aux_1 a p

def NullSubject.SubjectAssignment.allowsProDropAt (a : SubjectAssignment) (p : Person) : Prop

Per-person pro-drop: the language drops a matrix finite subject of person p.

Equations

• a.allowsProDropAt p = (a (NullSubject.SubjectContext.matrixFinite p) = NullSubject.Exponent.null)

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableAllowsProDropAt (a : SubjectAssignment) (p : Person) : Decidable (a.allowsProDropAt p)

Equations

• a.instDecidableAllowsProDropAt p = NullSubject.SubjectAssignment.instDecidableAllowsProDropAt._aux_1 a p

def NullSubject.SubjectAssignment.licensesAntiAgreementAt (a : SubjectAssignment) (p : Person) : Prop

Per-person anti-agreement licensing: the language drops a matrix finite subject of person p under Ā-extraction even when it cannot drop the same subject in situ ([Bai18]).

Equations

• a.licensesAntiAgreementAt p = (a (NullSubject.SubjectContext.matrixExtracted p) = NullSubject.Exponent.null ∧ a (NullSubject.SubjectContext.matrixFinite p) = NullSubject.Exponent.overt)

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableLicensesAntiAgreementAt (a : SubjectAssignment) (p : Person) : Decidable (a.licensesAntiAgreementAt p)

Equations

• a.instDecidableLicensesAntiAgreementAt p = NullSubject.SubjectAssignment.instDecidableLicensesAntiAgreementAt._aux_1 a p

def NullSubject.SubjectAssignment.hasOvertPRO (a : SubjectAssignment) : Prop

The language has overt PRO iff EVERY thematic person realizes controlled-subject position overtly. The honest quantified version of [Ost26]'s "overt PRO" parameter.

Equations

• a.hasOvertPRO = ∀ p ∈ NullSubject.thematicPersons, a.hasOvertPROAt p

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableHasOvertPRO (a : SubjectAssignment) : Decidable a.hasOvertPRO

Equations

• a.instDecidableHasOvertPRO = NullSubject.SubjectAssignment.instDecidableHasOvertPRO._aux_1 a

def NullSubject.SubjectAssignment.allowsProDrop (a : SubjectAssignment) : Prop

The language allows pro-drop iff SOME thematic person can be dropped in matrix finite position.

Equations

• a.allowsProDrop = ∃ p ∈ NullSubject.thematicPersons, a.allowsProDropAt p

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableAllowsProDrop (a : SubjectAssignment) : Decidable a.allowsProDrop

Equations

• a.instDecidableAllowsProDrop = NullSubject.SubjectAssignment.instDecidableAllowsProDrop._aux_1 a

def NullSubject.SubjectAssignment.isPartialProDrop (a : SubjectAssignment) : Prop

The language is partially pro-drop: it drops some thematic persons but not all. Hebrew (1/2 only), Brazilian Portuguese (3rd-person dependent), Finnish (1/2 only).

Equations

• a.isPartialProDrop = (a.allowsProDrop ∧ ¬∀ p ∈ NullSubject.thematicPersons, a.allowsProDropAt p)

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableIsPartialProDrop (a : SubjectAssignment) : Decidable a.isPartialProDrop

Equations

• a.instDecidableIsPartialProDrop = NullSubject.SubjectAssignment.instDecidableIsPartialProDrop._aux_1 a

def NullSubject.SubjectAssignment.licensesAntiAgreement (a : SubjectAssignment) : Prop

The language exhibits the anti-agreement effect: SOME thematic person triggers null subjects only under Ā-extraction.

Equations

• a.licensesAntiAgreement = ∃ p ∈ NullSubject.thematicPersons, a.licensesAntiAgreementAt p

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableLicensesAntiAgreement (a : SubjectAssignment) : Decidable a.licensesAntiAgreement

Equations

• a.instDecidableLicensesAntiAgreement = NullSubject.SubjectAssignment.instDecidableLicensesAntiAgreement._aux_1 a

def NullSubject.SubjectAssignment.toProDropProfile (a : SubjectAssignment) : ProDropProfile

Project the fine assignment down to the coarse two-Boolean profile. The Bool fields of ProDropProfile are typological observables (the data); the abstract SubjectAssignment predicates are Prop, so we project via decide.

Equations

• a.toProDropProfile = { allowsProDrop := decide a.allowsProDrop, hasOvertPRO := decide a.hasOvertPRO }

@[reducible, inline]

abbrev NullSubject.SubjectAssignment.Satisfies (a : SubjectAssignment) : Prop

[Ost26]'s implicational universal applied to the abstract assignment. Defined via the projection so there is one canonical Satisfies definition (ProDropProfile.Satisfies) and the assignment-level form is its lift.

Equations

• a.Satisfies = a.toProDropProfile.Satisfies

@[implicit_reducible]

instance NullSubject.SubjectAssignment.instDecidableSatisfies (a : SubjectAssignment) : Decidable a.Satisfies

Equations

• a.instDecidableSatisfies = a.toProDropProfile.instDecidableSatisfies