Adger 2003: C-Selection and Subcategorization @cite{adger-2003}

Replicates Adger's c-selection account of subcategorization (Core Syntax ch. 3 §3.5–§3.6) on linglib's Minimalism substrate via the Derivation.WellFormed predicate from Theories/Syntax/Minimalism/Selection.lean.

Adger's apparatus (recap)

Each lexical head bears interpretable categorial features [F] (e.g. [V] for verbs) and uninterpretable c-selectional features [uG] (e.g. [uN] for transitive verbs). Adger's checking system:

• (104) Full Interpretation: structure at the semantic interface contains no uninterpretable features
• (105) Checking Requirement: uninterpretable [uF] must be checked, and once checked deletes
• (106) Checking under Sisterhood: [uF] on Y is checked when Y is sister to Z bearing matching [F]
• (110) kiss [V, uN]: V interpretable, uN uninterpretable
• (114) *Anson demonized is bad because demonize's [uN] is unchecked

Substrate mapping

Adger	linglib
interpretable [F]	SimpleLI.cat : Cat
uninterpretable [uG]	SimpleLI.sel : SelStack (a List Cat)
Full Interpretation	Derivation.WellFormed (Selection.lean)
first Merge / complement	Step.emR (consumes one pending feature)
second Merge / specifier	Step.emL (no consumption)

verbToSelStack (in Theories/Syntax/Minimalism/Derivations.lean) derives the SelStack from VerbEntry.complementType:

complementType	SelStack	English class
.none	[]	intransitive
.np	[.D]	transitive
.np_np	[.D, .D]	ditransitive

Sections

• §1 grammatical proper-noun derivations are well-formed
• §2 ungrammatical c-selection violations fail well-formedness
• §3 subcategorization_data_match agrees with Phenomena.ArgumentStructure.Subcategorization.data
• §4 substrate finding: bare common nouns expose a known limitation in the canonical Derivations.lean derivations
• §5 resolution: Adger ch. 7's null-D wrapper (nullDWrap in Selection.lean) projects bare common nouns as DPs that satisfy verbs' [uD] c-selection

§0: Lexicon — Fragment-grounded SO building blocks

Migrated from the deleted Theories/Syntax/Minimalism/Derivations.lean; instances belong in Phenomena per the architecture audit. Each SO is a leaf with Cat and SelStack derived from its Fragment lexical entry.

LIToken id allocation (one-derivation scope)

Every leaf carries a Nat id used by Step.im/movement to identify chains. The scheme below partitions ids into ranges so that ids are distinct across SOs that may co-occur in a derivation:

Range	Use
1–9	Pronouns
10–19	Proper-noun DPs
20–29	Common-noun bare Ns
30–39	Verb leaves
40–49	Determiners
100–199	§2 ungrammatical-derivation seeds
200–299	§5 null-D-wrapped derivation seeds
9000+	Silent / null-D heads (nullDWrap)

def Adger2003.heSO : Minimalist.SyntacticObject

Equations

• Adger2003.heSO = Minimalist.FromFragments.pronounToSO Fragments.English.Pronouns.he 1

def Adger2003.herSO : Minimalist.SyntacticObject

Equations

• Adger2003.herSO = Minimalist.FromFragments.pronounToSO Fragments.English.Pronouns.her 2

def Adger2003.theySO : Minimalist.SyntacticObject

Equations

• Adger2003.theySO = Minimalist.FromFragments.pronounToSO Fragments.English.Pronouns.they 3

def Adger2003.johnSO : Minimalist.SyntacticObject

Equations

• Adger2003.johnSO = Minimalist.FromFragments.nounToSO Fragments.English.Nouns.john 10

def Adger2003.marySO : Minimalist.SyntacticObject

Equations

• Adger2003.marySO = Minimalist.FromFragments.nounToSO Fragments.English.Nouns.mary 11

def Adger2003.catSO : Minimalist.SyntacticObject

Equations

