Symbol Reference: ⟨ ... ⟩ — Explicit Syntactic Antiquotation / Splicing Brackets & Tuple Delimiters

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

Formula Display:
Proof Trees:

⟨ ... ⟩ \(\langle \dots \rangle\) — Explicit Syntactic Antiquotation / Splicing Brackets & Tuple Delimiters

Splices a meta-level syntactic expression u : A.Expression (such as Dec_A(c) for a valid code c ∈ Code_A) into a quoted syntactic template ‹ ... ›; kept distinct from semantic valuation ⟦e⟧_ρ = Val_ρ(e).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
⟨ ... ⟩
\(\langle \dots \rangle\)
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 A.Expression → A.Expression (inside ‹...›; or Class → A.Expression via Dec_A) | Pair Constructor
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \langle \dots \rangle
How to Understand It

In MKTD1 and MKTD2, the angle brackets ⟨ ... ⟩ serve two documented syntactic roles and must not be conflated with semantic valuation ⟦e⟧_ρ = Val_ρ(e):

  1. Explicit Syntactic Antiquotation (Splicing) inside ‹ ... ›: When writing a quoted formula ‹ ∀x:Class. ⟨Dec_Fm(c)⟩ ›, the sub-expression inside ⟨ ... ⟩ is evaluated at the meta-level to an AST in A.Expression and spliced into the surrounding syntax tree. For any valid code c ∈ Code_A, ‹ ⟨Dec_A(c)⟩ › = Enc_A(Dec_A(c)) = c. (By contrast, semantic valuation in a model under assignment ρ is written with double white square brackets ⟦e⟧_ρ = Val_ρ(e); see symbols/binder-brackets.html.)
  2. Ordered Tuple / Pair Construction: Outside quotation contexts, ⟨a, b⟩ or (x, y) denotes ordered pairing (Entry DefDunaevOrderedPair (3.76) / dependent pair in Entry DefSigmaModel (3.38)).
Canonical Law / Usage ‹(𝒯 ⊢ ⟨Enc(𝛂)⟩) ⇒ 𝛂›
Related Symbols & Kernel Entries