Chomsky (1981) — Binding Principles A/B/C [Cho81]

Lectures on Government and Binding. Foris.

The Government-and-Binding binding theory of [Cho81] classifies nominal expressions into three types and constrains their distribution by c-command + a local binding domain:

• Principle A: an anaphor must be bound (c-commanded by a coindexed antecedent) in its local domain
• Principle B: a pronoun must be free (not bound) in its local domain
• Principle C: an R-expression must be free everywhere

This file holds the textbook minimal-pair paradigm (reflexiveCoreferenceData, pronominalDisjointReferenceData, referentialExpressionFreedomData, complementaryDistributionData, reciprocalCoreferenceData) and the per-class binding requirements as data (CoreferencePattern), and verifies the Minimalist binding implementation (the relocated c-command CommandRelation instance below) against the pairs.

Companion to Reinhart1976.lean (which formalizes the c-command relation that Principles A/B/C presuppose) and to SagWasowBender2003.lean (the HPSG re-axiomatization that subsumes Principle C under Principle B); Hudson1990.lean (DG) and Cooper2023/Basic.lean (TTR) verify their analyses against the same tables.

Coreference / binding (relocated from Minimalist/Coreference.lean)

Binding via c-command and locality ([Cho81]). The binding principles themselves are not restated here: this section supplies Minimalism's command relation (c-command, read off the phrase-structure tree) as a Syntax.Binding.CommandRelation instance, and the framework-neutral engine (Syntax/Binding/Basic.lean) derives Principles A/B/C and the coreference predictions from it. The instance is language-neutral; the theorems below combine it with English's binding-class classifier.

C-command from tree geometry

def Chomsky1981.toSyntacticObject (clause : Binding.SimpleClause) : Minimalist.SyntacticObject

Build a phrase-structure tree from a clause: transitive {subj, {verb, obj}} (subject specifier, verb–object a head-complement pair), intransitive {subj, verb}. C-command follows from the geometry. Built planar-first so the containment / c-command decision procedures reduce.

Equations

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

def Chomsky1981.subjectCCommandsObject (clause : Binding.SimpleClause) : Prop

Subject c-commands object: in {subj, {verb, obj}}, the subject's sister {verb, obj} contains the object.

Equations

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

@[implicit_reducible]

instance Chomsky1981.instDecidableSubjectCCommandsObject (clause : Binding.SimpleClause) : Decidable (subjectCCommandsObject clause)

Equations

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

def Chomsky1981.objectCCommandsSubject (clause : Binding.SimpleClause) : Prop

Object does not c-command subject: in {subj, {verb, obj}}, the object's sister verb does not contain the subject.

Equations

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

@[implicit_reducible]

instance Chomsky1981.instDecidableObjectCCommandsSubject (clause : Binding.SimpleClause) : Decidable (objectCCommandsSubject clause)

Equations

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

def Chomsky1981.sameLocalDomain (clause : Binding.SimpleClause) : Prop

Both positions are in the local clause tree (the minimal domain).

Equations

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

@[implicit_reducible]

instance Chomsky1981.instDecidableSameLocalDomain (clause : Binding.SimpleClause) : Decidable (sameLocalDomain clause)

Equations

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

Minimalism as a command relation

def Chomsky1981.commands (c : Binding.SimpleClause) : Binding.Pos → Binding.Pos → Prop

The Minimalist command relation: c-command read off the tree.

Equations

• Chomsky1981.commands c Binding.Pos.subject Binding.Pos.object = Chomsky1981.subjectCCommandsObject c
• Chomsky1981.commands c Binding.Pos.object Binding.Pos.subject = Chomsky1981.objectCCommandsSubject c
• Chomsky1981.commands c x✝¹ x✝ = False

def Chomsky1981.sameDomain (c : Binding.SimpleClause) : Binding.Pos → Binding.Pos → Prop

Locality: in a simple clause all positions share the one binding domain.

Equations

• Chomsky1981.sameDomain c x✝¹ x✝ = Chomsky1981.sameLocalDomain c

