Null Subjects: Pro-Drop and Overt PRO @cite{ostrove-2026}

Framework-agnostic typological parameter: whether a language permits null thematic subjects (pro-drop) and whether the subject of an obligatory-control clause must be overt.

This file is in Core/ because the parameter is theory-neutral — any syntactic framework (Minimalism, HPSG, LFG, Construction Grammar) must engage with it. Theory-laden explanations of the parameter (rich-agreement licensing, the EPP, topic drop, etc.) belong in Theories/Syntax/<framework>/. Theory-laden bridges — e.g. a function that derives hasOvertPRO from a Minimalist minimal-pronoun inventory — likewise live with the theory they presuppose (Theories/Syntax/Minimalism/MinimalPronoun.lean).

The implicational universal

If a language requires the subject of obligatory control clauses (i.e., PRO) to be overt, then that language will not allow pro-drop. (@cite{ostrove-2026})

This is a one-way implication: non-pro-drop does not entail overt PRO. English is non-pro-drop but has null PRO; Mixtec (SMPM) and Gã have overt PRO and are non-pro-drop; Italian has null PRO and is pro-drop. The fourth cell — overt PRO + pro-drop — is predicted absent.

Layering

This file holds the coarse two-Boolean view (ProDropProfile). The fine per-person/per-context view (SubjectAssignment) lives in Universals.lean, which projects down to ProDropProfile and reuses the Satisfies definition here. Defining the universal once at the coarse layer and lifting it to the fine layer keeps the typological content singly authored.

structure Phenomena.NullSubject.ProDropProfile : Type

A language's pro-drop / overt-PRO profile. The two Booleans are the typological observables; @cite{ostrove-2026}'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).

def Phenomena.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 Phenomena.NullSubject.instDecidableEqProDropProfile : DecidableEq ProDropProfile

Equations

• Phenomena.NullSubject.instDecidableEqProDropProfile = Phenomena.NullSubject.instDecidableEqProDropProfile.decEq

@[implicit_reducible]

instance Phenomena.NullSubject.instReprProDropProfile : Repr ProDropProfile

Equations

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

def Phenomena.NullSubject.instReprProDropProfile.repr : ProDropProfile → Nat → Std.Format

Equations

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

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

@cite{ostrove-2026}'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 Phenomena.NullSubject.ProDropProfile.instDecidableSatisfies (p : ProDropProfile) : Decidable p.Satisfies

Equations

• p.instDecidableSatisfies = id inferInstance

theorem Phenomena.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 Phenomena.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 Phenomena.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 Phenomena.NullSubject.Typology : Type

The four cells of the typology. The fourth (overt PRO + pro-drop) is predicted absent by @cite{ostrove-2026}'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 Phenomena.NullSubject.instDecidableEqTypology : DecidableEq Typology

Equations

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

@[implicit_reducible]

instance Phenomena.NullSubject.instReprTypology : Repr Typology

Equations

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

def Phenomena.NullSubject.instReprTypology.repr : Typology → Nat → Std.Format

Equations

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

def Phenomena.NullSubject.Typology.isAttested : Typology → Prop

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Phenomena.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 Phenomena.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.