Chomsky (1981) — Binding Principles A/B/C @cite{chomsky-1981}

Lectures on Government and Binding. Foris.

The Government-and-Binding binding theory of @cite{chomsky-1981} 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 verifies the implementation in Theories/Syntax/Minimalism/Coreference.lean against the empirical minimal-pair data in Phenomena/Anaphora/Coreference.lean.

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).

def Chomsky1981.capturesCoreferenceData (phenom : Paradigms.AcceptabilityJudgment.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

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

@[implicit_reducible]

instance Chomsky1981.instDecidableCapturesCoreferenceData (phenom : Paradigms.AcceptabilityJudgment.PhenomenonData) : Decidable (capturesCoreferenceData phenom)

Equations

• Chomsky1981.instDecidableCapturesCoreferenceData phenom = id inferInstance

theorem Chomsky1981.captures_reflexive_coreference : capturesCoreferenceData Phenomena.Anaphora.Coreference.reflexiveCoreferenceData

Minimalism captures reflexiveCoreferenceData.

theorem Chomsky1981.captures_complementary_distribution : capturesCoreferenceData Phenomena.Anaphora.Coreference.complementaryDistributionData

Minimalism captures complementaryDistributionData.

theorem Chomsky1981.captures_pronominal_disjoint_reference : capturesCoreferenceData Phenomena.Anaphora.Coreference.pronominalDisjointReferenceData

Minimalism captures pronominalDisjointReferenceData.

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

Per-pair verification of reflexive binding judgments.

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

Reciprocal binding: plural antecedent required, singular blocked.