@[implicit_reducible]

instance Chomsky1981.instDecidableSameDomain (c : Binding.SimpleClause) (i j : Binding.Pos) : Decidable (sameDomain c i j)

Equations

• Chomsky1981.instDecidableSameDomain c i j = Chomsky1981.instDecidableSameDomain._aux_1 c i j

@[implicit_reducible]

instance Chomsky1981.instCommandRelation : Binding.CommandRelation

Minimalism is an instance of the abstract command relation ([BP90]). The binding principles (Syntax.Binding.grammaticalForCoreference etc.) come from the engine; the theorems below apply them with this instance in scope and a language classifier.

Equations

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

def Chomsky1981.reflexiveCoreferenceData : Features.MinimalPairs.PhenomenonData

Reflexives require local c-commanding antecedent.

Equations

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

def Chomsky1981.pronominalDisjointReferenceData : Features.MinimalPairs.PhenomenonData

Pronouns cannot corefer with local c-commanding antecedent.

Equations

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

def Chomsky1981.referentialExpressionFreedomData : Features.MinimalPairs.PhenomenonData

Full nominals cannot corefer with c-commanding pronoun.

Equations

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

def Chomsky1981.complementaryDistributionData : Features.MinimalPairs.PhenomenonData

Reflexives and pronouns in complementary distribution.

Equations

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

def Chomsky1981.reciprocalCoreferenceData : Features.MinimalPairs.PhenomenonData

Reciprocals require a plural/coordinated antecedent and local binding.

Equations

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

inductive Chomsky1981.AnaphorType : Type

Types of anaphoric expressions.

• reflexive : AnaphorType
• reciprocal : AnaphorType
• pronoun : AnaphorType
• name : AnaphorType
• description : AnaphorType

def Chomsky1981.instReprAnaphorType.repr : AnaphorType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Chomsky1981.instReprAnaphorType : Repr AnaphorType

Equations

• Chomsky1981.instReprAnaphorType = { reprPrec := Chomsky1981.instReprAnaphorType.repr }

@[implicit_reducible]

instance Chomsky1981.instDecidableEqAnaphorType : DecidableEq AnaphorType

Equations

• Chomsky1981.instDecidableEqAnaphorType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Chomsky1981.Domain : Type

Domain types for coreference constraints.

• local_ : Domain
• nonlocal : Domain
• any : Domain

def Chomsky1981.instReprDomain.repr : Domain → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Chomsky1981.instReprDomain.repr Chomsky1981.Domain.local_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chomsky1981.Domain.local_")).group prec✝
• Chomsky1981.instReprDomain.repr Chomsky1981.Domain.any prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chomsky1981.Domain.any")).group prec✝

@[implicit_reducible]

instance Chomsky1981.instReprDomain : Repr Domain

Equations

• Chomsky1981.instReprDomain = { reprPrec := Chomsky1981.instReprDomain.repr }

@[implicit_reducible]

instance Chomsky1981.instDecidableEqDomain : DecidableEq Domain

Equations

• Chomsky1981.instDecidableEqDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Chomsky1981.CoreferencePattern : Type

Coreference requirements for an anaphor type.

• anaphorType : AnaphorType
• requiresAntecedent : Bool
• antecedentDomain : Option Domain

@[implicit_reducible]

instance Chomsky1981.instReprCoreferencePattern : Repr CoreferencePattern

Equations

• Chomsky1981.instReprCoreferencePattern = { reprPrec := Chomsky1981.instReprCoreferencePattern.repr }

def Chomsky1981.instReprCoreferencePattern.repr : CoreferencePattern → ℕ → Std.Format

Equations

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

def Chomsky1981.reflexivePattern : CoreferencePattern

Principle A as data: anaphors are bound in the local domain.

Equations

• Chomsky1981.reflexivePattern = { anaphorType := Chomsky1981.AnaphorType.reflexive, requiresAntecedent := true, antecedentDomain := some Chomsky1981.Domain.local_ }