• Adger2003.catSO = Minimalist.FromFragments.nounToSO Fragments.English.Nouns.cat 20

def Adger2003.pizzaSO : Minimalist.SyntacticObject

Equations

• Adger2003.pizzaSO = Minimalist.FromFragments.nounToSO Fragments.English.Nouns.pizza 21

def Adger2003.bookSO : Minimalist.SyntacticObject

Equations

• Adger2003.bookSO = Minimalist.FromFragments.nounToSO Fragments.English.Nouns.book 22

def Adger2003.sleepsSO : Minimalist.SyntacticObject

Equations

• Adger2003.sleepsSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.sleep 30

def Adger2003.seesSO : Minimalist.SyntacticObject

Equations

• Adger2003.seesSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.see 31

def Adger2003.eatsSO : Minimalist.SyntacticObject

Equations

• Adger2003.eatsSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.eat 32

def Adger2003.arrivesSO : Minimalist.SyntacticObject

Equations

• Adger2003.arrivesSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.arrive 33

def Adger2003.devoursSO : Minimalist.SyntacticObject

Equations

• Adger2003.devoursSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.devour 34

def Adger2003.givesSO : Minimalist.SyntacticObject

Equations

• Adger2003.givesSO = Minimalist.FromFragments.verbToSO Fragments.English.Predicates.Verbal.give 35

def Adger2003.theSO : Minimalist.SyntacticObject

Equations

• Adger2003.theSO = Minimalist.mkLeafPhon Minimalist.Cat.D [Minimalist.Cat.N] "the" 40

def Adger2003.john_sleeps : Minimalist.Derivation

"John sleeps": [S John sleeps] — intransitive.

Equations

• Adger2003.john_sleeps = { initial := Adger2003.sleepsSO, steps := [Minimalist.Step.emL Adger2003.johnSO] }

def Adger2003.mary_arrives : Minimalist.Derivation

"Mary arrives": [S Mary arrives] — intransitive.

Equations

• Adger2003.mary_arrives = { initial := Adger2003.arrivesSO, steps := [Minimalist.Step.emL Adger2003.marySO] }

def Adger2003.john_sees_mary : Minimalist.Derivation

"John sees Mary": [S John [VP sees Mary]] — transitive.

Equations

• Adger2003.john_sees_mary = { initial := Adger2003.seesSO, steps := [Minimalist.Step.emR Adger2003.marySO, Minimalist.Step.emL Adger2003.johnSO] }

def Adger2003.mary_sees_john : Minimalist.Derivation

"Mary sees John" — transitive variant.

Equations

• Adger2003.mary_sees_john = { initial := Adger2003.seesSO, steps := [Minimalist.Step.emR Adger2003.johnSO, Minimalist.Step.emL Adger2003.marySO] }

def Adger2003.he_sees_her : Minimalist.Derivation

"He sees her": pronouns project D directly.

Equations

• Adger2003.he_sees_her = { initial := Adger2003.seesSO, steps := [Minimalist.Step.emR Adger2003.herSO, Minimalist.Step.emL Adger2003.heSO] }

def Adger2003.mary_eats_pizza : Minimalist.Derivation

"Mary eats pizza": transitive with bare common-noun complement.

Equations

• Adger2003.mary_eats_pizza = { initial := Adger2003.eatsSO, steps := [Minimalist.Step.emR Adger2003.pizzaSO, Minimalist.Step.emL Adger2003.marySO] }

def Adger2003.the_cat_eats_pizza : Minimalist.Derivation

"The cat eats pizza": determiner+N subject, bare common-noun object.

Equations

• Adger2003.the_cat_eats_pizza = { initial := Adger2003.eatsSO, steps := [Minimalist.Step.emR Adger2003.pizzaSO, Minimalist.Step.emL (Minimalist.merge Adger2003.theSO Adger2003.catSO)] }

def Adger2003.john_devours_pizza : Minimalist.Derivation

"John devours pizza": transitive with bare common-noun complement.

