theorem Phenomena.Coordination.nonConstituentCoord_is_grammatical : CCG.john_likes_and_mary_hates_beans.cat = some CCG.S

theorem Phenomena.Coordination.standardCoord_is_grammatical : CCG.john_sleeps.cat = some CCG.S

def Phenomena.Coordination.john_sleeps_and_mary_sleeps : CCG.DerivStep

Equations

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

theorem Phenomena.Coordination.nonConstituentCoord_harder_than_standard : john_sleeps_and_mary_sleeps.opCount < CCG.john_likes_and_mary_hates_beans.opCount

theorem Phenomena.Coordination.standardCoord_harder_than_simple : CCG.john_sleeps.opCount < john_sleeps_and_mary_sleeps.opCount

theorem Phenomena.Coordination.ccg_derives_nonconstituent_coordination : johnLikesAndMaryHatesBeans.bothGrammatical = true ∧ CCG.john_likes_and_mary_hates_beans.cat = some CCG.S ∧ (CCG.john_likes_and_mary_hates_beans.interp CCG.toySemLexicon).isSome = true

LINKING THEOREM: CCG derives both sides of the semantic equivalence

The phenomena-level data (from Phenomena/Coordination/Data.lean): "John likes and Mary hates beans" ≡ "John likes beans and Mary hates beans"

CCG's prediction: both sentences derive and receive equivalent meanings.

This theorem proves CCG derives the non-constituent coordination sentence. (The full equivalence proof would require implementing the spelled-out derivation too.)

theorem Phenomena.Coordination.ccg_coordination_semantics_correct (e : Semantics.Montague.ToyEntity) : CCG.coordMeaningAt e = CCG.pointwiseConjAt e

THE SUBSTANTIVE SEMANTIC THEOREM

CCG derives the meaning of "John likes and Mary hates beans" as the conjunction of two predications:

⟦John likes and Mary hates beans⟧ = ⟦John likes⟧(beans) ∧ ⟦Mary hates⟧(beans)

This is non-trivial because it requires:

1. Type-raising John and Mary to S/(S\NP)
2. Composing with the verbs to get S/NP
3. Coordinating with generalized conjunction (pointwise ∧)
4. Applying to the shared object

The theorem proves CCG's compositional semantics matches the empirical observation.