def Chomsky1981.pronounPattern : CoreferencePattern

Principle B as data: pronouns are free in the local domain.

Equations

• Chomsky1981.pronounPattern = { anaphorType := Chomsky1981.AnaphorType.pronoun, requiresAntecedent := false, antecedentDomain := some Chomsky1981.Domain.nonlocal }

def Chomsky1981.namePattern : CoreferencePattern

Principle C as data: R-expressions are free everywhere.

Equations

• Chomsky1981.namePattern = { anaphorType := Chomsky1981.AnaphorType.name, requiresAntecedent := false, antecedentDomain := none }

def Chomsky1981.reciprocalPattern : CoreferencePattern

Reciprocal coreference pattern: requires a c-commanding antecedent that denotes a plurality. The antecedent can be syntactically singular in some languages (e.g., Hungarian null pronouns bound by a plural matrix subject; [Rak19], [DH24] §2). The domain is local for the pronoun antecedent, but the reciprocal's semantic contribution can scope wider (I-reading).

Equations

• Chomsky1981.reciprocalPattern = { anaphorType := Chomsky1981.AnaphorType.reciprocal, requiresAntecedent := true, antecedentDomain := some Chomsky1981.Domain.local_ }

def Chomsky1981.capturesCoreferenceData (phenom : Features.MinimalPairs.PhenomenonData) : Prop

Coverage of a PhenomenonData set under Minimalist binding theory.

Stated Prop-valued (with a Decidable instance) because the underlying grammaticalForCoreference predicate is Prop-valued.

Equations

• Chomsky1981.capturesCoreferenceData phenom = ∀ p ∈ phenom.pairs, Chomsky1981.grammaticalForCoreference✝ p.lhs ∧ ¬Chomsky1981.grammaticalForCoreference✝ p.rhs

@[implicit_reducible]

instance Chomsky1981.instDecidableCapturesCoreferenceData (phenom : Features.MinimalPairs.PhenomenonData) : Decidable (capturesCoreferenceData phenom)

Equations

• Chomsky1981.instDecidableCapturesCoreferenceData phenom = id inferInstance

theorem Chomsky1981.captures_reflexive_coreference : capturesCoreferenceData reflexiveCoreferenceData

Minimalism captures reflexiveCoreferenceData.

theorem Chomsky1981.captures_complementary_distribution : capturesCoreferenceData complementaryDistributionData

Minimalism captures complementaryDistributionData.

theorem Chomsky1981.captures_pronominal_disjoint_reference : capturesCoreferenceData pronominalDisjointReferenceData

Minimalism captures pronominalDisjointReferenceData.

theorem Chomsky1981.reflexive_pairs_captured : (Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.john✝, Chomsky1981.sees✝, Chomsky1981.himself✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.himself✝, Chomsky1981.sees✝, Chomsky1981.john✝]) ∧ (Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.mary✝, Chomsky1981.sees✝, Chomsky1981.herself✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.herself✝, Chomsky1981.sees✝, Chomsky1981.mary✝]) ∧ (Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.they✝, Chomsky1981.see✝, Chomsky1981.themselves✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.themselves✝, Chomsky1981.see✝, Chomsky1981.them✝]) ∧ (Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.john✝, Chomsky1981.sees✝, Chomsky1981.himself✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.john✝, Chomsky1981.sees✝, Chomsky1981.herself✝]) ∧ Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.they✝, Chomsky1981.see✝, Chomsky1981.themselves✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.they✝, Chomsky1981.see✝, Chomsky1981.himself✝]

Per-pair verification of reflexive binding judgments.

theorem Chomsky1981.reciprocal_plural_antecedent : Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.they✝, Chomsky1981.see✝, Chomsky1981.eachOther✝] ∧ ¬Chomsky1981.grammaticalForCoreference✝ [Chomsky1981.john✝, Chomsky1981.sees✝, Chomsky1981.eachOther✝]

Reciprocal binding: plural antecedent required, singular blocked.