Universals over Subject Assignments

A SubjectAssignment is the abstract interface a syntactic theory must provide to be evaluated against pro-drop / overt-PRO universals: a function from a SubjectContext (locus of decision) to an Exponent (null vs overt).

Stating the universals over this abstract function type — rather than over a particular framework's inventory structure (DM vocabulary items, HPSG pro-form lexical entries, LFG f-structure features) — keeps the typological claims framework-neutral. Each framework provides its own projection from its inventory type to a SubjectAssignment; the universals here apply to all of them uniformly.

Honest quantification

hasOvertPRO is ∀ p ∈ thematicPersons, a (.controlled p) = .overt (decidable by decide). allowsProDrop is ∃ p ∈ thematicPersons, a (.matrixFinite p) = .null. The Ostrove universal then has its strongest content: if EVERY thematic person is overt in PRO position, NO thematic person can be dropped in matrix position.

Per-person predicates allowsProDropAt/hasOvertPROAt expose the finer grain that partial-pro-drop languages (Hebrew: 1/2 only; Brazilian Portuguese: 3rd-person dependent; Finnish: 1/2 only) and anti-agreement languages (overt only when in situ) require.

The Satisfies predicate is defined exactly once

The two-Boolean ProDropProfile (in Basic.lean) is the projected view; SubjectAssignment.Satisfies is defined as (toProDropProfile a).Satisfies rather than re-stipulated. The bridge is then a real reduction (loss of per-person information), not the identity.

@[reducible, inline]

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

Equations

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

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

Per-person controlled-subject (PRO) overtness.

Equations

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

@[implicit_reducible]

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

Equations

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

def Phenomena.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 (Phenomena.NullSubject.SubjectContext.matrixFinite p) = Phenomena.NullSubject.Exponent.null)

@[implicit_reducible]

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

Equations

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

def Phenomena.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 (@cite{baier-2018}).

Equations

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

@[implicit_reducible]

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

Equations

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

def Phenomena.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 @cite{ostrove-2026}'s "overt PRO" parameter.

Equations

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

@[implicit_reducible]

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

Equations

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

def Phenomena.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 ∈ Phenomena.NullSubject.thematicPersons, a.allowsProDropAt p

@[implicit_reducible]

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

Equations

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

def Phenomena.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 ∈ Phenomena.NullSubject.thematicPersons, a.allowsProDropAt p)

@[implicit_reducible]

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

Equations

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

def Phenomena.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 ∈ Phenomena.NullSubject.thematicPersons, a.licensesAntiAgreementAt p

@[implicit_reducible]

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

Equations

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

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

Bridge to the legacy two-Boolean profile in Basic.lean. 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 Phenomena.NullSubject.SubjectAssignment.Satisfies (a : SubjectAssignment) : Prop

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

Equations

• a.instDecidableSatisfies = a.toProDropProfile.instDecidableSatisfies