structure Phenomena.Coordination.SemanticEquivalence : Type

Theory-neutral data: a non-constituent coordination sentence paired with its semantically equivalent fully-spelled-out version. Both are grammatical; native speakers judge them to have the same truth conditions. (Originally in Coordination/Data.lean; inlined 0.230.270 per the provenance-tracking policy.)

• sentence : List String

  The non-constituent coordination sentence

• equivalentTo : List String

  The semantically equivalent spelled-out version

• bothGrammatical : Bool

  Both are grammatical

@[implicit_reducible]

instance Phenomena.Coordination.instReprSemanticEquivalence : Repr SemanticEquivalence

Equations

• Phenomena.Coordination.instReprSemanticEquivalence = { reprPrec := Phenomena.Coordination.instReprSemanticEquivalence.repr }

def Phenomena.Coordination.instReprSemanticEquivalence.repr : SemanticEquivalence → ℕ → Std.Format

Equations

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

def Phenomena.Coordination.johnLikesAndMaryHatesBeans : SemanticEquivalence

"John likes and Mary hates beans" ≡ "John likes beans and Mary hates beans" — the canonical non-constituent coordination test pair (@cite{steedman-2000}).

Equations

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

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.