Equations

• Adger2003.john_devours_pizza = { initial := Adger2003.devoursSO, steps := [Minimalist.Step.emR Adger2003.pizzaSO, Minimalist.Step.emL Adger2003.johnSO] }

def Adger2003.john_gives_mary_book : Minimalist.Derivation

"John gives Mary book": ditransitive. (Word order is gives book Mary in linearization — see substantive note in the audit; the Larson 1988 shell would put goal Mary as inner complement and theme the book as outer.)

Equations

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

Phase 1.0 substrate caveat: Derivation.WellFormed is Decidable only via a noncomputable instance ... classical infer_instance because WellFormed routes through checkedFinal? (Selection.lean:178), which is noncomputable via three Phase 1.0 placeholders: SyntacticObject.checkedSel?, leftmostLeaf, and Step.applyChecked (each lifting through Quot.out). Concrete-instance decide checks fail at kernel reduction. TODO Phase 2: once LCA-based head/leftmostLeaf/checkedSel land, restore by decide.

theorem Adger2003.john_sleeps_wellFormed : john_sleeps.WellFormed

"John sleeps" — intransitive: empty pending stack consumed trivially.

theorem Adger2003.mary_arrives_wellFormed : mary_arrives.WellFormed

"Mary arrives" — intransitive variant.

theorem Adger2003.john_sees_mary_wellFormed : john_sees_mary.WellFormed

"John sees Mary" — transitive: see's [.D] is checked by Mary's D.

theorem Adger2003.mary_sees_john_wellFormed : mary_sees_john.WellFormed

"Mary sees John" — symmetric variant.

theorem Adger2003.he_sees_her_wellFormed : he_sees_her.WellFormed

"He sees her" — pronouns also project D, so this checks too.

def Adger2003.mary_arrives_john_bad : Minimalist.Derivation

"*Mary arrives John" — intransitive with spurious complement. arrive's pending = [] so the emR john step has nothing to check against and applyChecked returns none.

Equations

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

def Adger2003.john_sees_bad : Minimalist.Derivation

"*John sees" — transitive missing required complement. see's [.D] is never checked, so the final pending = [.D] ≠ [].

Equations

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

theorem Adger2003.mary_arrives_john_not_wellFormed : ¬mary_arrives_john_bad.WellFormed

theorem Adger2003.john_sees_not_wellFormed : ¬john_sees_bad.WellFormed

theorem Adger2003.subcategorization_data_match : john_sleeps.WellFormed ∧ ¬mary_arrives_john_bad.WellFormed ∧ john_sees_mary.WellFormed ∧ ¬john_sees_bad.WellFormed

Adger's c-selection predictions agree with Phenomena.ArgumentStructure.Subcategorization.data on the proper-noun fragment of the contrast set:

Frame	Grammatical	Ungrammatical
intransitive	"John sleeps"	"*Mary arrives John"
transitive	"John sees Mary"	"*John sees"

The full data file's bare-common-noun examples are addressed in §4.

Bare common nouns under strict c-selection

The existing *_pizza / *_book derivations in Theories/Syntax/Minimalism/Derivations.lean use bare common nouns (cat = .N per nounToSO for non-proper entries) as direct objects of verbs that c-select [.D]. Per Adger ch. 7 Functional Categories II — the DP, bare common nouns require null-D wrapping to project as DPs and check verbs' [uD]. linglib's substrate currently encodes common nouns as N without this wrapping, so strict c-selection flags these derivations as ill-formed even though their intended English glosses are grammatical.

This is a substrate-encoding artifact, not a pedagogical ill-formedness. Resolving it requires one of: (a) introducing a null-D wrapper for bare common nouns (Adger ch. 7); (b) allowing verbs to alternately c-select N (counter to standard Minimalism); (c) treating bare common nouns as having an implicit kind-denoting D feature.

Out of scope for this study; the well-formedness predicate's strictness makes the gap visible (rather than silently passing), which is what linglib aims for. The three examples below pin the current behaviour.

