Symbol Reference: ( ) { } [ ] | , . — Structural Delimiters, Grouping Parentheses, Comprehension Bars & Binder Dots

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

Formula Display:
Proof Trees:

( ) { } [ ] | , . \(( \dots ) \; \{ \dots \} \; [ \dots ] \; | \; , \; .\) — Structural Delimiters, Grouping Parentheses, Comprehension Bars & Binder Dots

Every parenthesis, brace, bracket, comprehension separator bar |, tuple comma ,, and binder scope dot . in Obelisk formulas is individually tokenized and clickable.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
( ) { } [ ] | , .
\(( \dots ) \; \{ \dots \} \; [ \dots ] \; | \; , \; .\)
Category Delimiters & Structural Punctuation
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 Syntactic Punctuation
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form ( \dots ) \; \{ \dots \} \; [ \dots ] \; | \; , \; .
How to Understand It

Meaning of Structural Punctuation in Obelisk Formulas:

  • Parentheses ( ... ): Explicit operator precedence grouping, function/predicate application f(x), and ordered pair notation (x, y) (Entry DefEmptySet (3.04)).
  • Curly Braces { ... } and Separator Bar |: Object-level class comprehension {x:Class | 𝛂(x)} (Entry DefIsSet (3.02)), singleton {x}, and unordered pair {x, y} (Entry DefIsProperClass (3.03)).
  • Square Brackets [ ... ]: Substitution notation 𝛂[x/t] and equivalence classes (Entries DefUnaryUnion (3.19)–DefBigDomain (3.21)).
  • Binder Dot . and Comma ,: Separates a typed variable binding ∀(x:Class). 𝛂 (or bound quantifier header ∀(x ∈ Y), 𝛂) from the matrix formula, or separates tuple arguments.
Canonical Law / Usage {x:Class | (x ∈ A) ∧ (x ∈ B)}
Related Symbols & Kernel Entries