Symbol Reference: ⦃ ... ⦄ / ⟪ ... ⟫ — Metalevel Comprehension Braces & Double Angle Brackets

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

⦃ ... ⦄ / ⟪ ... ⟫ \(\{\!| \dots |\!\} \; / \; \llangle \dots \rrangle\) — Metalevel Comprehension Braces & Double Angle Brackets

Distinguishes metatheoretic set/class comprehension and AST packaging (⦃ ... ⦄ and ⟪ ... ⟫) from object-level braces { ... } and single angle brackets ⟨ ... ⟩.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
⦃ ... ⦄ / ⟪ ... ⟫
\(\{\!| \dots |\!\} \; / \; \llangle \dots \rrangle\)
Category Quotation & Antiquotation (Reflection Layer)
SML AST Constructor Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)
Constructor Arguments Typed arguments as specified by the Signature / Sort field above
Metatype / Signature Meta-Comprehension / Metatheoretic Structural Delimiters
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \{\!| \dots |\!\} \; / \; \llangle \dots \rrangle
How to Understand It

In MKTD1 and MKTD2, object-level class comprehension uses {x:Class | 𝛂(x)} (or the canonical binder (κ(x:Class). 𝛂(x))). When reasoning in the metatheory about syntactic environments, AST node tuples, or conglomerate-level collections, we use:

  • White Curly Brackets ⦃ ... ⦄ (U+2983 / U+2984): Meta-level collection or comprehension over syntactic objects/classes.
  • Double Angle Brackets ⟪ ... ⟫ (U+27EA / U+27EB): Meta-level AST node packaging, telescope grouping, and deep quotation contexts.
Canonical Law / Usage ⦃ x:Class | 𝛂(x) ⦄
Related Symbols & Kernel Entries