theorem Adger2003.john_devours_pizza_not_wellFormed_bare : ¬john_devours_pizza.WellFormed

"John devours pizza" with bare pizza (.N) fails devour's [uD].

theorem Adger2003.mary_eats_pizza_not_wellFormed_bare : ¬mary_eats_pizza.WellFormed

"Mary eats pizza" — same pattern with eat.

theorem Adger2003.john_gives_mary_book_not_wellFormed_bare : ¬john_gives_mary_book.WellFormed

"John gives Mary book" — book (.N) is the inner complement and fails give's first [uD].

Null-D-wrapped DPs are well-formed

@cite{adger-2003} ch. 7 (Functional Categories II — the DP) treats bare common nouns as DPs headed by a phonologically silent D. Selection.lean provides nullDWrap : SyntacticObject → Nat → SyntacticObject, which constructs (∅ᴅ, n): the silent D's [uN] feature is checked internally against the noun's .N, yielding a saturated DP with outerCat = .D and checkedSel = some [].

The parallel *_DP derivations below mirror the canonical sentences from Derivations.lean but route the common-noun complement through nullDWrap, producing well-formed structures. The phonYield is unchanged because nullD has an empty phonForm.

def Adger2003.pizzaDP : Minimalist.SyntacticObject

Bare pizza (cat = .N) wrapped under null D, projecting a saturated DP.

Equations

• Adger2003.pizzaDP = Minimalist.nullDWrap (Minimalist.FromFragments.nounToSO Fragments.English.Nouns.pizza 200) 9200

def Adger2003.bookDP : Minimalist.SyntacticObject

Bare book under null D.

Equations

• Adger2003.bookDP = Minimalist.nullDWrap (Minimalist.FromFragments.nounToSO Fragments.English.Nouns.book 201) 9201

def Adger2003.john_devours_pizza_DP : Minimalist.Derivation

"John devours pizza" with null-D-wrapped DP complement. devour's [uD] is checked by the wrapped DP's outer .D.

Equations

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

def Adger2003.mary_eats_pizza_DP : Minimalist.Derivation

"Mary eats pizza" — same pattern with eat.

Equations

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

def Adger2003.john_gives_mary_book_DP : Minimalist.Derivation

"John gives Mary book": ditransitive with book as inner complement (direct object) wrapped under null D, Mary as proper-noun outer complement (indirect object). Both [uD] features on give are checked.

Equations

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

theorem Adger2003.john_devours_pizza_DP_wellFormed : john_devours_pizza_DP.WellFormed

theorem Adger2003.mary_eats_pizza_DP_wellFormed : mary_eats_pizza_DP.WellFormed

theorem Adger2003.john_gives_mary_book_DP_wellFormed : john_gives_mary_book_DP.WellFormed

Surface form

By construction, nullD's phonForm is empty, so the null-D-wrapped derivations linearize to the same surface strings as the canonical bare- noun derivations — only the internal structure differs. PhonYield equality theorems analogous to Derivations.lean's *_phon are deferred: the foldl-over-steps + nested phonYield append exceeds decide's reduction budget and is not closeable by rfl, and the existing Derivations.lean precedent (native_decide) is non-mathlib-compatible per CLAUDE.md. A structured proof via explicit unfolding lemmas is the right next step but out of scope here.

theorem Adger2003.nullD_resolves_substrate_finding : ¬john_devours_pizza.WellFormed ∧ john_devours_pizza_DP.WellFormed ∧ ¬mary_eats_pizza.WellFormed ∧ mary_eats_pizza_DP.WellFormed ∧ ¬john_gives_mary_book.WellFormed ∧ john_gives_mary_book_DP.WellFormed

Combined: the §4 ill-formed bare-noun derivations and the §5 null-D-wrapped DP derivations form a minimal pair that operationalises Adger ch. 7's claim that argumental nominals are DPs.