Mereological Syntax → Semantics Bridge

[adger-2025] [borer-2005] [wang-sun-2026]

Connects the syntactic visibility predicate (labelInOnePartChain) from mereological syntax to the atoms-restriction Number.atomsOf — the individuating operation [wang-sun-2026] and [adger-2025] assume for the classifier head of a [borer-2005]-style nominal spine — closing the gap between two independent uses of mereology in the library:

1. Semantic mereology (Semantics/Mereology.lean): part-whole over entities. CUM (cumulative), QUA (quantized), Number.atomsOf (restriction to atoms).
2. Syntactic mereology (Mereological/): 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 (Number.atomsOf) applies:

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

This is the formal content of [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), Number.atomsOf 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 Number.atomsOf P else P

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

Classifier-parametric variant: further restricts 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 Number.atomsOf fun (x : α) => P x ∧ cl x 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 cl : α → Prop) (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 [borer-2005]'s thesis that root predicates are cumulative.