Mereological Syntax → Semantics Bridge

@cite{adger-2025} @cite{borer-2005} @cite{wang-sun-2026}

Connects the syntactic visibility predicate (labelInOnePartChain) from mereological syntax to the semantic individuation operator (Div) from @cite{borer-2005}'s nominal theory, closing the gap between two independent uses of mereology in the library:

1. Semantic mereology (Core/Mereology.lean): part-whole over entities. CUM (cumulative), QUA (quantized), Div (individuation to atoms).
2. Syntactic mereology (MereologicalSyntax/): part-of over syntactic objects. SynObj, subjoin, Dimensionality.

The syntactic parthood structure determines which semantic operations compose into the denotation. Whether Cl is in D's 1-part chain determines whether individuation (Div) applies:

• Cl visible (in 1-part chain) → Div applies → QUA → sortal
• Cl invisible (cross-dimensional) → root passes through → CUM → mensural

This is the formal content of @cite{wang-sun-2026}'s 的-contrast.

def MereologicalSyntax.individuates (d : SynObj) : Bool

Whether the classifier is structurally visible from a syntactic node: true iff Cl is in the node's 1-part chain. This syntactic predicate determines whether semantic individuation applies.

Equations

• MereologicalSyntax.individuates d = MereologicalSyntax.labelInOnePartChain MereologicalSyntax.MLabel.Cl d

noncomputable def MereologicalSyntax.nominalDenotation {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) : α → Prop

The nominal denotation at a syntactic node, given a root predicate P.

When Cl is visible (in the node's 1-part chain), Div applies: the denotation picks out atomic instances of P (sortal/count). When Cl is invisible, P passes through unmodified (mensural/mass).

Equations

• MereologicalSyntax.nominalDenotation d P = if MereologicalSyntax.individuates d = true then Interfaces.SyntaxSemantics.Borer2005.Div P else P

noncomputable def MereologicalSyntax.nominalDenotationCL {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) (cl : Interfaces.SyntaxSemantics.Borer2005.ClassifierPred α) : α → Prop

Classifier-parametric variant: uses DivCL to further restrict which atoms qualify, based on the classifier's semantic content (e.g., 张 zhāng restricts to flat-surface atoms).

Equations

• MereologicalSyntax.nominalDenotationCL d P cl = if MereologicalSyntax.individuates d = true then Interfaces.SyntaxSemantics.Borer2005.DivCL P cl else P

theorem MereologicalSyntax.visible_cl_gives_qua {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) (hv : individuates d = true) : Mereology.QUA (nominalDenotation d P)

Core bridge: when Cl is visible, the nominal denotation is quantized. Syntactic visibility → semantic individuation → QUA.

theorem MereologicalSyntax.invisible_cl_preserves_root {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) (hv : individuates d = false) : nominalDenotation d P = P

When Cl is invisible, the denotation equals the root predicate.

theorem MereologicalSyntax.visible_cl_gives_qua_CL {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) (cl : Interfaces.SyntaxSemantics.Borer2005.ClassifierPred α) (hv : individuates d = true) : Mereology.QUA (nominalDenotationCL d P cl)

Classifier-parametric bridge: visible Cl with classifier predicate still yields QUA.

theorem MereologicalSyntax.invisible_cl_cum {α : Type u_1} [SemilatticeSup α] (d : SynObj) (P : α → Prop) (hv : individuates d = false) (hc : Mereology.CUM P) : Mereology.CUM (nominalDenotation d P)

When Cl is invisible and the root is cumulative, the denotation is cumulative — the mass/mensural reading.

theorem MereologicalSyntax.de_semantic_contrast {α : Type u_1} [SemilatticeSup α] (d_no_de d_de : SynObj) (P : α → Prop) (h_vis : individuates d_no_de = true) (h_invis : individuates d_de = false) (hc : Mereology.CUM P) : Mereology.QUA (nominalDenotation d_no_de P) ∧ Mereology.CUM (nominalDenotation d_de P)

The structural semantic contrast: the same root predicate, in two structures differing only in dimensional attachment, yields opposite mereological properties.

The hypothesis CUM P is @cite{borer-2005}'s thesis that root predicates are cumulative.